thus for G1, G2 being sequence of ExtREAL st ( for n being Element of NAT holds G1 . n = H₁(n) ) & ( for n being Element of NAT holds G2 . n = H₁(n) ) holds
G1 = G2 from BINOP_2:sch 1(); :: thesis: verum