let r be Real; :: thesis: for i, j, n being Nat st 1 <= i & i < j & j <= n holds
Mx2Tran (Rotation (i,j,n,r)) is base_rotation
let i, j, n be Nat; :: thesis: ( 1 <= i & i < j & j <= n implies Mx2Tran (Rotation (i,j,n,r)) is base_rotation )
assume A1: ( 1 <= i & i < j & j <= n ) ; :: thesis: Mx2Tran (Rotation (i,j,n,r)) is base_rotation
set S = the carrier of (TOP-REAL n);
set G = GFuncs the carrier of (TOP-REAL n);
reconsider M = Mx2Tran (Rotation (i,j,n,r)) as Element of (GFuncs the carrier of (TOP-REAL n)) by MONOID_0:73;
take F = <*M*>; :: according to MATRTOP3:def 5 :: thesis: ( Mx2Tran (Rotation (i,j,n,r)) = 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 = Mx2Tran (Rotation (i,j,n,r)) by GROUP_4:9; :: 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)) )
then k in {1} by FINSEQ_1:2, FINSEQ_1:38;
then A2: k = 1 by TARSKI:def 1;
F . 1 = M by FINSEQ_1:40;
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)) ) by A1, A2; :: thesis: verum