let n be Nat; :: thesis: for f being additive homogeneous Function of (),() holds
( not f is rotation or Det () = 1. F_Real or Det () = - () )

let f be additive homogeneous Function of (),(); :: thesis: ( not f is rotation or Det () = 1. F_Real or Det () = - () )
set M = AutMt f;
set MM = Mx2Tran ();
set TR = TOP-REAL n;
A1: ( len () = n & width () = 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 ;
assume f is rotation ; :: thesis: ( Det () = 1. F_Real or Det () = - () )
then A4: Mx2Tran () is rotation by Def6;
then consider h being additive homogeneous Function of (),() such that
A5: h is base_rotation and
A6: h * (Mx2Tran ()) is {n} -support-yielding by Th36;
set R = AutMt h;
A7: h = Mx2Tran () by Def6;
then ( n in NAT & Det () = 1. F_Real ) by ;
then A8: Det (() * ()) = (Det ()) * () by MATRIXR2:45
.= (Det ()) * 1
.= Det () ;
width () = n by MATRIX_0:24;
then A9: h * (Mx2Tran ()) = Mx2Tran (() * ()) by ;
per cases ( AutMt (h * (Mx2Tran ())) = 1. (F_Real,n) or ( AutMt (h * (Mx2Tran ())) <> 1. (F_Real,n) & AutMt (h * (Mx2Tran ())) = AxialSymmetry (n,n) ) ) by A4, A5, A6, Th35;
suppose AutMt (h * (Mx2Tran ())) = 1. (F_Real,n) ; :: thesis: ( Det () = 1. F_Real or Det () = - () )
hence ( Det () = 1. F_Real or Det () = - () ) by A3, A8, A9, Def6; :: thesis: verum
end;
suppose A10: ( AutMt (h * (Mx2Tran ())) <> 1. (F_Real,n) & AutMt (h * (Mx2Tran ())) = AxialSymmetry (n,n) ) ; :: thesis: ( Det () = 1. F_Real or Det () = - () )
set cTR = the carrier of ();
n <> 0
proof
A11: ( dom (h * (Mx2Tran ())) = the carrier of () & dom (id the carrier of ()) = the carrier of () ) by FUNCT_2:52;
assume n = 0 ; :: thesis: contradiction
then A12: the carrier of () = {(0. ())} by ;
rng (h * (Mx2Tran ())) c= the carrier of () by RELAT_1:def 19;
then ( rng (id the carrier of ()) = the carrier of () & rng (h * (Mx2Tran ())) = the carrier of () ) by ;
then h * (Mx2Tran ()) = id () by
.= 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)) = - () by Th4;
hence ( Det () = 1. F_Real or Det () = - () ) by A8, A9, A10, Def6; :: thesis: verum
end;
end;