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₁[ Element of 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

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 A13
.= (g . a,n) + 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 Element of NAT holds S₁[n] from NAT_1:sch 1(A17, A15);

A19: 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 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:9; :: thesis: verum