reconsider n9 = n as Element of NAT by ORDINAL1:def 13;
defpred S₁[ Nat, Function, set ] means $3 = $2 * f;
set FX = PFuncs ((field f),(field f));
reconsider ID = id (field f) as Element of PFuncs ((field f),(field f)) by PARTFUN1:119;
A1: for n being Element of NAT
for x being Element of PFuncs ((field f),(field f)) ex y being Element of PFuncs ((field f),(field f)) st S₁[n,x,y]

proof

( dom f c= field f & rng f c= field f ) by XBOOLE_1:7;
then reconsider h = f as PartFunc of (field f),(field f) by RELSET_1:11;
let n be Element of NAT ; :: thesis: for x being Element of PFuncs ((field f),(field f)) ex y being Element of PFuncs ((field f),(field f)) st S₁[n,x,y]
let x be Element of PFuncs ((field f),(field f)); :: thesis: ex y being Element of PFuncs ((field f),(field f)) st S₁[n,x,y]
reconsider g = x as PartFunc of (field f),(field f) by PARTFUN1:120;
g * h is Element of PFuncs ((field f),(field f)) by PARTFUN1:119;
hence ex y being Element of PFuncs ((field f),(field f)) st S₁[n,x,y] ; :: thesis: verum

end;

consider p being Function of NAT,(PFuncs ((field f),(field f))) such that
A2: ( p . 0 = ID & ( for n being Element of NAT holds S₁[n,p . n,p . (n + 1)] ) ) from RECDEF_1:sch 2(A1);
A3: for n being Nat holds S₁[n,p . n,p . (n + 1)]

proof

let n be Nat; :: thesis: S₁[n,p . n,p . (n + 1)]
n in NAT by ORDINAL1:def 13;
hence S₁[n,p . n,p . (n + 1)] by A2; :: thesis: verum

end;

p . n9 is PartFunc of (field f),(field f) by PARTFUN1:120;
hence ex b₁ being Function ex p being Function of NAT,(PFuncs ((field f),(field f))) st
( b₁ = p . n & p . 0 = id (field f) & ( for k being Nat holds p . (k + 1) = (p . k) * f ) ) by A2, A3; :: thesis: verum