let f, g be Function of [: the carrier of G,NAT:], the carrier of G; ( ( 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)) `) ) )
; f = g
now 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;
for n being Element of NAT holds f . (h,n) = g . (h,n)let n be
Element of
NAT ;
f . (h,n) = g . (h,n)defpred S1[
Nat]
means f . [h,$1] = g . [h,$1];
A11:
now for n being Nat st S1[n] holds
S1[n + 1]let n be
Nat;
( S1[n] implies S1[n + 1] )assume A12:
S1[
n]
;
S1[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
S1[
n + 1]
;
verum end; f . [h,0] =
f . (
h,
0)
.=
0. G
by A9
.=
g . (
h,
0)
by A10
.=
g . [h,0]
;
then A14:
S1[
0 ]
;
for
n being
Nat holds
S1[
n]
from NAT_1:sch 2(A14, A11);
hence
f . (
h,
n)
= g . (
h,
n)
;
verum end;
hence
f = g
; verum