let i be Integer; :: thesis: for c being Complex
for s being Real holds Rotate (c,s) = Rotate (c,(s + ((2 * PI) * i)))
let c be Complex; :: thesis: for s being Real holds Rotate (c,s) = Rotate (c,(s + ((2 * PI) * i)))
let s be Real; :: thesis: Rotate (c,s) = Rotate (c,(s + ((2 * PI) * i)))
( cos (s + (Arg c)) = cos ((s + (Arg c)) + ((2 * PI) * i)) & sin (s + (Arg c)) = sin ((s + (Arg c)) + ((2 * PI) * i)) ) by COMPLEX2:8, COMPLEX2:9;
hence Rotate (c,s) = Rotate (c,(s + ((2 * PI) * i))) ; :: thesis: verum