let r, s be Real; :: thesis: 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); :: thesis: ( 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;
hereby :: thesis: ( (Rotate s) . p in Sphere ((0. (TOP-REAL 2)),r) implies p in Sphere ((0. (TOP-REAL 2)),r) )
assume p in Sphere ((0. (TOP-REAL 2)),r) ; :: thesis: (Rotate s) . p in Sphere ((0. (TOP-REAL 2)),r)
then |.p.| = r by TOPREAL9:12;
hence (Rotate s) . p in Sphere ((0. (TOP-REAL 2)),r) by A1, A2, TOPREAL9:9; :: thesis: verum
end;
assume (Rotate s) . p in Sphere ((0. (TOP-REAL 2)),r) ; :: thesis: 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; :: thesis: verum