:: deftheorem Def5 defines -powers TOPGEN_3:def 5 :
for X being set
for r being Real
for b₃ being sequence of REAL holds
( b₃ = X -powers r iff for i being Nat holds
( ( i in X & b₃ . i = r |^ i ) or ( not i in X & b₃ . i = 0 ) ) );