theorem Th57: :: COMPLEX2:59

for a, b being Complex
for r being Real holds Rotate ((a - b),r) = (Rotate (a,r)) - (Rotate (b,r))