reconsider fZ = f as Element of PFuncs ( the carrier of V, the carrier of W) by PARTFUN1:45;
defpred S1[ set , set , set ] means ex g being PartFunc of V,W st
( $2 = g & $3 = bD (g,h) );
A1:
for n being Nat
for x being Element of PFuncs ( the carrier of V, the carrier of W) ex y being Element of PFuncs ( the carrier of V, the carrier of W) st S1[n,x,y]
proof
let n be
Nat;
for x being Element of PFuncs ( the carrier of V, the carrier of W) ex y being Element of PFuncs ( the carrier of V, the carrier of W) st S1[n,x,y]let x be
Element of
PFuncs ( the
carrier of
V, the
carrier of
W);
ex y being Element of PFuncs ( the carrier of V, the carrier of W) st S1[n,x,y]
reconsider x9 =
x as
PartFunc of
V,
W by PARTFUN1:46;
reconsider y =
bD (
x9,
h) as
Element of
PFuncs ( the
carrier of
V, the
carrier of
W)
by PARTFUN1:45;
ex
w being
PartFunc of
V,
W st
(
x = w &
y = bD (
w,
h) )
;
hence
ex
y being
Element of
PFuncs ( the
carrier of
V, the
carrier of
W) st
S1[
n,
x,
y]
;
verum
end;
consider g being sequence of (PFuncs ( the carrier of V, the carrier of W)) 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 the carrier of V, the carrier of W ;
take
g
; ( g . 0 = f & ( for n being Nat holds g . (n + 1) = bD ((g . n),h) ) )
thus
g . 0 = f
by A2; for n being Nat holds g . (n + 1) = bD ((g . n),h)
let i be Nat; g . (i + 1) = bD ((g . i),h)
S1[i,g . i,g . (i + 1)]
by A2;
hence
g . (i + 1) = bD ((g . i),h)
; verum