let X be set ; :: thesis: for A1 being SetSequence of X holds Partial_Union (Partial_Diff_Union A1) = Partial_Union A1
let A1 be SetSequence of X; :: thesis: Partial_Union (Partial_Diff_Union A1) = Partial_Union A1
for n being Nat holds (Partial_Union (Partial_Diff_Union A1)) . n = (Partial_Union A1) . n

proof

set A2 = Partial_Diff_Union A1;
defpred S₁[ set ] means (Partial_Union (Partial_Diff_Union A1)) . $1 = (Partial_Union A1) . $1;
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: (Partial_Union (Partial_Diff_Union A1)) . k = (Partial_Union A1) . k ; :: thesis: S₁[k + 1]
thus (Partial_Union (Partial_Diff_Union A1)) . (k + 1) = ((Partial_Diff_Union A1) . (k + 1)) \/ ((Partial_Union (Partial_Diff_Union A1)) . k) by Def2
.= ((A1 . (k + 1)) \ ((Partial_Union A1) . k)) \/ ((Partial_Union A1) . k) by A2, Def3
.= (A1 . (k + 1)) \/ ((Partial_Union A1) . k) by XBOOLE_1:39
.= (Partial_Union A1) . (k + 1) by Def2 ; :: thesis: verum

end;

(Partial_Union (Partial_Diff_Union A1)) . 0 = (Partial_Diff_Union A1) . 0 by Def2
.= A1 . 0 by Def3
.= (Partial_Union A1) . 0 by Def2 ;
then A3: S₁[ 0 ] ;
thus for k being Nat holds S₁[k] from NAT_1:sch 2(A3, A1); :: thesis: verum

end;

hence Partial_Union (Partial_Diff_Union A1) = Partial_Union A1 ; :: thesis: verum