for n being Nat
for r being non zero Real st n is even holds
r to_power n > 0