let n be Nat; :: thesis: for f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) holds
( not f is rotation or Det (AutMt f) = 1. F_Real or Det (AutMt f) = - (1. F_Real) )
let f be additive homogeneous Function of (TOP-REAL n),(TOP-REAL n); :: thesis: ( not f is rotation or Det (AutMt f) = 1. F_Real or Det (AutMt f) = - (1. F_Real) )
set M = AutMt f;
set MM = Mx2Tran (AutMt f);
set TR = TOP-REAL n;
A1: ( len (AutMt f) = n & width (AutMt f) = n ) by MATRIX_0:24;
A2: ( n = 0 implies n = 0 ) ;
( n = 0 or n >= 1 ) by NAT_1:14;
then A3: ( ( Det (1. (F_Real,n)) = 1_ F_Real & n >= 1 ) or ( Det (1. (F_Real,n)) = 1. F_Real & n = 0 ) ) by MATRIXR2:41, MATRIX_7:16;
assume f is rotation ; :: thesis: ( Det (AutMt f) = 1. F_Real or Det (AutMt f) = - (1. F_Real) )
then A4: Mx2Tran (AutMt f) is rotation by Def6;
then consider h being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) such that
A5: h is base_rotation and
A6: h * (Mx2Tran (AutMt f)) is {n} -support-yielding by Th36;
set R = AutMt h;
A7: h = Mx2Tran (AutMt h) by Def6;
then ( n in NAT & Det (AutMt h) = 1. F_Real ) by A5, Lm10, ORDINAL1:def 12;
then A8: Det ((AutMt f) * (AutMt h)) = (Det (AutMt f)) * (1. F_Real) by MATRIXR2:45
.= (Det (AutMt f)) * 1
.= Det (AutMt f) ;
width (AutMt h) = n by MATRIX_0:24;
then A9: h * (Mx2Tran (AutMt f)) = Mx2Tran ((AutMt f) * (AutMt h)) by A1, A2, A7, MATRTOP1:32;

per cases ( AutMt (h * (Mx2Tran (AutMt f))) = 1. (F_Real,n) or ( AutMt (h * (Mx2Tran (AutMt f))) <> 1. (F_Real,n) & AutMt (h * (Mx2Tran (AutMt f))) = AxialSymmetry (n,n) ) ) by A4, A5, A6, Th35;

suppose AutMt (h * (Mx2Tran (AutMt f))) = 1. (F_Real,n) ; :: thesis: ( Det (AutMt f) = 1. F_Real or Det (AutMt f) = - (1. F_Real) )

hence ( Det (AutMt f) = 1. F_Real or Det (AutMt f) = - (1. F_Real) ) by A3, A8, A9, Def6; :: thesis: verum

end;

suppose A10: ( AutMt (h * (Mx2Tran (AutMt f))) <> 1. (F_Real,n) & AutMt (h * (Mx2Tran (AutMt f))) = AxialSymmetry (n,n) ) ; :: thesis: ( Det (AutMt f) = 1. F_Real or Det (AutMt f) = - (1. F_Real) )

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

proof

A11: ( dom (h * (Mx2Tran (AutMt 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 A12: the carrier of (TOP-REAL n) = {(0. (TOP-REAL n))} by EUCLID:22, EUCLID:77;
rng (h * (Mx2Tran (AutMt 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 (h * (Mx2Tran (AutMt f))) = the carrier of (TOP-REAL n) ) by A12, ZFMISC_1:33;
then h * (Mx2Tran (AutMt f)) = id (TOP-REAL n) by A11, A12, FUNCT_1:7
.= Mx2Tran (1. (F_Real,n)) by MATRTOP1:33 ;
hence contradiction by A10, Def6; :: thesis: verum

end;

then n in Seg n by FINSEQ_1:3;
then Det (AxialSymmetry (n,n)) = - (1. F_Real) by Th4;
hence ( Det (AutMt f) = 1. F_Real or Det (AutMt f) = - (1. F_Real) ) by A8, A9, A10, Def6; :: thesis: verum

end;

end;