:: deftheorem DefPower defines powerfact LIOUVIL1:def 4 :
for b being Nat
for b₂ being Real_Sequence holds
( b₂ = powerfact b iff for i being Nat holds b₂ . i = 1 / (b to_power (i !)) );