reconsider fZ = f as Element of PFuncs ( the carrier of V, the carrier of W) by PARTFUN1:45;

defpred S_{1}[ set , set , set ] means ex g being PartFunc of V,W st

( $2 = g & $3 = fD (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 S_{1}[n,x,y]

A2: ( g . 0 = fZ & ( for n being Nat holds S_{1}[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 ; :: thesis: ( g . 0 = f & ( for n being Nat holds g . (n + 1) = fD ((g . n),h) ) )

thus g . 0 = f by A2; :: thesis: for n being Nat holds g . (n + 1) = fD ((g . n),h)

let i be Nat; :: thesis: g . (i + 1) = fD ((g . i),h)

S_{1}[i,g . i,g . (i + 1)]
by A2;

hence g . (i + 1) = fD ((g . i),h) ; :: thesis: verum

defpred S

( $2 = g & $3 = fD (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 S

proof

consider g being sequence of (PFuncs ( the carrier of V, the carrier of W)) such that
let n be Nat; :: thesis: 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 S_{1}[n,x,y]

let x be Element of PFuncs ( the carrier of V, the carrier of W); :: thesis: ex y being Element of PFuncs ( the carrier of V, the carrier of W) st S_{1}[n,x,y]

reconsider x9 = x as PartFunc of the carrier of V, the carrier of W by PARTFUN1:46;

reconsider y = fD (x9,h) as Element of PFuncs ( the carrier of V, the carrier of W) by PARTFUN1:45;

ex w being PartFunc of the carrier of V, the carrier of W st

( x = w & y = fD (w,h) ) ;

hence ex y being Element of PFuncs ( the carrier of V, the carrier of W) st S_{1}[n,x,y]
; :: thesis: verum

end;let x be Element of PFuncs ( the carrier of V, the carrier of W); :: thesis: ex y being Element of PFuncs ( the carrier of V, the carrier of W) st S

reconsider x9 = x as PartFunc of the carrier of V, the carrier of W by PARTFUN1:46;

reconsider y = fD (x9,h) as Element of PFuncs ( the carrier of V, the carrier of W) by PARTFUN1:45;

ex w being PartFunc of the carrier of V, the carrier of W st

( x = w & y = fD (w,h) ) ;

hence ex y being Element of PFuncs ( the carrier of V, the carrier of W) st S

A2: ( g . 0 = fZ & ( for n being Nat holds S

reconsider g = g as Functional_Sequence of the carrier of V, the carrier of W ;

take g ; :: thesis: ( g . 0 = f & ( for n being Nat holds g . (n + 1) = fD ((g . n),h) ) )

thus g . 0 = f by A2; :: thesis: for n being Nat holds g . (n + 1) = fD ((g . n),h)

let i be Nat; :: thesis: g . (i + 1) = fD ((g . i),h)

S

hence g . (i + 1) = fD ((g . i),h) ; :: thesis: verum