for o1, o2 being BinOp of COMPLEX st ( for a, b being Complex holds o1 . (a,b) = F₁(a,b) ) & ( for a, b being Complex holds o2 . (a,b) = F₁(a,b) ) holds
o1 = o2