let X be set ; :: thesis: for S being SigmaField of X
for N being Function of NAT,S ex 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) ) )
let S be SigmaField of X; :: thesis: for N being Function of NAT,S ex 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) ) )
let N be Function of NAT,S; :: thesis: ex 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) ) )
reconsider S = S as non empty set ;
defpred S₁[ set , set , set ] means for A, B being Element of S
for c being Element of 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 Element of NAT
for A being Element of S ex B being Element of S st S₁[c,A,B]

proof

let c be Element of NAT ; :: thesis: for A being Element of S ex B being Element of S st S₁[c,A,B]
let A be Element of S; :: thesis: ex B being Element of S st S₁[c,A,B]
reconsider B = (N . (c + 1)) \ (N . c) as Element of S ;
take B ; :: thesis: S₁[c,A,B]
thus S₁[c,A,B] ; :: thesis: verum

end;

consider F being Function of NAT,S such that
A2: ( F . 0 = A & ( for n being Element of NAT holds S₁[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch 2(A1);
for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \ (N . n)

proof

let n be Element of NAT ; :: thesis: F . (n + 1) = (N . (n + 1)) \ (N . n)
for a, b being Element of S
for s being Element of 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;

hence ex 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) ) ) by A2; :: thesis: verum