let X be set ; :: thesis: for S being SigmaField of X
for N, F being sequence of S st F . 0 = N . 0 & ( for n being Nat holds
( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ) holds
union (rng F) = union (rng N)
let S be SigmaField of X; :: thesis: for N, F being sequence of S st F . 0 = N . 0 & ( for n being Nat holds
( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ) holds
union (rng F) = union (rng N)
let N, F be sequence of S; :: thesis: ( F . 0 = N . 0 & ( for n being Nat holds
( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ) implies union (rng F) = union (rng N) )
assume that
A1: F . 0 = N . 0 and
A2: for n being Nat holds
( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ; :: thesis: union (rng F) = union (rng N)
thus union (rng F) c= union (rng N) :: according to XBOOLE_0:def 10 :: thesis: union (rng N) c= union (rng F)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (rng F) or x in union (rng N) )
assume x in union (rng F) ; :: thesis: x in union (rng N)
then consider Y being set such that
A3: x in Y and
A4: Y in rng F by TARSKI:def 4;
consider n being object such that
A5: n in dom F and
A6: Y = F . n by A4, FUNCT_1:def 3;
reconsider n = n as Element of NAT by A5;
A7: ( ex k being Nat st n = k + 1 implies ex Z being set st
( x in Z & Z in rng N ) )

proof

given k being Nat such that A8: n = k + 1 ; :: thesis: ex Z being set st
( x in Z & Z in rng N )
reconsider k = k as Element of NAT by ORDINAL1:def 12;
Y = (N . (k + 1)) \ (N . k) by A2, A6, A8;
then x in N . (k + 1) by A3, XBOOLE_0:def 5;
hence ex Z being set st
( x in Z & Z in rng N ) by FUNCT_2:4; :: thesis: verum

end;

( n = 0 implies ex Z being set st
( x in Z & Z in rng N ) ) by A1, A3, A6, FUNCT_2:4;
hence x in union (rng N) by A7, NAT_1:6, TARSKI:def 4; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (rng N) or x in union (rng F) )
assume x in union (rng N) ; :: thesis: x in union (rng F)
then consider Y being set such that
A9: x in Y and
A10: Y in rng N by TARSKI:def 4;
A11: ex n being object st
( n in dom N & Y = N . n ) by A10, FUNCT_1:def 3;
ex Z being set st
( x in Z & Z in rng F )

proof

ex s being Element of NAT st x in F . s

proof

defpred S₁[ Nat] means x in N . $1;
A12: ex k being Nat st S₁[k] by A9, A11;
ex k being Nat st
( S₁[k] & ( for r being Nat st S₁[r] holds
k <= r ) ) from NAT_1:sch 5(A12);
then consider k being Nat such that
A13: x in N . k and
A14: for r being Nat st x in N . r holds
k <= r ;
A15: ( ex l being Nat st k = l + 1 implies ex s being Element of NAT st x in F . s )

proof

given l being Nat such that A16: k = l + 1 ; :: thesis: ex s being Element of NAT st x in F . s
take k ; :: thesis: ( k is Element of NAT & x in F . k )
reconsider l = l as Element of NAT by ORDINAL1:def 12;
A17: not x in N . l

proof

assume x in N . l ; :: thesis: contradiction
then l + 1 <= l by A14, A16;
hence contradiction by NAT_1:13; :: thesis: verum

end;

F . (l + 1) = (N . (l + 1)) \ (N . l) by A2;
hence ( k is Element of NAT & x in F . k ) by A13, A16, A17, XBOOLE_0:def 5; :: thesis: verum

end;

( k = 0 implies ex s being Element of NAT st x in F . s ) by A1, A13;
hence ex s being Element of NAT st x in F . s by A15, NAT_1:6; :: thesis: verum

end;

hence ex Z being set st
( x in Z & Z in rng F ) by FUNCT_2:4; :: thesis: verum

end;

hence x in union (rng F) by TARSKI:def 4; :: thesis: verum