now :: thesis: for n being Nat holds (superior_setsequence S) . n in Si

then
rng (superior_setsequence S) c= Si
by NAT_1:52;let n be Nat; :: thesis: (superior_setsequence S) . n in Si

reconsider DSeq = S ^\ n as SetSequence of X ;

reconsider n1 = n as Nat ;

A1: Union DSeq in Si by PROB_1:17;

Union DSeq = union (rng DSeq) by CARD_3:def 4;

then Union DSeq = union { (S . k) where k is Nat : n1 <= k } by Th6;

hence (superior_setsequence S) . n in Si by A1, Def3; :: thesis: verum

end;reconsider DSeq = S ^\ n as SetSequence of X ;

reconsider n1 = n as Nat ;

A1: Union DSeq in Si by PROB_1:17;

Union DSeq = union (rng DSeq) by CARD_3:def 4;

then Union DSeq = union { (S . k) where k is Nat : n1 <= k } by Th6;

hence (superior_setsequence S) . n in Si by A1, Def3; :: thesis: verum

hence superior_setsequence S is SetSequence of Si by RELAT_1:def 19; :: thesis: verum