let n be Nat; :: thesis: for M being Matrix of n,F_Real st Mx2Tran M is base_rotation holds
Det M = 1. F_Real

let M be Matrix of n,F_Real; :: thesis: ( Mx2Tran M is base_rotation implies Det M = 1. F_Real )
set TR = TOP-REAL n;
set G = GFuncs the carrier of ();
assume Mx2Tran M is base_rotation ; :: thesis:
then consider F being FinSequence of (GFuncs the carrier of ()) such that
A1: Mx2Tran M = Product F and
A2: for k being Nat st k in dom F holds
ex i, j being Nat ex r being Real st
( 1 <= i & i < j & j <= n & F . k = Mx2Tran (Rotation (i,j,n,r)) ) ;
defpred S1[ Nat] means ( \$1 <= len F implies ( Product (F | \$1) is base_rotation Function of (),() & ( for M being Matrix of n,F_Real st Mx2Tran M = Product (F | \$1) holds
Det M = 1. F_Real ) ) );
A3: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; :: thesis: ( S1[m] implies S1[m + 1] )
A4: ( n = 0 implies n = 0 ) ;
set m1 = m + 1;
assume A5: S1[m] ; :: thesis: S1[m + 1]
assume A6: m + 1 <= len F ; :: thesis: ( Product (F | (m + 1)) is base_rotation Function of (),() & ( for M being Matrix of n,F_Real st Mx2Tran M = Product (F | (m + 1)) holds
Det M = 1. F_Real ) )

then reconsider P = Product (F | m) as base_rotation Function of (),() by ;
set R = AutMt P;
A7: ( width () = n & len () = n ) by MATRIX_0:24;
1 <= m + 1 by NAT_1:11;
then A8: m + 1 in dom F by ;
then consider i, j being Nat, r being Real such that
A9: ( 1 <= i & i < j & j <= n ) and
A10: F . (m + 1) = Mx2Tran (Rotation (i,j,n,r)) by A2;
set O = Rotation (i,j,n,r);
reconsider MO = Mx2Tran (Rotation (i,j,n,r)) as Element of (GFuncs the carrier of ()) by MONOID_0:73;
F | (m + 1) = (F | m) ^ <*MO*> by ;
then A11: Product (F | (m + 1)) = (Product (F | m)) * MO by GROUP_4:6
.= (Mx2Tran (Rotation (i,j,n,r))) * P by MONOID_0:70 ;
Mx2Tran (Rotation (i,j,n,r)) is base_rotation by ;
hence Product (F | (m + 1)) is base_rotation Function of (),() by A11; :: thesis: for M being Matrix of n,F_Real st Mx2Tran M = Product (F | (m + 1)) holds
Det M = 1. F_Real

A12: ( width (Rotation (i,j,n,r)) = n & len (Rotation (i,j,n,r)) = n ) by MATRIX_0:24;
let M be Matrix of n,F_Real; :: thesis: ( Mx2Tran M = Product (F | (m + 1)) implies Det M = 1. F_Real )
assume A13: Mx2Tran M = Product (F | (m + 1)) ; :: thesis:
Mx2Tran M = (Mx2Tran (Rotation (i,j,n,r))) * (Mx2Tran ()) by
.= Mx2Tran (() * (Rotation (i,j,n,r))) by ;
then A14: M = () * (Rotation (i,j,n,r)) by MATRTOP1:34;
P = Mx2Tran () by Def6;
then A15: Det () = 1. F_Real by ;
( len () = n & Det (Rotation (i,j,n,r)) = 1. F_Real ) by ;
hence Det M = () * () by
.= () * 1
.= 1. F_Real ;
:: thesis: verum
end;
A16: F | (len F) = F by FINSEQ_1:58;
A17: S1[ 0 ]
proof
assume 0 <= len F ; :: thesis: ( Product (F | 0) is base_rotation Function of (),() & ( for M being Matrix of n,F_Real st Mx2Tran M = Product (F | 0) holds
Det M = 1. F_Real ) )

A18: Mx2Tran (1. (F_Real,n)) = id () by MATRTOP1:33;
F | 0 = <*> the carrier of (GFuncs the carrier of ()) ;
then A19: Product (F | 0) = 1_ (GFuncs the carrier of ()) by GROUP_4:8
.= the_unity_wrt the multF of (GFuncs the carrier of ()) by GROUP_1:22
.= id () by MONOID_0:75 ;
hence Product (F | 0) is base_rotation Function of (),() ; :: thesis: for M being Matrix of n,F_Real st Mx2Tran M = Product (F | 0) holds
Det M = 1. F_Real

( n = 0 or n >= 1 ) by NAT_1:14;
then A20: ( ( Det (1. (F_Real,n)) = 1_ F_Real & n >= 1 ) or ( Det (1. (F_Real,n)) = 1. F_Real & n = 0 ) ) by ;
let M be Matrix of n,F_Real; :: thesis: ( Mx2Tran M = Product (F | 0) implies Det M = 1. F_Real )
thus ( Mx2Tran M = Product (F | 0) implies Det M = 1. F_Real ) by ; :: thesis: verum
end;
for m being Nat holds S1[m] from NAT_1:sch 2(A17, A3);
hence Det M = 1. F_Real by ; :: thesis: verum