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: (Partial_Diff_Union XSeq) . m in Si

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

per cases ( m = 0 or ex k being Nat st m = k + 1 ) by NAT_1:6;

case m = 0 ; :: thesis: (Partial_Diff_Union XSeq) . m in Si

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

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;

end;

end;

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

end;

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