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

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

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

defpred S_{1}[ set ] means (Partial_Union (Partial_Diff_Union A1)) . $1 = (Partial_Union A1) . $1;

A1: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

.= A1 . 0 by Def3

.= (Partial_Union A1) . 0 by Def2 ;

then A3: S_{1}[ 0 ]
;

thus for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A3, A1); :: thesis: verum

end;defpred S

A1: for k being Nat st S

S

proof

(Partial_Union (Partial_Diff_Union A1)) . 0 =
(Partial_Diff_Union A1) . 0
by Def2
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A2: (Partial_Union (Partial_Diff_Union A1)) . k = (Partial_Union A1) . k ; :: thesis: S_{1}[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;assume A2: (Partial_Union (Partial_Diff_Union A1)) . k = (Partial_Union A1) . k ; :: thesis: S

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

.= A1 . 0 by Def3

.= (Partial_Union A1) . 0 by Def2 ;

then A3: S

thus for k being Nat holds S