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 ) ) );
A12: 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 A13: 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 A13; :: 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(A12);
defpred S₂[ Element of NAT ] means f . $1 is Function;
A16: 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] )
reconsider h = p . (i + 1) as Function ;
assume f . i is Function ; :: thesis: S₂[i + 1]
then reconsider g = f . i as Function ;
f . (i + 1) = h * g by A15;
hence S₂[i + 1] ; :: thesis: verum

end;

A17: S₂[ 0 ] by A14;
A18: for i being Element of NAT holds S₂[i] from NAT_1:sch 1(A17, A16);
then reconsider F = f . (len p) as Function ;
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 NAT by A14, PARTFUN1:def 4, RELAT_1:def 18;
take F ; :: thesis: ex f being ManySortedFunction of NAT 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 ) )
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