let f, g be Function of [: the carrier of R,NAT:], the carrier of R; :: thesis: ( ( for a being Element of R holds
( f . (a,0) = 0. R & ( for n being Element of NAT holds f . (a,(n + 1)) = (f . (a,n)) + a ) ) ) & ( for a being Element of R holds
( g . (a,0) = 0. R & ( for n being Element of NAT holds g . (a,(n + 1)) = (g . (a,n)) + a ) ) ) implies f = g )
assume A13: for a being Element of R holds
( f . (a,0) = 0. R & ( for n being Element of NAT holds f . (a,(n + 1)) = (f . (a,n)) + a ) ) ; :: thesis: ( ex a being Element of R st
( g . (a,0) = 0. R implies ex n being Element of NAT st not g . (a,(n + 1)) = (g . (a,n)) + a ) or f = g )
defpred S₁[ Nat] means for a being Element of R holds f . (a,$1) = g . (a,$1);
assume A14: for a being Element of R holds
( g . (a,0) = 0. R & ( for n being Element of NAT holds g . (a,(n + 1)) = (g . (a,n)) + a ) ) ; :: thesis: f = g

A15: 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 A16: S₁[n] ; :: thesis: S₁[n + 1]

now :: thesis: for a being Element of R holds f . (a,(n + 1)) = g . (a,(n + 1))

let a be Element of R; :: thesis: f . (a,(n + 1)) = g . (a,(n + 1))
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
thus f . (a,(n + 1)) = (f . (a,nn)) + a by A13
.= (g . (a,nn)) + a by A16
.= g . (a,(n + 1)) by A14 ; :: thesis: verum

end;

hence S₁[n + 1] ; :: thesis: verum

end;

A17: S₁[ 0 ]

proof

let a be Element of R; :: thesis: f . (a,0) = g . (a,0)
thus f . (a,0) = 0. R by A13
.= g . (a,0) by A14 ; :: thesis: verum

end;

A18: for n being Nat holds S₁[n] from NAT_1:sch 2(A17, A15);

A19: now :: thesis: for x being object st x in [: the carrier of R,NAT:] holds
f . x = g . x

let x be object ; :: thesis: ( x in [: the carrier of R,NAT:] implies f . x = g . x )
assume x in [: the carrier of R,NAT:] ; :: thesis: f . x = g . x
then consider v, u being object such that
A20: v in the carrier of R and
A21: u in NAT and
A22: x = [v,u] by ZFMISC_1:def 2;
reconsider v = v as Element of R by A20;
reconsider u = u as Element of NAT by A21;
thus f . x = f . (v,u) by A22
.= g . (v,u) by A18
.= g . x by A22 ; :: thesis: verum

end;

( dom f = [: the carrier of R,NAT:] & dom g = [: the carrier of R,NAT:] ) by FUNCT_2:def 1;
hence f = g by A19, FUNCT_1:2; :: thesis: verum