:: deftheorem Def1 defines GeoSeq PREPOWER:def 1 :
for a being Real
for b₂ being Real_Sequence holds
( b₂ = a GeoSeq iff for m being Nat holds b₂ . m = a |^ m );