theorem :: COMPLEX2:51

for a being Complex holds Rotate (a,0) = a by COMPTRIG:62;