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.|| )
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 A2: 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.|| )
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.|| )
A3: 1 / p > 0 by A1, XREAL_1:141;

A4: now

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

end;

A8: now

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

end;

A10: for n being Element of NAT holds 0 <= ((seq_id x) rto_power p) . n

proof

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

end;

(seq_id x) rto_power p is summable by A1, A2, Def2;
then A12: 0 <= Sum ((seq_id x) rto_power p) by A10, SERIES_1:21;
A13: (Sum ((seq_id x) rto_power p)) to_power (1 / p) = the norm of lp . x by A2, Def3
.= ||.x.|| by NORMSP_1:def 1 ;

A14: now

A15: ||.x.|| = the norm of lp . x by NORMSP_1:def 1
.= (Sum ((seq_id x) rto_power p)) to_power (1 / p) by A2, Def3 ;
A16: ||.y.|| = the norm of lp . y by NORMSP_1:def 1
.= (Sum ((seq_id y) rto_power p)) to_power (1 / p) by A2, Def3 ;
(seq_id x) + (seq_id y) = seq_id ((seq_id x) + (seq_id y)) by RSSPACE:3
.= seq_id (x + y) by A1, A2, Th10 ;
then A17: (Sum (((seq_id x) + (seq_id y)) rto_power p)) to_power (1 / p) = the norm of lp . (x + y) by A2, Def3
.= ||.(x + y).|| by NORMSP_1:def 1 ;
A18: (seq_id x) rto_power p is summable by A1, A2, Th10;
(seq_id y) rto_power p is summable by A1, A2, Th10;
hence ||.(x + y).|| <= ||.x.|| + ||.y.|| by A1, A15, A16, A17, A18, Th3; :: thesis: verum

end;

A19: ||.x.|| = the norm of lp . x by NORMSP_1:def 1
.= (Sum ((seq_id x) rto_power p)) to_power (1 / p) by A2, Def3 ;
||.(a * x).|| = the norm of lp . (a * x) by NORMSP_1:def 1
.= (Sum ((seq_id (a * x)) rto_power p)) to_power (1 / p) by A2, Def3
.= (abs a) * ||.x.|| by A1, A2, 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 A3, A4, A8, A12, A13, A14, Lm1; :: thesis: verum