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 S_{1}[ 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 S_{1}[m] holds

S_{1}[m + 1]

A14: S_{1}[ 0 ]
_{1}[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

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 S

( g is homogeneous & g is additive & g is being_homeomorphism & g is rotation ) );

A3: for m being Nat st S

S

proof

A13:
F | (len F) = F
by FINSEQ_1:58;
let m be Nat; :: thesis: ( S_{1}[m] implies S_{1}[m + 1] )

assume A4: S_{1}[m]
; :: thesis: S_{1}[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;assume A4: S

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

A14: S

proof

for m being Nat holds S
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;( 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

hence ( f is homogeneous & f is additive & f is rotation & f is being_homeomorphism ) by A1, A13; :: thesis: verum