let f, g be Function of [: the carrier of G,NAT:], the carrier of G; :: thesis: ( ( for x being Element of G holds
( f . (x,0) = 0. G & ( for n being Nat holds f . (x,(n + 1)) = x \ ((f . (x,n)) `) ) ) ) & ( for x being Element of G holds
( g . (x,0) = 0. G & ( for n being Nat holds g . (x,(n + 1)) = x \ ((g . (x,n)) `) ) ) ) implies f = g )
assume that
A9: for h being Element of G holds
( f . (h,0) = 0. G & ( for n being Nat holds f . (h,(n + 1)) = h \ ((f . (h,n)) `) ) ) and
A10: for h being Element of G holds
( g . (h,0) = 0. G & ( for n being Nat holds g . (h,(n + 1)) = h \ ((g . (h,n)) `) ) ) ; :: thesis: f = g

now :: thesis: for h being Element of G
for n being Element of NAT holds f . (h,n) = g . (h,n)

let h be Element of G; :: thesis: for n being Element of NAT holds f . (h,n) = g . (h,n)
let n be Element of NAT ; :: thesis: f . (h,n) = g . (h,n)
defpred S₁[ Nat] means f . [h,$1] = g . [h,$1];

A11: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A12: S₁[n] ; :: thesis: S₁[n + 1]
A13: g . [h,n] = g . (h,n) ;
f . [h,(n + 1)] = f . (h,(n + 1))
.= h \ ((f . (h,n)) `) by A9
.= g . (h,(n + 1)) by A10, A12, A13
.= g . [h,(n + 1)] ;
hence S₁[n + 1] ; :: thesis: verum

end;

f . [h,0] = f . (h,0)
.= 0. G by A9
.= g . (h,0) by A10
.= g . [h,0] ;
then A14: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A14, A11);
hence f . (h,n) = g . (h,n) ; :: thesis: verum

end;

hence f = g ; :: thesis: verum