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 = {} & ( for n being Nat holds F . (n + 1) = (N . 0) \ (N . n) ) )
let S be SigmaField of X; for N being sequence of S ex F being sequence of S st
( F . 0 = {} & ( for n being Nat holds F . (n + 1) = (N . 0) \ (N . n) ) )
let N be sequence of S; ex F being sequence of S st
( F . 0 = {} & ( for n being Nat holds F . (n + 1) = (N . 0) \ (N . 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 . 0) \ (N . c);
reconsider A = {} as Element of S by PROB_1:4;
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 . 0) \ (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 . 0) \ (N . n)
hence
ex F being sequence of S st
( F . 0 = {} & ( for n being Nat holds F . (n + 1) = (N . 0) \ (N . n) ) )
by A2; verum