defpred S₁[ set ] means (Partial_Union XSeq) . X in Si;
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: (Partial_Union XSeq) . k in Si ; :: thesis: S₁[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 S₁[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: S₁[ 0 ] ;
for k being Nat holds S₁[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