let X be set ; :: thesis: for S being SigmaField of X
for N, F being Function of NAT ,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 Function of NAT ,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 Function of NAT ,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 A1: ( 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) ) ) ) ; :: 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) & N . n c= N . (n + 1) ) by A1;
hence N . (n + 1) = (F . (n + 1)) \/ (N . n) by 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