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)

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 )

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 N) or x in union (rng F) )
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 ) )

( 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;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

( n = 0 implies ex Z being set st
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;( 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

( 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

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

hence
x in union (rng F)
by TARSKI:def 4; :: thesis: verum
ex s being Element of NAT st x in F . s

( x in Z & Z in rng F ) by FUNCT_2:4; :: thesis: verum

end;proof

hence
ex Z being set st
defpred S_{1}[ Nat] means x in N . $1;

A12: ex k being Nat st S_{1}[k]
by A9, A11;

ex k being Nat st

( S_{1}[k] & ( for r being Nat st S_{1}[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 )

hence ex s being Element of NAT st x in F . s by A15, NAT_1:6; :: thesis: verum

end;A12: ex k being Nat st S

ex k being Nat st

( S

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

( k = 0 implies ex s being Element of NAT st x in F . s )
by A1, A13;
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

hence ( k is Element of NAT & x in F . k ) by A13, A16, A17, XBOOLE_0:def 5; :: thesis: verum

end;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

F . (l + 1) = (N . (l + 1)) \ (N . l)
by A2;
assume
x in N . l
; :: thesis: contradiction

then l + 1 <= l by A14, A16;

hence contradiction by NAT_1:13; :: thesis: verum

end;then l + 1 <= l by A14, A16;

hence contradiction by NAT_1:13; :: thesis: verum

hence ( k is Element of NAT & x in F . k ) by A13, A16, A17, XBOOLE_0:def 5; :: thesis: verum

hence ex s being Element of NAT st x in F . s by A15, NAT_1:6; :: thesis: verum

( x in Z & Z in rng F ) by FUNCT_2:4; :: thesis: verum