:: deftheorem Def5 defines base_rotation MATRTOP3:def 5 :
for n being Nat
for f being Function of (TOP-REAL n),(TOP-REAL n) holds
( f is base_rotation iff ex F being FinSequence of (GFuncs the carrier of (TOP-REAL n)) st
( f = Product F & ( 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)) ) ) ) );