let X be set ; :: thesis: for S being SigmaField of X

for G, F being sequence of S st G . 0 = {} & ( for n being Nat holds

( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds

union (rng G) = (F . 0) \ (meet (rng F))

let S be SigmaField of X; :: thesis: for G, F being sequence of S st G . 0 = {} & ( for n being Nat holds

( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds

union (rng G) = (F . 0) \ (meet (rng F))

let G, F be sequence of S; :: thesis: ( G . 0 = {} & ( for n being Nat holds

( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) implies union (rng G) = (F . 0) \ (meet (rng F)) )

assume that

A1: G . 0 = {} and

A2: for n being Nat holds

( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ; :: thesis: union (rng G) = (F . 0) \ (meet (rng F))

A3: dom G = NAT by FUNCT_2:def 1;

thus union (rng G) c= (F . 0) \ (meet (rng F)) :: according to XBOOLE_0:def 10 :: thesis: (F . 0) \ (meet (rng F)) c= union (rng G)

assume A11: A in (F . 0) \ (meet (rng F)) ; :: thesis: A in union (rng G)

then not A in meet (rng F) by XBOOLE_0:def 5;

then A12: ex Y being set st

( Y in rng F & not A in Y ) by SETFAM_1:def 1;

A in F . 0 by A11, XBOOLE_0:def 5;

then consider Y being set such that

A13: A in F . 0 and

A14: Y in rng F and

A15: not A in Y by A12;

dom F = NAT by FUNCT_2:def 1;

then consider n being object such that

A16: n in NAT and

A17: Y = F . n by A14, FUNCT_1:def 3;

reconsider n = n as Element of NAT by A16;

A in (F . 0) \ (F . n) by A13, A15, A17, XBOOLE_0:def 5;

then A18: A in G . (n + 1) by A2;

G . (n + 1) in rng G by FUNCT_2:4;

hence A in union (rng G) by A18, TARSKI:def 4; :: thesis: verum

for G, F being sequence of S st G . 0 = {} & ( for n being Nat holds

( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds

union (rng G) = (F . 0) \ (meet (rng F))

let S be SigmaField of X; :: thesis: for G, F being sequence of S st G . 0 = {} & ( for n being Nat holds

( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds

union (rng G) = (F . 0) \ (meet (rng F))

let G, F be sequence of S; :: thesis: ( G . 0 = {} & ( for n being Nat holds

( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) implies union (rng G) = (F . 0) \ (meet (rng F)) )

assume that

A1: G . 0 = {} and

A2: for n being Nat holds

( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ; :: thesis: union (rng G) = (F . 0) \ (meet (rng F))

A3: dom G = NAT by FUNCT_2:def 1;

thus union (rng G) c= (F . 0) \ (meet (rng F)) :: according to XBOOLE_0:def 10 :: thesis: (F . 0) \ (meet (rng F)) c= union (rng G)

proof

let A be object ; :: according to TARSKI:def 3 :: thesis: ( not A in (F . 0) \ (meet (rng F)) or A in union (rng G) )
let A be object ; :: according to TARSKI:def 3 :: thesis: ( not A in union (rng G) or A in (F . 0) \ (meet (rng F)) )

assume A in union (rng G) ; :: thesis: A in (F . 0) \ (meet (rng F))

then consider Z being set such that

A4: A in Z and

A5: Z in rng G by TARSKI:def 4;

consider n being object such that

A6: n in NAT and

A7: Z = G . n by A3, A5, FUNCT_1:def 3;

reconsider n = n as Element of NAT by A6;

consider k being Nat such that

A8: n = k + 1 by A1, A4, A7, NAT_1:6;

reconsider k = k as Element of NAT by ORDINAL1:def 12;

set Y = F . k;

A9: A in (F . 0) \ (F . k) by A2, A4, A7, A8;

then ( F . k in rng F & not A in F . k ) by FUNCT_2:4, XBOOLE_0:def 5;

then A10: not A in meet (rng F) by SETFAM_1:def 1;

A in F . 0 by A9, XBOOLE_0:def 5;

hence A in (F . 0) \ (meet (rng F)) by A10, XBOOLE_0:def 5; :: thesis: verum

end;assume A in union (rng G) ; :: thesis: A in (F . 0) \ (meet (rng F))

then consider Z being set such that

A4: A in Z and

A5: Z in rng G by TARSKI:def 4;

consider n being object such that

A6: n in NAT and

A7: Z = G . n by A3, A5, FUNCT_1:def 3;

reconsider n = n as Element of NAT by A6;

consider k being Nat such that

A8: n = k + 1 by A1, A4, A7, NAT_1:6;

reconsider k = k as Element of NAT by ORDINAL1:def 12;

set Y = F . k;

A9: A in (F . 0) \ (F . k) by A2, A4, A7, A8;

then ( F . k in rng F & not A in F . k ) by FUNCT_2:4, XBOOLE_0:def 5;

then A10: not A in meet (rng F) by SETFAM_1:def 1;

A in F . 0 by A9, XBOOLE_0:def 5;

hence A in (F . 0) \ (meet (rng F)) by A10, XBOOLE_0:def 5; :: thesis: verum

assume A11: A in (F . 0) \ (meet (rng F)) ; :: thesis: A in union (rng G)

then not A in meet (rng F) by XBOOLE_0:def 5;

then A12: ex Y being set st

( Y in rng F & not A in Y ) by SETFAM_1:def 1;

A in F . 0 by A11, XBOOLE_0:def 5;

then consider Y being set such that

A13: A in F . 0 and

A14: Y in rng F and

A15: not A in Y by A12;

dom F = NAT by FUNCT_2:def 1;

then consider n being object such that

A16: n in NAT and

A17: Y = F . n by A14, FUNCT_1:def 3;

reconsider n = n as Element of NAT by A16;

A in (F . 0) \ (F . n) by A13, A15, A17, XBOOLE_0:def 5;

then A18: A in G . (n + 1) by A2;

G . (n + 1) in rng G by FUNCT_2:4;

hence A in union (rng G) by A18, TARSKI:def 4; :: thesis: verum