for n being Nat holds #Z n = FPower ((1. F_Real),n)