let r1, r2 be Real; :: thesis: for p being Point of (TOP-REAL 2) st p = CircleMap . r2 holds
(RotateCircle (1,(- (Arg p)))) . (CircleMap . r1) = CircleMap . (r1 - r2)
let p be Point of (TOP-REAL 2); :: thesis: ( p = CircleMap . r2 implies (RotateCircle (1,(- (Arg p)))) . (CircleMap . r1) = CircleMap . (r1 - r2) )
assume A1: p = CircleMap . r2 ; :: thesis: (RotateCircle (1,(- (Arg p)))) . (CircleMap . r1) = CircleMap . (r1 - r2)
set s = - (Arg p);
reconsider q = CircleMap . (R^1 r1), w = CircleMap . (R^1 (r1 - r2)) as Point of (TOP-REAL 2) by PRE_TOPC:25;
|.q.| = 1 by TOPREALB:12;
then q <> 0. (TOP-REAL 2) by TOPRNS_1:23;
then consider i being Integer such that
A2: Arg ((Rotate (- (Arg p))) . q) = ((- (Arg p)) + (Arg q)) + ((2 * PI) * i) by Th43;
A3: Arg p = (2 * PI) * (frac r2) by A1, Th36;
A4: |.((Rotate (- (Arg p))) . q).| = |.q.| by Th41
.= 1 by TOPREALB:12
.= |.w.| by TOPREALB:12 ;
consider j being Integer such that
A5: frac (r1 - r2) = ((frac r1) - (frac r2)) + j and
( j = 0 or j = 1 ) by Th4;
A6: Arg ((Rotate (- (Arg p))) . q) = ((- ((2 * PI) * (frac r2))) + ((2 * PI) * (frac r1))) + ((2 * PI) * i) by A2, A3, Th36
.= ((2 * PI) * (frac (r1 - r2))) + ((2 * PI) * (i - j)) by A5
.= (Arg w) + ((2 * PI) * (i - j)) by Th36 ;
thus (RotateCircle (1,(- (Arg p)))) . (CircleMap . r1) = (Rotate (- (Arg p))) . q by FUNCT_1:49
.= CircleMap . (r1 - r2) by A4, A6, Th35 ; :: thesis: verum