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 Element of 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 Element of NAT holds g . x,(n + 1) = x \ ((g . x,n) ` ) ) ) ) implies f = g )
assume that
A24: for h being Element of G holds
( f . h,0 = 0. G & ( for n being Element of NAT holds f . h,(n + 1) = h \ ((f . h,n) ` ) ) ) and
A25: for h being Element of G holds
( g . h,0 = 0. G & ( for n being Element of NAT holds g . h,(n + 1) = h \ ((g . h,n) ` ) ) ) ; :: thesis: f = g

now

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₁[ Element of NAT ] means f . [h,$1] = g . [h,$1];
f . [h,0 ] = f . h,0
.= 0. G by A24
.= g . h,0 by A25
.= g . [h,0 ] ;
then A26: S₁[ 0 ] ;

A27: now

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A28: S₁[n] ; :: thesis: S₁[n + 1]
A29: ( f . [h,n] = f . h,n & g . [h,n] = g . h,n ) ;
f . [h,(n + 1)] = f . h,(n + 1)
.= h \ ((f . h,n) ` ) by A24
.= g . h,(n + 1) by A25, A28, A29
.= g . [h,(n + 1)] ;
hence S₁[n + 1] ; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A26, A27);
hence f . h,n = g . h,n ; :: thesis: verum

end;

hence f = g by BINOP_1:2; :: thesis: verum