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