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

proof

let m be Nat; :: thesis:

now :: thesis:

per cases by NAT_1:6;

case m = 0 ; :: thesis:

hence (Partial_Diff_Union XSeq) . m in Si by A1; :: thesis:

end;

case ex k being Nat st m = k + 1 ; :: thesis:

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:

end;

end;

end;

hence (Partial_Diff_Union XSeq) . m in Si ; :: thesis:

end;

then rng (Partial_Diff_Union XSeq) c= Si by NAT_1:52;
hence Partial_Diff_Union XSeq is Si -valued ; :: thesis: