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)

proof

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;

hence f = g by BINOP_1:def 21; :: thesis: verum