let X be set ; :: thesis: for S being SigmaField of X
for N, G 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)) \ (G . n) ) )

let S be SigmaField of X; :: thesis: for N, G 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)) \ (G . n) ) )

let N, G 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)) \ (G . n) ) )

defpred S1[ 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)) \ (G . c);
A1: for c being Nat
for A being Element of S ex B being Element of S st S1[c,A,B]
proof
let c be Nat; :: thesis: for A being Element of S ex B being Element of S st S1[c,A,B]
let A be Element of S; :: thesis: ex B being Element of S st S1[c,A,B]
consider B being set such that
A2: B = (N . (c + 1)) \ (G . c) ;
reconsider B = B as Element of S by A2;
take B ; :: thesis: S1[c,A,B]
thus S1[c,A,B] by A2; :: thesis: verum
end;
consider F being sequence of S such that
A3: ( F . 0 = N . 0 & ( for n being Nat holds S1[n,F . n,F . (n + 1)] ) ) from for n being Nat holds F . (n + 1) = (N . (n + 1)) \ (G . n)
proof
let n be Nat; :: thesis: F . (n + 1) = (N . (n + 1)) \ (G . 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)) \ (G . s) by A3;
hence F . (n + 1) = (N . (n + 1)) \ (G . n) ; :: thesis: verum
end;
hence ex F being sequence of S st
( F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \ (G . n) ) ) by A3; :: thesis: verum