let X be set ; :: thesis: for S being SigmaField of X
for N, G, F being Function of NAT ,S st G . 0 = N . 0 & ( for n being Element of NAT holds G . (n + 1) = (N . (n + 1)) \/ (G . n) ) & F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \ (G . n) ) holds
for n, m being Element of NAT st n < m holds
F . n misses F . m
let S be SigmaField of X; :: thesis: for N, G, F being Function of NAT ,S st G . 0 = N . 0 & ( for n being Element of NAT holds G . (n + 1) = (N . (n + 1)) \/ (G . n) ) & F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \ (G . n) ) holds
for n, m being Element of NAT st n < m holds
F . n misses F . m
let N, G, F be Function of NAT ,S; :: thesis: ( G . 0 = N . 0 & ( for n being Element of NAT holds G . (n + 1) = (N . (n + 1)) \/ (G . n) ) & F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \ (G . n) ) implies for n, m being Element of NAT st n < m holds
F . n misses F . m )
assume A1: ( G . 0 = N . 0 & ( for n being Element of NAT holds G . (n + 1) = (N . (n + 1)) \/ (G . n) ) & F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \ (G . n) ) ) ; :: thesis: for n, m being Element of NAT st n < m holds
F . n misses F . m
let n, m be Element of NAT ; :: thesis: ( n < m implies F . n misses F . m )
assume A2: n < m ; :: thesis: F . n misses F . m
then ( 0 <= m & 0 <> m ) by NAT_1:2;
then consider k being Nat such that
A3: m = k + 1 by NAT_1:6;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
F . (k + 1) = (N . (k + 1)) \ (G . k) by A1;
then A4: G . k misses F . (k + 1) by XBOOLE_1:79;
n <= k by A2, A3, NAT_1:13;
then F . n c= G . k by A1, Th8;
hence (F . n) /\ (F . m) = ((F . n) /\ (G . k)) /\ (F . (k + 1)) by A3, XBOOLE_1:28
.= (F . n) /\ ((G . k) /\ (F . (k + 1))) by XBOOLE_1:16
.= (F . n) /\ {} by A4, XBOOLE_0:def 7
.= {} ;
:: according to XBOOLE_0:def 7 :: thesis: verum