defpred S1[ set ] means (Partial_Union XSeq) . X in Si;
A1: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A2: (Partial_Union XSeq) . k in Si ; :: thesis: S1[k + 1]
((Partial_Union XSeq) . k) \/ (XSeq . (k + 1)) is Event of Si by A2, PROB_1:21;
then ((Partial_Union XSeq) . k) \/ (XSeq . (k + 1)) in Si ;
hence S1[k + 1] by Def2; :: thesis: verum
end;
( XSeq . 0 in rng XSeq & (Partial_Union XSeq) . 0 = XSeq . 0 ) by Def2, NAT_1:51;
then A3: S1[ 0 ] ;
for k being Nat holds S1[k] from NAT_1:sch 2(A3, A1);
 then rng (Partial_Union XSeq) c= Si by NAT_1:52;
hence Partial_Union XSeq is Si -valued ; :: thesis: verum