set TR = TOP-REAL n;
set cTR = the carrier of ();
let f be Function of (),(); :: 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:
then reconsider F = f as additive homogeneous Function of (),() ;
set M = AutMt F;
per cases ( Det () = 1. F_Real or ( Det () = - () & not f is base_rotation ) ) by ;
suppose Det () = 1. F_Real ; :: thesis:
end;
suppose A2: ( Det () = - () & not f is base_rotation ) ; :: thesis:
n <> 0
proof
A3: ( dom f = the carrier of () & dom (id the carrier of ()) = the carrier of () ) by FUNCT_2:52;
assume n = 0 ; :: thesis: contradiction
then A4: the carrier of () = {(0. ())} by ;
rng f c= the carrier of () by RELAT_1:def 19;
then ( rng (id the carrier of ()) = the carrier of () & rng f = the carrier of () ) by ;
then f = id () by ;
hence contradiction by A2; :: thesis: verum
end;
then A5: n in Seg n by FINSEQ_1:3;
A6: dom f = the carrier of () 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))) = [#] () ) 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 ()) by
.= f by ;
hence f is being_homeomorphism by ; :: thesis: verum
end;
end;