reconsider fZ = f as Element of PFuncs (REAL,REAL) by PARTFUN1:45;
defpred S1[ set , set , set ] means ex g being PartFunc of REAL,REAL st
( \$2 = g & \$3 = cD (g,h) );
A1: for n being Nat
for x being Element of PFuncs (REAL,REAL) ex y being Element of PFuncs (REAL,REAL) st S1[n,x,y]
proof
let n be Nat; :: thesis: for x being Element of PFuncs (REAL,REAL) ex y being Element of PFuncs (REAL,REAL) st S1[n,x,y]
let x be Element of PFuncs (REAL,REAL); :: thesis: ex y being Element of PFuncs (REAL,REAL) st S1[n,x,y]
reconsider x9 = x as PartFunc of REAL,REAL by PARTFUN1:46;
reconsider y = cD (x9,h) as Element of PFuncs (REAL,REAL) by PARTFUN1:45;
ex w being PartFunc of REAL,REAL st
( x = w & y = cD (w,h) ) ;
hence ex y being Element of PFuncs (REAL,REAL) st S1[n,x,y] ; :: thesis: verum
end;
consider g being sequence of () such that
A2: ( g . 0 = fZ & ( for n being Nat holds S1[n,g . n,g . (n + 1)] ) ) from reconsider g = g as Functional_Sequence of REAL,REAL ;
take g ; :: thesis: ( g . 0 = f & ( for n being Nat holds g . (n + 1) = cD ((g . n),h) ) )
thus g . 0 = f by A2; :: thesis: for n being Nat holds g . (n + 1) = cD ((g . n),h)
let i be Nat; :: thesis: g . (i + 1) = cD ((g . i),h)
S1[i,g . i,g . (i + 1)] by A2;
hence g . (i + 1) = cD ((g . i),h) ; :: thesis: verum