set TR = TOP-REAL n;
set G = GFuncs the carrier of ();
let f be Function of (),(); :: 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 ()) 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 (),() 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 (),() by MONOID_0:73;
assume A5: m + 1 <= len F ; :: thesis: for g being Function of (),() 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 ;
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 ()) by MONOID_0:73;
A9: F | (m + 1) = (F | m) ^ <*M*> by ;
let g be Function of (),(); :: 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
.= (Mx2Tran (Rotation (i,j,n,r))) * P by MONOID_0:70 ;
A12: Mx2Tran (Rotation (i,j,n,r)) is rotation by ;
( P is homogeneous & P is additive & P is being_homeomorphism & P is rotation ) by ;
hence ( g is homogeneous & g is additive & g is being_homeomorphism & g is rotation ) by ; :: 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 (),() st g = Product (F | 0) holds
( g is homogeneous & g is additive & g is being_homeomorphism & g is rotation )

let g be Function of (),(); :: 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 ()) ;
then g = 1_ (GFuncs the carrier of ()) by
.= the_unity_wrt the multF of (GFuncs the carrier of ()) by GROUP_1:22
.= id () 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 ; :: thesis: verum