let x, y be Real; :: thesis: for u, v being Element of REAL 2 st u = <*x,y*> & v = <*y,x*> holds

|.u.| = |.v.|

let u, v be Element of REAL 2; :: thesis: ( u = <*x,y*> & v = <*y,x*> implies |.u.| = |.v.| )

assume A1: ( u = <*x,y*> & v = <*y,x*> ) ; :: thesis: |.u.| = |.v.|

then A3: ( len v = 2 & v . 1 = y & v . 2 = x ) by FINSEQ_1:44;

( len u = 2 & u . 1 = x & u . 2 = y ) by A1, FINSEQ_1:44;

hence |.u.| = sqrt ((x ^2) + (y ^2)) by EUCLID_3:22

.= |.v.| by A3, EUCLID_3:22 ;

:: thesis: verum

|.u.| = |.v.|

let u, v be Element of REAL 2; :: thesis: ( u = <*x,y*> & v = <*y,x*> implies |.u.| = |.v.| )

assume A1: ( u = <*x,y*> & v = <*y,x*> ) ; :: thesis: |.u.| = |.v.|

then A3: ( len v = 2 & v . 1 = y & v . 2 = x ) by FINSEQ_1:44;

( len u = 2 & u . 1 = x & u . 2 = y ) by A1, FINSEQ_1:44;

hence |.u.| = sqrt ((x ^2) + (y ^2)) by EUCLID_3:22

.= |.v.| by A3, EUCLID_3:22 ;

:: thesis: verum