theorem Th15: :: MATRTOP3:15

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
(@ p) "*" (Col ((Rotation (i,j,n,r)),i)) = ((p . i) * (cos r)) + ((p . j) * (- (sin r)))