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

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

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

A12: 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 A13: S₁[n] ; :: thesis: S₁[n + 1]
A14: g . [n,h] = g . (n,h) ;
f . [(n + 1),h] = f . ((n + 1),h)
.= (f . (n,h)) + h by A10
.= g . ((n + 1),h) by A11, A13, A14
.= g . [(n + 1),h] ;
hence S₁[n + 1] ; :: thesis: verum

end;

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

end;

hence f = g ; :: thesis: verum