let f, g be LinearOperator of [:X,Y:],[:Y,X:]; :: thesis: ( f is one-to-one & f is onto & f is isometric & ( for x being Point of X

for y being Point of Y holds f . (x,y) = [y,x] ) & g is one-to-one & g is onto & g is isometric & ( for x being Point of X

for y being Point of Y holds g . (x,y) = [y,x] ) implies f = g )

assume A27: ( f is one-to-one & f is onto & f is isometric & ( for x being Point of X

for y being Point of Y holds f . (x,y) = [y,x] ) ) ; :: thesis: ( not g is one-to-one or not g is onto or not g is isometric or ex x being Point of X ex y being Point of Y st not g . (x,y) = [y,x] or f = g )

assume A28: ( g is one-to-one & g is onto & g is isometric & ( for x being Point of X

for y being Point of Y holds g . (x,y) = [y,x] ) ) ; :: thesis: f = g

for x, y being set st x in the carrier of X & y in the carrier of Y holds

f . (x,y) = g . (x,y)

for y being Point of Y holds f . (x,y) = [y,x] ) & g is one-to-one & g is onto & g is isometric & ( for x being Point of X

for y being Point of Y holds g . (x,y) = [y,x] ) implies f = g )

assume A27: ( f is one-to-one & f is onto & f is isometric & ( for x being Point of X

for y being Point of Y holds f . (x,y) = [y,x] ) ) ; :: thesis: ( not g is one-to-one or not g is onto or not g is isometric or ex x being Point of X ex y being Point of Y st not g . (x,y) = [y,x] or f = g )

assume A28: ( g is one-to-one & g is onto & g is isometric & ( for x being Point of X

for y being Point of Y holds g . (x,y) = [y,x] ) ) ; :: thesis: f = g

for x, y being set st x in the carrier of X & y in the carrier of Y holds

f . (x,y) = g . (x,y)

proof

hence
f = g
by BINOP_1:def 21; :: thesis: verum
let x, y be set ; :: thesis: ( x in the carrier of X & y in the carrier of Y implies f . (x,y) = g . (x,y) )

assume A29: ( x in the carrier of X & y in the carrier of Y ) ; :: thesis: f . (x,y) = g . (x,y)

then reconsider x1 = x as Point of X ;

reconsider y1 = y as Point of Y by A29;

thus f . (x,y) = [y1,x1] by A27

.= g . (x,y) by A28 ; :: thesis: verum

end;assume A29: ( x in the carrier of X & y in the carrier of Y ) ; :: thesis: f . (x,y) = g . (x,y)

then reconsider x1 = x as Point of X ;

reconsider y1 = y as Point of Y by A29;

thus f . (x,y) = [y1,x1] by A27

.= g . (x,y) by A28 ; :: thesis: verum