let f, g be Function of [: the carrier of X,NAT:], the carrier of X; :: thesis: ( ( 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 ) ) ; :: thesis: f = g

( 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 ) ) ; :: thesis: f = g

now :: thesis: for h being Element of X

for n being Nat holds f . (h,n) = g . (h,n)

hence
f = g
; :: thesis: verumfor n being Nat holds f . (h,n) = g . (h,n)

let h be Element of X; :: thesis: for n being Nat holds f . (h,n) = g . (h,n)

let n be Nat; :: thesis: f . (h,n) = g . (h,n)

defpred S_{1}[ Nat] means f . [h,$1] = g . [h,$1];

.= 0. X by A10

.= g . (h,0) by A11

.= g . [h,0] ;

then A15: S_{1}[ 0 ]
;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A15, A12);

hence f . (h,n) = g . (h,n) ; :: thesis: verum

end;let n be Nat; :: thesis: f . (h,n) = g . (h,n)

defpred S

A12: now :: thesis: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]

f . [h,0] =
f . (h,0)
S

let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A13: S_{1}[n]
; :: thesis: S_{1}[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 S_{1}[n + 1]
; :: thesis: verum

end;assume A13: S

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 S

.= 0. X by A10

.= g . (h,0) by A11

.= g . [h,0] ;

then A15: S

for n being Nat holds S

hence f . (h,n) = g . (h,n) ; :: thesis: verum