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);

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

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 A5:
[y,x] in (Exch (Y,X)) " Z
; :: thesis: [x,y] in Zassume 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;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

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