let X be non empty set ; :: thesis: for S being Field_Subset of X
for E being Set_Sequence of S
for i being Nat holds (Partial_Union E) . i in S
let S be Field_Subset of X; :: thesis: for E being Set_Sequence of S
for i being Nat holds (Partial_Union E) . i in S
let E be Set_Sequence of S; :: thesis: for i being Nat holds (Partial_Union E) . i in S
defpred S₁[ Nat] means (Partial_Union E) . $1 in S;
(Partial_Union E) . 0 = E . 0 by PROB_3:def 2;
then A1: S₁[ 0 ] ;
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

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

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
hence for i being Nat holds (Partial_Union E) . i in S ; :: thesis: verum