:: deftheorem Def3 defines Rotate JORDAN24:def 3 :
for a being Real
for b₂ being Function of (TOP-REAL 2),(TOP-REAL 2) holds
( b₂ = Rotate a iff for p being Point of (TOP-REAL 2) holds b₂ . p = |[(Re (Rotate (((p `1) + ((p `2) * <i>)),a))),(Im (Rotate (((p `1) + ((p `2) * <i>)),a)))]| );