A1: for f1, f2 being sequence of NAT st ( for x being Element of NAT holds f1 . x = Euler x ) & ( for x being Element of NAT holds f2 . x = Euler 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 = Euler k ) & ( for k being Element of NAT holds f2 . k = Euler k ) implies f1 = f2 )
assume ( ( for k being Element of NAT holds f1 . k = Euler k ) & ( for k being Element of NAT holds f2 . k = Euler k ) ) ; :: thesis: f1 = f2
hence f1 = f2 by A1; :: thesis: verum