let X be set ; :: thesis: for F being Field_Subset of X
for FSets being Set_Sequence of F holds Partial_Union FSets is Set_Sequence of F
let F be Field_Subset of X; :: thesis: for FSets being Set_Sequence of F holds Partial_Union FSets is Set_Sequence of F
let FSets be Set_Sequence of F; :: thesis: Partial_Union FSets is Set_Sequence of F
defpred S₁[ Nat] means (Partial_Union FSets) . $1 in F;
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
A2: (Partial_Union FSets) . (k + 1) = ((Partial_Union FSets) . k) \/ (FSets . (k + 1)) by PROB_3:def 2;
assume S₁[k] ; :: thesis: S₁[k + 1]
hence S₁[k + 1] by A2, PROB_1:3; :: thesis: verum

end;

(Partial_Union FSets) . 0 = FSets . 0 by PROB_3:def 2;
then A3: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A1);
hence Partial_Union FSets is Set_Sequence of F by Def2; :: thesis: verum