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

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