A1: rng XSeq c= Si by RELAT_1:def 19;
A2: ( XSeq . 0 in rng XSeq & (Partial_Diff_Union XSeq) . 0 = XSeq . 0 ) by Def3, NAT_1:52;
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

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, A2; :: 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
A3: m = k + 1 ;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
A4: (Partial_Union XSeq) . k in rng (Partial_Union XSeq) by NAT_1:52;
( XSeq . (k + 1) in rng XSeq & rng (@Partial_Union XSeq) c= Si ) by NAT_1:52, RELAT_1:def 19;
then (XSeq . (k + 1)) \ ((Partial_Union XSeq) . k) in Si by A1, A4, PROB_1:12;
hence (Partial_Diff_Union XSeq) . m in Si by A3, 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:53;
hence Partial_Diff_Union XSeq is SetSequence of Si by RELAT_1:def 19; :: thesis: verum