theorem Th13: :: MATRTOP3:13

for r being Real
for i, j, n being Nat st 1 <= i & i < j & j <= n holds
Det (Rotation (i,j,n,r)) = 1. F_Real