let i be Integer; :: thesis: for s being Real holds Rotate s = Rotate (s + ((2 * PI) * i))
let s be Real; :: thesis: Rotate s = Rotate (s + ((2 * PI) * i))
let p be Point of (TOP-REAL 2); :: according to FUNCT_2:def 8 :: thesis: (Rotate s) . p = (Rotate (s + ((2 * PI) * i))) . p
set q = (p `1) + ((p `2) * <i>);
A1: Rotate (((p `1) + ((p `2) * <i>)),s) = Rotate (((p `1) + ((p `2) * <i>)),(s + ((2 * PI) * i))) by Th39;
thus (Rotate s) . p = |[(Re (Rotate (((p `1) + ((p `2) * <i>)),s))),(Im (Rotate (((p `1) + ((p `2) * <i>)),s)))]| by JORDAN24:def 3
.= (Rotate (s + ((2 * PI) * i))) . p by A1, JORDAN24:def 3 ; :: thesis: verum