for i being Nat holds (power F_Real) . ((- (1_ F_Real)),i) in F_Rat