let X be set ; :: thesis: for F being Field_Subset of X

for FSets being Set_Sequence of F holds Partial_Diff_Union FSets is Set_Sequence of F

let F be Field_Subset of X; :: thesis: for FSets being Set_Sequence of F holds Partial_Diff_Union FSets is Set_Sequence of F

let FSets be Set_Sequence of F; :: thesis: Partial_Diff_Union FSets is Set_Sequence of F

defpred S_{1}[ Nat] means (Partial_Diff_Union FSets) . $1 in F;

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

S_{1}[k + 1]

then A3: S_{1}[ 0 ]
;

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

hence Partial_Diff_Union FSets is Set_Sequence of F by Def2; :: thesis: verum

for FSets being Set_Sequence of F holds Partial_Diff_Union FSets is Set_Sequence of F

let F be Field_Subset of X; :: thesis: for FSets being Set_Sequence of F holds Partial_Diff_Union FSets is Set_Sequence of F

let FSets be Set_Sequence of F; :: thesis: Partial_Diff_Union FSets is Set_Sequence of F

defpred S

A1: for k being Nat st S

S

proof

(Partial_Diff_Union FSets) . 0 = FSets . 0
by PROB_3:def 3;
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume S_{1}[k]
; :: thesis: S_{1}[k + 1]

Partial_Union FSets is Set_Sequence of F by Th15;

then A2: (Partial_Union FSets) . k in F by Def2;

(Partial_Diff_Union FSets) . (k + 1) = (FSets . (k + 1)) \ ((Partial_Union FSets) . k) by PROB_3:def 3;

hence S_{1}[k + 1]
by A2, PROB_1:6; :: thesis: verum

end;assume S

Partial_Union FSets is Set_Sequence of F by Th15;

then A2: (Partial_Union FSets) . k in F by Def2;

(Partial_Diff_Union FSets) . (k + 1) = (FSets . (k + 1)) \ ((Partial_Union FSets) . k) by PROB_3:def 3;

hence S

then A3: S

for n being Nat holds S

hence Partial_Diff_Union FSets is Set_Sequence of F by Def2; :: thesis: verum