let I1, I2 be LinearOperator of [:X,Y:],(product <*X,Y*>); ( ( for x being Point of X
for y being Point of Y holds I1 . (x,y) = <*x,y*> ) & ( for x being Point of X
for y being Point of Y holds I2 . (x,y) = <*x,y*> ) implies I1 = I2 )
assume that
A1:
for x being Point of X
for y being Point of Y holds I1 . (x,y) = <*x,y*>
and
A2:
for x being Point of X
for y being Point of Y holds I2 . (x,y) = <*x,y*>
; I1 = I2
for x, y being set st x in the carrier of X & y in the carrier of Y holds
I1 . (x,y) = I2 . (x,y)
hence
I1 = I2
by BINOP_1:def 21; verum