set TR = TOP-REAL n;
set cTR = the carrier of (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 Th36, Th37;

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

then f is base_rotation by Th36;
hence AutMt f is Orthogonal by L; :: thesis: verum

end;

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

E: 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 n = 0 ;
then A5: the carrier of (TOP-REAL n) = {(0. (TOP-REAL n))} by JORDAN2C:105, EUCLID:22;
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 A5, RELAT_1:45, ZFMISC_1:33;
then f = id (TOP-REAL n) by A3, A5, FUNCT_1:7;
hence contradiction by A2; :: thesis: verum

end;

then A6: n in Seg n by FINSEQ_1:3;
set A = AxialSymmetry (n,n);
set MA = Mx2Tran (AxialSymmetry (n,n));
AutMt (Mx2Tran (AxialSymmetry (n,n))) = AxialSymmetry (n,n) by Def6;
then A10: f * (Mx2Tran (AxialSymmetry (n,n))) is base_rotation by A2, A6, Th38;
( AxialSymmetry (n,n) is diagonal & (AxialSymmetry (n,n)) ~ = AxialSymmetry (n,n) ) by A6, Th15;
then (AxialSymmetry (n,n)) @ = (AxialSymmetry (n,n)) ~ by LLL;
then E0: ( AxialSymmetry (n,n) is Orthogonal & AutMt (f * (Mx2Tran (AxialSymmetry (n,n)))) is Orthogonal ) by A10, L, MATRIX_6:def 7;
E2: AutMt (f * (Mx2Tran (AxialSymmetry (n,n)))) = (AutMt (Mx2Tran (AxialSymmetry (n,n)))) * (AutMt f) by TA
.= (AxialSymmetry (n,n)) * (AutMt f) by Def6 ;
(AxialSymmetry (n,n)) ~ is_reverse_of AxialSymmetry (n,n) by MATRIX_6:def 4;
then E1: ((AxialSymmetry (n,n)) ~) * (AxialSymmetry (n,n)) = 1. (F_Real,n) by MATRIX_6:def 2;
( width ((AxialSymmetry (n,n)) ~) = n & len (AxialSymmetry (n,n)) = n & width (AxialSymmetry (n,n)) = n & len (AutMt f) = n ) by MATRIX_1:24;
then ((AxialSymmetry (n,n)) ~) * ((AxialSymmetry (n,n)) * (AutMt f)) = (((AxialSymmetry (n,n)) ~) * (AxialSymmetry (n,n))) * (AutMt f) by MATRIX_3:33
.= AutMt f by E1, MATRIX_3:18 ;
hence AutMt f is Orthogonal by E, E0, MATRIX_6:59, E2; :: thesis: verum

end;

end;