defpred S₁[ set , set , set ] means ex g being PartFunc of REAL ,REAL st
( $2 = g & $3 = cD g,h );
A1: for n being Element of NAT
for x being Element of PFuncs REAL ,REAL ex y being Element of PFuncs REAL ,REAL st S₁[n,x,y]

proof

let n be Element of NAT ; :: thesis: for x being Element of PFuncs REAL ,REAL ex y being Element of PFuncs REAL ,REAL st S₁[n,x,y]
let x be Element of PFuncs REAL ,REAL ; :: thesis: ex y being Element of PFuncs REAL ,REAL st S₁[n,x,y]
reconsider x' = x as PartFunc of REAL ,REAL by PARTFUN1:120;
reconsider y = cD x',h as Element of PFuncs REAL ,REAL by PARTFUN1:119;
ex w being PartFunc of REAL ,REAL st
( x = w & y = cD w,h ) ;
hence ex y being Element of PFuncs REAL ,REAL st S₁[n,x,y] ; :: thesis: verum

end;

reconsider fZ = f as Element of PFuncs REAL ,REAL by PARTFUN1:119;
consider g being Function of NAT ,(PFuncs REAL ,REAL ) such that
A2: ( g . 0 = fZ & ( for n being Element of NAT holds S₁[n,g . n,g . (n + 1)] ) ) from RECDEF_1:sch 2(A1);
defpred S₂[ Nat] means g . $1 is PartFunc of REAL ,REAL ;
reconsider g = g as Functional_Sequence of REAL ,REAL ;
take g ; :: thesis: ( g . 0 = f & ( for n being Element of NAT holds g . (n + 1) = cD (g . n),h ) )
thus g . 0 = f by A2; :: thesis: for n being Element of NAT holds g . (n + 1) = cD (g . n),h
let i be natural number ; :: thesis: ( i is Element of REAL & i is Element of NAT implies g . (i + 1) = cD (g . i),h )
i in NAT by ORDINAL1:def 13;
then S₁[i,g . i,g . (i + 1)] by A2;
hence ( i is Element of REAL & i is Element of NAT implies g . (i + 1) = cD (g . i),h ) ; :: thesis: verum