reconsider e = 0 as Function ;
defpred S₁[ Element of NAT , set , set ] means ( ( $2 is not Function & $3 = e ) or ( $2 is Function & ( for g, h being Function st g = $2 & h = p . ($1 + 1) holds
$3 = h * g ) ) );
A10: for n being Element of NAT
for x being set ex y being set st S₁[n,x,y]

proof

let n be Element of NAT ; :: thesis: for x being set ex y being set st S₁[n,x,y]
let x be set ; :: thesis: ex y being set st S₁[n,x,y]
reconsider h = p . (n + 1) as Function ;

per cases ( x is Function or not x is Function ) ;

suppose x is Function ; :: thesis: ex y being set st S₁[n,x,y]

then reconsider g = x as Function ;
take y = h * g; :: thesis: S₁[n,x,y]
thus S₁[n,x,y] ; :: thesis: verum

end;

suppose A11: x is not Function ; :: thesis: ex y being set st S₁[n,x,y]

take y = 0 ; :: thesis: S₁[n,x,y]
thus S₁[n,x,y] by A11; :: thesis: verum

end;

end;

end;

consider f being Function such that
A14: ( dom f = NAT & f . 0 = id X ) and
A15: for n being Element of NAT holds S₁[n,f . n,f . (n + 1)] from RECDEF_1:sch 1(A10);
defpred S₂[ Element of NAT ] means f . $1 is Function;
A16: S₂[ 0 ] by A14;
A17: for i being Element of NAT st S₂[i] holds
S₂[i + 1]

proof

let i be Element of NAT ; :: thesis: ( S₂[i] implies S₂[i + 1] )
assume f . i is Function ; :: thesis: S₂[i + 1]
then reconsider g = f . i as Function ;
reconsider h = p . (i + 1) as Function ;
f . (i + 1) = h * g by A15;
hence S₂[i + 1] ; :: thesis: verum

end;

A18: for i being Element of NAT holds S₂[i] from NAT_1:sch 1(A16, A17);
then reconsider F = f . (len p) as Function ;
take F ; :: thesis: ex f being ManySortedFunction of st
( F = f . (len p) & f . 0 = id X & ( for i being Element of NAT st i + 1 in dom p holds
for g, h being Function st g = f . i & h = p . (i + 1) holds
f . (i + 1) = h * g ) )
f is Function-yielding

proof

let x be set ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in proj1 f or f . x is set )
assume x in dom f ; :: thesis: f . x is set
hence f . x is set by A14, A18; :: thesis: verum

end;

then reconsider f = f as ManySortedFunction of by A14, PARTFUN1:def 4, RELAT_1:def 18;
take f ; :: thesis: ( F = f . (len p) & f . 0 = id X & ( for i being Element of NAT st i + 1 in dom p holds
for g, h being Function st g = f . i & h = p . (i + 1) holds
f . (i + 1) = h * g ) )
thus ( F = f . (len p) & f . 0 = id X ) by A14; :: thesis: for i being Element of NAT st i + 1 in dom p holds
for g, h being Function st g = f . i & h = p . (i + 1) holds
f . (i + 1) = h * g
let i be Element of NAT ; :: thesis: ( i + 1 in dom p implies for g, h being Function st g = f . i & h = p . (i + 1) holds
f . (i + 1) = h * g )
thus ( i + 1 in dom p implies for g, h being Function st g = f . i & h = p . (i + 1) holds
f . (i + 1) = h * g ) by A15; :: thesis: verum