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

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