let s be Real; :: thesis: for p being Point of (TOP-REAL 2) holds |.((Rotate s) . p).| = |.p.|
let p be Point of (TOP-REAL 2); :: thesis: |.((Rotate s) . p).| = |.p.|
set c = euc2cpx p;
set q = (Rotate s) . p;
A1: ( Re (Rotate ((euc2cpx p),s)) = |.(euc2cpx p).| * (cos (s + (Arg (euc2cpx p)))) & Im (Rotate ((euc2cpx p),s)) = |.(euc2cpx p).| * (sin (s + (Arg (euc2cpx p)))) ) by COMPLEX1:12;
(Rotate s) . p = cpx2euc (Rotate ((euc2cpx p),s)) by JORDAN24:def 3;
then A2: ( ((Rotate s) . p) `1 = Re (Rotate ((euc2cpx p),s)) & ((Rotate s) . p) `2 = Im (Rotate ((euc2cpx p),s)) ) by EUCLID:52;
|.p.| ^2 = (|.(euc2cpx p).| ^2) * 1 by EUCLID_3:25
.= (|.(euc2cpx p).| ^2) * (((cos (s + (Arg (euc2cpx p)))) ^2) + ((sin (s + (Arg (euc2cpx p)))) ^2)) by SIN_COS:29
.= ((|.(euc2cpx p).| * (cos (s + (Arg (euc2cpx p))))) ^2) + ((|.(euc2cpx p).| * (sin (s + (Arg (euc2cpx p))))) ^2)
.= |.((Rotate s) . p).| ^2 by A1, A2, JGRAPH_1:29 ;
hence |.p.| = |.((Rotate s) . p).| by Th1; :: thesis: verum