reconsider fZ = f | Z as Element of PFuncs ((REAL m),REAL) by PARTFUN1:45;
defpred S₁[ set , set , set ] means ex k being Nat ex h being PartFunc of (REAL m),REAL st
( $1 = k & $2 = h & $3 = h `partial| (Z,(I /. (k + 1))) );
A1: for n being Nat
for x being Element of PFuncs ((REAL m),REAL) ex y being Element of PFuncs ((REAL m),REAL) st S₁[n,x,y]

proof

let n be Nat; :: thesis: for x being Element of PFuncs ((REAL m),REAL) ex y being Element of PFuncs ((REAL m),REAL) st S₁[n,x,y]
let x be Element of PFuncs ((REAL m),REAL); :: thesis: ex y being Element of PFuncs ((REAL m),REAL) st S₁[n,x,y]
reconsider x9 = x as PartFunc of (REAL m),REAL by PARTFUN1:46;
reconsider y = x9 `partial| (Z,(I /. (n + 1))) as Element of PFuncs ((REAL m),REAL) by PARTFUN1:45;
ex h being PartFunc of (REAL m),REAL st
( x = h & y = h `partial| (Z,(I /. (n + 1))) ) ;
hence ex y being Element of PFuncs ((REAL m),REAL) st S₁[n,x,y] ; :: thesis: verum

end;

consider g being sequence of (PFuncs ((REAL m),REAL)) such that
A2: ( g . 0 = fZ & ( for n being Nat holds S₁[n,g . n,g . (n + 1)] ) ) from RECDEF_1:sch 2(A1);
reconsider g = g as Functional_Sequence of (REAL m),REAL ;
take g ; :: thesis: ( g . 0 = f | Z & ( for i being Nat holds g . (i + 1) = (g . i) `partial| (Z,(I /. (i + 1))) ) )
thus g . 0 = f | Z by A2; :: thesis: for i being Nat holds g . (i + 1) = (g . i) `partial| (Z,(I /. (i + 1)))
let i be Nat; :: thesis: g . (i + 1) = (g . i) `partial| (Z,(I /. (i + 1)))
S<sub>1</sub>[i,g . i,g . (i + 1)] by A2;
hence g . (i + 1) = (g . i) `partial| (Z,(I /. (i + 1))) ; :: thesis: verum