:: deftheorem Def1 defines to_power HEINE:def 1 :
for seq being Real_Sequence
for k being Nat
for b₃ being Real_Sequence holds
( b₃ = k to_power seq iff for n being Nat holds b₃ . n = k to_power (seq . n) );