reconsider e = 0 as Function ;
defpred S1[ 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 Nat
for x being set ex y being set st S1[n,x,y]
proof
let n be Nat; :: thesis: for x being set ex y being set st S1[n,x,y]
let x be set ; :: thesis: ex y being set st S1[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 S1[n,x,y]
then reconsider g = x as Function ;
take h * g ; :: thesis: S1[n,x,h * g]
thus S1[n,x,h * g] ; :: thesis: verum
end;
suppose A13: x is not Function ; :: thesis: ex y being set st S1[n,x,y]
take 0 ; :: thesis: S1[n,x, 0 ]
thus S1[n,x, 0 ] 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 Nat holds S1[n,f . n,f . (n + 1)] from RECDEF_1:sch 1(A12);
 defpred S2[ Nat] means f . $1 is Function;
A16: for i being Nat st S2[i] holds
S2[i + 1]
proof
let i be Nat; :: thesis: ( S2[i] implies S2[i + 1] )
reconsider h = p . (i + 1) as Function ;
assume f . i is Function ; :: thesis: S2[i + 1]
then reconsider g = f . i as Function ;
f . (i + 1) = h * g by A15;
hence S2[i + 1] ; :: thesis: verum
end;
A17: S2[ 0 ] by A14;
A18: for i being Nat holds S2[i] from NAT_1:sch 2(A17, A16);
 then reconsider F = f . (len p) as Function ;
f is Function-yielding by A14, A18;
then reconsider f = f as ManySortedFunction of NAT by A14, PARTFUN1:def 2, 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 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 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 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 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