let n be Nat; :: thesis: for X being set
for A being Subset of X
for A1 being SetSequence of X holds (inferior_setsequence (A1 (\) A)) . n = ((inferior_setsequence A1) . n) \ A
let X be set ; :: thesis: for A being Subset of X
for A1 being SetSequence of X holds (inferior_setsequence (A1 (\) A)) . n = ((inferior_setsequence A1) . n) \ A
let A be Subset of X; :: thesis: for A1 being SetSequence of X holds (inferior_setsequence (A1 (\) A)) . n = ((inferior_setsequence A1) . n) \ A
let A1 be SetSequence of X; :: thesis: (inferior_setsequence (A1 (\) A)) . n = ((inferior_setsequence A1) . n) \ A
(inferior_setsequence (A1 (\) A)) . n = Intersection ((A1 (\) A) ^\ n) by Th1
.= Intersection ((A1 ^\ n) (\) A) by Th19
.= (Intersection (A1 ^\ n)) \ A by Th36
.= ((inferior_setsequence A1) . n) \ A by Th1 ;
hence (inferior_setsequence (A1 (\) A)) . n = ((inferior_setsequence A1) . n) \ A ; :: thesis: verum