let x, y be Real; 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; ( u = <*x,y*> & v = <*y,x*> implies |.u.| = |.v.| )
assume A1:
( u = <*x,y*> & v = <*y,x*> )
; |.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
;
verum