defpred S_{1}[ 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 S_{1}[x,y,z]

A2: for x being Element of the carrier of X

for y being Element of the carrier of Y holds S_{1}[x,y,f . (x,y)]
from BINOP_1:sch 3(A1);

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)

for p being Point of [:X,Y:]

for r being Real holds f . (r * p) = r * (f . p)

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

q in rng f

hence ( f is one-to-one & f is onto ) by A14, FUNCT_2:19; :: 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).|| = ||.p.||

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

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 S

proof

consider f being Function of [: the carrier of X, the carrier of Y:], the carrier of [:Y,X:] such that
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 S_{1}[x,y,z]

let y be Element of the carrier of Y; :: thesis: ex z being Element of the carrier of [:Y,X:] st S_{1}[x,y,z]

[y,x] is Point of [:Y,X:] ;

hence ex z being Element of the carrier of [:Y,X:] st S_{1}[x,y,z]
; :: thesis: verum

end;let y be Element of the carrier of Y; :: thesis: ex z being Element of the carrier of [:Y,X:] st S

[y,x] is Point of [:Y,X:] ;

hence ex z being Element of the carrier of [:Y,X:] st S

A2: for x being Element of the carrier of X

for y being Element of the carrier of Y holds S

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

then A10:
f is additive
;
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 A4, A5, PRVECT_3:18

.= [(y1 + y2),(x1 + x2)] by A2

.= (f . p1) + (f . p2) by A8, A9, PRVECT_3:18 ; :: thesis: verum

end;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 A4, A5, PRVECT_3:18

.= [(y1 + y2),(x1 + x2)] by A2

.= (f . p1) + (f . p2) by A8, A9, PRVECT_3:18 ; :: thesis: verum

for p being Point of [:X,Y:]

for r being Real holds f . (r * p) = r * (f . p)

proof

then reconsider f = f as LinearOperator of [:X,Y:],[:Y,X:] by A10, LOPBAN_1:def 5;
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 A11, PRVECT_3:18

.= [(r * y),(r * x)] by A2

.= r * (f . p) by A12, PRVECT_3:18 ; :: thesis: verum

end;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 A11, PRVECT_3:18

.= [(r * y),(r * x)] by A2

.= r * (f . p) by A12, PRVECT_3:18 ; :: thesis: verum

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

for q being object st q in the carrier of [:Y,X:] holds
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 A15, PRVECT_3:18;

consider x2 being Point of X, y2 being Point of Y such that

A17: p2 = [x2,y2] by A15, PRVECT_3:18;

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 A15, A18, XTUPLE_0:1;

hence p1 = p2 by A16, A17; :: thesis: verum

end;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 A15, PRVECT_3:18;

consider x2 being Point of X, y2 being Point of Y such that

A17: p2 = [x2,y2] by A15, PRVECT_3:18;

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 A15, A18, XTUPLE_0:1;

hence p1 = p2 by A16, A17; :: thesis: verum

q in rng f

proof

then
rng f = the carrier of [:Y,X:]
by TARSKI:def 3;
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 A2, A22 ;

hence q in rng f by FUNCT_2:4; :: thesis: verum

end;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 A2, A22 ;

hence q in rng f by FUNCT_2:4; :: thesis: verum

hence ( f is one-to-one & f is onto ) by A14, FUNCT_2:19; :: 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).|| = ||.p.||

proof

hence
f is isometric
by NDIFF_7:7; :: thesis: for x being Point of X
let p be Point of [:X,Y:]; :: thesis: ||.(f . p).|| = ||.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 = <*||.x.||,||.y.||*> & ||.p.|| = |.u.| ) by A23, PRVECT_3:18;

consider v being Element of REAL 2 such that

A26: ( v = <*||.y.||,||.x.||*> & ||.q.|| = |.v.| ) by PRVECT_3:18;

thus ||.(f . p).|| = ||.p.|| by A24, A25, A26, Th6; :: thesis: verum

end;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 = <*||.x.||,||.y.||*> & ||.p.|| = |.u.| ) by A23, PRVECT_3:18;

consider v being Element of REAL 2 such that

A26: ( v = <*||.y.||,||.x.||*> & ||.q.|| = |.v.| ) by PRVECT_3:18;

thus ||.(f . p).|| = ||.p.|| by A24, A25, A26, Th6; :: thesis: verum

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