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

proof

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

end;

consider p being Function of NAT ,(PFuncs ((dom f) \/ (rng f)),((dom f) \/ (rng 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 ((dom f) \/ (rng f)),((dom f) \/ (rng f)) by PARTFUN1:120;
hence ex b₁ being Function ex p being Function of NAT ,(PFuncs ((dom f) \/ (rng f)),((dom f) \/ (rng f))) st
( b₁ = p . n & p . 0 = id ((dom f) \/ (rng f)) & ( for k being Nat ex g being Function st
( g = p . k & p . (k + 1) = g * f ) ) ) by A2, A3; :: thesis: verum