theorem Th14: :: MATRTOP3:14

for r being Real
for i, j, k, n being Nat
for p being Point of (TOP-REAL n) st 1 <= i & i < j & j <= n & k in Seg n & k <> i & k <> j holds
(@ p) "*" (Col ((Rotation (i,j,n,r)),k)) = p . k