deffunc H₁( 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₁(n,g . n) ) ) from NAT_1:sch 11();
defpred S₁[ Nat] means g . $1 in the carrier of X;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
then reconsider gk = g . k as Element of X ;
g . (k + 1) = the multF of X . [gk,z] by A1;
hence S₁[k + 1] ; :: thesis: verum

end;

A3: S₁[ 0 ] by A1;
for n being Nat holds S₁[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