set S = the carrier of (TOP-REAL n);
set G = GFuncs the carrier of (TOP-REAL n);
take F = <*> the carrier of (GFuncs the carrier of (TOP-REAL n)); :: according to MATRTOP3:def 5 :: thesis: ( id (TOP-REAL n) = 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)) ) ) )
thus Product F = 1_ (GFuncs the carrier of (TOP-REAL n)) by 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 ; :: thesis: 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)) )
let k be Nat; :: thesis: ( k in dom F implies ex i, j being Nat ex r being Real st
( 1 <= i & i < j & j <= n & F . k = Mx2Tran (Rotation (i,j,n,r)) ) )
assume k in dom F ; :: thesis: ex i, j being Nat ex r being Real st
( 1 <= i & i < j & j <= n & F . k = Mx2Tran (Rotation (i,j,n,r)) )
hence ex i, j being Nat ex r being Real st
( 1 <= i & i < j & j <= n & F . k = Mx2Tran (Rotation (i,j,n,r)) ) ; :: thesis: verum