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)

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

hence
( N . 0 = F . 0 & ( for n being Element of NAT holds N . (n + 1) = (F . (n + 1)) \/ (N . n) ) )
by A1; :: thesis: verum
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;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