set TR = TOP-REAL n;

set cTR = the carrier of (TOP-REAL n);

set M = AutMt f;

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 Th37, Th38;

end;

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

A2:
n > 0

set A = AxialSymmetry (n,n);

set MA = Mx2Tran (AxialSymmetry (n,n));

AutMt (Mx2Tran (AxialSymmetry (n,n))) = AxialSymmetry (n,n) by Def6;

then A6: f * (Mx2Tran (AxialSymmetry (n,n))) is base_rotation by A1, A5, Th39;

( AxialSymmetry (n,n) is V254( F_Real ) & (AxialSymmetry (n,n)) ~ = AxialSymmetry (n,n) ) by A5, Th7;

then (AxialSymmetry (n,n)) @ = (AxialSymmetry (n,n)) ~ by Th2;

then A7: ( AxialSymmetry (n,n) is Orthogonal & AutMt (f * (Mx2Tran (AxialSymmetry (n,n)))) is Orthogonal ) by A6, Lm11, MATRIX_6:def 7;

A8: AutMt (f * (Mx2Tran (AxialSymmetry (n,n)))) = (AutMt (Mx2Tran (AxialSymmetry (n,n)))) * (AutMt f) by Th29

.= (AxialSymmetry (n,n)) * (AutMt f) by Def6 ;

(AxialSymmetry (n,n)) ~ is_reverse_of AxialSymmetry (n,n) by MATRIX_6:def 4;

then A9: ((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_0: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 A9, MATRIX_3:18 ;

hence AutMt f is Orthogonal by A2, A7, A8, MATRIX_6:59; :: 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 n = 0 ;

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 A1; :: thesis: verum

end;assume n <= 0 ; :: thesis: contradiction

then n = 0 ;

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 A1; :: thesis: verum

set A = AxialSymmetry (n,n);

set MA = Mx2Tran (AxialSymmetry (n,n));

AutMt (Mx2Tran (AxialSymmetry (n,n))) = AxialSymmetry (n,n) by Def6;

then A6: f * (Mx2Tran (AxialSymmetry (n,n))) is base_rotation by A1, A5, Th39;

( AxialSymmetry (n,n) is V254( F_Real ) & (AxialSymmetry (n,n)) ~ = AxialSymmetry (n,n) ) by A5, Th7;

then (AxialSymmetry (n,n)) @ = (AxialSymmetry (n,n)) ~ by Th2;

then A7: ( AxialSymmetry (n,n) is Orthogonal & AutMt (f * (Mx2Tran (AxialSymmetry (n,n)))) is Orthogonal ) by A6, Lm11, MATRIX_6:def 7;

A8: AutMt (f * (Mx2Tran (AxialSymmetry (n,n)))) = (AutMt (Mx2Tran (AxialSymmetry (n,n)))) * (AutMt f) by Th29

.= (AxialSymmetry (n,n)) * (AutMt f) by Def6 ;

(AxialSymmetry (n,n)) ~ is_reverse_of AxialSymmetry (n,n) by MATRIX_6:def 4;

then A9: ((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_0: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 A9, MATRIX_3:18 ;

hence AutMt f is Orthogonal by A2, A7, A8, MATRIX_6:59; :: thesis: verum