let n be Nat; :: thesis: for f being additive homogeneous Function of (),() st f is base_rotation holds
AutMt f is Orthogonal

let f be additive homogeneous Function of (),(); :: thesis: ( f is base_rotation implies AutMt f is Orthogonal )
set TR = TOP-REAL n;
set G = GFuncs the carrier of ();
assume f is base_rotation ; :: thesis:
then consider F being FinSequence of (GFuncs the carrier of ()) such that
A1: f = 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)) ) ;
A3: f = Mx2Tran () by Def6;
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
M is Orthogonal ) ) );
A4: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; :: thesis: ( S1[m] implies S1[m + 1] )
A5: ( n = 0 implies n = 0 ) ;
set m1 = m + 1;
assume A6: S1[m] ; :: thesis: S1[m + 1]
assume A7: 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
M is Orthogonal ) )

then reconsider P = Product (F | m) as base_rotation Function of (),() by ;
set R = AutMt P;
A8: ( width () = n & len () = n ) by MATRIX_0:24;
1 <= m + 1 by NAT_1:11;
then A9: m + 1 in dom F by ;
then consider i, j being Nat, r being Real such that
A10: ( 1 <= i & i < j & j <= n ) and
A11: 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 A12: 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 A12; :: thesis: for M being Matrix of n,F_Real st Mx2Tran M = Product (F | (m + 1)) holds
M is Orthogonal

A13: ( 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 M is Orthogonal )
assume A14: Mx2Tran M = Product (F | (m + 1)) ; :: thesis: M is Orthogonal
Mx2Tran M = (Mx2Tran (Rotation (i,j,n,r))) * (Mx2Tran ()) by
.= Mx2Tran (() * (Rotation (i,j,n,r))) by ;
then A15: M = () * (Rotation (i,j,n,r)) by MATRTOP1:34;
P = Mx2Tran () by Def6;
then A16: ( AutMt P is Orthogonal & n > i ) by ;
( len () = n & Rotation (i,j,n,r) is Orthogonal & n > 0 ) by ;
hence M is Orthogonal by ; :: thesis: verum
end;
A17: F | (len F) = F by FINSEQ_1:58;
A18: 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
M is Orthogonal ) )

A19: Mx2Tran (1. (F_Real,n)) = id () by MATRTOP1:33;
F | 0 = <*> the carrier of (GFuncs the carrier of ()) ;
then A20: 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
M is Orthogonal

A21: 1. (F_Real,n) is Orthogonal by MATRIX_6:58;
let M be Matrix of n,F_Real; :: thesis: ( Mx2Tran M = Product (F | 0) implies M is Orthogonal )
thus ( Mx2Tran M = Product (F | 0) implies M is Orthogonal ) by ; :: thesis: verum
end;
for m being Nat holds S1[m] from NAT_1:sch 2(A18, A4);
hence AutMt f is Orthogonal by A1, A17, A3; :: thesis: verum