A1:
( XSeq . 0 in rng XSeq & (Partial_Diff_Union XSeq) . 0 = XSeq . 0 )
by Def3, NAT_1:51;

for m being Nat holds (Partial_Diff_Union XSeq) . m in Si

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

for m being Nat holds (Partial_Diff_Union XSeq) . m in Si

proof

then
rng (Partial_Diff_Union XSeq) c= Si
by NAT_1:52;
let m be Nat; :: thesis: (Partial_Diff_Union XSeq) . m in Si

end;now :: thesis: ( ( m = 0 & (Partial_Diff_Union XSeq) . m in Si ) or ( ex k being Nat st m = k + 1 & (Partial_Diff_Union XSeq) . m in Si ) )end;

hence
(Partial_Diff_Union XSeq) . m in Si
; :: thesis: verumper cases
( m = 0 or ex k being Nat st m = k + 1 )
by NAT_1:6;

end;

case
ex k being Nat st m = k + 1
; :: thesis: (Partial_Diff_Union XSeq) . m in Si

then consider k being Nat such that

A2: m = k + 1 ;

reconsider k = k as Element of NAT by ORDINAL1:def 12;

(XSeq . (k + 1)) \ ((Partial_Union XSeq) . k) in Si ;

hence (Partial_Diff_Union XSeq) . m in Si by A2, Def3; :: thesis: verum

end;A2: m = k + 1 ;

reconsider k = k as Element of NAT by ORDINAL1:def 12;

(XSeq . (k + 1)) \ ((Partial_Union XSeq) . k) in Si ;

hence (Partial_Diff_Union XSeq) . m in Si by A2, Def3; :: thesis: verum

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