for r1, r2 being Real
for p being Point of (TOP-REAL 2) st p = CircleMap . r2 holds
(RotateCircle (1,(- (Arg p)))) . (CircleMap . r1) = CircleMap . (r1 - r2)