deffunc H_{1}( set , set ) -> set = the multF of X . [$2,z];

consider g being Function such that

A1: ( dom g = NAT & g . 0 = 1. X & ( for n being Nat holds g . (n + 1) = H_{1}(n,g . n) ) )
from NAT_1:sch 11();

defpred S_{1}[ Nat] means g . $1 in the carrier of X;

A2: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
by A1;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A3, A2);

then for n being object st n in NAT holds

g . n in the carrier of X ;

then reconsider g0 = g as sequence of X by A1, FUNCT_2:3;

take g0 ; :: thesis: ( g0 . 0 = 1. X & ( for n being Nat holds g0 . (n + 1) = (g0 . n) * z ) )

thus ( g0 . 0 = 1. X & ( for n being Nat holds g0 . (n + 1) = (g0 . n) * z ) ) by A1; :: thesis: verum

consider g being Function such that

A1: ( dom g = NAT & g . 0 = 1. X & ( for n being Nat holds g . (n + 1) = H

defpred S

A2: for k being Nat st S

S

proof

A3:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume S_{1}[k]
; :: thesis: S_{1}[k + 1]

then reconsider gk = g . k as Element of X ;

g . (k + 1) = the multF of X . [gk,z] by A1;

hence S_{1}[k + 1]
; :: thesis: verum

end;assume S

then reconsider gk = g . k as Element of X ;

g . (k + 1) = the multF of X . [gk,z] by A1;

hence S

for n being Nat holds S

then for n being object st n in NAT holds

g . n in the carrier of X ;

then reconsider g0 = g as sequence of X by A1, FUNCT_2:3;

take g0 ; :: thesis: ( g0 . 0 = 1. X & ( for n being Nat holds g0 . (n + 1) = (g0 . n) * z ) )

thus ( g0 . 0 = 1. X & ( for n being Nat holds g0 . (n + 1) = (g0 . n) * z ) ) by A1; :: thesis: verum