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

let f be additive homogeneous Function of (),(); :: thesis: ( f is rotation implies ( Det () = 1. F_Real iff f is base_rotation ) )
set TR = TOP-REAL n;
set cTR = the carrier of ();
set M = AutMt f;
set MM = Mx2Tran ();
A1: ( len () = n & width () = n ) by MATRIX_0:24;
A2: ( n = 0 implies n = 0 ) ;
A3: Mx2Tran () = f by Def6;
assume A4: f is rotation ; :: thesis: ( Det () = 1. F_Real iff f is base_rotation )
then consider h being additive homogeneous Function of (),() such that
A5: h is base_rotation and
A6: h * (Mx2Tran ()) is {n} -support-yielding by ;
set R = AutMt h;
A7: width () = n by MATRIX_0:24;
A8: h = Mx2Tran () by Def6;
A9: ( AutMt (h * (Mx2Tran ())) = 1. (F_Real,n) or AutMt (h * (Mx2Tran ())) = AxialSymmetry (n,n) ) by A4, A3, A5, A6, Th35;
( Det () = 1. F_Real implies Mx2Tran () is base_rotation )
proof
assume A10: Det () = 1. F_Real ; :: thesis:
( Det () = 1. F_Real & n in NAT ) by ;
then A11: Det (() * ()) = () * () by
.= 1 * ()
.= 1. F_Real
.= 1 ;
A12: rng (Mx2Tran ()) c= the carrier of () by RELAT_1:def 19;
A13: rng h = [#] () by ;
A14: ( dom h = [#] () & h is one-to-one ) by ;
A15: dom (h ") = [#] () by ;
A16: id () = Mx2Tran (1. (F_Real,n)) by MATRTOP1:33;
h * (Mx2Tran ()) = id the carrier of ()
proof
assume A17: h * (Mx2Tran ()) <> id the carrier of () ; :: thesis: contradiction
n <> 0
proof
A18: ( dom (h * (Mx2Tran ())) = the carrier of () & dom (id the carrier of ()) = the carrier of () ) by FUNCT_2:52;
assume n = 0 ; :: thesis: contradiction
then A19: 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 ;
hence contradiction by A17, A18, A19, FUNCT_1:7; :: thesis: verum
end;
then A20: n in Seg n by FINSEQ_1:3;
Mx2Tran (AutMt (h * (Mx2Tran ()))) = h * (Mx2Tran ()) by Def6;
then Mx2Tran (AxialSymmetry (n,n)) = Mx2Tran (() * ()) by A1, A2, A9, A8, A7, A16, A17, MATRTOP1:32;
then AxialSymmetry (n,n) = () * () by MATRTOP1:34;
then Det (AxialSymmetry (n,n)) = Det (() * ()) ;
hence contradiction by A11, A20, Th4; :: thesis: verum
end;
then (h ") * (h * (Mx2Tran ())) = h " by ;
then h " = ((h ") * h) * (Mx2Tran ()) by RELAT_1:36
.= (id the carrier of ()) * (Mx2Tran ()) by
.= Mx2Tran () by ;
hence Mx2Tran () is base_rotation by A5; :: thesis: verum
end;
hence ( Det () = 1. F_Real iff f is base_rotation ) by ; :: thesis: verum