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).|| = |.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).|| = |.a.| * ||.x.|| )
A2: 1 / p > 0 by A1, XREAL_1:139;
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).|| = |.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).|| = |.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).|| = |.a.| * ||.x.|| )
A4: (seq_id y) rto_power p is summable by A1, A3, Th10;
A5: ||.y.|| = (Sum ((seq_id y) rto_power p)) to_power (1 / p) by A3, Def3;
A6: ||.x.|| = (Sum ((seq_id x) rto_power p)) to_power (1 / p) by A3, Def3;

A7: now :: thesis: ( ||.x.|| = 0 implies x = 0. lp )

A8: ||.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 Nat holds 0 = (seq_id x) . n by A1, A10, A8, Th12;
hence x = Zeroseq by A9, RSSPACE:5
.= 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) = ||.x.|| by A3, Def3;

A13: now :: thesis: ( x = 0. lp implies ||.x.|| = 0 )

assume x = 0. lp ; :: thesis: ||.x.|| = 0
then x = Zeroseq by A1, A3, Th10;
then A14: for n being Nat holds (seq_id x) . n = 0 by RSSPACE:4;
thus ||.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).|| = |.a.| * ||.x.|| )
A15: for n being Nat holds 0 <= ((seq_id x) rto_power p) . n

proof

set xp = (seq_id x) rto_power p;
let n be Nat; :: thesis: 0 <= ((seq_id x) rto_power p) . n
A16: ( 0 < |.((seq_id x) . n).| or 0 = |.((seq_id x) . n).| ) by COMPLEX1:46;
((seq_id x) rto_power p) . n = |.((seq_id x) . n).| to_power p by Def1;
hence 0 <= ((seq_id x) rto_power p) . n by A1, A16, POWER:34, POWER:def 2; :: thesis: verum

end;

(seq_id x) + (seq_id y) = seq_id ((seq_id x) + (seq_id y))
.= seq_id (x + y) by A1, A3, Th10 ;
then A17: (Sum (((seq_id x) + (seq_id y)) rto_power p)) to_power (1 / p) = ||.(x + y).|| by A3, Def3;
(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.|| = (Sum ((seq_id x) rto_power p)) to_power (1 / p) by A3, Def3;
||.(a * x).|| = (Sum ((seq_id (a * x)) rto_power p)) to_power (1 / p) by A3, Def3
.= |.a.| * ||.x.|| by A1, A3, A19, Lm7 ;
hence ( ( ||.x.|| = 0 implies x = 0. lp ) & ( x = 0. lp implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.a.| * ||.x.|| ) by A2, A7, A13, A15, A11, A12, A18, Lm1, SERIES_1:18; :: thesis: verum