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

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