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 Element of NAT holds
( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ) holds
( N . 0 = F . 0 & ( for n being Element of NAT holds N . (n + 1) = (F . (n + 1)) \/ (N . n) ) )
let S be SigmaField of X; :: thesis: for N, F being sequence of S st F . 0 = N . 0 & ( for n being Element of NAT holds
( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ) holds
( N . 0 = F . 0 & ( for n being Element of NAT holds N . (n + 1) = (F . (n + 1)) \/ (N . n) ) )
let N, F be sequence of S; :: thesis: ( F . 0 = N . 0 & ( for n being Element of NAT holds
( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ) implies ( N . 0 = F . 0 & ( for n being Element of NAT holds N . (n + 1) = (F . (n + 1)) \/ (N . n) ) ) )
assume that
A1: F . 0 = N . 0 and
A2: for n being Element of NAT holds
( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ; :: thesis: ( N . 0 = F . 0 & ( for n being Element of NAT holds N . (n + 1) = (F . (n + 1)) \/ (N . n) ) )
for n being Element of NAT holds N . (n + 1) = (F . (n + 1)) \/ (N . n)
proof
let n be Element of NAT ; :: thesis: N . (n + 1) = (F . (n + 1)) \/ (N . n)
F . (n + 1) = (N . (n + 1)) \ (N . n) by A2;
hence N . (n + 1) = (F . (n + 1)) \/ (N . n) by A2, XBOOLE_1:45; :: thesis: verum
end;
hence ( N . 0 = F . 0 & ( for n being Element of NAT holds N . (n + 1) = (F . (n + 1)) \/ (N . n) ) ) by A1; :: thesis: verum