theorem Th17: :: MATRTOP3:17

for r1, r2 being Real
for i, j, n being Nat st 1 <= i & i < j & j <= n holds
(Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2)) = Rotation (i,j,n,(r1 + r2))