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;

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;

end;

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

n <> 0

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;proof

then A5:
n in Seg n
by FINSEQ_1:3;
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;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

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