for k being Nat
for th being Real holds
( (th * <i>) |^ (2 * k) = ((- 1) |^ k) * (th |^ (2 * k)) & (th * <i>) |^ ((2 * k) + 1) = (((- 1) |^ k) * (th |^ ((2 * k) + 1))) * <i> )