:: deftheorem Def3 defines l_norm^ LP_SPACE:def 3 :
for p being Real
for b₂ being Function of (the_set_of_RealSequences_l^ p),REAL holds
( b₂ = l_norm^ p iff for x being object st x in the_set_of_RealSequences_l^ p holds
b₂ . x = (Sum ((seq_id x) rto_power p)) to_power (1 / p) );