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