let n be Nat; :: thesis: for p being Point of ()
for r being Real
for f being additive homogeneous rotation Function of (),() st f is onto holds
( f .: (Ball (p,r)) = Ball ((f . p),r) & f .: (cl_Ball (p,r)) = cl_Ball ((f . p),r) & f .: (Sphere (p,r)) = Sphere ((f . p),r) )

let p be Point of (); :: thesis: for r being Real
for f being additive homogeneous rotation Function of (),() st f is onto holds
( f .: (Ball (p,r)) = Ball ((f . p),r) & f .: (cl_Ball (p,r)) = cl_Ball ((f . p),r) & f .: (Sphere (p,r)) = Sphere ((f . p),r) )

let r be Real; :: thesis: for f being additive homogeneous rotation Function of (),() st f is onto holds
( f .: (Ball (p,r)) = Ball ((f . p),r) & f .: (cl_Ball (p,r)) = cl_Ball ((f . p),r) & f .: (Sphere (p,r)) = Sphere ((f . p),r) )

set TR = TOP-REAL n;
let f be additive homogeneous rotation Function of (),(); :: thesis: ( f is onto implies ( f .: (Ball (p,r)) = Ball ((f . p),r) & f .: (cl_Ball (p,r)) = cl_Ball ((f . p),r) & f .: (Sphere (p,r)) = Sphere ((f . p),r) ) )
assume f is onto ; :: thesis: ( f .: (Ball (p,r)) = Ball ((f . p),r) & f .: (cl_Ball (p,r)) = cl_Ball ((f . p),r) & f .: (Sphere (p,r)) = Sphere ((f . p),r) )
A2: - (f . p) = (- 1) * (f . p) by RLVECT_1:16
.= f . ((- 1) * p) by TOPREAL9:def 4
.= f . (- p) by RLVECT_1:16 ;
A3: rng f = the carrier of () by FUNCT_2:def 3;
thus f .: (Ball (p,r)) = Ball ((f . p),r) :: thesis: ( f .: (cl_Ball (p,r)) = cl_Ball ((f . p),r) & f .: (Sphere (p,r)) = Sphere ((f . p),r) )
proof
thus f .: (Ball (p,r)) c= Ball ((f . p),r) :: according to XBOOLE_0:def 10 :: thesis: Ball ((f . p),r) c= f .: (Ball (p,r))
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: (Ball (p,r)) or y in Ball ((f . p),r) )
assume y in f .: (Ball (p,r)) ; :: thesis: y in Ball ((f . p),r)
then consider x being object such that
A4: x in dom f and
A5: x in Ball (p,r) and
A6: f . x = y by FUNCT_1:def 6;
reconsider q = x as Point of () by A4;
(f . q) - (f . p) = f . (q - p) by ;
then A7: |.((f . q) - (f . p)).| = |.(q - p).| by MATRTOP3:def 4;
|.(q - p).| < r by ;
hence y in Ball ((f . p),r) by A7, A6; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Ball ((f . p),r) or y in f .: (Ball (p,r)) )
assume A8: y in Ball ((f . p),r) ; :: thesis: y in f .: (Ball (p,r))
then consider x being object such that
A9: x in dom f and
A10: f . x = y by ;
reconsider x = x as Point of () by A9;
(f . x) - (f . p) = f . (x - p) by ;
then A11: |.((f . x) - (f . p)).| = |.(x - p).| by MATRTOP3:def 4;
|.((f . x) - (f . p)).| < r by ;
then x in Ball (p,r) by A11;
hence y in f .: (Ball (p,r)) by ; :: thesis: verum
end;
thus f .: (cl_Ball (p,r)) = cl_Ball ((f . p),r) :: thesis: f .: (Sphere (p,r)) = Sphere ((f . p),r)
proof
thus f .: (cl_Ball (p,r)) c= cl_Ball ((f . p),r) :: according to XBOOLE_0:def 10 :: thesis: cl_Ball ((f . p),r) c= f .: (cl_Ball (p,r))
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: (cl_Ball (p,r)) or y in cl_Ball ((f . p),r) )
assume y in f .: (cl_Ball (p,r)) ; :: thesis: y in cl_Ball ((f . p),r)
then consider x being object such that
A12: x in dom f and
A13: x in cl_Ball (p,r) and
A14: f . x = y by FUNCT_1:def 6;
reconsider q = x as Point of () by A12;
(f . q) - (f . p) = f . (q - p) by ;
then A15: |.((f . q) - (f . p)).| = |.(q - p).| by MATRTOP3:def 4;
|.(q - p).| <= r by ;
hence y in cl_Ball ((f . p),r) by ; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in cl_Ball ((f . p),r) or y in f .: (cl_Ball (p,r)) )
assume A16: y in cl_Ball ((f . p),r) ; :: thesis: y in f .: (cl_Ball (p,r))
then consider x being object such that
A17: x in dom f and
A18: f . x = y by ;
reconsider x = x as Point of () by A17;
(f . x) - (f . p) = f . (x - p) by ;
then A19: |.((f . x) - (f . p)).| = |.(x - p).| by MATRTOP3:def 4;
|.((f . x) - (f . p)).| <= r by ;
then x in cl_Ball (p,r) by A19;
hence y in f .: (cl_Ball (p,r)) by ; :: thesis: verum
end;
thus f .: (Sphere (p,r)) c= Sphere ((f . p),r) :: according to XBOOLE_0:def 10 :: thesis: Sphere ((f . p),r) c= f .: (Sphere (p,r))
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: (Sphere (p,r)) or y in Sphere ((f . p),r) )
assume y in f .: (Sphere (p,r)) ; :: thesis: y in Sphere ((f . p),r)
then consider x being object such that
A20: x in dom f and
A21: x in Sphere (p,r) and
A22: f . x = y by FUNCT_1:def 6;
reconsider q = x as Point of () by A20;
(f . q) - (f . p) = f . (q - p) by ;
then A23: |.((f . q) - (f . p)).| = |.(q - p).| by MATRTOP3:def 4;
|.(q - p).| = r by ;
hence y in Sphere ((f . p),r) by ; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Sphere ((f . p),r) or y in f .: (Sphere (p,r)) )
assume A24: y in Sphere ((f . p),r) ; :: thesis: y in f .: (Sphere (p,r))
then consider x being object such that
A25: x in dom f and
A26: f . x = y by ;
reconsider x = x as Point of () by A25;
(f . x) - (f . p) = f . (x - p) by ;
then A27: |.((f . x) - (f . p)).| = |.(x - p).| by MATRTOP3:def 4;
|.((f . x) - (f . p)).| = r by ;
then x in Sphere (p,r) by A27;
hence y in f .: (Sphere (p,r)) by ; :: thesis: verum