:: deftheorem Def7 defines powersFS NUMBER10:def 7 :
for b, e being Real
for n being Nat
for b₄ being FinSequence of REAL holds
( b₄ = powersFS (b,e,n) iff ( len b₄ = n & ( for i being Nat st 1 <= i & i <= n holds
b₄ . i = (b + i) to_power e ) ) );