defpred S_{1}[ set ] means (Partial_Union XSeq) . X in Si;

A1: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

then A3: S_{1}[ 0 ]
;

for k being Nat holds S_{1}[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

A1: for k being Nat st S

S

proof

( XSeq . 0 in rng XSeq & (Partial_Union XSeq) . 0 = XSeq . 0 )
by Def2, NAT_1:51;
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A2: (Partial_Union XSeq) . k in Si ; :: thesis: S_{1}[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_{1}[k + 1]
by Def2; :: thesis: verum

end;assume A2: (Partial_Union XSeq) . k in Si ; :: thesis: S

((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

then A3: S

for k being Nat holds S

then rng (Partial_Union XSeq) c= Si by NAT_1:52;

hence Partial_Union XSeq is Si -valued ; :: thesis: verum