let it1, it2 be BinOp of (Funcs (A,COMPLEX)); :: thesis: ( ( 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) ; :: thesis: 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) ; :: thesis: it1 = it2

now :: thesis: for f, g being Element of Funcs (A,COMPLEX) holds it1 . (f,g) = it2 . (f,g)

hence
it1 = it2
; :: thesis: verumlet f, g be Element of Funcs (A,COMPLEX); :: thesis: it1 . (f,g) = it2 . (f,g)

thus it1 . (f,g) = multcomplex .: (f,g) by A2

.= it2 . (f,g) by A3 ; :: thesis: verum

end;thus it1 . (f,g) = multcomplex .: (f,g) by A2

.= it2 . (f,g) by A3 ; :: thesis: verum