let r, s be Real; for p being Point of (TOP-REAL 2) holds
( p in Sphere ((0. (TOP-REAL 2)),r) iff (Rotate s) . p in Sphere ((0. (TOP-REAL 2)),r) )
let p be Point of (TOP-REAL 2); ( p in Sphere ((0. (TOP-REAL 2)),r) iff (Rotate s) . p in Sphere ((0. (TOP-REAL 2)),r) )
A1:
|.p.| = |.((Rotate s) . p).|
by Th41;
A2:
((Rotate s) . p) - (0. (TOP-REAL 2)) = (Rotate s) . p
by RLVECT_1:13;
assume
(Rotate s) . p in Sphere ((0. (TOP-REAL 2)),r)
; p in Sphere ((0. (TOP-REAL 2)),r)
then A3:
|.((Rotate s) . p).| = r
by TOPREAL9:12;
A4:
(Rotate (- s)) . ((Rotate (- (- s))) . p) = p
by Th46;
((Rotate (- s)) . ((Rotate s) . p)) - (0. (TOP-REAL 2)) = (Rotate (- s)) . ((Rotate s) . p)
by RLVECT_1:13;
hence
p in Sphere ((0. (TOP-REAL 2)),r)
by A4, A3, A1, TOPREAL9:9; verum