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
A4:
for x being Point of X
for y being Point of Y holds I1 . (x,y) = <*x,y*>
and
A5:
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)
proof
let x,
y be
set ;
( x in the carrier of X & y in the carrier of Y implies I1 . (x,y) = I2 . (x,y) )
assume
x in the
carrier of
X
;
( not y in the carrier of Y or I1 . (x,y) = I2 . (x,y) )
then reconsider x1 =
x as
Point of
X ;
assume
y in the
carrier of
Y
;
I1 . (x,y) = I2 . (x,y)
then reconsider y1 =
y as
Point of
Y ;
thus I1 . (
x,
y) =
<*x1,y1*>
by A4
.=
I2 . (
x,
y)
by A5
;
verum
end;
hence
I1 = I2
by BINOP_1:def 21; verum