let X be set ; 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; 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; 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 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)) \ (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 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]
reconsider B =
(N . (c + 1)) \ (N . c) as
Element of
S ;
take
B
;
S1[c,A,B]
thus
S1[
c,
A,
B]
;
verum
end;
consider F being sequence of S such that
A2:
( F . 0 = A & ( 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)) \ (N . n)
proof
let n be
Nat;
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)
;
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)) \ (N . n) ) )
by A2; verum