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

A4: now

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

now

let a be Element of R; :: thesis: f . ((n + 1),a) = g . ((n + 1),a)
thus f . ((n + 1),a) = a + (f . (n,a)) by A2
.= a + (g . (n,a)) by A5
.= g . ((n + 1),a) by A3 ; :: thesis: verum

end;

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

end;

A6: S₁[ 0 ]

proof

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

end;

A7: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A6, A4);

A8: now

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

end;

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