:: deftheorem Def1 defines rto_power LP_SPACE:def 1 :
for x being Real_Sequence
for p being Real
for b₃ being Real_Sequence holds
( b₃ = x rto_power p iff for n being Nat holds b₃ . n = |.(x . n).| to_power p );