defpred S1[ object , object , object ] means \$3 = [\$2,\$1];
A1: for x being Element of the carrier of X
for y being Element of the carrier of Y ex z being Element of the carrier of [:Y,X:] st S1[x,y,z]
proof
let x be Element of the carrier of X; :: thesis: for y being Element of the carrier of Y ex z being Element of the carrier of [:Y,X:] st S1[x,y,z]
let y be Element of the carrier of Y; :: thesis: ex z being Element of the carrier of [:Y,X:] st S1[x,y,z]
[y,x] is Point of [:Y,X:] ;
hence ex z being Element of the carrier of [:Y,X:] st S1[x,y,z] ; :: thesis: verum
end;
consider f being Function of [: the carrier of X, the carrier of Y:], the carrier of [:Y,X:] such that
A2: for x being Element of the carrier of X
for y being Element of the carrier of Y holds S1[x,y,f . (x,y)] from reconsider f = f as Function of [:X,Y:],[:Y,X:] ;
for p1, p2 being Point of [:X,Y:] holds f . (p1 + p2) = (f . p1) + (f . p2)
proof
let p1, p2 be Point of [:X,Y:]; :: thesis: f . (p1 + p2) = (f . p1) + (f . p2)
consider x1 being Point of X, y1 being Point of Y such that
A4: p1 = [x1,y1] by PRVECT_3:18;
consider x2 being Point of X, y2 being Point of Y such that
A5: p2 = [x2,y2] by PRVECT_3:18;
reconsider q1 = [y1,x1] as Point of [:Y,X:] ;
reconsider q2 = [y2,x2] as Point of [:Y,X:] ;
A8: f . p1 = f . (x1,y1) by A4
.= q1 by A2 ;
A9: f . p2 = f . (x2,y2) by A5
.= q2 by A2 ;
thus f . (p1 + p2) = f . ((x1 + x2),(y1 + y2)) by
.= [(y1 + y2),(x1 + x2)] by A2
.= (f . p1) + (f . p2) by ; :: thesis: verum
end;
then A10: f is additive ;
for p being Point of [:X,Y:]
for r being Real holds f . (r * p) = r * (f . p)
proof
let p be Point of [:X,Y:]; :: thesis: for r being Real holds f . (r * p) = r * (f . p)
let r be Real; :: thesis: f . (r * p) = r * (f . p)
consider x being Point of X, y being Point of Y such that
A11: p = [x,y] by PRVECT_3:18;
reconsider q = [y,x] as Point of [:Y,X:] ;
reconsider rq = [(r * y),(r * x)] as Point of [:Y,X:] ;
A12: f . p = f . (x,y) by A11
.= q by A2 ;
thus f . (r * p) = f . ((r * x),(r * y)) by
.= [(r * y),(r * x)] by A2
.= r * (f . p) by ; :: thesis: verum
end;
then reconsider f = f as LinearOperator of [:X,Y:],[:Y,X:] by ;
take f ; :: 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] ) )

A14: for p1, p2 being object st p1 in the carrier of [:X,Y:] & p2 in the carrier of [:X,Y:] & f . p1 = f . p2 holds
p1 = p2
proof
let p1, p2 be object ; :: thesis: ( p1 in the carrier of [:X,Y:] & p2 in the carrier of [:X,Y:] & f . p1 = f . p2 implies p1 = p2 )
assume A15: ( p1 in the carrier of [:X,Y:] & p2 in the carrier of [:X,Y:] & f . p1 = f . p2 ) ; :: thesis: p1 = p2
consider x1 being Point of X, y1 being Point of Y such that
A16: p1 = [x1,y1] by ;
consider x2 being Point of X, y2 being Point of Y such that
A17: p2 = [x2,y2] by ;
A18: f . p1 = f . (x1,y1) by A16
.= [y1,x1] by A2 ;
f . p2 = f . (x2,y2) by A17
.= [y2,x2] by A2 ;
then ( x1 = x2 & y1 = y2 ) by ;
hence p1 = p2 by ; :: thesis: verum
end;
for q being object st q in the carrier of [:Y,X:] holds
q in rng f
proof
let q be object ; :: thesis: ( q in the carrier of [:Y,X:] implies q in rng f )
assume q in the carrier of [:Y,X:] ; :: thesis: q in rng f
then consider y being Point of Y, x being Point of X such that
A22: q = [y,x] by PRVECT_3:18;
reconsider p = [x,y] as Point of [:X,Y:] ;
f . p = f . (x,y)
.= q by ;
hence q in rng f by FUNCT_2:4; :: thesis: verum
end;
then rng f = the carrier of [:Y,X:] by TARSKI:def 3;
hence ( f is one-to-one & f is onto ) by ; :: thesis: ( f is isometric & ( for x being Point of X
for y being Point of Y holds f . (x,y) = [y,x] ) )

for p being Point of [:X,Y:] holds ||.(f . p).|| =
proof
let p be Point of [:X,Y:]; :: thesis: ||.(f . p).|| =
consider x being Point of X, y being Point of Y such that
A23: p = [x,y] by PRVECT_3:18;
reconsider q = [y,x] as Point of [:Y,X:] ;
A24: f . p = f . (x,y) by A23
.= q by A2 ;
consider u being Element of REAL 2 such that
A25: ( u = & = |.u.| ) by ;
consider v being Element of REAL 2 such that
A26: ( v = & = |.v.| ) by PRVECT_3:18;
thus ||.(f . p).|| = by A24, A25, A26, Th6; :: thesis: verum
end;
hence f is isometric by NDIFF_7:7; :: thesis: for x being Point of X
for y being Point of Y holds f . (x,y) = [y,x]

thus for x being Point of X
for y being Point of Y holds f . (x,y) = [y,x] by A2; :: thesis: verum