for n being even Nat
for x being Element of F_Real holds x |^ n >= 0. F_Real