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 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 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 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 Nat st not g . ((n + 1),a) = a + (g . (n,a)) ) or f = g )
defpred S₁[ 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 Nat holds g . ((n + 1),a) = a + (g . (n,a)) ) ) ; :: thesis: f = g

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

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

let a be Element of R; :: thesis: f . ((n + 1),a) = g . ((n + 1),a)
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
thus f . ((n + 1),a) = a + (f . (nn,a)) by A2
.= a + (g . (nn,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 Nat holds S₁[n] from NAT_1:sch 2(A6, A4);

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

let x be object ; :: 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 object 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