set S = the carrier of ();
set G = GFuncs the carrier of ();
take F = <*> the carrier of (GFuncs the carrier of ()); :: according to MATRTOP3:def 5 :: thesis: ( id () = 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 ()) by GROUP_4:8
.= the_unity_wrt the multF of (GFuncs the carrier of ()) by GROUP_1:22
.= id () 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