reconsider fZ = f | Z as Element of PFuncs ((REAL m),REAL) by PARTFUN1:45;
defpred S1[ 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 S1[n,x,y]
proof
let n be
Nat;
for x being Element of PFuncs ((REAL m),REAL) ex y being Element of PFuncs ((REAL m),REAL) st S1[n,x,y]let x be
Element of
PFuncs (
(REAL m),
REAL);
ex y being Element of PFuncs ((REAL m),REAL) st S1[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
S1[
n,
x,
y]
;
verum
end;
consider g being sequence of (PFuncs ((REAL m),REAL)) such that
A2:
( g . 0 = fZ & ( for n being Nat holds S1[n,g . n,g . (n + 1)] ) )
from RECDEF_1:sch 2(A1);
reconsider g = g as Functional_Sequence of (REAL m),REAL ;
take
g
; ( 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; for i being Nat holds g . (i + 1) = (g . i) `partial| (Z,(I /. (i + 1)))
let i be Nat; g . (i + 1) = (g . i) `partial| (Z,(I /. (i + 1)))
S1[i,g . i,g . (i + 1)]
by A2;
hence
g . (i + 1) = (g . i) `partial| (Z,(I /. (i + 1)))
; verum