thus for s1, s2 being Complex_Sequence st ( for x being Element of NAT holds s1 . x = H₃(x) ) & ( for x being Element of NAT holds s2 . x = H₃(x) ) holds
s1 = s2 from BINOP_2:sch 1(); :: thesis: verum