theorem Th40: :: POLYDIFF:40

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