A1: for f1, f2 being sequence of 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();
let f1, f2 be sequence of 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 ( ( for k being Element of NAT holds f1 . k = Fib k ) & ( for k being Element of NAT holds f2 . k = Fib k ) ) ; :: thesis: f1 = f2
hence f1 = f2 by A1; :: thesis: verum