let it1, it2 be BinOp of (Funcs (A,COMPLEX)); ( ( for f, g being Element of Funcs (A,COMPLEX) holds it1 . (f,g) = multcomplex .: (f,g) ) & ( for f, g being Element of Funcs (A,COMPLEX) holds it2 . (f,g) = multcomplex .: (f,g) ) implies it1 = it2 )
assume that
A2:
for f, g being Element of Funcs (A,COMPLEX) holds it1 . (f,g) = multcomplex .: (f,g)
and
A3:
for f, g being Element of Funcs (A,COMPLEX) holds it2 . (f,g) = multcomplex .: (f,g)
; it1 = it2
hence
it1 = it2
; verum