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