let f1, f2 be Function of NAT ,NAT ; :: thesis: ( ( for k being Element of NAT holds f1 . k = Fib k ) & ( for k being Element of NAT holds f2 . k = Fib k ) implies f1 = f2 )
assume that
A1: for k being Element of NAT holds f1 . k = Fib k and
A2: for k being Element of NAT holds f2 . k = Fib k ; :: thesis: f1 = f2
for f1, f2 being Function of NAT ,NAT st ( for x being Element of NAT holds f1 . x = Fib x ) & ( for x being Element of NAT holds f2 . x = Fib x ) holds
f1 = f2 from BINOP_2:sch 1();
hence f1 = f2 by A1, A2; :: thesis: verum