let o1, o2 be BinOp of COMPLEX; :: thesis: ( ( for a, b being Complex holds o1 . (a,b) = F₁(a,b) ) & ( for a, b being Complex holds o2 . (a,b) = F₁(a,b) ) implies o1 = o2 )
assume that
A1: for a, b being Complex holds o1 . (a,b) = F₁(a,b) and
A2: for a, b being Complex holds o2 . (a,b) = F₁(a,b) ; :: thesis: o1 = o2

now :: thesis: for a, b being Element of COMPLEX holds o1 . (a,b) = o2 . (a,b)

let a, b be Element of COMPLEX ; :: thesis: o1 . (a,b) = o2 . (a,b)
thus o1 . (a,b) = F₁(a,b) by A1
.= o2 . (a,b) by A2 ; :: thesis: verum

end;

hence o1 = o2 ; :: thesis: verum