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 S1[ Nat] means (Partial_Diff_Union FSets) . \$1 in F;
A1: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume S1[k] ; :: thesis: S1[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 S1[k + 1] by ; :: thesis: verum
end;
(Partial_Diff_Union FSets) . 0 = FSets . 0 by PROB_3:def 3;
then A3: S1[ 0 ] ;
for n being Nat holds S1[n] from NAT_1:sch 2(A3, A1);
hence Partial_Diff_Union FSets is Set_Sequence of F by Def2; :: thesis: verum