theorem Th10: :: LP_SPACE:10

for p being Real st 1 <= p holds
for lp being non empty NORMSTR st lp = NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #) holds
( the carrier of lp = the_set_of_RealSequences_l^ p & ( for x being set holds
( x is VECTOR of lp iff ( x is Real_Sequence & (seq_id x) rto_power p is summable ) ) ) & 0. lp = Zeroseq & ( for x being VECTOR of lp holds x = seq_id x ) & ( for x, y being VECTOR of lp holds x + y = (seq_id x) + (seq_id y) ) & ( for r being Real
for x being VECTOR of lp holds r * x = r (#) (seq_id x) ) & ( for x being VECTOR of lp holds
( - x = - (seq_id x) & seq_id (- x) = - (seq_id x) ) ) & ( for x, y being VECTOR of lp holds x - y = (seq_id x) - (seq_id y) ) & ( for x being VECTOR of lp holds (seq_id x) rto_power p is summable ) & ( for x being VECTOR of lp holds ||.x.|| = (Sum ((seq_id x) rto_power p)) to_power (1 / p) ) )