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

for N, G, F being sequence of S st G . 0 = N . 0 & ( for n being Nat holds G . (n + 1) = (N . (n + 1)) \/ (G . n) ) & F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \ (G . n) ) holds

for n, m being Nat st n < m holds

F . n misses F . m

let S be SigmaField of X; :: thesis: for N, G, F being sequence of S st G . 0 = N . 0 & ( for n being Nat holds G . (n + 1) = (N . (n + 1)) \/ (G . n) ) & F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \ (G . n) ) holds

for n, m being Nat st n < m holds

F . n misses F . m

let N, G, F be sequence of S; :: thesis: ( G . 0 = N . 0 & ( for n being Nat holds G . (n + 1) = (N . (n + 1)) \/ (G . n) ) & F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \ (G . n) ) implies for n, m being Nat st n < m holds

F . n misses F . m )

assume that

A1: ( G . 0 = N . 0 & ( for n being Nat holds G . (n + 1) = (N . (n + 1)) \/ (G . n) ) & F . 0 = N . 0 ) and

A2: for n being Nat holds F . (n + 1) = (N . (n + 1)) \ (G . n) ; :: thesis: for n, m being Nat st n < m holds

F . n misses F . m

let n, m be Nat; :: thesis: ( n < m implies F . n misses F . m )

assume A3: n < m ; :: thesis: F . n misses F . m

then 0 <> m by NAT_1:2;

then consider k being Nat such that

A4: m = k + 1 by NAT_1:6;

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

F . (k + 1) = (N . (k + 1)) \ (G . k) by A2;

then A5: G . k misses F . (k + 1) by XBOOLE_1:79;

n <= k by A3, A4, NAT_1:13;

hence (F . n) /\ (F . m) = ((F . n) /\ (G . k)) /\ (F . (k + 1)) by A1, A2, A4, Th7, XBOOLE_1:28

.= (F . n) /\ ((G . k) /\ (F . (k + 1))) by XBOOLE_1:16

.= (F . n) /\ {} by A5

.= {} ;

:: according to XBOOLE_0:def 7 :: thesis: verum

for N, G, F being sequence of S st G . 0 = N . 0 & ( for n being Nat holds G . (n + 1) = (N . (n + 1)) \/ (G . n) ) & F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \ (G . n) ) holds

for n, m being Nat st n < m holds

F . n misses F . m

let S be SigmaField of X; :: thesis: for N, G, F being sequence of S st G . 0 = N . 0 & ( for n being Nat holds G . (n + 1) = (N . (n + 1)) \/ (G . n) ) & F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \ (G . n) ) holds

for n, m being Nat st n < m holds

F . n misses F . m

let N, G, F be sequence of S; :: thesis: ( G . 0 = N . 0 & ( for n being Nat holds G . (n + 1) = (N . (n + 1)) \/ (G . n) ) & F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \ (G . n) ) implies for n, m being Nat st n < m holds

F . n misses F . m )

assume that

A1: ( G . 0 = N . 0 & ( for n being Nat holds G . (n + 1) = (N . (n + 1)) \/ (G . n) ) & F . 0 = N . 0 ) and

A2: for n being Nat holds F . (n + 1) = (N . (n + 1)) \ (G . n) ; :: thesis: for n, m being Nat st n < m holds

F . n misses F . m

let n, m be Nat; :: thesis: ( n < m implies F . n misses F . m )

assume A3: n < m ; :: thesis: F . n misses F . m

then 0 <> m by NAT_1:2;

then consider k being Nat such that

A4: m = k + 1 by NAT_1:6;

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

F . (k + 1) = (N . (k + 1)) \ (G . k) by A2;

then A5: G . k misses F . (k + 1) by XBOOLE_1:79;

n <= k by A3, A4, NAT_1:13;

hence (F . n) /\ (F . m) = ((F . n) /\ (G . k)) /\ (F . (k + 1)) by A1, A2, A4, Th7, XBOOLE_1:28

.= (F . n) /\ ((G . k) /\ (F . (k + 1))) by XBOOLE_1:16

.= (F . n) /\ {} by A5

.= {} ;

:: according to XBOOLE_0:def 7 :: thesis: verum