let p be Real; :: thesis: ( 1 <= p implies 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
for x, y being Point of lp
for a being Real holds
( ( ||.x.|| = 0 implies x = 0. lp ) & ( x = 0. lp implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = (abs a) * ||.x.|| ) )
assume A1: 1 <= p ; :: thesis: 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
for x, y being Point of lp
for a being Real holds
( ( ||.x.|| = 0 implies x = 0. lp ) & ( x = 0. lp implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = (abs a) * ||.x.|| )
A2: 1 / p > 0 by A1, XREAL_1:141;
let lp be non empty NORMSTR ; :: thesis: ( 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) #) implies for x, y being Point of lp
for a being Real holds
( ( ||.x.|| = 0 implies x = 0. lp ) & ( x = 0. lp implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = (abs a) * ||.x.|| ) )
assume A3: 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) #) ; :: thesis: for x, y being Point of lp
for a being Real holds
( ( ||.x.|| = 0 implies x = 0. lp ) & ( x = 0. lp implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = (abs a) * ||.x.|| )
let x, y be Point of lp; :: thesis: for a being Real holds
( ( ||.x.|| = 0 implies x = 0. lp ) & ( x = 0. lp implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = (abs a) * ||.x.|| )
A4: (seq_id y) rto_power p is summable by A1, A3, Th10;
A5: ||.y.|| = the normF of lp . y
.= (Sum ((seq_id y) rto_power p)) to_power (1 / p) by A3, Def3 ;
A6: ||.x.|| = the normF of lp . x
.= (Sum ((seq_id x) rto_power p)) to_power (1 / p) by A3, Def3 ;

A7: now

A8: ||.x.|| = the normF of lp . x
.= (Sum ((seq_id x) rto_power p)) to_power (1 / p) by A3, Def3 ;
A9: x in the_set_of_RealSequences by A1, A3, Def2;
assume A10: ||.x.|| = 0 ; :: thesis: x = 0. lp
(seq_id x) rto_power p is summable by A1, A3, Th10;
then for n being Element of NAT holds 0 = (seq_id x) . n by A1, A10, A8, Th12;
hence x = Zeroseq by A9, RSSPACE:def 6
.= 0. lp by A1, A3, Th10 ;
:: thesis: verum

end;

A11: (seq_id x) rto_power p is summable by A1, A3, Def2;
A12: (Sum ((seq_id x) rto_power p)) to_power (1 / p) = the normF of lp . x by A3, Def3
.= ||.x.|| ;

A13: now

assume x = 0. lp ; :: thesis: ||.x.|| = 0
then x = Zeroseq by A1, A3, Th10;
then A14: for n being Element of NAT holds (seq_id x) . n = 0 by RSSPACE:def 6;
thus ||.x.|| = the normF of lp . x
.= (Sum ((seq_id x) rto_power p)) to_power (1 / p) by A3, Def3
.= 0 by A1, A14, Th11 ; :: thesis: verum

end;

let a be Real; :: thesis: ( ( ||.x.|| = 0 implies x = 0. lp ) & ( x = 0. lp implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = (abs a) * ||.x.|| )
A15: for n being Element of NAT holds 0 <= ((seq_id x) rto_power p) . n

proof

set xp = (seq_id x) rto_power p;
let n be Element of NAT ; :: thesis: 0 <= ((seq_id x) rto_power p) . n
A16: ( 0 < abs ((seq_id x) . n) or 0 = abs ((seq_id x) . n) ) by COMPLEX1:132;
((seq_id x) rto_power p) . n = (abs ((seq_id x) . n)) to_power p by Def1;
hence 0 <= ((seq_id x) rto_power p) . n by A1, A16, POWER:39, POWER:def 2; :: thesis: verum

end;

(seq_id x) + (seq_id y) = seq_id ((seq_id x) + (seq_id y)) by RSSPACE:3
.= seq_id (x + y) by A1, A3, Th10 ;
then A17: (Sum (((seq_id x) + (seq_id y)) rto_power p)) to_power (1 / p) = the normF of lp . (x + y) by A3, Def3
.= ||.(x + y).|| ;
(seq_id x) rto_power p is summable by A1, A3, Th10;
then A18: ||.(x + y).|| <= ||.x.|| + ||.y.|| by A1, A6, A5, A17, A4, Th3;
A19: ||.x.|| = the normF of lp . x
.= (Sum ((seq_id x) rto_power p)) to_power (1 / p) by A3, Def3 ;
||.(a * x).|| = the normF of lp . (a * x)
.= (Sum ((seq_id (a * x)) rto_power p)) to_power (1 / p) by A3, Def3
.= (abs a) * ||.x.|| by A1, A3, A19, Lm8 ;
hence ( ( ||.x.|| = 0 implies x = 0. lp ) & ( x = 0. lp implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = (abs a) * ||.x.|| ) by A2, A7, A13, A15, A11, A12, A18, Lm1, SERIES_1:21; :: thesis: verum