theorem Th23: :: MATRTOP3:23

for r being Real
for i, j, n being Nat
for p being Point of (TOP-REAL n) st 1 <= i & i < j & j <= n holds
(Mx2Tran (Rotation (i,j,n,r))) . p = ((((p | (i -' 1)) ^ <*(((p . i) * (cos r)) + ((p . j) * (- (sin r))))*>) ^ ((p /^ i) | ((j -' i) -' 1))) ^ <*(((p . i) * (sin r)) + ((p . j) * (cos r)))*>) ^ (p /^ j)