superior_setsequence S is SetSequence of

proof

now

let n be Nat; :: thesis: (superior_setsequence S) . n in Si
reconsider DSeq = S ^\ n as SetSequence of X ;
reconsider n1 = n as Element of NAT by ORDINAL1:def 13;
for m being Nat holds DSeq . m in Si

proof

let m be Nat; :: thesis: DSeq . m in Si
Y: DSeq . m = S . (m + n1) by NAT_1:def 3;
X: S . (m + n1) in rng S by NAT_1:52;
rng S c= Si by RELAT_1:def 19;
hence DSeq . m in Si by X, Y; :: thesis: verum

end;

then rng DSeq c= Si by NAT_1:53;
then DSeq is SetSequence of by RELAT_1:def 19;
then B4: Union DSeq in Si by PROB_1:46;
Union DSeq = union (rng DSeq) by CARD_3:def 4;
then Union DSeq = union { (S . k) where k is Element of NAT : n1 <= k } by Th11;
hence (superior_setsequence S) . n in Si by B4, def3; :: thesis: verum

end;

then rng (superior_setsequence S) c= Si by NAT_1:53;
hence superior_setsequence S is SetSequence of by RELAT_1:def 19; :: thesis: verum

end;

hence superior_setsequence S is SetSequence of ; :: thesis: verum