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

for N being sequence of S ex F being sequence of S st

( F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \ (N . n) ) )

let S be SigmaField of X; :: thesis: for N being sequence of S ex F being sequence of S st

( F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \ (N . n) ) )

let N be sequence of S; :: thesis: ex F being sequence of S st

( F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \ (N . n) ) )

reconsider S = S as non empty set ;

defpred S_{1}[ set , set , set ] means for A, B being Element of S

for c being Nat st c = $1 & A = $2 & B = $3 holds

B = (N . (c + 1)) \ (N . c);

reconsider A = N . 0 as Element of S ;

A1: for c being Nat

for A being Element of S ex B being Element of S st S_{1}[c,A,B]

A2: ( F . 0 = A & ( for n being Nat holds S_{1}[n,F . n,F . (n + 1)] ) )
from RECDEF_1:sch 2(A1);

for n being Nat holds F . (n + 1) = (N . (n + 1)) \ (N . n)

( F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \ (N . n) ) ) by A2; :: thesis: verum

for N being sequence of S ex F being sequence of S st

( F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \ (N . n) ) )

let S be SigmaField of X; :: thesis: for N being sequence of S ex F being sequence of S st

( F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \ (N . n) ) )

let N be sequence of S; :: thesis: ex F being sequence of S st

( F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \ (N . n) ) )

reconsider S = S as non empty set ;

defpred S

for c being Nat st c = $1 & A = $2 & B = $3 holds

B = (N . (c + 1)) \ (N . c);

reconsider A = N . 0 as Element of S ;

A1: for c being Nat

for A being Element of S ex B being Element of S st S

proof

consider F being sequence of S such that
let c be Nat; :: thesis: for A being Element of S ex B being Element of S st S_{1}[c,A,B]

let A be Element of S; :: thesis: ex B being Element of S st S_{1}[c,A,B]

reconsider B = (N . (c + 1)) \ (N . c) as Element of S ;

take B ; :: thesis: S_{1}[c,A,B]

thus S_{1}[c,A,B]
; :: thesis: verum

end;let A be Element of S; :: thesis: ex B being Element of S st S

reconsider B = (N . (c + 1)) \ (N . c) as Element of S ;

take B ; :: thesis: S

thus S

A2: ( F . 0 = A & ( for n being Nat holds S

for n being Nat holds F . (n + 1) = (N . (n + 1)) \ (N . n)

proof

hence
ex F being sequence of S st
let n be Nat; :: thesis: F . (n + 1) = (N . (n + 1)) \ (N . n)

for a, b being Element of S

for s being Nat st s = n & a = F . n & b = F . (n + 1) holds

b = (N . (s + 1)) \ (N . s) by A2;

hence F . (n + 1) = (N . (n + 1)) \ (N . n) ; :: thesis: verum

end;for a, b being Element of S

for s being Nat st s = n & a = F . n & b = F . (n + 1) holds

b = (N . (s + 1)) \ (N . s) by A2;

hence F . (n + 1) = (N . (n + 1)) \ (N . n) ; :: thesis: verum

( F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \ (N . n) ) ) by A2; :: thesis: verum