let f, g be Function of [: the carrier of X,NAT:], the carrier of X; ( ( for h being Element of X holds
( f . (h,0) = 0. X & ( for n being Nat holds f . (h,(n + 1)) = (f . (h,n)) * h ) ) ) & ( for h being Element of X holds
( g . (h,0) = 0. X & ( for n being Nat holds g . (h,(n + 1)) = (g . (h,n)) * h ) ) ) implies f = g )
assume that
A10:
for h being Element of X holds
( f . (h,0) = 0. X & ( for n being Nat holds f . (h,(n + 1)) = (f . (h,n)) * h ) )
and
A11:
for h being Element of X holds
( g . (h,0) = 0. X & ( for n being Nat holds g . (h,(n + 1)) = (g . (h,n)) * h ) )
; f = g
now for h being Element of X
for n being Nat holds f . (h,n) = g . (h,n)let h be
Element of
X;
for n being Nat holds f . (h,n) = g . (h,n)let n be
Nat;
f . (h,n) = g . (h,n)defpred S1[
Nat]
means f . [h,$1] = g . [h,$1];
A12:
now for n being Nat st S1[n] holds
S1[n + 1]let n be
Nat;
( S1[n] implies S1[n + 1] )assume A13:
S1[
n]
;
S1[n + 1]A14:
g . [h,n] = g . (
h,
n)
;
f . [h,(n + 1)] =
f . (
h,
(n + 1))
.=
(f . (h,n)) * h
by A10
.=
g . (
h,
(n + 1))
by A11, A13, A14
.=
g . [h,(n + 1)]
;
hence
S1[
n + 1]
;
verum end; f . [h,0] =
f . (
h,
0)
.=
0. X
by A10
.=
g . (
h,
0)
by A11
.=
g . [h,0]
;
then A15:
S1[
0 ]
;
for
n being
Nat holds
S1[
n]
from NAT_1:sch 2(A15, A12);
hence
f . (
h,
n)
= g . (
h,
n)
;
verum end;
hence
f = g
; verum