set TR = TOP-REAL n;
set cTR = the carrier of (TOP-REAL n);
let f be Function of (TOP-REAL n),(TOP-REAL n); :: thesis: ( f is homogeneous & f is additive & f is rotation implies f is being_homeomorphism )
assume A1: ( f is homogeneous & f is additive & f is rotation ) ; :: thesis: f is being_homeomorphism
then reconsider F = f as additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) ;
set M = AutMt F;

per cases ( Det (AutMt F) = 1. F_Real or ( Det (AutMt F) = - (1. F_Real) & not f is base_rotation ) ) by A1, Th37, Th38;

suppose Det (AutMt F) = 1. F_Real ; :: thesis: f is being_homeomorphism

then f is base_rotation by A1, Th37;
hence f is being_homeomorphism ; :: thesis: verum

end;

suppose A2: ( Det (AutMt F) = - (1. F_Real) & not f is base_rotation ) ; :: thesis: f is being_homeomorphism

n <> 0

proof

A3: ( dom f = the carrier of (TOP-REAL n) & dom (id the carrier of (TOP-REAL n)) = the carrier of (TOP-REAL n) ) by FUNCT_2:52;
assume n = 0 ; :: thesis: contradiction
then A4: the carrier of (TOP-REAL n) = {(0. (TOP-REAL n))} by EUCLID:22, EUCLID:77;
rng f c= the carrier of (TOP-REAL n) by RELAT_1:def 19;
then ( rng (id the carrier of (TOP-REAL n)) = the carrier of (TOP-REAL n) & rng f = the carrier of (TOP-REAL n) ) by A4, ZFMISC_1:33;
then f = id (TOP-REAL n) by A3, A4, FUNCT_1:7;
hence contradiction by A2; :: thesis: verum

end;

then A5: n in Seg n by FINSEQ_1:3;
A6: dom f = the carrier of (TOP-REAL n) by FUNCT_2:52;
set A = AxialSymmetry (n,n);
set MA = Mx2Tran (AxialSymmetry (n,n));
A7: (Mx2Tran (AxialSymmetry (n,n))) " is being_homeomorphism by TOPS_2:56;
A8: ( Mx2Tran (AxialSymmetry (n,n)) is one-to-one & rng (Mx2Tran (AxialSymmetry (n,n))) = [#] (TOP-REAL n) ) by TOPS_2:def 5;
AutMt (Mx2Tran (AxialSymmetry (n,n))) = AxialSymmetry (n,n) by Def6;
then A9: f * (Mx2Tran (AxialSymmetry (n,n))) is base_rotation by A1, A2, A5, Th39;
(f * (Mx2Tran (AxialSymmetry (n,n)))) * ((Mx2Tran (AxialSymmetry (n,n))) ") = f * ((Mx2Tran (AxialSymmetry (n,n))) * ((Mx2Tran (AxialSymmetry (n,n))) ")) by RELAT_1:36
.= f * (id the carrier of (TOP-REAL n)) by A8, TOPS_2:52
.= f by A6, RELAT_1:51 ;
hence f is being_homeomorphism by A9, A7, TOPS_2:57; :: thesis: verum

end;

end;