let X, Y be RealNormSpace; :: thesis: for Z being Subset of [:X,Y:]
for x, y being object holds
( [x,y] in Z iff [y,x] in (Exch (Y,X)) " Z )
let Z be Subset of [:X,Y:]; :: thesis: for x, y being object holds
( [x,y] in Z iff [y,x] in (Exch (Y,X)) " Z )
let x, y be object ; :: thesis: ( [x,y] in Z iff [y,x] in (Exch (Y,X)) " Z )
set I = Exch (Y,X);

hereby :: thesis: ( [y,x] in (Exch (Y,X)) " Z implies [x,y] in Z )

assume A1: [x,y] in Z ; :: thesis: [y,x] in (Exch (Y,X)) " Z
then consider x1 being Point of X, y1 being Point of Y such that
A2: [x,y] = [x1,y1] by PRVECT_3:18;
A3: ( x = x1 & y = y1 ) by A2, XTUPLE_0:1;
A4: [x,y] = (Exch (Y,X)) . (y1,x1) by A2, Def1
.= (Exch (Y,X)) . [y,x] by A3 ;
[y1,x1] in the carrier of [:Y,X:] ;
hence [y,x] in (Exch (Y,X)) " Z by A1, A3, A4, FUNCT_2:38; :: thesis: verum

end;

assume A5: [y,x] in (Exch (Y,X)) " Z ; :: thesis: [x,y] in Z
then consider y1 being Point of Y, x1 being Point of X such that
A6: [y,x] = [y1,x1] by PRVECT_3:18;
A7: ( x = x1 & y = y1 ) by A6, XTUPLE_0:1;
(Exch (Y,X)) . [y,x] = (Exch (Y,X)) . (y1,x1) by A6
.= [x,y] by A7, Def1 ;
hence [x,y] in Z by A5, FUNCT_2:38; :: thesis: verum