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 A12: 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 )
assume A13: 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
defpred S₁[ Element of NAT ] means for a being Element of R holds f . a,$1 = g . a,$1;
A14: S₁[ 0 ]

proof

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

end;

A15: now

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A16: S₁[n] ; :: thesis: S₁[n + 1]

now

let a be Element of R; :: thesis: f . a,(n + 1) = g . a,(n + 1)
thus f . a,(n + 1) = (f . a,n) + a by A12
.= (g . a,n) + a by A16
.= g . a,(n + 1) by A13 ; :: thesis: verum

end;

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

end;

A17: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A14, A15);
A18: dom f = [:the carrier of R,NAT :] by FUNCT_2:def 1;
A19: dom g = [:the carrier of R,NAT :] by FUNCT_2:def 1;

now

let x be set ; :: 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 set such that
A20: ( v in the carrier of R & u in NAT & x = [v,u] ) by ZFMISC_1:def 2;
reconsider u = u as Element of NAT by A20;
reconsider v = v as Element of R by A20;
thus f . x = f . v,u by A20
.= g . v,u by A17
.= g . x by A20 ; :: thesis: verum

end;

hence f = g by A18, A19, FUNCT_1:9; :: thesis: verum