set TR = TOP-REAL n;
set G = GFuncs the carrier of (TOP-REAL n);
let f be Function of (TOP-REAL n),(TOP-REAL n); :: thesis: ( f is base_rotation implies ( f is homogeneous & f is additive & f is rotation & f is being_homeomorphism ) )
assume f is base_rotation ; :: thesis: ( f is homogeneous & f is additive & f is rotation & f is being_homeomorphism )
then consider F being FinSequence of (GFuncs the carrier of (TOP-REAL n)) 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)) ) ;
defpred S1[ Nat] means ( n <= len F implies for g being Function of (TOP-REAL n),(TOP-REAL n) st g = Product (F | n) holds
( g is homogeneous & g is additive & g is being_homeomorphism & g is rotation ) );
A3: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; :: thesis: ( S1[m] implies S1[m + 1] )
assume A4: S1[m] ; :: thesis: S1[m + 1]
set m1 = m + 1;
reconsider P = Product (F | m) as Function of (TOP-REAL n),(TOP-REAL n) by MONOID_0:73;
assume A5: m + 1 <= len F ; :: thesis: for g being Function of (TOP-REAL n),(TOP-REAL n) st g = Product (F | (m + 1)) holds
( g is homogeneous & g is additive & g is being_homeomorphism & g is rotation )
1 <= m + 1 by NAT_1:11;
then A6: m + 1 in dom F by A5, FINSEQ_3:25;
then consider i, j being Nat, r being Real such that
A7: ( 1 <= i & i < j & j <= n ) and
A8: F . (m + 1) = Mx2Tran (Rotation (i,j,n,r)) by A2;
reconsider M = Mx2Tran (Rotation (i,j,n,r)) as Element of (GFuncs the carrier of (TOP-REAL n)) by MONOID_0:73;
A9: F | (m + 1) = (F | m) ^ <*M*> by A6, A8, FINSEQ_5:10;
let g be Function of (TOP-REAL n),(TOP-REAL n); :: thesis: ( g = Product (F | (m + 1)) implies ( g is homogeneous & g is additive & g is being_homeomorphism & g is rotation ) )
assume A10: g = Product (F | (m + 1)) ; :: thesis: ( g is homogeneous & g is additive & g is being_homeomorphism & g is rotation )
A11: g = (Product (F | m)) * M by A9, A10, GROUP_4:6
.= (Mx2Tran (Rotation (i,j,n,r))) * P by MONOID_0:70 ;
A12: Mx2Tran (Rotation (i,j,n,r)) is rotation by A7, Lm7;
( P is homogeneous & P is additive & P is being_homeomorphism & P is rotation ) by A4, A5, NAT_1:13;
hence ( g is homogeneous & g is additive & g is being_homeomorphism & g is rotation ) by A11, A12, Lm8, TOPS_2:57; :: thesis: verum
end;
A13: F | (len F) = F by FINSEQ_1:58;
A14: S1[ 0 ]
proof
assume 0 <= len F ; :: thesis: for g being Function of (TOP-REAL n),(TOP-REAL n) st g = Product (F | 0) holds
( g is homogeneous & g is additive & g is being_homeomorphism & g is rotation )
let g be Function of (TOP-REAL n),(TOP-REAL n); :: thesis: ( g = Product (F | 0) implies ( g is homogeneous & g is additive & g is being_homeomorphism & g is rotation ) )
assume A15: g = Product (F | 0) ; :: thesis: ( g is homogeneous & g is additive & g is being_homeomorphism & g is rotation )
F | 0 = <*> the carrier of (GFuncs the carrier of (TOP-REAL n)) ;
then g = 1_ (GFuncs the carrier of (TOP-REAL n)) by A15, GROUP_4:8
.= the_unity_wrt the multF of (GFuncs the carrier of (TOP-REAL n)) by GROUP_1:22
.= id (TOP-REAL n) by MONOID_0:75 ;
hence ( g is homogeneous & g is additive & g is being_homeomorphism & g is rotation ) ; :: thesis: verum
end;
for m being Nat holds S1[m] from NAT_1:sch 2(A14, A3);
 hence ( f is homogeneous & f is additive & f is rotation & f is being_homeomorphism ) by A1, A13; :: thesis: verum