let X be set ; 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; 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; 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;
for A being Element of S ex B being Element of S st S1[c,A,B]let A be
Element of
S;
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
;
S1[c,A,B]
thus
S1[
c,
A,
B]
by A2;
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 RECDEF_1:sch 2(A1);
for n being Nat holds F . (n + 1) = (N . (n + 1)) \ (G . n)
proof
let n be
Nat;
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)
;
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; verum