let it1, it2 be BinOp of (BoundedLinearOperators (X,X)); ( ( for f, g being Element of BoundedLinearOperators (X,X) holds it1 . (f,g) = f * g ) & ( for f, g being Element of BoundedLinearOperators (X,X) holds it2 . (f,g) = f * g ) implies it1 = it2 )
assume that
A2:
for f, g being Element of BoundedLinearOperators (X,X) holds it1 . (f,g) = f * g
and
A3:
for f, g being Element of BoundedLinearOperators (X,X) holds it2 . (f,g) = f * g
; it1 = it2
hence
it1 = it2
by BINOP_1:2; verum