:: LP_SPACE semantic presentation

begin

definition
let x be Real_Sequence;
let p be Real;
funcx rto_power p ->  Real_Sequence means :Def1: :: LP_SPACE:def 1
 for n being Element of NAT holds it . n = (abs (x . n)) to_power p;
existence
 ex b1 being Real_Sequence st
for n being Element of NAT holds b1 . n = (abs (x . n)) to_power p
proof
deffunc H1( set ) ->  Element of REAL = (abs (x . $1)) to_power p;
 ex q1 being Real_Sequence st
for n being Element of NAT holds q1 . n = H1(n) from SEQ_1:sch_1();
then consider q1 being Real_Sequence such that
A1: for n being Element of NAT holds q1 . n = (abs (x . n)) to_power p ;
take  q1 ; ::_thesis: for n being Element of NAT holds q1 . n = (abs (x . n)) to_power p
thus  for n being Element of NAT holds q1 . n = (abs (x . n)) to_power p by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Real_Sequence st ( for n being Element of NAT holds b1 . n = (abs (x . n)) to_power p ) & ( for n being Element of NAT holds b2 . n = (abs (x . n)) to_power p ) holds
b1 = b2
proof
let a1, a2 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds a1 . n = (abs (x . n)) to_power p ) & ( for n being Element of NAT holds a2 . n = (abs (x . n)) to_power p ) implies a1 = a2 )
assume that
A2: for n being Element of NAT holds a1 . n = (abs (x . n)) to_power p and
A3: for n being Element of NAT holds a2 . n = (abs (x . n)) to_power p ; ::_thesis: a1 = a2
 for s being set st s in NAT holds
a1 . s = a2 . s
proof
let s be set ; ::_thesis: ( s in NAT implies a1 . s = a2 . s )
assume A4: s in NAT ; ::_thesis: a1 . s = a2 . s
a1 . s = (abs (x . s)) to_power p by A2, A4
.= a2 . s by A3, A4 ;
hence  a1 . s = a2 . s ; ::_thesis: verum
end;
hence  a1 = a2 by FUNCT_2:12; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines rto_power LP_SPACE:def_1_:_
 for x being Real_Sequence
for p being Real
for b3 being Real_Sequence holds
( b3 = x rto_power p iff for n being Element of NAT holds b3 . n = (abs (x . n)) to_power p );

definition
let p be Real;
assume A1: p >= 1 ;
func the_set_of_RealSequences_l^ p ->  non empty Subset of Linear_Space_of_RealSequences means :Def2: :: LP_SPACE:def 2
 for x being set holds
( x in it iff ( x in the_set_of_RealSequences & (seq_id x) rto_power p is summable ) );
existence
 ex b1 being non empty Subset of Linear_Space_of_RealSequences st
for x being set holds
( x in b1 iff ( x in the_set_of_RealSequences & (seq_id x) rto_power p is summable ) )
proof
defpred S1[ set ] means (seq_id $1) rto_power p is summable ;
consider IT being set  such that
A2: for x being set holds
( x in IT iff ( x in the_set_of_RealSequences & S1[x] ) ) from XBOOLE_0:sch_1();
 for x being set st x in IT holds
x in the_set_of_RealSequences by A2;
then A3: IT is Subset of the_set_of_RealSequences by TARSKI:def_3;
 (seq_id Zeroseq) rto_power p is absolutely_summable
proof
reconsider rseq = (seq_id Zeroseq) rto_power p as Real_Sequence ;
now__::_thesis:_for_n_being_Element_of_NAT_holds_rseq_._n_=_0
let n be Element of NAT ; ::_thesis: rseq . n = 0
thus rseq . n = (abs ((seq_id Zeroseq) . n)) to_power p by Def1
.= (abs 0) to_power p by RSSPACE:def_6
.= 0 to_power p by ABSVALUE:2
.= 0 by A1, POWER:def_2 ; ::_thesis: verum
end;
hence  (seq_id Zeroseq) rto_power p is absolutely_summable by COMSEQ_3:3; ::_thesis: verum
end;
then  not IT is empty by A2;
hence  ex b1 being non empty Subset of Linear_Space_of_RealSequences st
for x being set holds
( x in b1 iff ( x in the_set_of_RealSequences & (seq_id x) rto_power p is summable ) ) by A2, A3, RSSPACE:def_7; ::_thesis: verum
end;
uniqueness
 for b1, b2 being non empty Subset of Linear_Space_of_RealSequences st ( for x being set holds
( x in b1 iff ( x in the_set_of_RealSequences & (seq_id x) rto_power p is summable ) ) ) & ( for x being set holds
( x in b2 iff ( x in the_set_of_RealSequences & (seq_id x) rto_power p is summable ) ) ) holds
b1 = b2
proof
let X1, X2 be non empty Subset of Linear_Space_of_RealSequences; ::_thesis: ( ( for x being set holds
( x in X1 iff ( x in the_set_of_RealSequences & (seq_id x) rto_power p is summable ) ) ) & ( for x being set holds
( x in X2 iff ( x in the_set_of_RealSequences & (seq_id x) rto_power p is summable ) ) ) implies X1 = X2 )
assume that
A4: for x being set holds
( x in X1 iff ( x in the_set_of_RealSequences & (seq_id x) rto_power p is summable ) ) and
A5: for x being set holds
( x in X2 iff ( x in the_set_of_RealSequences & (seq_id x) rto_power p is summable ) ) ; ::_thesis: X1 = X2
A6: X2 c= X1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X2 or x in X1 )
assume A7: x in X2 ; ::_thesis: x in X1
then A8: (seq_id x) rto_power p is summable by A5;
 x in the_set_of_RealSequences by A5, A7;
hence  x in X1 by A4, A8; ::_thesis: verum
end;
 X1 c= X2
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X1 or x in X2 )
assume A9: x in X1 ; ::_thesis: x in X2
then A10: (seq_id x) rto_power p is summable by A4;
 x in the_set_of_RealSequences by A4, A9;
hence  x in X2 by A5, A10; ::_thesis: verum
end;
hence  X1 = X2 by A6, XBOOLE_0:def_10; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines the_set_of_RealSequences_l^ LP_SPACE:def_2_:_
 for p being Real st p >= 1 holds
for b2 being non empty Subset of Linear_Space_of_RealSequences holds
( b2 = the_set_of_RealSequences_l^ p iff for x being set holds
( x in b2 iff ( x in the_set_of_RealSequences & (seq_id x) rto_power p is summable ) ) );

      Lm1:  for x1, y1 being Real st x1 >= 0 & y1 > 0 holds
x1 to_power y1 >= 0
proof
let x1, y1 be Real; ::_thesis: ( x1 >= 0 & y1 > 0 implies x1 to_power y1 >= 0 )
assume that
A1: x1 >= 0 and
A2: y1 > 0 ; ::_thesis: x1 to_power y1 >= 0
 ( x1 > 0 or x1 = 0 ) by A1;
hence  x1 to_power y1 >= 0 by A2, POWER:34, POWER:def_2; ::_thesis: verum
end;

Lm2:  for y1, x1, x2 being Real st y1 > 0 & x1 >= 0 & x2 >= 0 holds
(x1 * x2) to_power y1 = (x1 to_power y1) * (x2 to_power y1)
proof
let y1, x1, x2 be Real; ::_thesis: ( y1 > 0 & x1 >= 0 & x2 >= 0 implies (x1 * x2) to_power y1 = (x1 to_power y1) * (x2 to_power y1) )
assume that
A1: y1 > 0 and
A2: x1 >= 0 and
A3: x2 >= 0 ; ::_thesis: (x1 * x2) to_power y1 = (x1 to_power y1) * (x2 to_power y1)
percases ( ( x1 > 0 & x2 > 0 ) or ( x1 > 0 & x2 = 0 ) or ( x1 = 0 & x2 > 0 ) or ( x1 = 0 & x2 = 0 ) ) by A2, A3;
suppose ( x1 > 0 & x2 > 0 ) ; ::_thesis: (x1 * x2) to_power y1 = (x1 to_power y1) * (x2 to_power y1)
hence  (x1 * x2) to_power y1 = (x1 to_power y1) * (x2 to_power y1) by POWER:30; ::_thesis: verum
end;
supposeA4: ( x1 > 0 & x2 = 0 ) ; ::_thesis: (x1 * x2) to_power y1 = (x1 to_power y1) * (x2 to_power y1)
then  x2 to_power y1 = 0 by A1, POWER:def_2;
hence  (x1 * x2) to_power y1 = (x1 to_power y1) * (x2 to_power y1) by A4; ::_thesis: verum
end;
supposeA5: ( x1 = 0 & x2 > 0 ) ; ::_thesis: (x1 * x2) to_power y1 = (x1 to_power y1) * (x2 to_power y1)
then  x1 to_power y1 = 0 by A1, POWER:def_2;
hence  (x1 * x2) to_power y1 = (x1 to_power y1) * (x2 to_power y1) by A5; ::_thesis: verum
end;
supposeA6: ( x1 = 0 & x2 = 0 ) ; ::_thesis: (x1 * x2) to_power y1 = (x1 to_power y1) * (x2 to_power y1)
then  x2 to_power y1 = 0 by A1, POWER:def_2;
hence  (x1 * x2) to_power y1 = (x1 to_power y1) * (x2 to_power y1) by A6; ::_thesis: verum
end;
end;
end;

theorem Th1: :: LP_SPACE:1
for a, b, c being Real st a >= 0 & a < b & c > 0 holds
a to_power c < b to_power c
proof
let a, b, c be Real; ::_thesis: ( a >= 0 & a < b & c > 0 implies a to_power c < b to_power c )
 ( a = 0 & c > 0 implies a to_power c = 0 ) by POWER:def_2;
hence  ( a >= 0 & a < b & c > 0 implies a to_power c < b to_power c ) by POWER:34, POWER:37; ::_thesis: verum
end;

Lm3:  for p being Real st 1 = p holds
for a, b being Real_Sequence
for n being Element of NAT holds ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p))
proof
let p be Real; ::_thesis: ( 1 = p implies for a, b being Real_Sequence
for n being Element of NAT holds ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p)) )
assume A1: p = 1 ; ::_thesis: for a, b being Real_Sequence
for n being Element of NAT holds ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p))
let a, b be Real_Sequence; ::_thesis: for n being Element of NAT holds ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p))
let n be Element of NAT ; ::_thesis: ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p))
A2: now__::_thesis:_for_n_being_Element_of_NAT_holds_
(_((a_+_b)_rto_power_p)_._n_=_abs_((a_+_b)_._n)_&_(a_rto_power_p)_._n_=_abs_(a_._n)_&_(b_rto_power_p)_._n_=_abs_(b_._n)_)
let n be Element of NAT ; ::_thesis: ( ((a + b) rto_power p) . n = abs ((a + b) . n) & (a rto_power p) . n = abs (a . n) & (b rto_power p) . n = abs (b . n) )
thus ((a + b) rto_power p) . n = (abs ((a + b) . n)) to_power p by Def1
.= abs ((a + b) . n) by A1, POWER:25 ; ::_thesis: ( (a rto_power p) . n = abs (a . n) & (b rto_power p) . n = abs (b . n) )
thus (a rto_power p) . n = (abs (a . n)) to_power p by Def1
.= abs (a . n) by A1, POWER:25 ; ::_thesis: (b rto_power p) . n = abs (b . n)
thus (b rto_power p) . n = (abs (b . n)) to_power p by Def1
.= abs (b . n) by A1, POWER:25 ; ::_thesis: verum
end;
then  (a + b) rto_power p = abs (a + b) by SEQ_1:12;
then A3: ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) = (Partial_Sums (abs (a + b))) . n by A1, POWER:25;
 a rto_power p = abs a by A2, SEQ_1:12;
then A4: ((Partial_Sums (a rto_power p)) . n) to_power (1 / p) = (Partial_Sums (abs a)) . n by A1, POWER:25;
deffunc H1( Element of NAT ) ->  Element of REAL = (abs (a . $1)) + (abs (b . $1));
consider c being Real_Sequence such that
A5: for n being Element of NAT holds c . n = H1(n) from SEQ_1:sch_1();
A6: for n being Element of NAT holds abs ((a + b) . n) <= (abs (b . n)) + (abs (a . n))
proof
let n be Element of NAT ; ::_thesis: abs ((a + b) . n) <= (abs (b . n)) + (abs (a . n))
 abs ((a + b) . n) = abs ((a . n) + (b . n)) by SEQ_1:7;
hence  abs ((a + b) . n) <= (abs (b . n)) + (abs (a . n)) by COMPLEX1:56; ::_thesis: verum
end;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(abs_(a_+_b))_._n_<=_c_._n
let n be Element of NAT ; ::_thesis: (abs (a + b)) . n <= c . n
A7: abs ((a + b) . n) = (abs (a + b)) . n by SEQ_1:12;
 abs ((a + b) . n) <= (abs (b . n)) + (abs (a . n)) by A6;
hence  (abs (a + b)) . n <= c . n by A5, A7; ::_thesis: verum
end;
then A8: (Partial_Sums (abs (a + b))) . n <= (Partial_Sums c) . n by SERIES_1:14;
now__::_thesis:_for_n_being_Element_of_NAT_holds_c_._n_=_((abs_a)_+_(abs_b))_._n
let n be Element of NAT ; ::_thesis: c . n = ((abs a) + (abs b)) . n
A9: abs (a . n) = (abs a) . n by SEQ_1:12;
 abs (b . n) = (abs b) . n by SEQ_1:12;
hence c . n = ((abs a) . n) + ((abs b) . n) by A5, A9
.= ((abs a) + (abs b)) . n by SEQ_1:7 ;
::_thesis: verum
end;
then  for n being set st n in NAT holds
c . n = ((abs a) + (abs b)) . n ;
then A10: c = (abs a) + (abs b) by FUNCT_2:12;
 b rto_power p = abs b by A2, SEQ_1:12;
then A11: ((Partial_Sums (b rto_power p)) . n) to_power (1 / p) = (Partial_Sums (abs b)) . n by A1, POWER:25;
 Partial_Sums ((abs a) + (abs b)) = (Partial_Sums (abs a)) + (Partial_Sums (abs b)) by SERIES_1:5;
hence  ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p)) by A3, A4, A11, A10, A8, SEQ_1:7; ::_thesis: verum
end;

theorem Th2: :: LP_SPACE:2
for p being Real st 1 <= p holds
for a, b being Real_Sequence
for n being Element of NAT holds ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p))
proof
let p be Real; ::_thesis: ( 1 <= p implies for a, b being Real_Sequence
for n being Element of NAT holds ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p)) )
assume A1: 1 <= p ; ::_thesis: for a, b being Real_Sequence
for n being Element of NAT holds ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p))
let a, b be Real_Sequence; ::_thesis: for n being Element of NAT holds ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p))
set ap = a rto_power p;
set bp = b rto_power p;
set ab = (a + b) rto_power p;
let n be Element of NAT ; ::_thesis: ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p))
now__::_thesis:_(_(_p_>_1_&_((Partial_Sums_((a_+_b)_rto_power_p))_._n)_to_power_(1_/_p)_<=_(((Partial_Sums_(a_rto_power_p))_._n)_to_power_(1_/_p))_+_(((Partial_Sums_(b_rto_power_p))_._n)_to_power_(1_/_p))_)_or_(_p_=_1_&_((Partial_Sums_((a_+_b)_rto_power_p))_._n)_to_power_(1_/_p)_<=_(((Partial_Sums_(a_rto_power_p))_._n)_to_power_(1_/_p))_+_(((Partial_Sums_(b_rto_power_p))_._n)_to_power_(1_/_p))_)_)
percases ( p > 1 or p = 1 ) by A1, XXREAL_0:1;
caseA2: p > 1 ; ::_thesis: ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p))
now__::_thesis:_for_n_being_Element_of_NAT_holds_
(_(a_rto_power_p)_._n_=_(abs_(a_._n))_to_power_p_&_(b_rto_power_p)_._n_=_(abs_(b_._n))_to_power_p_&_((a_+_b)_rto_power_p)_._n_=_(abs_((a_._n)_+_(b_._n)))_to_power_p_)
let n be Element of NAT ; ::_thesis: ( (a rto_power p) . n = (abs (a . n)) to_power p & (b rto_power p) . n = (abs (b . n)) to_power p & ((a + b) rto_power p) . n = (abs ((a . n) + (b . n))) to_power p )
thus  (a rto_power p) . n = (abs (a . n)) to_power p by Def1; ::_thesis: ( (b rto_power p) . n = (abs (b . n)) to_power p & ((a + b) rto_power p) . n = (abs ((a . n) + (b . n))) to_power p )
thus  (b rto_power p) . n = (abs (b . n)) to_power p by Def1; ::_thesis: ((a + b) rto_power p) . n = (abs ((a . n) + (b . n))) to_power p
((a + b) rto_power p) . n = (abs ((a + b) . n)) to_power p by Def1
.= (abs ((a . n) + (b . n))) to_power p by SEQ_1:7 ;
hence  ((a + b) rto_power p) . n = (abs ((a . n) + (b . n))) to_power p ; ::_thesis: verum
end;
hence  ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p)) by A2, HOLDER_1:7; ::_thesis: verum
end;
case p = 1 ; ::_thesis: ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p))
hence  ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p)) by Lm3; ::_thesis: verum
end;
end;
end;
hence  ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p)) ; ::_thesis: verum
end;

Lm4:  for a, b being Real_Sequence
for p being Real st 1 = p & a rto_power p is summable & b rto_power p is summable holds
( (a + b) rto_power p is summable & (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum (a rto_power p)) to_power (1 / p)) + ((Sum (b rto_power p)) to_power (1 / p)) )
proof
let a, b be Real_Sequence; ::_thesis: for p being Real st 1 = p & a rto_power p is summable & b rto_power p is summable holds
( (a + b) rto_power p is summable & (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum (a rto_power p)) to_power (1 / p)) + ((Sum (b rto_power p)) to_power (1 / p)) )
let p be Real; ::_thesis: ( 1 = p & a rto_power p is summable & b rto_power p is summable implies ( (a + b) rto_power p is summable & (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum (a rto_power p)) to_power (1 / p)) + ((Sum (b rto_power p)) to_power (1 / p)) ) )
assume that
A1: p = 1 and
A2: a rto_power p is summable and
A3: b rto_power p is summable ; ::_thesis: ( (a + b) rto_power p is summable & (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum (a rto_power p)) to_power (1 / p)) + ((Sum (b rto_power p)) to_power (1 / p)) )
A4: now__::_thesis:_for_n_being_Element_of_NAT_holds_
(_((a_+_b)_rto_power_p)_._n_=_abs_((a_+_b)_._n)_&_(a_rto_power_p)_._n_=_abs_(a_._n)_&_(b_rto_power_p)_._n_=_abs_(b_._n)_)
let n be Element of NAT ; ::_thesis: ( ((a + b) rto_power p) . n = abs ((a + b) . n) & (a rto_power p) . n = abs (a . n) & (b rto_power p) . n = abs (b . n) )
thus ((a + b) rto_power p) . n = (abs ((a + b) . n)) to_power p by Def1
.= abs ((a + b) . n) by A1, POWER:25 ; ::_thesis: ( (a rto_power p) . n = abs (a . n) & (b rto_power p) . n = abs (b . n) )
thus (a rto_power p) . n = (abs (a . n)) to_power p by Def1
.= abs (a . n) by A1, POWER:25 ; ::_thesis: (b rto_power p) . n = abs (b . n)
thus (b rto_power p) . n = (abs (b . n)) to_power p by Def1
.= abs (b . n) by A1, POWER:25 ; ::_thesis: verum
end;
then A5: (a + b) rto_power p = abs (a + b) by SEQ_1:12;
A6: a = seq_id a by RSSPACE:1;
A7: a rto_power p = abs a by A4, SEQ_1:12;
then  a is absolutely_summable by A2, SERIES_1:def_4;
then reconsider a1 = a as VECTOR of l1_Space by A6, RSSPACE3:6;
 abs b is summable by A3, A4, SEQ_1:12;
then A8: (abs a) + (abs b) is summable by A2, A7, SERIES_1:7;
A9: b rto_power p = abs b by A4, SEQ_1:12;
then A10: (Sum (b rto_power p)) to_power (1 / p) = Sum (abs b) by A1, POWER:25;
A11: b = seq_id b by RSSPACE:1;
 b is absolutely_summable by A3, A9, SERIES_1:def_4;
then reconsider b1 = b as VECTOR of l1_Space by A11, RSSPACE3:6;
A12: ||.b1.|| = the normF of l1_Space . b1
.= Sum (abs (seq_id b1)) by RSSPACE3:def_2, RSSPACE3:def_3 ;
A13: seq_id b1 = b by RSSPACE:1;
deffunc H1( Element of NAT ) ->  Element of REAL = (abs (a . $1)) + (abs (b . $1));
consider c being Real_Sequence such that
A14: for n being Element of NAT holds c . n = H1(n) from SEQ_1:sch_1();
A15: now__::_thesis:_for_n_being_Element_of_NAT_holds_
(_(abs_(a_+_b))_._n_>=_0_&_c_._n_=_(abs_(a_._n))_+_(abs_(b_._n))_&_c_._n_=_((abs_a)_._n)_+_((abs_b)_._n)_&_(abs_(a_+_b))_._n_<=_c_._n_)
let n be Element of NAT ; ::_thesis: ( (abs (a + b)) . n >= 0 & c . n = (abs (a . n)) + (abs (b . n)) & c . n = ((abs a) . n) + ((abs b) . n) & (abs (a + b)) . n <= c . n )
A16: (abs (a + b)) . n = abs ((a + b) . n) by SEQ_1:12;
hence  (abs (a + b)) . n >= 0 by COMPLEX1:46; ::_thesis: ( c . n = (abs (a . n)) + (abs (b . n)) & c . n = ((abs a) . n) + ((abs b) . n) & (abs (a + b)) . n <= c . n )
thus  c . n = (abs (a . n)) + (abs (b . n)) by A14; ::_thesis: ( c . n = ((abs a) . n) + ((abs b) . n) & (abs (a + b)) . n <= c . n )
(abs (a . n)) + (abs (b . n)) = ((abs a) . n) + (abs (b . n)) by SEQ_1:12
.= ((abs a) . n) + ((abs b) . n) by SEQ_1:12 ;
hence  c . n = ((abs a) . n) + ((abs b) . n) by A14; ::_thesis: (abs (a + b)) . n <= c . n
 abs ((a + b) . n) = abs ((a . n) + (b . n)) by SEQ_1:7;
then  (abs (a + b)) . n <= (abs (a . n)) + (abs (b . n)) by A16, COMPLEX1:56;
hence  (abs (a + b)) . n <= c . n by A14; ::_thesis: verum
end;
then  c = (abs a) + (abs b) by SEQ_1:7;
hence  (a + b) rto_power p is summable by A5, A8, A15, SERIES_1:20; ::_thesis: (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum (a rto_power p)) to_power (1 / p)) + ((Sum (b rto_power p)) to_power (1 / p))
A17: ||.a1.|| = the normF of l1_Space . a1
.= Sum (abs (seq_id a1)) by RSSPACE3:def_2, RSSPACE3:def_3 ;
A18: seq_id a1 = a by RSSPACE:1;
A19: ||.(a1 + b1).|| = the normF of l1_Space . (a1 + b1)
.= Sum (abs (seq_id (a1 + b1))) by RSSPACE3:def_2, RSSPACE3:def_3
.= Sum (abs (seq_id ((seq_id a1) + (seq_id b1)))) by RSSPACE3:6
.= Sum (abs ((seq_id a1) + (seq_id b1))) by RSSPACE:1 ;
A20: ||.(a1 + b1).|| <= ||.a1.|| + ||.b1.|| by RSSPACE3:7;
 (Sum (a rto_power p)) to_power (1 / p) = Sum (abs a) by A1, A7, POWER:25;
hence  (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum (a rto_power p)) to_power (1 / p)) + ((Sum (b rto_power p)) to_power (1 / p)) by A1, A5, A10, A20, A19, A17, A12, A18, A13, POWER:25; ::_thesis: verum
end;

theorem Th3: :: LP_SPACE:3
for a, b being Real_Sequence
for p being Real st 1 <= p & a rto_power p is summable & b rto_power p is summable holds
( (a + b) rto_power p is summable & (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum (a rto_power p)) to_power (1 / p)) + ((Sum (b rto_power p)) to_power (1 / p)) )
proof
let a, b be Real_Sequence; ::_thesis: for p being Real st 1 <= p & a rto_power p is summable & b rto_power p is summable holds
( (a + b) rto_power p is summable & (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum (a rto_power p)) to_power (1 / p)) + ((Sum (b rto_power p)) to_power (1 / p)) )
let p be Real; ::_thesis: ( 1 <= p & a rto_power p is summable & b rto_power p is summable implies ( (a + b) rto_power p is summable & (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum (a rto_power p)) to_power (1 / p)) + ((Sum (b rto_power p)) to_power (1 / p)) ) )
assume that
A1: 1 <= p and
A2: a rto_power p is summable and
A3: b rto_power p is summable ; ::_thesis: ( (a + b) rto_power p is summable & (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum (a rto_power p)) to_power (1 / p)) + ((Sum (b rto_power p)) to_power (1 / p)) )
set ab = (a + b) rto_power p;
set bp = b rto_power p;
set ap = a rto_power p;
A4: now__::_thesis:_for_n_being_Element_of_NAT_holds_
(_(a_rto_power_p)_._n_=_(abs_(a_._n))_to_power_p_&_(b_rto_power_p)_._n_=_(abs_(b_._n))_to_power_p_&_((a_+_b)_rto_power_p)_._n_=_(abs_((a_._n)_+_(b_._n)))_to_power_p_)
let n be Element of NAT ; ::_thesis: ( (a rto_power p) . n = (abs (a . n)) to_power p & (b rto_power p) . n = (abs (b . n)) to_power p & ((a + b) rto_power p) . n = (abs ((a . n) + (b . n))) to_power p )
thus  (a rto_power p) . n = (abs (a . n)) to_power p by Def1; ::_thesis: ( (b rto_power p) . n = (abs (b . n)) to_power p & ((a + b) rto_power p) . n = (abs ((a . n) + (b . n))) to_power p )
thus  (b rto_power p) . n = (abs (b . n)) to_power p by Def1; ::_thesis: ((a + b) rto_power p) . n = (abs ((a . n) + (b . n))) to_power p
((a + b) rto_power p) . n = (abs ((a + b) . n)) to_power p by Def1
.= (abs ((a . n) + (b . n))) to_power p by SEQ_1:7 ;
hence  ((a + b) rto_power p) . n = (abs ((a . n) + (b . n))) to_power p ; ::_thesis: verum
end;
now__::_thesis:_(_(_p_>_1_&_(Sum_((a_+_b)_rto_power_p))_to_power_(1_/_p)_<=_((Sum_(a_rto_power_p))_to_power_(1_/_p))_+_((Sum_(b_rto_power_p))_to_power_(1_/_p))_&_(a_+_b)_rto_power_p_is_summable_)_or_(_p_=_1_&_(Sum_((a_+_b)_rto_power_p))_to_power_(1_/_p)_<=_((Sum_(a_rto_power_p))_to_power_(1_/_p))_+_((Sum_(b_rto_power_p))_to_power_(1_/_p))_&_(a_+_b)_rto_power_p_is_summable_)_)
percases ( p > 1 or p = 1 ) by A1, XXREAL_0:1;
case p > 1 ; ::_thesis: ( (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum (a rto_power p)) to_power (1 / p)) + ((Sum (b rto_power p)) to_power (1 / p)) & (a + b) rto_power p is summable )
hence  ( (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum (a rto_power p)) to_power (1 / p)) + ((Sum (b rto_power p)) to_power (1 / p)) & (a + b) rto_power p is summable ) by A2, A3, A4, HOLDER_1:13; ::_thesis: verum
end;
case p = 1 ; ::_thesis: ( (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum (a rto_power p)) to_power (1 / p)) + ((Sum (b rto_power p)) to_power (1 / p)) & (a + b) rto_power p is summable )
hence  ( (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum (a rto_power p)) to_power (1 / p)) + ((Sum (b rto_power p)) to_power (1 / p)) & (a + b) rto_power p is summable ) by A2, A3, Lm4; ::_thesis: verum
end;
end;
end;
hence  ( (a + b) rto_power p is summable & (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum (a rto_power p)) to_power (1 / p)) + ((Sum (b rto_power p)) to_power (1 / p)) ) ; ::_thesis: verum
end;

theorem Th4: :: LP_SPACE:4
for p being Real st 1 <= p holds
the_set_of_RealSequences_l^ p is linearly-closed
proof
let p be Real; ::_thesis: ( 1 <= p implies the_set_of_RealSequences_l^ p is linearly-closed )
assume A1: p >= 1 ; ::_thesis: the_set_of_RealSequences_l^ p is linearly-closed
set W = the_set_of_RealSequences_l^ p;
A2: for v, u being VECTOR of Linear_Space_of_RealSequences st v in the_set_of_RealSequences_l^ p & u in the_set_of_RealSequences_l^ p holds
v + u in the_set_of_RealSequences_l^ p
proof
let v, u be VECTOR of Linear_Space_of_RealSequences; ::_thesis: ( v in the_set_of_RealSequences_l^ p & u in the_set_of_RealSequences_l^ p implies v + u in the_set_of_RealSequences_l^ p )
assume that
A3: v in the_set_of_RealSequences_l^ p and
A4: u in the_set_of_RealSequences_l^ p ; ::_thesis: v + u in the_set_of_RealSequences_l^ p
A5: (seq_id (v + u)) rto_power p is summable
proof
 v in the_set_of_RealSequences by A1, A3, Def2;
then reconsider vq = v as Real_Sequence by RSSPACE:def_1;
set up = (seq_id u) rto_power p;
set vp = (seq_id v) rto_power p;
set p1 = 1 / p;
A6: (seq_id v) rto_power p = vq rto_power p by RSSPACE:1;
A7: now__::_thesis:_for_n_being_Element_of_NAT_holds_
(_((seq_id_v)_rto_power_p)_._n_=_(abs_((seq_id_v)_._n))_to_power_p_&_((seq_id_u)_rto_power_p)_._n_=_(abs_((seq_id_u)_._n))_to_power_p_&_0_<=_abs_((seq_id_v)_._n)_&_(_0_<_abs_((seq_id_v)_._n)_or_0_=_abs_((seq_id_v)_._n)_)_&_0_<=_((seq_id_v)_rto_power_p)_._n_&_0_<=_abs_((seq_id_u)_._n)_&_(_0_<_abs_((seq_id_u)_._n)_or_0_=_abs_((seq_id_u)_._n)_)_&_0_<=_((seq_id_u)_rto_power_p)_._n_)
let n be Element of NAT ; ::_thesis: ( ((seq_id v) rto_power p) . n = (abs ((seq_id v) . n)) to_power p & ((seq_id u) rto_power p) . n = (abs ((seq_id u) . n)) to_power p & 0 <= abs ((seq_id v) . n) & ( 0 < abs ((seq_id v) . n) or 0 = abs ((seq_id v) . n) ) & 0 <= ((seq_id v) rto_power p) . n & 0 <= abs ((seq_id u) . n) & ( 0 < abs ((seq_id u) . n) or 0 = abs ((seq_id u) . n) ) & 0 <= ((seq_id u) rto_power p) . n )
thus A8: ((seq_id v) rto_power p) . n = (abs ((seq_id v) . n)) to_power p by Def1; ::_thesis: ( ((seq_id u) rto_power p) . n = (abs ((seq_id u) . n)) to_power p & 0 <= abs ((seq_id v) . n) & ( 0 < abs ((seq_id v) . n) or 0 = abs ((seq_id v) . n) ) & 0 <= ((seq_id v) rto_power p) . n & 0 <= abs ((seq_id u) . n) & ( 0 < abs ((seq_id u) . n) or 0 = abs ((seq_id u) . n) ) & 0 <= ((seq_id u) rto_power p) . n )
thus A9: ((seq_id u) rto_power p) . n = (abs ((seq_id u) . n)) to_power p by Def1; ::_thesis: ( 0 <= abs ((seq_id v) . n) & ( 0 < abs ((seq_id v) . n) or 0 = abs ((seq_id v) . n) ) & 0 <= ((seq_id v) rto_power p) . n & 0 <= abs ((seq_id u) . n) & ( 0 < abs ((seq_id u) . n) or 0 = abs ((seq_id u) . n) ) & 0 <= ((seq_id u) rto_power p) . n )
thus  0 <= abs ((seq_id v) . n) by COMPLEX1:46; ::_thesis: ( ( 0 < abs ((seq_id v) . n) or 0 = abs ((seq_id v) . n) ) & 0 <= ((seq_id v) rto_power p) . n & 0 <= abs ((seq_id u) . n) & ( 0 < abs ((seq_id u) . n) or 0 = abs ((seq_id u) . n) ) & 0 <= ((seq_id u) rto_power p) . n )
thus  ( 0 < abs ((seq_id v) . n) or 0 = abs ((seq_id v) . n) ) by COMPLEX1:46; ::_thesis: ( 0 <= ((seq_id v) rto_power p) . n & 0 <= abs ((seq_id u) . n) & ( 0 < abs ((seq_id u) . n) or 0 = abs ((seq_id u) . n) ) & 0 <= ((seq_id u) rto_power p) . n )
hence  0 <= ((seq_id v) rto_power p) . n by A1, A8, POWER:34, POWER:def_2; ::_thesis: ( 0 <= abs ((seq_id u) . n) & ( 0 < abs ((seq_id u) . n) or 0 = abs ((seq_id u) . n) ) & 0 <= ((seq_id u) rto_power p) . n )
thus  0 <= abs ((seq_id u) . n) by COMPLEX1:46; ::_thesis: ( ( 0 < abs ((seq_id u) . n) or 0 = abs ((seq_id u) . n) ) & 0 <= ((seq_id u) rto_power p) . n )
thus  ( 0 < abs ((seq_id u) . n) or 0 = abs ((seq_id u) . n) ) by COMPLEX1:46; ::_thesis: 0 <= ((seq_id u) rto_power p) . n
hence  0 <= ((seq_id u) rto_power p) . n by A1, A9, POWER:34, POWER:def_2; ::_thesis: verum
end;
 (seq_id v) rto_power p is summable by A1, A3, Def2;
then  Partial_Sums ((seq_id v) rto_power p) is bounded_above by A7, SERIES_1:17;
then consider r being real number  such that
A10: for n being set st n in dom (Partial_Sums ((seq_id v) rto_power p)) holds
(Partial_Sums ((seq_id v) rto_power p)) . n < r by SEQ_2:def_1;
A11: 1 / p > 0 by A1, XREAL_1:139;
reconsider r = r as Real by XREAL_0:def_1;
A12: Partial_Sums ((seq_id v) rto_power p) is V39() by A7, SERIES_1:16;
now__::_thesis:_for_n_being_set_st_n_in_dom_(Partial_Sums_((seq_id_v)_rto_power_p))_holds_
((Partial_Sums_((seq_id_v)_rto_power_p))_._n)_to_power_(1_/_p)_<_r_to_power_(1_/_p)
let n be set ; ::_thesis: ( n in dom (Partial_Sums ((seq_id v) rto_power p)) implies ((Partial_Sums ((seq_id v) rto_power p)) . n) to_power (1 / p) < r to_power (1 / p) )
assume A13: n in dom (Partial_Sums ((seq_id v) rto_power p)) ; ::_thesis: ((Partial_Sums ((seq_id v) rto_power p)) . n) to_power (1 / p) < r to_power (1 / p)
reconsider n1 = n as Element of NAT by A13, SEQ_1:2;
 0 <= ((seq_id v) rto_power p) . 0 by A7;
then A14: 0 <= (Partial_Sums ((seq_id v) rto_power p)) . 0 by SERIES_1:def_1;
 (Partial_Sums ((seq_id v) rto_power p)) . 0 <= (Partial_Sums ((seq_id v) rto_power p)) . n1 by A12, SEQM_3:11;
hence  ((Partial_Sums ((seq_id v) rto_power p)) . n) to_power (1 / p) < r to_power (1 / p) by A11, A10, A13, A14, Th1; ::_thesis: verum
end;
then consider q being Real such that
A15: for n being set st n in dom (Partial_Sums ((seq_id v) rto_power p)) holds
((Partial_Sums ((seq_id v) rto_power p)) . n) to_power (1 / p) < q ;
 u in the_set_of_RealSequences by A1, A4, Def2;
then reconsider uq = u as Real_Sequence by RSSPACE:def_1;
A16: seq_id u = uq by RSSPACE:1;
A17: (seq_id v) + (seq_id u) = seq_id ((seq_id v) + (seq_id u)) by RSSPACE:1
.= seq_id (v + u) by RSSPACE:2, RSSPACE:def_7 ;
 (seq_id u) rto_power p is summable by A1, A4, Def2;
then  Partial_Sums ((seq_id u) rto_power p) is bounded_above by A7, SERIES_1:17;
then consider r1 being real number  such that
A18: for n being set st n in dom (Partial_Sums ((seq_id u) rto_power p)) holds
(Partial_Sums ((seq_id u) rto_power p)) . n < r1 by SEQ_2:def_1;
reconsider r1 = r1 as Real by XREAL_0:def_1;
A19: Partial_Sums ((seq_id u) rto_power p) is V39() by A7, SERIES_1:16;
now__::_thesis:_for_n_being_set_st_n_in_dom_(Partial_Sums_((seq_id_u)_rto_power_p))_holds_
((Partial_Sums_((seq_id_u)_rto_power_p))_._n)_to_power_(1_/_p)_<_r1_to_power_(1_/_p)
let n be set ; ::_thesis: ( n in dom (Partial_Sums ((seq_id u) rto_power p)) implies ((Partial_Sums ((seq_id u) rto_power p)) . n) to_power (1 / p) < r1 to_power (1 / p) )
assume A20: n in dom (Partial_Sums ((seq_id u) rto_power p)) ; ::_thesis: ((Partial_Sums ((seq_id u) rto_power p)) . n) to_power (1 / p) < r1 to_power (1 / p)
reconsider n1 = n as Element of NAT by A20, SEQ_1:2;
 0 <= ((seq_id u) rto_power p) . 0 by A7;
then A21: 0 <= (Partial_Sums ((seq_id u) rto_power p)) . 0 by SERIES_1:def_1;
 (Partial_Sums ((seq_id u) rto_power p)) . 0 <= (Partial_Sums ((seq_id u) rto_power p)) . n1 by A19, SEQM_3:11;
hence  ((Partial_Sums ((seq_id u) rto_power p)) . n) to_power (1 / p) < r1 to_power (1 / p) by A11, A18, A20, A21, Th1; ::_thesis: verum
end;
then consider q1 being Real such that
A22: for n being set st n in dom (Partial_Sums ((seq_id u) rto_power p)) holds
((Partial_Sums ((seq_id u) rto_power p)) . n) to_power (1 / p) < q1 ;
A23: (seq_id u) rto_power p = uq rto_power p by RSSPACE:1;
set g = q + q1;
A24: p * (1 / p) = (p * 1) / p by XCMPLX_1:74
.= 1 by A1, XCMPLX_1:60 ;
now__::_thesis:_for_n_being_Element_of_NAT_holds_
(_(_for_n_being_Element_of_NAT_holds_
(_(_0_<_abs_((vq_+_uq)_._n)_or_0_=_abs_((vq_+_uq)_._n)_)_&_0_<=_((vq_+_uq)_rto_power_p)_._n_)_)_&_(Partial_Sums_((vq_+_uq)_rto_power_p))_._n_<_(q_+_q1)_to_power_p_)
let n be Element of NAT ; ::_thesis: ( ( for n being Element of NAT holds
( ( 0 < abs ((vq + uq) . n) or 0 = abs ((vq + uq) . n) ) & 0 <= ((vq + uq) rto_power p) . n ) ) & (Partial_Sums ((vq + uq) rto_power p)) . n < (q + q1) to_power p )
A25: now__::_thesis:_(_(Partial_Sums_((vq_+_uq)_rto_power_p))_._n_>_0_implies_(((Partial_Sums_((vq_+_uq)_rto_power_p))_._n)_to_power_(1_/_p))_to_power_p_=_(Partial_Sums_((vq_+_uq)_rto_power_p))_._n_)
assume  (Partial_Sums ((vq + uq) rto_power p)) . n > 0 ; ::_thesis: (((Partial_Sums ((vq + uq) rto_power p)) . n) to_power (1 / p)) to_power p = (Partial_Sums ((vq + uq) rto_power p)) . n
hence (((Partial_Sums ((vq + uq) rto_power p)) . n) to_power (1 / p)) to_power p = ((Partial_Sums ((vq + uq) rto_power p)) . n) to_power ((1 / p) * p) by POWER:33
.= (Partial_Sums ((vq + uq) rto_power p)) . n by A24, POWER:25 ;
::_thesis: verum
end;
 NAT = dom (Partial_Sums ((seq_id u) rto_power p)) by SEQ_1:2;
then A26: ((Partial_Sums ((seq_id u) rto_power p)) . n) to_power (1 / p) < q1 by A22;
 NAT = dom (Partial_Sums ((seq_id v) rto_power p)) by SEQ_1:2;
then A27: (((Partial_Sums ((seq_id u) rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums ((seq_id v) rto_power p)) . n) to_power (1 / p)) < q + q1 by A15, A26, XREAL_1:8;
 ((Partial_Sums ((vq + uq) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums ((seq_id u) rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums ((seq_id v) rto_power p)) . n) to_power (1 / p)) by A1, A6, A23, Th2;
then A28: ((Partial_Sums ((vq + uq) rto_power p)) . n) to_power (1 / p) < q + q1 by A27, XXREAL_0:2;
A29: now__::_thesis:_(_(Partial_Sums_((vq_+_uq)_rto_power_p))_._n_=_0_implies_(((Partial_Sums_((vq_+_uq)_rto_power_p))_._n)_to_power_(1_/_p))_to_power_p_=_(Partial_Sums_((vq_+_uq)_rto_power_p))_._n_)
assume A30: (Partial_Sums ((vq + uq) rto_power p)) . n = 0 ; ::_thesis: (((Partial_Sums ((vq + uq) rto_power p)) . n) to_power (1 / p)) to_power p = (Partial_Sums ((vq + uq) rto_power p)) . n
hence (((Partial_Sums ((vq + uq) rto_power p)) . n) to_power (1 / p)) to_power p = 0 to_power p by A11, POWER:def_2
.= (Partial_Sums ((vq + uq) rto_power p)) . n by A1, A30, POWER:def_2 ;
::_thesis: verum
end;
hereby  ::_thesis: (Partial_Sums ((vq + uq) rto_power p)) . n < (q + q1) to_power p
let n be Element of NAT ; ::_thesis: ( ( 0 < abs ((vq + uq) . n) or 0 = abs ((vq + uq) . n) ) & 0 <= ((vq + uq) rto_power p) . n )
thus A32: ( 0 < abs ((vq + uq) . n) or 0 = abs ((vq + uq) . n) ) by COMPLEX1:46; ::_thesis: 0 <= ((vq + uq) rto_power p) . n
 ((vq + uq) rto_power p) . n = (abs ((vq + uq) . n)) to_power p by Def1;
hence  0 <= ((vq + uq) rto_power p) . n by A1, A32, POWER:34, POWER:def_2; ::_thesis: verum
end;
then A33: 0 <= ((vq + uq) rto_power p) . 0 ;
A34: (Partial_Sums ((vq + uq) rto_power p)) . 0 <= (Partial_Sums ((vq + uq) rto_power p)) . n by A31, SEQM_3:11, SERIES_1:16;
then  0 <= (Partial_Sums ((vq + uq) rto_power p)) . n by A33, SERIES_1:def_1;
then  ((Partial_Sums ((vq + uq) rto_power p)) . n) to_power (1 / p) >= 0 by A11, Lm1;
hence  (Partial_Sums ((vq + uq) rto_power p)) . n < (q + q1) to_power p by A1, A28, A25, A29, A34, A33, Th1, SERIES_1:def_1; ::_thesis: verum
end;
then A35: for n being Element of NAT holds
( Partial_Sums ((vq + uq) rto_power p) is bounded_above & 0 <= ((vq + uq) rto_power p) . n ) by SEQ_2:def_3;
 seq_id v = vq by RSSPACE:1;
hence  (seq_id (v + u)) rto_power p is summable by A35, A16, A17, SERIES_1:17; ::_thesis: verum
end;
v + u = (seq_id v) + (seq_id u) by RSSPACE:2, RSSPACE:def_7
.= seq_id ((seq_id v) + (seq_id u)) by RSSPACE:1
.= seq_id (v + u) by RSSPACE:2, RSSPACE:def_7 ;
then reconsider w = v + u as Real_Sequence ;
reconsider w = w as set ;
 w in the_set_of_RealSequences by RSSPACE:def_1;
hence  v + u in the_set_of_RealSequences_l^ p by A1, A5, Def2; ::_thesis: verum
end;
 for a being Real
for v being VECTOR of Linear_Space_of_RealSequences st v in the_set_of_RealSequences_l^ p holds
a * v in the_set_of_RealSequences_l^ p
proof
let a be Real; ::_thesis: for v being VECTOR of Linear_Space_of_RealSequences st v in the_set_of_RealSequences_l^ p holds
a * v in the_set_of_RealSequences_l^ p
let v be VECTOR of Linear_Space_of_RealSequences; ::_thesis: ( v in the_set_of_RealSequences_l^ p implies a * v in the_set_of_RealSequences_l^ p )
assume A36: v in the_set_of_RealSequences_l^ p ; ::_thesis: a * v in the_set_of_RealSequences_l^ p
 (seq_id (a * v)) rto_power p is summable
proof
set vp = (seq_id v) rto_power p;
A37: now__::_thesis:_for_n_being_Element_of_NAT_holds_
(_0_<=_abs_((seq_id_v)_._n)_&_(_0_<_abs_((seq_id_v)_._n)_or_0_=_abs_((seq_id_v)_._n)_)_&_0_<=_((seq_id_v)_rto_power_p)_._n_)
let n be Element of NAT ; ::_thesis: ( 0 <= abs ((seq_id v) . n) & ( 0 < abs ((seq_id v) . n) or 0 = abs ((seq_id v) . n) ) & 0 <= ((seq_id v) rto_power p) . n )
thus  0 <= abs ((seq_id v) . n) by COMPLEX1:46; ::_thesis: ( ( 0 < abs ((seq_id v) . n) or 0 = abs ((seq_id v) . n) ) & 0 <= ((seq_id v) rto_power p) . n )
thus A38: ( 0 < abs ((seq_id v) . n) or 0 = abs ((seq_id v) . n) ) by COMPLEX1:46; ::_thesis: 0 <= ((seq_id v) rto_power p) . n
 ((seq_id v) rto_power p) . n = (abs ((seq_id v) . n)) to_power p by Def1;
hence  0 <= ((seq_id v) rto_power p) . n by A1, A38, POWER:34, POWER:def_2; ::_thesis: verum
end;
 (seq_id v) rto_power p is summable by A1, A36, Def2;
then  Partial_Sums ((seq_id v) rto_power p) is bounded_above by A37, SERIES_1:17;
then consider r being real number  such that
A39: for n being set st n in dom (Partial_Sums ((seq_id v) rto_power p)) holds
(Partial_Sums ((seq_id v) rto_power p)) . n < r by SEQ_2:def_1;
A40: seq_id (a * v) = seq_id (a (#) (seq_id v)) by RSSPACE:3, RSSPACE:def_7
.= a (#) (seq_id v) by RSSPACE:1 ;
A41: for n being Element of NAT holds (Partial_Sums ((seq_id (a * v)) rto_power p)) . n = ((abs a) to_power p) * ((Partial_Sums ((seq_id v) rto_power p)) . n)
proof
let n be Element of NAT ; ::_thesis: (Partial_Sums ((seq_id (a * v)) rto_power p)) . n = ((abs a) to_power p) * ((Partial_Sums ((seq_id v) rto_power p)) . n)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq_id_(a_*_v))_rto_power_p)_._n_=_(((abs_a)_to_power_p)_(#)_((seq_id_v)_rto_power_p))_._n
let n be Element of NAT ; ::_thesis: ((seq_id (a * v)) rto_power p) . n = (((abs a) to_power p) (#) ((seq_id v) rto_power p)) . n
A42: abs a >= 0 by COMPLEX1:46;
A43: abs ((seq_id v) . n) >= 0 by COMPLEX1:46;
A44: (a (#) (seq_id v)) . n = a * ((seq_id v) . n) by SEQ_1:9;
((a (#) (seq_id v)) rto_power p) . n = (abs ((a (#) (seq_id v)) . n)) to_power p by Def1
.= ((abs a) * (abs ((seq_id v) . n))) to_power p by A44, COMPLEX1:65
.= ((abs a) to_power p) * ((abs ((seq_id v) . n)) to_power p) by A1, A42, A43, Lm2 ;
hence ((seq_id (a * v)) rto_power p) . n = ((abs a) to_power p) * (((seq_id v) rto_power p) . n) by A40, Def1
.= (((abs a) to_power p) (#) ((seq_id v) rto_power p)) . n by SEQ_1:9 ;
::_thesis: verum
end;
then  for n being set st n in NAT holds
((seq_id (a * v)) rto_power p) . n = (((abs a) to_power p) (#) ((seq_id v) rto_power p)) . n ;
then A45: (seq_id (a * v)) rto_power p = ((abs a) to_power p) (#) ((seq_id v) rto_power p) by FUNCT_2:12;
 Partial_Sums (((abs a) to_power p) (#) ((seq_id v) rto_power p)) = ((abs a) to_power p) (#) (Partial_Sums ((seq_id v) rto_power p)) by SERIES_1:9;
hence  (Partial_Sums ((seq_id (a * v)) rto_power p)) . n = ((abs a) to_power p) * ((Partial_Sums ((seq_id v) rto_power p)) . n) by A45, SEQ_1:9; ::_thesis: verum
end;
A46: ( 0 < (abs a) to_power p or 0 = (abs a) to_power p ) by A1, Lm1, COMPLEX1:46;
A47: now__::_thesis:_for_n_being_set_st_n_in_dom_(Partial_Sums_((seq_id_v)_rto_power_p))_holds_
(_n_in_dom_(Partial_Sums_((seq_id_(a_*_v))_rto_power_p))_&_(_((abs_a)_to_power_p)_*_((Partial_Sums_((seq_id_v)_rto_power_p))_._n)_<_((abs_a)_to_power_p)_*_r_or_((abs_a)_to_power_p)_*_((Partial_Sums_((seq_id_v)_rto_power_p))_._n)_=_((abs_a)_to_power_p)_*_r_)_)
let n be set ; ::_thesis: ( n in dom (Partial_Sums ((seq_id v) rto_power p)) implies ( n in dom (Partial_Sums ((seq_id (a * v)) rto_power p)) & ( ((abs a) to_power p) * ((Partial_Sums ((seq_id v) rto_power p)) . n) < ((abs a) to_power p) * r or ((abs a) to_power p) * ((Partial_Sums ((seq_id v) rto_power p)) . n) = ((abs a) to_power p) * r ) ) )
assume A48: n in dom (Partial_Sums ((seq_id v) rto_power p)) ; ::_thesis: ( n in dom (Partial_Sums ((seq_id (a * v)) rto_power p)) & ( ((abs a) to_power p) * ((Partial_Sums ((seq_id v) rto_power p)) . n) < ((abs a) to_power p) * r or ((abs a) to_power p) * ((Partial_Sums ((seq_id v) rto_power p)) . n) = ((abs a) to_power p) * r ) )
 dom (Partial_Sums ((seq_id v) rto_power p)) = NAT by SEQ_1:1;
hence  n in dom (Partial_Sums ((seq_id (a * v)) rto_power p)) by A48, SEQ_1:1; ::_thesis: ( ((abs a) to_power p) * ((Partial_Sums ((seq_id v) rto_power p)) . n) < ((abs a) to_power p) * r or ((abs a) to_power p) * ((Partial_Sums ((seq_id v) rto_power p)) . n) = ((abs a) to_power p) * r )
thus  ( ((abs a) to_power p) * ((Partial_Sums ((seq_id v) rto_power p)) . n) < ((abs a) to_power p) * r or ((abs a) to_power p) * ((Partial_Sums ((seq_id v) rto_power p)) . n) = ((abs a) to_power p) * r ) by A39, A46, A48, XREAL_1:68; ::_thesis: verum
end;
A49: for n being set holds
( not n in dom (Partial_Sums ((seq_id (a * v)) rto_power p)) or (Partial_Sums ((seq_id (a * v)) rto_power p)) . n < ((abs a) to_power p) * r or (Partial_Sums ((seq_id (a * v)) rto_power p)) . n = ((abs a) to_power p) * r )
proof
let n be set ; ::_thesis: ( not n in dom (Partial_Sums ((seq_id (a * v)) rto_power p)) or (Partial_Sums ((seq_id (a * v)) rto_power p)) . n < ((abs a) to_power p) * r or (Partial_Sums ((seq_id (a * v)) rto_power p)) . n = ((abs a) to_power p) * r )
assume A50: n in dom (Partial_Sums ((seq_id (a * v)) rto_power p)) ; ::_thesis: ( (Partial_Sums ((seq_id (a * v)) rto_power p)) . n < ((abs a) to_power p) * r or (Partial_Sums ((seq_id (a * v)) rto_power p)) . n = ((abs a) to_power p) * r )
reconsider n1 = n as Element of NAT by A50, SEQ_1:1;
 n in NAT by A50, SEQ_1:1;
then  n in dom (Partial_Sums ((seq_id v) rto_power p)) by SEQ_1:1;
then  ( ((abs a) to_power p) * ((Partial_Sums ((seq_id v) rto_power p)) . n) < ((abs a) to_power p) * r or ((abs a) to_power p) * ((Partial_Sums ((seq_id v) rto_power p)) . n) = ((abs a) to_power p) * r ) by A47;
then  ( (Partial_Sums ((seq_id (a * v)) rto_power p)) . n1 < ((abs a) to_power p) * r or (Partial_Sums ((seq_id (a * v)) rto_power p)) . n1 = ((abs a) to_power p) * r ) by A41;
hence  ( (Partial_Sums ((seq_id (a * v)) rto_power p)) . n < ((abs a) to_power p) * r or (Partial_Sums ((seq_id (a * v)) rto_power p)) . n = ((abs a) to_power p) * r ) ; ::_thesis: verum
end;
 ex r1 being real number st
for n being set st n in dom (Partial_Sums ((seq_id (a * v)) rto_power p)) holds
(Partial_Sums ((seq_id (a * v)) rto_power p)) . n < r1
proof
take r1 = (((abs a) to_power p) * r) + 1; ::_thesis: for n being set st n in dom (Partial_Sums ((seq_id (a * v)) rto_power p)) holds
(Partial_Sums ((seq_id (a * v)) rto_power p)) . n < r1
reconsider r1 = r1 as real number ;
 for n being set st n in dom (Partial_Sums ((seq_id (a * v)) rto_power p)) holds
(Partial_Sums ((seq_id (a * v)) rto_power p)) . n < r1
proof
A51: ((abs a) to_power p) * r < (((abs a) to_power p) * r) + 1 by XREAL_1:29;
let n be set ; ::_thesis: ( n in dom (Partial_Sums ((seq_id (a * v)) rto_power p)) implies (Partial_Sums ((seq_id (a * v)) rto_power p)) . n < r1 )
assume  n in dom (Partial_Sums ((seq_id (a * v)) rto_power p)) ; ::_thesis: (Partial_Sums ((seq_id (a * v)) rto_power p)) . n < r1
hence  (Partial_Sums ((seq_id (a * v)) rto_power p)) . n < r1 by A49, A51, XXREAL_0:2; ::_thesis: verum
end;
hence  for n being set st n in dom (Partial_Sums ((seq_id (a * v)) rto_power p)) holds
(Partial_Sums ((seq_id (a * v)) rto_power p)) . n < r1 ; ::_thesis: verum
end;
then A52: Partial_Sums ((seq_id (a * v)) rto_power p) is bounded_above by SEQ_2:def_1;
 for n being Element of NAT holds ((seq_id (a * v)) rto_power p) . n >= 0
proof
set b = a (#) (seq_id v);
let n be Element of NAT ; ::_thesis: ((seq_id (a * v)) rto_power p) . n >= 0
 (a (#) (seq_id v)) . n = a * ((seq_id v) . n) by SEQ_1:9;
then  ((a (#) (seq_id v)) rto_power p) . n = (abs (a * ((seq_id v) . n))) to_power p by Def1;
hence  ((seq_id (a * v)) rto_power p) . n >= 0 by A1, A40, Lm1, COMPLEX1:46; ::_thesis: verum
end;
hence  (seq_id (a * v)) rto_power p is summable by A52, SERIES_1:17; ::_thesis: verum
end;
hence  a * v in the_set_of_RealSequences_l^ p by A1, Def2, RSSPACE:def_7; ::_thesis: verum
end;
hence  the_set_of_RealSequences_l^ p is linearly-closed by A2, RLSUB_1:def_1; ::_thesis: verum
end;

theorem Th5: :: LP_SPACE:5
for p being Real st 1 <= p holds
RLSStruct(# (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)) #) is Subspace of Linear_Space_of_RealSequences
proof
let p be Real; ::_thesis: ( 1 <= p implies RLSStruct(# (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)) #) is Subspace of Linear_Space_of_RealSequences )
assume  1 <= p ; ::_thesis: RLSStruct(# (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)) #) is Subspace of Linear_Space_of_RealSequences
then  the_set_of_RealSequences_l^ p is linearly-closed by Th4;
hence  RLSStruct(# (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)) #) is Subspace of Linear_Space_of_RealSequences by RSSPACE:11; ::_thesis: verum
end;

theorem :: LP_SPACE:6
for p being Real st 1 <= p holds
( RLSStruct(# (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)) #) is Abelian & RLSStruct(# (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)) #) is add-associative & RLSStruct(# (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)) #) is right_zeroed & RLSStruct(# (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)) #) is right_complementable & RLSStruct(# (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)) #) is vector-distributive & RLSStruct(# (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)) #) is scalar-distributive & RLSStruct(# (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)) #) is scalar-associative & RLSStruct(# (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)) #) is scalar-unital ) by Th5;

theorem :: LP_SPACE:7
for p being Real st 1 <= p holds
RLSStruct(# (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)) #) is RealLinearSpace by Th5;

definition
let p be Real;
func l_norm^ p ->  Function of (the_set_of_RealSequences_l^ p),REAL means :Def3: :: LP_SPACE:def 3
 for x being set st x in the_set_of_RealSequences_l^ p holds
it . x = (Sum ((seq_id x) rto_power p)) to_power (1 / p);
existence
 ex b1 being Function of (the_set_of_RealSequences_l^ p),REAL st
for x being set st x in the_set_of_RealSequences_l^ p holds
b1 . x = (Sum ((seq_id x) rto_power p)) to_power (1 / p)
proof
deffunc H1( set ) ->  Element of REAL = (Sum ((seq_id $1) rto_power p)) to_power (1 / p);
A1: for z being set st z in the_set_of_RealSequences_l^ p holds
H1(z) in REAL ;
 ex f being Function of (the_set_of_RealSequences_l^ p),REAL st
for x being set st x in the_set_of_RealSequences_l^ p holds
f . x = H1(x) from FUNCT_2:sch_2(A1);
hence  ex b1 being Function of (the_set_of_RealSequences_l^ p),REAL st
for x being set st x in the_set_of_RealSequences_l^ p holds
b1 . x = (Sum ((seq_id x) rto_power p)) to_power (1 / p) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of (the_set_of_RealSequences_l^ p),REAL st ( for x being set st x in the_set_of_RealSequences_l^ p holds
b1 . x = (Sum ((seq_id x) rto_power p)) to_power (1 / p) ) & ( for x being set st x in the_set_of_RealSequences_l^ p holds
b2 . x = (Sum ((seq_id x) rto_power p)) to_power (1 / p) ) holds
b1 = b2
proof
let NORM1, NORM2 be Function of (the_set_of_RealSequences_l^ p),REAL; ::_thesis: ( ( for x being set st x in the_set_of_RealSequences_l^ p holds
NORM1 . x = (Sum ((seq_id x) rto_power p)) to_power (1 / p) ) & ( for x being set st x in the_set_of_RealSequences_l^ p holds
NORM2 . x = (Sum ((seq_id x) rto_power p)) to_power (1 / p) ) implies NORM1 = NORM2 )
assume that
A2: for x being set st x in the_set_of_RealSequences_l^ p holds
NORM1 . x = (Sum ((seq_id x) rto_power p)) to_power (1 / p) and
A3: for x being set st x in the_set_of_RealSequences_l^ p holds
NORM2 . x = (Sum ((seq_id x) rto_power p)) to_power (1 / p) ; ::_thesis: NORM1 = NORM2
A4: for z being set st z in the_set_of_RealSequences_l^ p holds
NORM1 . z = NORM2 . z
proof
let z be set ; ::_thesis: ( z in the_set_of_RealSequences_l^ p implies NORM1 . z = NORM2 . z )
assume A5: z in the_set_of_RealSequences_l^ p ; ::_thesis: NORM1 . z = NORM2 . z
 NORM1 . z = (Sum ((seq_id z) rto_power p)) to_power (1 / p) by A2, A5;
hence  NORM1 . z = NORM2 . z by A3, A5; ::_thesis: verum
end;
A6: dom NORM2 = the_set_of_RealSequences_l^ p by FUNCT_2:def_1;
 dom NORM1 = the_set_of_RealSequences_l^ p by FUNCT_2:def_1;
hence  NORM1 = NORM2 by A6, A4, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines l_norm^ LP_SPACE:def_3_:_
 for p being Real
for b2 being Function of (the_set_of_RealSequences_l^ p),REAL holds
( b2 = l_norm^ p iff for x being set st x in the_set_of_RealSequences_l^ p holds
b2 . x = (Sum ((seq_id x) rto_power p)) to_power (1 / p) );

theorem Th8: :: LP_SPACE:8
for p being Real st 1 <= p holds
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) #) is RealLinearSpace
proof
let p be Real; ::_thesis: ( 1 <= p implies 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) #) is RealLinearSpace )
assume  1 <= p ; ::_thesis: 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) #) is RealLinearSpace
then  RLSStruct(# (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)) #) is RealLinearSpace by Th5;
hence  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) #) is RealLinearSpace by RSSPACE3:2; ::_thesis: verum
end;

theorem Th9: :: LP_SPACE:9
for p being Real st p >= 1 holds
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) #) is Subspace of Linear_Space_of_RealSequences
proof
set V = Linear_Space_of_RealSequences ;
let p be Real; ::_thesis: ( p >= 1 implies 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) #) is Subspace of Linear_Space_of_RealSequences )
assume A1: 1 <= p ; ::_thesis: 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) #) is Subspace of Linear_Space_of_RealSequences
set lSpacep = 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) #);
reconsider lSpacep = 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) #) as RealLinearSpace by A1, Th8;
set w1 = RLSStruct(# the carrier of lSpacep, the ZeroF of lSpacep, the addF of lSpacep, the Mult of lSpacep #);
A2: RLSStruct(# the carrier of lSpacep, the ZeroF of lSpacep, the addF of lSpacep, the Mult of lSpacep #) is Subspace of Linear_Space_of_RealSequences by A1, Th5;
then A3: the Mult of lSpacep = the Mult of Linear_Space_of_RealSequences | [:REAL, the carrier of lSpacep:] by RLSUB_1:def_2;
 0. RLSStruct(# the carrier of lSpacep, the ZeroF of lSpacep, the addF of lSpacep, the Mult of lSpacep #) = 0. Linear_Space_of_RealSequences by A2, RLSUB_1:def_2;
then A4: 0. lSpacep = 0. Linear_Space_of_RealSequences ;
 the addF of lSpacep = the addF of Linear_Space_of_RealSequences || the carrier of lSpacep by A2, RLSUB_1:def_2;
hence  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) #) is Subspace of Linear_Space_of_RealSequences by A4, A3, RLSUB_1:def_2; ::_thesis: verum
end;

begin

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) ) )
proof
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
( 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) ) ) )
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
( 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) ) )
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 ( 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) ) ) )
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: ( 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) ) )
A3: for x being VECTOR of lp holds ||.x.|| = (Sum ((seq_id x) rto_power p)) to_power (1 / p) by A2, Def3;
A4: for x, y being VECTOR of lp holds x + y = (seq_id x) + (seq_id y)
proof
let x, y be VECTOR of lp; ::_thesis: x + y = (seq_id x) + (seq_id y)
A5: lp is Subspace of Linear_Space_of_RealSequences by A1, A2, Th9;
then reconsider x1 = x as VECTOR of Linear_Space_of_RealSequences by RLSUB_1:10;
reconsider y1 = y as VECTOR of Linear_Space_of_RealSequences by A5, RLSUB_1:10;
set L1 = Linear_Space_of_RealSequences ;
set W = the_set_of_RealSequences_l^ p;
 dom the addF of Linear_Space_of_RealSequences = [: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:] by FUNCT_2:def_1;
then A6: dom ( the addF of Linear_Space_of_RealSequences || (the_set_of_RealSequences_l^ p)) = [:(the_set_of_RealSequences_l^ p),(the_set_of_RealSequences_l^ p):] by RELAT_1:62;
 the_set_of_RealSequences_l^ p is linearly-closed by A1, Th4;
then x + y = ( the addF of Linear_Space_of_RealSequences || (the_set_of_RealSequences_l^ p)) . [x,y] by A2, RSSPACE:def_8
.= x1 + y1 by A2, A6, FUNCT_1:47 ;
hence  x + y = (seq_id x) + (seq_id y) by RSSPACE:2, RSSPACE:def_7; ::_thesis: verum
end;
A7: for r being Real
for x being VECTOR of lp holds r * x = r (#) (seq_id x)
proof
set W = the_set_of_RealSequences_l^ p;
set L1 = Linear_Space_of_RealSequences ;
let r be Real; ::_thesis: for x being VECTOR of lp holds r * x = r (#) (seq_id x)
let x be VECTOR of lp; ::_thesis: r * x = r (#) (seq_id x)
 dom the Mult of Linear_Space_of_RealSequences = [:REAL, the carrier of Linear_Space_of_RealSequences:] by FUNCT_2:def_1;
then A8: dom ( the Mult of Linear_Space_of_RealSequences | [:REAL,(the_set_of_RealSequences_l^ p):]) = [:REAL,(the_set_of_RealSequences_l^ p):] by RELAT_1:62, ZFMISC_1:96;
 lp is Subspace of Linear_Space_of_RealSequences by A1, A2, Th9;
then reconsider x1 = x as VECTOR of Linear_Space_of_RealSequences by RLSUB_1:10;
 the_set_of_RealSequences_l^ p is linearly-closed by A1, Th4;
then r * x = ( the Mult of Linear_Space_of_RealSequences | [:REAL,(the_set_of_RealSequences_l^ p):]) . [r,x] by A2, RSSPACE:def_9
.= r * x1 by A2, A8, FUNCT_1:47 ;
hence  r * x = r (#) (seq_id x) by RSSPACE:3, RSSPACE:def_7; ::_thesis: verum
end;
 the_set_of_RealSequences_l^ p is linearly-closed by A1, Th4;
then A9: 0. lp = 0. Linear_Space_of_RealSequences by A2, RSSPACE:def_10
.= Zeroseq by RSSPACE:def_7 ;
A10: for x being set holds
( x is Element of lp iff ( x is Real_Sequence & (seq_id x) rto_power p is summable ) )
proof
let x be set ; ::_thesis: ( x is Element of lp iff ( x is Real_Sequence & (seq_id x) rto_power p is summable ) )
 ( x in the_set_of_RealSequences_l^ p iff ( (seq_id x) rto_power p is summable & x in the_set_of_RealSequences ) ) by A1, Def2;
hence  ( x is Element of lp iff ( x is Real_Sequence & (seq_id x) rto_power p is summable ) ) by A2, RSSPACE:def_1; ::_thesis: verum
end;
A11: for x being set st x is VECTOR of lp holds
x = seq_id x
proof
let x be set ; ::_thesis: ( x is VECTOR of lp implies x = seq_id x )
 ( x in the_set_of_RealSequences iff x is Real_Sequence ) by RSSPACE:def_1;
hence  ( x is VECTOR of lp implies x = seq_id x ) by A1, A2, Def2, RSSPACE:1; ::_thesis: verum
end;
A12: for x being VECTOR of lp holds
( - x = - (seq_id x) & seq_id (- x) = - (seq_id x) )
proof
let x be VECTOR of lp; ::_thesis: ( - x = - (seq_id x) & seq_id (- x) = - (seq_id x) )
 lp is Subspace of Linear_Space_of_RealSequences by A1, A2, Th9;
then  - x = (- 1) * x by RLVECT_1:16
.= - (seq_id x) by A7 ;
hence  ( - x = - (seq_id x) & seq_id (- x) = - (seq_id x) ) by A11; ::_thesis: verum
end;
 for x, y being VECTOR of lp holds x - y = (seq_id x) - (seq_id y)
proof
let x, y be VECTOR of lp; ::_thesis: x - y = (seq_id x) - (seq_id y)
thus x - y = (seq_id x) + (seq_id (- y)) by A4
.= (seq_id x) - (seq_id y) by A12 ; ::_thesis: verum
end;
hence  ( 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) ) ) by A2, A10, A11, A9, A4, A7, A12, A3; ::_thesis: verum
end;

theorem Th11: :: LP_SPACE:11
for p being Real st p >= 1 holds
for rseq being Real_Sequence st ( for n being Element of NAT holds rseq . n = 0 ) holds
( rseq rto_power p is summable & (Sum (rseq rto_power p)) to_power (1 / p) = 0 )
proof
let p be Real; ::_thesis: ( p >= 1 implies for rseq being Real_Sequence st ( for n being Element of NAT holds rseq . n = 0 ) holds
( rseq rto_power p is summable & (Sum (rseq rto_power p)) to_power (1 / p) = 0 ) )
assume A1: p >= 1 ; ::_thesis: for rseq being Real_Sequence st ( for n being Element of NAT holds rseq . n = 0 ) holds
( rseq rto_power p is summable & (Sum (rseq rto_power p)) to_power (1 / p) = 0 )
A2: 1 / p > 0 by A1, XREAL_1:139;
let rseq be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds rseq . n = 0 ) implies ( rseq rto_power p is summable & (Sum (rseq rto_power p)) to_power (1 / p) = 0 ) )
assume A3: for n being Element of NAT holds rseq . n = 0 ; ::_thesis: ( rseq rto_power p is summable & (Sum (rseq rto_power p)) to_power (1 / p) = 0 )
A4: for n being Element of NAT holds (rseq rto_power p) . n = 0
proof
let n be Element of NAT ; ::_thesis: (rseq rto_power p) . n = 0
 rseq . n = 0 by A3;
then  abs (rseq . n) = 0 by ABSVALUE:2;
then  (abs (rseq . n)) to_power p = 0 by A1, POWER:def_2;
hence  (rseq rto_power p) . n = 0 by Def1; ::_thesis: verum
end;
A5: for m being Element of NAT holds (Partial_Sums (rseq rto_power p)) . m = 0
proof
defpred S1[ Element of NAT ] means (rseq rto_power p) . $1 = (Partial_Sums (rseq rto_power p)) . $1;
let m be Element of NAT ; ::_thesis: (Partial_Sums (rseq rto_power p)) . m = 0
A6: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A7: (rseq rto_power p) . k = (Partial_Sums (rseq rto_power p)) . k ; ::_thesis: S1[k + 1]
thus (rseq rto_power p) . (k + 1) = 0 + ((rseq rto_power p) . (k + 1))
.= ((rseq rto_power p) . k) + ((rseq rto_power p) . (k + 1)) by A4
.= (Partial_Sums (rseq rto_power p)) . (k + 1) by A7, SERIES_1:def_1 ; ::_thesis: verum
end;
A8: S1[ 0 ] by SERIES_1:def_1;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A8, A6);
hence (Partial_Sums (rseq rto_power p)) . m = (rseq rto_power p) . m
.= 0 by A4 ;
::_thesis: verum
end;
A9: for e being real number st 0 < e holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((Partial_Sums (rseq rto_power p)) . m) - 0) < e
proof
let e be real number ; ::_thesis: ( 0 < e implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((Partial_Sums (rseq rto_power p)) . m) - 0) < e )
assume A10: 0 < e ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((Partial_Sums (rseq rto_power p)) . m) - 0) < e
take  0 ; ::_thesis: for m being Element of NAT st 0 <= m holds
abs (((Partial_Sums (rseq rto_power p)) . m) - 0) < e
let m be Element of NAT ; ::_thesis: ( 0 <= m implies abs (((Partial_Sums (rseq rto_power p)) . m) - 0) < e )
assume  0 <= m ; ::_thesis: abs (((Partial_Sums (rseq rto_power p)) . m) - 0) < e
abs (((Partial_Sums (rseq rto_power p)) . m) - 0) = abs (0 - 0) by A5
.= 0 by ABSVALUE:def_1 ;
hence  abs (((Partial_Sums (rseq rto_power p)) . m) - 0) < e by A10; ::_thesis: verum
end;
then A11: Partial_Sums (rseq rto_power p) is convergent by SEQ_2:def_6;
then  lim (Partial_Sums (rseq rto_power p)) = 0 by A9, SEQ_2:def_7;
then  Sum (rseq rto_power p) = 0 by SERIES_1:def_3;
hence  ( rseq rto_power p is summable & (Sum (rseq rto_power p)) to_power (1 / p) = 0 ) by A2, A11, POWER:def_2, SERIES_1:def_2; ::_thesis: verum
end;

theorem Th12: :: LP_SPACE:12
for p being Real st 1 <= p holds
for rseq being Real_Sequence st rseq rto_power p is summable & (Sum (rseq rto_power p)) to_power (1 / p) = 0 holds
for n being natural number holds rseq . n = 0
proof
let p be Real; ::_thesis: ( 1 <= p implies for rseq being Real_Sequence st rseq rto_power p is summable & (Sum (rseq rto_power p)) to_power (1 / p) = 0 holds
for n being natural number holds rseq . n = 0 )
assume A1: 1 <= p ; ::_thesis: for rseq being Real_Sequence st rseq rto_power p is summable & (Sum (rseq rto_power p)) to_power (1 / p) = 0 holds
for n being natural number holds rseq . n = 0
A2: 1 / p > 0 by A1, XREAL_1:139;
let rseq be Real_Sequence; ::_thesis: ( rseq rto_power p is summable & (Sum (rseq rto_power p)) to_power (1 / p) = 0 implies for n being natural number holds rseq . n = 0 )
assume that
A3: rseq rto_power p is summable and
A4: (Sum (rseq rto_power p)) to_power (1 / p) = 0 ; ::_thesis: for n being natural number holds rseq . n = 0
A5: for i being Element of NAT holds (rseq rto_power p) . i >= 0
proof
let i be Element of NAT ; ::_thesis: (rseq rto_power p) . i >= 0
 (rseq rto_power p) . i = (abs (rseq . i)) to_power p by Def1;
hence  (rseq rto_power p) . i >= 0 by A1, Lm1, COMPLEX1:46; ::_thesis: verum
end;
then ((Sum (rseq rto_power p)) to_power (1 / p)) to_power p = (Sum (rseq rto_power p)) to_power ((1 / p) * p) by A1, A2, A3, HOLDER_1:2, SERIES_1:18
.= (Sum (rseq rto_power p)) to_power 1 by A1, XCMPLX_1:106
.= Sum (rseq rto_power p) by POWER:25 ;
then A6: Sum (rseq rto_power p) = 0 by A1, A4, POWER:def_2;
now__::_thesis:_for_n_being_natural_number_holds_rseq_._n_=_0
let n be natural number ; ::_thesis: rseq . n = 0
reconsider n9 = n as Element of NAT by ORDINAL1:def_12;
A7: 0 to_power (1 / p) = 0 by A2, POWER:def_2;
 (rseq rto_power p) . n9 = (abs (rseq . n9)) to_power p by Def1;
then A8: (abs (rseq . n)) to_power p = 0 by A3, A5, A6, RSSPACE:17;
((abs (rseq . n)) to_power p) to_power (1 / p) = (abs (rseq . n)) to_power (p * (1 / p)) by A1, A2, COMPLEX1:46, HOLDER_1:2
.= (abs (rseq . n)) to_power 1 by A1, XCMPLX_1:106
.= abs (rseq . n) by POWER:25 ;
hence  rseq . n = 0 by A8, A7, ABSVALUE:2; ::_thesis: verum
end;
hence  for n being natural number holds rseq . n = 0 ; ::_thesis: verum
end;

Lm5:  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
for x being Point of lp
for a being Real holds (seq_id (a * x)) rto_power p = ((abs a) to_power p) (#) ((seq_id x) rto_power p)
proof
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 being Point of lp
for a being Real holds (seq_id (a * x)) rto_power p = ((abs a) to_power p) (#) ((seq_id x) rto_power p) )
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 being Point of lp
for a being Real holds (seq_id (a * x)) rto_power p = ((abs a) to_power p) (#) ((seq_id x) rto_power p)
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 being Point of lp
for a being Real holds (seq_id (a * x)) rto_power p = ((abs a) to_power p) (#) ((seq_id x) rto_power p) )
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 being Point of lp
for a being Real holds (seq_id (a * x)) rto_power p = ((abs a) to_power p) (#) ((seq_id x) rto_power p)
let x be Point of lp; ::_thesis: for a being Real holds (seq_id (a * x)) rto_power p = ((abs a) to_power p) (#) ((seq_id x) rto_power p)
let a be Real; ::_thesis: (seq_id (a * x)) rto_power p = ((abs a) to_power p) (#) ((seq_id x) rto_power p)
now__::_thesis:_for_n1_being_set_st_n1_in_NAT_holds_
((seq_id_(a_*_x))_rto_power_p)_._n1_=_(((abs_a)_to_power_p)_(#)_((seq_id_x)_rto_power_p))_._n1
let n1 be set ; ::_thesis: ( n1 in NAT implies ((seq_id (a * x)) rto_power p) . n1 = (((abs a) to_power p) (#) ((seq_id x) rto_power p)) . n1 )
assume  n1 in NAT ; ::_thesis: ((seq_id (a * x)) rto_power p) . n1 = (((abs a) to_power p) (#) ((seq_id x) rto_power p)) . n1
then reconsider n = n1 as Element of NAT ;
A3: abs a >= 0 by COMPLEX1:46;
A4: abs ((seq_id x) . n) >= 0 by COMPLEX1:46;
((seq_id (a * x)) rto_power p) . n = (abs ((seq_id (a * x)) . n)) to_power p by Def1
.= (abs ((seq_id (a (#) (seq_id x))) . n)) to_power p by A1, A2, Th10
.= (abs ((a (#) (seq_id x)) . n)) to_power p by RSSPACE:1
.= (abs (a * ((seq_id x) . n))) to_power p by SEQ_1:9
.= ((abs a) * (abs ((seq_id x) . n))) to_power p by COMPLEX1:65
.= ((abs a) to_power p) * ((abs ((seq_id x) . n)) to_power p) by A1, A3, A4, Lm2
.= ((abs a) to_power p) * (((seq_id x) rto_power p) . n) by Def1
.= (((abs a) to_power p) (#) ((seq_id x) rto_power p)) . n by SEQ_1:9 ;
hence  ((seq_id (a * x)) rto_power p) . n1 = (((abs a) to_power p) (#) ((seq_id x) rto_power p)) . n1 ; ::_thesis: verum
end;
hence  (seq_id (a * x)) rto_power p = ((abs a) to_power p) (#) ((seq_id x) rto_power p) by FUNCT_2:12; ::_thesis: verum
end;

Lm6:  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
for x being Point of lp
for a being Real holds Sum ((seq_id (a * x)) rto_power p) = ((abs a) to_power p) * (Sum ((seq_id x) rto_power p))
proof
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 being Point of lp
for a being Real holds Sum ((seq_id (a * x)) rto_power p) = ((abs a) to_power p) * (Sum ((seq_id x) rto_power p)) )
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 being Point of lp
for a being Real holds Sum ((seq_id (a * x)) rto_power p) = ((abs a) to_power p) * (Sum ((seq_id x) rto_power p))
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 being Point of lp
for a being Real holds Sum ((seq_id (a * x)) rto_power p) = ((abs a) to_power p) * (Sum ((seq_id x) rto_power p)) )
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 being Point of lp
for a being Real holds Sum ((seq_id (a * x)) rto_power p) = ((abs a) to_power p) * (Sum ((seq_id x) rto_power p))
let x be Point of lp; ::_thesis: for a being Real holds Sum ((seq_id (a * x)) rto_power p) = ((abs a) to_power p) * (Sum ((seq_id x) rto_power p))
A3: (seq_id x) rto_power p is summable by A1, A2, Th10;
let a be Real; ::_thesis: Sum ((seq_id (a * x)) rto_power p) = ((abs a) to_power p) * (Sum ((seq_id x) rto_power p))
thus  Sum ((seq_id (a * x)) rto_power p) = Sum (((abs a) to_power p) (#) ((seq_id x) rto_power p)) by A1, A2, Lm5
.= ((abs a) to_power p) * (Sum ((seq_id x) rto_power p)) by A3, SERIES_1:10 ; ::_thesis: verum
end;

Lm7:  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
for x being Point of lp
for a being Real holds (Sum ((seq_id (a * x)) rto_power p)) to_power (1 / p) = (abs a) * ((Sum ((seq_id x) rto_power p)) to_power (1 / p))
proof
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 being Point of lp
for a being Real holds (Sum ((seq_id (a * x)) rto_power p)) to_power (1 / p) = (abs a) * ((Sum ((seq_id x) rto_power p)) to_power (1 / p)) )
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 being Point of lp
for a being Real holds (Sum ((seq_id (a * x)) rto_power p)) to_power (1 / p) = (abs a) * ((Sum ((seq_id x) rto_power p)) to_power (1 / p))
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 being Point of lp
for a being Real holds (Sum ((seq_id (a * x)) rto_power p)) to_power (1 / p) = (abs a) * ((Sum ((seq_id x) rto_power p)) to_power (1 / p)) )
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 being Point of lp
for a being Real holds (Sum ((seq_id (a * x)) rto_power p)) to_power (1 / p) = (abs a) * ((Sum ((seq_id x) rto_power p)) to_power (1 / p))
let x be Point of lp; ::_thesis: for a being Real holds (Sum ((seq_id (a * x)) rto_power p)) to_power (1 / p) = (abs a) * ((Sum ((seq_id x) rto_power p)) to_power (1 / p))
A4: now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq_id_x)_rto_power_p)_._n_>=_0
let n be Element of NAT ; ::_thesis: ((seq_id x) rto_power p) . n >= 0
 ((seq_id x) rto_power p) . n = (abs ((seq_id x) . n)) to_power p by Def1;
hence  ((seq_id x) rto_power p) . n >= 0 by A1, Lm1, COMPLEX1:46; ::_thesis: verum
end;
 (seq_id x) rto_power p is summable by A1, A3, Th10;
then A5: 0 <= Sum ((seq_id x) rto_power p) by A4, SERIES_1:18;
let a be Real; ::_thesis: (Sum ((seq_id (a * x)) rto_power p)) to_power (1 / p) = (abs a) * ((Sum ((seq_id x) rto_power p)) to_power (1 / p))
A6: (abs a) to_power p >= 0 by A1, Lm1, COMPLEX1:46;
thus (Sum ((seq_id (a * x)) rto_power p)) to_power (1 / p) = (((abs a) to_power p) * (Sum ((seq_id x) rto_power p))) to_power (1 / p) by A1, A3, Lm6
.= (((abs a) to_power p) to_power (1 / p)) * ((Sum ((seq_id x) rto_power p)) to_power (1 / p)) by A2, A5, A6, Lm2
.= ((abs a) to_power (p * (1 / p))) * ((Sum ((seq_id x) rto_power p)) to_power (1 / p)) by A1, A2, COMPLEX1:46, HOLDER_1:2
.= ((abs a) to_power 1) * ((Sum ((seq_id x) rto_power p)) to_power (1 / p)) by A1, XCMPLX_1:106
.= (abs a) * ((Sum ((seq_id x) rto_power p)) to_power (1 / p)) by POWER:25 ; ::_thesis: verum
end;

theorem Th13: :: LP_SPACE:13
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
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.|| )
proof
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: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).|| = (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__::_thesis:_(_||.x.||_=_0_implies_x_=_0._lp_)
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__::_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 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:46;
 ((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:34, POWER:def_2; ::_thesis: verum
end;
(seq_id x) + (seq_id y) = seq_id ((seq_id x) + (seq_id y)) by RSSPACE:1
.= 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, Lm7 ;
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:18; ::_thesis: verum
end;

theorem Th14: :: LP_SPACE:14
for p being Real st p >= 1 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
( lp is reflexive & lp is discerning & lp is RealNormSpace-like )
proof
let p be Real; ::_thesis: ( p >= 1 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
( lp is reflexive & lp is discerning & lp is RealNormSpace-like ) )
assume A1: p >= 1 ; ::_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
( lp is reflexive & lp is discerning & lp is RealNormSpace-like )
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 ( lp is reflexive & lp is discerning & lp is RealNormSpace-like ) )
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: ( lp is reflexive & lp is discerning & lp is RealNormSpace-like )
hence  ||.(0. lp).|| = 0 by A1, Th13; :: according to NORMSP_0:def_6 ::_thesis: ( lp is discerning & lp is RealNormSpace-like )
 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.|| ) by A1, Th13, A2;
hence  ( lp is discerning & lp is RealNormSpace-like ) by NORMSP_0:def_5, NORMSP_1:def_1; ::_thesis: verum
end;

theorem :: LP_SPACE:15
for p being Real st p >= 1 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
lp is RealNormSpace by Th9, Th14;

Lm8:  for p being Real st 0 < p holds
for c being Real
for seq being Real_Sequence st seq is convergent holds
for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = (abs ((seq . i) - c)) to_power p ) holds
( rseq is convergent & lim rseq = (abs ((lim seq) - c)) to_power p )
proof
let p be Real; ::_thesis: ( 0 < p implies for c being Real
for seq being Real_Sequence st seq is convergent holds
for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = (abs ((seq . i) - c)) to_power p ) holds
( rseq is convergent & lim rseq = (abs ((lim seq) - c)) to_power p ) )
assume A1: 0 < p ; ::_thesis: for c being Real
for seq being Real_Sequence st seq is convergent holds
for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = (abs ((seq . i) - c)) to_power p ) holds
( rseq is convergent & lim rseq = (abs ((lim seq) - c)) to_power p )
let c be Real; ::_thesis: for seq being Real_Sequence st seq is convergent holds
for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = (abs ((seq . i) - c)) to_power p ) holds
( rseq is convergent & lim rseq = (abs ((lim seq) - c)) to_power p )
let seq be Real_Sequence; ::_thesis: ( seq is convergent implies for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = (abs ((seq . i) - c)) to_power p ) holds
( rseq is convergent & lim rseq = (abs ((lim seq) - c)) to_power p ) )
assume A2: seq is convergent ; ::_thesis: for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = (abs ((seq . i) - c)) to_power p ) holds
( rseq is convergent & lim rseq = (abs ((lim seq) - c)) to_power p )
deffunc H1( set ) ->  Element of REAL = abs ((seq . $1) - c);
consider b being Real_Sequence such that
A3: for n being Element of NAT holds b . n = H1(n) from SEQ_1:sch_1();
let rseq be Real_Sequence; ::_thesis: ( ( for i being Element of NAT holds rseq . i = (abs ((seq . i) - c)) to_power p ) implies ( rseq is convergent & lim rseq = (abs ((lim seq) - c)) to_power p ) )
assume A4: for i being Element of NAT holds rseq . i = (abs ((seq . i) - c)) to_power p ; ::_thesis: ( rseq is convergent & lim rseq = (abs ((lim seq) - c)) to_power p )
A5: for n being Element of NAT holds rseq . n = (b . n) to_power p
proof
let n be Element of NAT ; ::_thesis: rseq . n = (b . n) to_power p
rseq . n = (abs ((seq . n) - c)) to_power p by A4
.= (b . n) to_power p by A3 ;
hence  rseq . n = (b . n) to_power p ; ::_thesis: verum
end;
A6: for n being Element of NAT holds 0 <= b . n
proof
let n be Element of NAT ; ::_thesis: 0 <= b . n
 b . n = abs ((seq . n) - c) by A3;
hence  0 <= b . n by COMPLEX1:46; ::_thesis: verum
end;
A7: lim b = abs ((lim seq) - c) by A2, A3, RSSPACE3:1;
 b is convergent by A2, A3, RSSPACE3:1;
hence  ( rseq is convergent & lim rseq = (abs ((lim seq) - c)) to_power p ) by A1, A7, A6, A5, HOLDER_1:10; ::_thesis: verum
end;

Lm9:  for p being Real st 0 < p holds
for c being Real
for seq, seq1 being Real_Sequence st seq is convergent & seq1 is convergent holds
for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = ((abs ((seq . i) - c)) to_power p) + (seq1 . i) ) holds
( rseq is convergent & lim rseq = ((abs ((lim seq) - c)) to_power p) + (lim seq1) )
proof
let p be Real; ::_thesis: ( 0 < p implies for c being Real
for seq, seq1 being Real_Sequence st seq is convergent & seq1 is convergent holds
for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = ((abs ((seq . i) - c)) to_power p) + (seq1 . i) ) holds
( rseq is convergent & lim rseq = ((abs ((lim seq) - c)) to_power p) + (lim seq1) ) )
assume A1: 0 < p ; ::_thesis: for c being Real
for seq, seq1 being Real_Sequence st seq is convergent & seq1 is convergent holds
for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = ((abs ((seq . i) - c)) to_power p) + (seq1 . i) ) holds
( rseq is convergent & lim rseq = ((abs ((lim seq) - c)) to_power p) + (lim seq1) )
let c be Real; ::_thesis: for seq, seq1 being Real_Sequence st seq is convergent & seq1 is convergent holds
for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = ((abs ((seq . i) - c)) to_power p) + (seq1 . i) ) holds
( rseq is convergent & lim rseq = ((abs ((lim seq) - c)) to_power p) + (lim seq1) )
let seq, seq1 be Real_Sequence; ::_thesis: ( seq is convergent & seq1 is convergent implies for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = ((abs ((seq . i) - c)) to_power p) + (seq1 . i) ) holds
( rseq is convergent & lim rseq = ((abs ((lim seq) - c)) to_power p) + (lim seq1) ) )
assume that
A2: seq is convergent and
A3: seq1 is convergent ; ::_thesis: for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = ((abs ((seq . i) - c)) to_power p) + (seq1 . i) ) holds
( rseq is convergent & lim rseq = ((abs ((lim seq) - c)) to_power p) + (lim seq1) )
deffunc H1( set ) ->  Element of REAL = (abs ((seq . $1) - c)) to_power p;
consider b being Real_Sequence such that
A4: for n being Element of NAT holds b . n = H1(n) from SEQ_1:sch_1();
let rseq be Real_Sequence; ::_thesis: ( ( for i being Element of NAT holds rseq . i = ((abs ((seq . i) - c)) to_power p) + (seq1 . i) ) implies ( rseq is convergent & lim rseq = ((abs ((lim seq) - c)) to_power p) + (lim seq1) ) )
assume A5: for i being Element of NAT holds rseq . i = ((abs ((seq . i) - c)) to_power p) + (seq1 . i) ; ::_thesis: ( rseq is convergent & lim rseq = ((abs ((lim seq) - c)) to_power p) + (lim seq1) )
now__::_thesis:_for_n_being_Element_of_NAT_holds_rseq_._n_=_(b_._n)_+_(seq1_._n)
let n be Element of NAT ; ::_thesis: rseq . n = (b . n) + (seq1 . n)
thus rseq . n = ((abs ((seq . n) - c)) to_power p) + (seq1 . n) by A5
.= (b . n) + (seq1 . n) by A4 ; ::_thesis: verum
end;
then A6: rseq = b + seq1 by SEQ_1:7;
A7: b is convergent by A1, A2, A4, Lm8;
hence  rseq is convergent by A3, A6, SEQ_2:5; ::_thesis: lim rseq = ((abs ((lim seq) - c)) to_power p) + (lim seq1)
 lim b = (abs ((lim seq) - c)) to_power p by A1, A2, A4, Lm8;
hence  lim rseq = ((abs ((lim seq) - c)) to_power p) + (lim seq1) by A3, A7, A6, SEQ_2:6; ::_thesis: verum
end;

Lm10:  for a, b being Real_Sequence holds a = (a + b) - b
proof
let a, b be Real_Sequence; ::_thesis: a = (a + b) - b
now__::_thesis:_for_n_being_Element_of_NAT_holds_((a_+_b)_-_b)_._n_=_a_._n
let n be Element of NAT ; ::_thesis: ((a + b) - b) . n = a . n
(a + (b + (- b))) . n = (a . n) + ((b + (- b)) . n) by SEQ_1:7
.= (a . n) + ((b . n) + ((- b) . n)) by SEQ_1:7
.= (a . n) + ((b . n) + (- (b . n))) by SEQ_1:10
.= a . n ;
hence  ((a + b) - b) . n = a . n by SEQ_1:13; ::_thesis: verum
end;
hence  a = (a + b) - b by FUNCT_2:63; ::_thesis: verum
end;

Lm11:  for p being Real st p >= 1 holds
for a, b being Real_Sequence st a rto_power p is summable & b rto_power p is summable holds
(a + b) rto_power p is summable
proof
let p be Real; ::_thesis: ( p >= 1 implies for a, b being Real_Sequence st a rto_power p is summable & b rto_power p is summable holds
(a + b) rto_power p is summable )
assume A1: p >= 1 ; ::_thesis: for a, b being Real_Sequence st a rto_power p is summable & b rto_power p is summable holds
(a + b) rto_power p is summable
let a, b be Real_Sequence; ::_thesis: ( a rto_power p is summable & b rto_power p is summable implies (a + b) rto_power p is summable )
assume that
A2: a rto_power p is summable and
A3: b rto_power p is summable ; ::_thesis: (a + b) rto_power p is summable
reconsider a1 = a, b1 = b as set ;
A4: a1 in the_set_of_RealSequences by RSSPACE:def_1;
then A5: seq_id a1 = a by RSSPACE:def_2;
then A6: a1 in the_set_of_RealSequences_l^ p by A1, A2, A4, Def2;
A7: b1 in the_set_of_RealSequences by RSSPACE:def_1;
then A8: seq_id b1 = b by RSSPACE:def_2;
then A9: b1 in the_set_of_RealSequences_l^ p by A1, A3, A7, Def2;
then reconsider b1 = b1 as VECTOR of Linear_Space_of_RealSequences ;
reconsider a1 = a1 as VECTOR of Linear_Space_of_RealSequences by A6;
A10: seq_id (a1 + b1) = seq_id ((seq_id a1) + (seq_id b1)) by RSSPACE:2, RSSPACE:def_7
.= a + b by A5, A8, RSSPACE:1 ;
 the_set_of_RealSequences_l^ p is linearly-closed by A1, Th4;
then  a1 + b1 in the_set_of_RealSequences_l^ p by A6, A9, RLSUB_1:def_1;
hence  (a + b) rto_power p is summable by A1, A10, Def2; ::_thesis: verum
end;

theorem Th16: :: LP_SPACE:16
for p being Real st 1 <= p holds
for lp being RealNormSpace 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 vseq being sequence of lp st vseq is Cauchy_sequence_by_Norm holds
vseq is convergent
proof
let p be Real; ::_thesis: ( 1 <= p implies for lp being RealNormSpace 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 vseq being sequence of lp st vseq is Cauchy_sequence_by_Norm holds
vseq is convergent )
assume A1: 1 <= p ; ::_thesis: for lp being RealNormSpace 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 vseq being sequence of lp st vseq is Cauchy_sequence_by_Norm holds
vseq is convergent
A2: 1 / p > 0 by A1, XREAL_1:139;
let lp be RealNormSpace; ::_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 vseq being sequence of lp st vseq is Cauchy_sequence_by_Norm holds
vseq is convergent )
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 vseq being sequence of lp st vseq is Cauchy_sequence_by_Norm holds
vseq is convergent
let vseq be sequence of lp; ::_thesis: ( vseq is Cauchy_sequence_by_Norm implies vseq is convergent )
assume A4: vseq is Cauchy_sequence_by_Norm ; ::_thesis: vseq is convergent
defpred S1[ set , set ] means  ex i being Element of NAT st
( $1 = i & ex rseqi being Real_Sequence st
( ( for n being Element of NAT holds rseqi . n = (seq_id (vseq . n)) . i ) & rseqi is convergent & $2 = lim rseqi ) );
A5: p * (1 / p) = (p * 1) / p by XCMPLX_1:74
.= 1 by A1, XCMPLX_1:60 ;
A6: for x being set st x in NAT holds
ex y being set st
( y in REAL & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in NAT implies ex y being set st
( y in REAL & S1[x,y] ) )
assume  x in NAT ; ::_thesis: ex y being set st
( y in REAL & S1[x,y] )
then reconsider i = x as Element of NAT ;
deffunc H1( Element of NAT ) ->  Element of REAL = (seq_id (vseq . $1)) . i;
consider rseqi being Real_Sequence such that
A7: for n being Element of NAT holds rseqi . n = H1(n) from SEQ_1:sch_1();
take  lim rseqi ; ::_thesis: ( lim rseqi in REAL & S1[x, lim rseqi] )
now__::_thesis:_for_e1_being_real_number_st_e1_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_k_<=_m_holds_
abs_((rseqi_._m)_-_(rseqi_._k))_<_e1
let e1 be real number ; ::_thesis: ( e1 > 0 implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((rseqi . m) - (rseqi . k)) < e1 )
assume A8: e1 > 0 ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((rseqi . m) - (rseqi . k)) < e1
reconsider e = e1 as Real by XREAL_0:def_1;
thus  ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((rseqi . m) - (rseqi . k)) < e1 ::_thesis: verum
proof
consider k being Element of NAT  such that
A9: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A4, A8, RSSPACE3:8;
 for m being Element of NAT st k <= m holds
abs ((rseqi . m) - (rseqi . k)) < e
proof
let m be Element of NAT ; ::_thesis: ( k <= m implies abs ((rseqi . m) - (rseqi . k)) < e )
assume A10: k <= m ; ::_thesis: abs ((rseqi . m) - (rseqi . k)) < e
A11: ||.((vseq . m) - (vseq . k)).|| = the normF of lp . ((vseq . m) - (vseq . k))
.= (Sum ((seq_id ((vseq . m) - (vseq . k))) rto_power p)) to_power (1 / p) by A3, Def3 ;
then  (Sum ((seq_id ((vseq . m) - (vseq . k))) rto_power p)) to_power (1 / p) < e by A9, A10;
then A12: ((Sum ((seq_id ((vseq . m) - (vseq . k))) rto_power p)) to_power (1 / p)) to_power p < e to_power p by A1, A11, Th1, NORMSP_1:4;
A13: now__::_thesis:_for_i_being_Element_of_NAT_holds_((seq_id_((vseq_._m)_-_(vseq_._k)))_rto_power_p)_._i_>=_0
let i be Element of NAT ; ::_thesis: ((seq_id ((vseq . m) - (vseq . k))) rto_power p) . i >= 0
 ((seq_id ((vseq . m) - (vseq . k))) rto_power p) . i = (abs ((seq_id ((vseq . m) - (vseq . k))) . i)) to_power p by Def1;
hence  ((seq_id ((vseq . m) - (vseq . k))) rto_power p) . i >= 0 by A1, Lm1, COMPLEX1:46; ::_thesis: verum
end;
reconsider vsem = vseq . m, vsek = vseq . k as VECTOR of lp ;
A14: now__::_thesis:_for_a,_b,_c_being_Real_st_a_=_0_&_b_>_0_&_c_>_0_holds_
a_to_power_(b_*_c)_=_0
let a, b, c be Real; ::_thesis: ( a = 0 & b > 0 & c > 0 implies a to_power (b * c) = 0 )
assume that
A15: a = 0 and
A16: b > 0 and
A17: c > 0 ; ::_thesis: a to_power (b * c) = 0
 b * c > 0 by A16, A17, XREAL_1:129;
hence  a to_power (b * c) = 0 by A15, POWER:def_2; ::_thesis: verum
end;
A18: now__::_thesis:_for_a,_b,_c_being_Real_st_a_=_0_&_b_>_0_&_c_>_0_holds_
(a_to_power_b)_to_power_c_=_0
let a, b, c be Real; ::_thesis: ( a = 0 & b > 0 & c > 0 implies (a to_power b) to_power c = 0 )
assume that
A19: a = 0 and
A20: b > 0 and
A21: c > 0 ; ::_thesis: (a to_power b) to_power c = 0
 a to_power b = 0 by A19, A20, POWER:def_2;
hence  (a to_power b) to_power c = 0 by A21, POWER:def_2; ::_thesis: verum
end;
A22: now__::_thesis:_for_a,_b,_c_being_Real_st_a_=_0_&_b_>_0_&_c_>_0_holds_
(a_to_power_b)_to_power_c_=_a_to_power_(b_*_c)
let a, b, c be Real; ::_thesis: ( a = 0 & b > 0 & c > 0 implies (a to_power b) to_power c = a to_power (b * c) )
assume that
A23: a = 0 and
A24: b > 0 and
A25: c > 0 ; ::_thesis: (a to_power b) to_power c = a to_power (b * c)
thus (a to_power b) to_power c = 0 by A18, A23, A24, A25
.= a to_power (b * c) by A14, A23, A24, A25 ; ::_thesis: verum
end;
A26: for a, b, c being Real st a >= 0 & b > 0 & c > 0 holds
(a to_power b) to_power c = a to_power (b * c)
proof
let a, b, c be Real; ::_thesis: ( a >= 0 & b > 0 & c > 0 implies (a to_power b) to_power c = a to_power (b * c) )
assume that
A27: a >= 0 and
A28: b > 0 and
A29: c > 0 ; ::_thesis: (a to_power b) to_power c = a to_power (b * c)
 ( a > 0 or a = 0 ) by A27;
hence  (a to_power b) to_power c = a to_power (b * c) by A22, A28, A29, POWER:33; ::_thesis: verum
end;
 ((seq_id ((vseq . m) - (vseq . k))) rto_power p) . i = (abs ((seq_id ((vseq . m) - (vseq . k))) . i)) to_power p by Def1;
then A30: (((seq_id ((vseq . m) - (vseq . k))) rto_power p) . i) to_power (1 / p) = (abs ((seq_id ((vseq . m) - (vseq . k))) . i)) to_power 1 by A1, A2, A5, A26, COMPLEX1:46
.= abs ((seq_id ((vseq . m) - (vseq . k))) . i) by POWER:25 ;
A31: rseqi . m = (seq_id (vseq . m)) . i by A7;
A32: (seq_id ((vseq . m) - (vseq . k))) rto_power p is summable by A1, A3, Th10;
then A33: ((seq_id ((vseq . m) - (vseq . k))) rto_power p) . i <= Sum ((seq_id ((vseq . m) - (vseq . k))) rto_power p) by A13, RSSPACE2:3;
((Sum ((seq_id ((vseq . m) - (vseq . k))) rto_power p)) to_power (1 / p)) to_power p = (Sum ((seq_id ((vseq . m) - (vseq . k))) rto_power p)) to_power ((1 / p) * p) by A1, A2, A32, A13, HOLDER_1:2, SERIES_1:18
.= Sum ((seq_id ((vseq . m) - (vseq . k))) rto_power p) by A5, POWER:25 ;
then A34: ((seq_id ((vseq . m) - (vseq . k))) rto_power p) . i < e to_power p by A12, A33, XXREAL_0:2;
A35: rseqi . k = (seq_id (vseq . k)) . i by A7;
 vsem - vsek = (seq_id vsem) - (seq_id vsek) by A1, A3, Th10;
then A36: abs ((seq_id ((vseq . m) - (vseq . k))) . i) = abs (((seq_id (vseq . m)) + (- (seq_id (vseq . k)))) . i) by RSSPACE:1
.= abs (((seq_id (vseq . m)) . i) + ((- (seq_id (vseq . k))) . i)) by SEQ_1:7
.= abs (((seq_id (vseq . m)) . i) + (- ((seq_id (vseq . k)) . i))) by SEQ_1:10
.= abs ((rseqi . m) - (rseqi . k)) by A31, A35 ;
(e to_power p) to_power (1 / p) = e to_power ((1 / p) * p) by A8, POWER:33
.= e to_power 1 by A1, XCMPLX_1:106
.= e by POWER:25 ;
hence  abs ((rseqi . m) - (rseqi . k)) < e by A2, A13, A30, A34, A36, Th1; ::_thesis: verum
end;
hence  ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((rseqi . m) - (rseqi . k)) < e1 ; ::_thesis: verum
end;
end;
then  rseqi is convergent by SEQ_4:41;
hence  ( lim rseqi in REAL & S1[x, lim rseqi] ) by A7; ::_thesis: verum
end;
consider f being Function of NAT,REAL such that
A37: for x being set st x in NAT holds
S1[x,f . x] from FUNCT_2:sch_1(A6);
reconsider tseq = f as Real_Sequence ;
A38: now__::_thesis:_for_i_being_Element_of_NAT_ex_rseqi_being_Real_Sequence_st_
(_(_for_n_being_Element_of_NAT_holds_rseqi_._n_=_(seq_id_(vseq_._n))_._i_)_&_rseqi_is_convergent_&_tseq_._i_=_lim_rseqi_)
let i be Element of NAT ; ::_thesis: ex rseqi being Real_Sequence st
( ( for n being Element of NAT holds rseqi . n = (seq_id (vseq . n)) . i ) & rseqi is convergent & tseq . i = lim rseqi )
reconsider x = i as set ;
 ex i0 being Element of NAT st
( x = i0 & ex rseqi being Real_Sequence st
( ( for n being Element of NAT holds rseqi . n = (seq_id (vseq . n)) . i0 ) & rseqi is convergent & f . x = lim rseqi ) ) by A37;
hence  ex rseqi being Real_Sequence st
( ( for n being Element of NAT holds rseqi . n = (seq_id (vseq . n)) . i ) & rseqi is convergent & tseq . i = lim rseqi ) ; ::_thesis: verum
end;
A39: for e being Real st e > 0 holds
ex k being Element of NAT st
for n being Element of NAT st n >= k holds
( ((seq_id tseq) - (seq_id (vseq . n))) rto_power p is summable & Sum (((seq_id tseq) - (seq_id (vseq . n))) rto_power p) < e )
proof
A40: for n, i being Element of NAT
for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) rto_power p)) . i ) holds
( rseq is convergent & lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . i )
proof
let n be Element of NAT ; ::_thesis: for i being Element of NAT
for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) rto_power p)) . i ) holds
( rseq is convergent & lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . i )
defpred S2[ Element of NAT ] means  for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) rto_power p)) . $1 ) holds
( rseq is convergent & lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . $1 );
A41: for m, k being Element of NAT holds seq_id ((vseq . m) - (vseq . k)) = (seq_id (vseq . m)) - (seq_id (vseq . k))
proof
let m, k be Element of NAT ; ::_thesis: seq_id ((vseq . m) - (vseq . k)) = (seq_id (vseq . m)) - (seq_id (vseq . k))
 seq_id ((vseq . m) - (vseq . k)) = seq_id ((seq_id (vseq . m)) - (seq_id (vseq . k))) by A1, A3, Th10;
hence  seq_id ((vseq . m) - (vseq . k)) = (seq_id (vseq . m)) - (seq_id (vseq . k)) by RSSPACE:1; ::_thesis: verum
end;
now__::_thesis:_for_i_being_Element_of_NAT_st_(_for_rseq_being_Real_Sequence_st_(_for_m_being_Element_of_NAT_holds_rseq_._m_=_(Partial_Sums_((seq_id_((vseq_._m)_-_(vseq_._n)))_rto_power_p))_._i_)_holds_
(_rseq_is_convergent_&_lim_rseq_=_(Partial_Sums_(((seq_id_tseq)_-_(seq_id_(vseq_._n)))_rto_power_p))_._i_)_)_holds_
for_rseq_being_Real_Sequence_st_(_for_m_being_Element_of_NAT_holds_rseq_._m_=_(Partial_Sums_((seq_id_((vseq_._m)_-_(vseq_._n)))_rto_power_p))_._(i_+_1)_)_holds_
(_rseq_is_convergent_&_lim_rseq_=_(Partial_Sums_(((seq_id_tseq)_-_(seq_id_(vseq_._n)))_rto_power_p))_._(i_+_1)_)
let i be Element of NAT ; ::_thesis: ( ( for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) rto_power p)) . i ) holds
( rseq is convergent & lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . i ) ) implies for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) rto_power p)) . (i + 1) ) holds
( rseq is convergent & lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . (i + 1) ) )
assume A42: for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) rto_power p)) . i ) holds
( rseq is convergent & lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . i ) ; ::_thesis: for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) rto_power p)) . (i + 1) ) holds
( rseq is convergent & lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . (i + 1) )
thus  for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) rto_power p)) . (i + 1) ) holds
( rseq is convergent & lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . (i + 1) ) ::_thesis: verum
proof
deffunc H1( Element of NAT ) ->  Element of REAL = (Partial_Sums ((seq_id ((vseq . $1) - (vseq . n))) rto_power p)) . i;
consider rseqb being Real_Sequence such that
A43: for m being Element of NAT holds rseqb . m = H1(m) from SEQ_1:sch_1();
consider rseq0 being Real_Sequence such that
A44: for m being Element of NAT holds rseq0 . m = (seq_id (vseq . m)) . (i + 1) and
A45: rseq0 is convergent and
A46: tseq . (i + 1) = lim rseq0 by A38;
let rseq be Real_Sequence; ::_thesis: ( ( for m being Element of NAT holds rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) rto_power p)) . (i + 1) ) implies ( rseq is convergent & lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . (i + 1) ) )
assume A47: for m being Element of NAT holds rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) rto_power p)) . (i + 1) ; ::_thesis: ( rseq is convergent & lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . (i + 1) )
A48: now__::_thesis:_for_m_being_Element_of_NAT_holds_rseq_._m_=_((abs_((rseq0_._m)_-_((seq_id_(vseq_._n))_._(i_+_1))))_to_power_p)_+_(rseqb_._m)
let m be Element of NAT ; ::_thesis: rseq . m = ((abs ((rseq0 . m) - ((seq_id (vseq . n)) . (i + 1)))) to_power p) + (rseqb . m)
thus rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) rto_power p)) . (i + 1) by A47
.= (((seq_id ((vseq . m) - (vseq . n))) rto_power p) . (i + 1)) + ((Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) rto_power p)) . i) by SERIES_1:def_1
.= ((((seq_id (vseq . m)) - (seq_id (vseq . n))) rto_power p) . (i + 1)) + ((Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) rto_power p)) . i) by A41
.= ((((seq_id (vseq . m)) - (seq_id (vseq . n))) rto_power p) . (i + 1)) + (rseqb . m) by A43
.= ((abs (((seq_id (vseq . m)) + (- (seq_id (vseq . n)))) . (i + 1))) to_power p) + (rseqb . m) by Def1
.= ((abs (((seq_id (vseq . m)) . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1)))) to_power p) + (rseqb . m) by SEQ_1:7
.= ((abs (((seq_id (vseq . m)) . (i + 1)) + (- ((seq_id (vseq . n)) . (i + 1))))) to_power p) + (rseqb . m) by SEQ_1:10
.= ((abs (((seq_id (vseq . m)) . (i + 1)) - ((seq_id (vseq . n)) . (i + 1)))) to_power p) + (rseqb . m)
.= ((abs ((rseq0 . m) - ((seq_id (vseq . n)) . (i + 1)))) to_power p) + (rseqb . m) by A44 ; ::_thesis: verum
end;
A49: lim rseqb = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . i by A42, A43;
A50: rseqb is convergent by A42, A43;
then  lim rseq = ((abs ((lim rseq0) - ((seq_id (vseq . n)) . (i + 1)))) to_power p) + (lim rseqb) by A1, A45, A48, Lm9
.= ((abs ((tseq . (i + 1)) + (- ((seq_id (vseq . n)) . (i + 1))))) to_power p) + (lim rseqb) by A46
.= ((abs ((tseq . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1)))) to_power p) + (lim rseqb) by SEQ_1:10
.= ((abs ((tseq - (seq_id (vseq . n))) . (i + 1))) to_power p) + (lim rseqb) by SEQ_1:7
.= (((tseq - (seq_id (vseq . n))) rto_power p) . (i + 1)) + ((Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . i) by A49, Def1
.= ((((seq_id tseq) - (seq_id (vseq . n))) rto_power p) . (i + 1)) + ((Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . i) by RSSPACE:1
.= (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . (i + 1) by SERIES_1:def_1 ;
hence  ( rseq is convergent & lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . (i + 1) ) by A1, A50, A45, A48, Lm9; ::_thesis: verum
end;
end;
then A51: for i being Element of NAT st S2[i] holds
S2[i + 1] ;
now__::_thesis:_for_rseq_being_Real_Sequence_st_(_for_m_being_Element_of_NAT_holds_rseq_._m_=_(Partial_Sums_((seq_id_((vseq_._m)_-_(vseq_._n)))_rto_power_p))_._0_)_holds_
(_rseq_is_convergent_&_lim_rseq_=_(Partial_Sums_(((seq_id_tseq)_-_(seq_id_(vseq_._n)))_rto_power_p))_._0_)
let rseq be Real_Sequence; ::_thesis: ( ( for m being Element of NAT holds rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) rto_power p)) . 0 ) implies ( rseq is convergent & lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . 0 ) )
assume A52: for m being Element of NAT holds rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) rto_power p)) . 0 ; ::_thesis: ( rseq is convergent & lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . 0 )
thus  ( rseq is convergent & lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . 0 ) ::_thesis: verum
proof
consider rseq0 being Real_Sequence such that
A53: for m being Element of NAT holds rseq0 . m = (seq_id (vseq . m)) . 0 and
A54: rseq0 is convergent and
A55: tseq . 0 = lim rseq0 by A38;
A56: for m being Element of NAT holds rseq . m = (abs ((rseq0 . m) - ((seq_id (vseq . n)) . 0))) to_power p
proof
let m be Element of NAT ; ::_thesis: rseq . m = (abs ((rseq0 . m) - ((seq_id (vseq . n)) . 0))) to_power p
rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) rto_power p)) . 0 by A52
.= ((seq_id ((vseq . m) - (vseq . n))) rto_power p) . 0 by SERIES_1:def_1
.= (((seq_id (vseq . m)) - (seq_id (vseq . n))) rto_power p) . 0 by A41
.= (abs (((seq_id (vseq . m)) + (- (seq_id (vseq . n)))) . 0)) to_power p by Def1
.= (abs (((seq_id (vseq . m)) . 0) + ((- (seq_id (vseq . n))) . 0))) to_power p by SEQ_1:7
.= (abs (((seq_id (vseq . m)) . 0) + (- ((seq_id (vseq . n)) . 0)))) to_power p by SEQ_1:10
.= (abs (((seq_id (vseq . m)) . 0) - ((seq_id (vseq . n)) . 0))) to_power p ;
hence  rseq . m = (abs ((rseq0 . m) - ((seq_id (vseq . n)) . 0))) to_power p by A53; ::_thesis: verum
end;
then  lim rseq = (abs ((lim rseq0) - ((seq_id (vseq . n)) . 0))) to_power p by A1, A54, Lm8
.= (abs ((tseq . 0) + (- ((seq_id (vseq . n)) . 0)))) to_power p by A55
.= (abs ((tseq . 0) + ((- (seq_id (vseq . n))) . 0))) to_power p by SEQ_1:10
.= (abs ((tseq - (seq_id (vseq . n))) . 0)) to_power p by SEQ_1:7
.= (abs (((seq_id tseq) + (- (seq_id (vseq . n)))) . 0)) to_power p by RSSPACE:1
.= (((seq_id tseq) + (- (seq_id (vseq . n)))) rto_power p) . 0 by Def1
.= (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . 0 by SERIES_1:def_1 ;
hence  ( rseq is convergent & lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . 0 ) by A1, A54, A56, Lm8; ::_thesis: verum
end;
end;
then A57: S2[ 0 ] ;
 for i being Element of NAT holds S2[i] from NAT_1:sch_1(A57, A51);
hence  for i being Element of NAT
for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) rto_power p)) . i ) holds
( rseq is convergent & lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . i ) ; ::_thesis: verum
end;
let e2 be Real; ::_thesis: ( e2 > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
( ((seq_id tseq) - (seq_id (vseq . n))) rto_power p is summable & Sum (((seq_id tseq) - (seq_id (vseq . n))) rto_power p) < e2 ) )
assume A58: e2 > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
( ((seq_id tseq) - (seq_id (vseq . n))) rto_power p is summable & Sum (((seq_id tseq) - (seq_id (vseq . n))) rto_power p) < e2 )
set e = e2 / 2;
set e1 = (e2 / 2) to_power (1 / p);
 e2 / 2 > 0 by A58, XREAL_1:215;
then  (e2 / 2) to_power (1 / p) > 0 by POWER:34;
then consider k being Element of NAT  such that
A59: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < (e2 / 2) to_power (1 / p) by A4, RSSPACE3:8;
A60: for m, n being Element of NAT st n >= k & m >= k holds
( (seq_id ((vseq . m) - (vseq . n))) rto_power p is summable & Sum ((seq_id ((vseq . m) - (vseq . n))) rto_power p) < e2 / 2 & ( for i being Element of NAT holds 0 <= ((seq_id ((vseq . m) - (vseq . n))) rto_power p) . i ) )
proof
let m, n be Element of NAT ; ::_thesis: ( n >= k & m >= k implies ( (seq_id ((vseq . m) - (vseq . n))) rto_power p is summable & Sum ((seq_id ((vseq . m) - (vseq . n))) rto_power p) < e2 / 2 & ( for i being Element of NAT holds 0 <= ((seq_id ((vseq . m) - (vseq . n))) rto_power p) . i ) ) )
assume that
A61: n >= k and
A62: m >= k ; ::_thesis: ( (seq_id ((vseq . m) - (vseq . n))) rto_power p is summable & Sum ((seq_id ((vseq . m) - (vseq . n))) rto_power p) < e2 / 2 & ( for i being Element of NAT holds 0 <= ((seq_id ((vseq . m) - (vseq . n))) rto_power p) . i ) )
 ||.((vseq . m) - (vseq . n)).|| < (e2 / 2) to_power (1 / p) by A59, A61, A62;
then  the normF of lp . ((vseq . m) - (vseq . n)) < (e2 / 2) to_power (1 / p) ;
then A63: (Sum ((seq_id ((vseq . m) - (vseq . n))) rto_power p)) to_power (1 / p) < (e2 / 2) to_power (1 / p) by A3, Def3;
A64: for i being Element of NAT holds ((seq_id ((vseq . m) - (vseq . n))) rto_power p) . i >= 0
proof
let i be Element of NAT ; ::_thesis: ((seq_id ((vseq . m) - (vseq . n))) rto_power p) . i >= 0
 ((seq_id ((vseq . m) - (vseq . n))) rto_power p) . i = (abs ((seq_id ((vseq . m) - (vseq . n))) . i)) to_power p by Def1;
hence  ((seq_id ((vseq . m) - (vseq . n))) rto_power p) . i >= 0 by A1, Lm1, COMPLEX1:46; ::_thesis: verum
end;
A65: (seq_id ((vseq . m) - (vseq . n))) rto_power p is summable by A1, A3, Th10;
then A66: (Sum ((seq_id ((vseq . m) - (vseq . n))) rto_power p)) to_power (1 / p) >= 0 by A2, A64, Lm1, SERIES_1:18;
A67: ((e2 / 2) to_power (1 / p)) to_power p = (e2 / 2) to_power ((1 / p) * p) by A58, POWER:33, XREAL_1:215
.= (e2 / 2) to_power 1 by A1, XCMPLX_1:106
.= e2 / 2 by POWER:25 ;
((Sum ((seq_id ((vseq . m) - (vseq . n))) rto_power p)) to_power (1 / p)) to_power p = (Sum ((seq_id ((vseq . m) - (vseq . n))) rto_power p)) to_power ((1 / p) * p) by A1, A2, A64, A65, HOLDER_1:2, SERIES_1:18
.= Sum ((seq_id ((vseq . m) - (vseq . n))) rto_power p) by A5, POWER:25 ;
hence  ( (seq_id ((vseq . m) - (vseq . n))) rto_power p is summable & Sum ((seq_id ((vseq . m) - (vseq . n))) rto_power p) < e2 / 2 & ( for i being Element of NAT holds 0 <= ((seq_id ((vseq . m) - (vseq . n))) rto_power p) . i ) ) by A1, A3, A64, A63, A67, A66, Th1, Th10; ::_thesis: verum
end;
A68: e2 > e2 / 2 by A58, XREAL_1:216;
 for n being Element of NAT st n >= k holds
( ((seq_id tseq) - (seq_id (vseq . n))) rto_power p is summable & Sum (((seq_id tseq) - (seq_id (vseq . n))) rto_power p) < e2 )
proof
let n be Element of NAT ; ::_thesis: ( n >= k implies ( ((seq_id tseq) - (seq_id (vseq . n))) rto_power p is summable & Sum (((seq_id tseq) - (seq_id (vseq . n))) rto_power p) < e2 ) )
assume A69: n >= k ; ::_thesis: ( ((seq_id tseq) - (seq_id (vseq . n))) rto_power p is summable & Sum (((seq_id tseq) - (seq_id (vseq . n))) rto_power p) < e2 )
A70: for i being Element of NAT st 0 <= i holds
(Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . i <= e2 / 2
proof
let i be Element of NAT ; ::_thesis: ( 0 <= i implies (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . i <= e2 / 2 )
assume  0 <= i ; ::_thesis: (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . i <= e2 / 2
deffunc H1( Element of NAT ) ->  Element of REAL = (Partial_Sums ((seq_id ((vseq . $1) - (vseq . n))) rto_power p)) . i;
consider rseq being Real_Sequence such that
A71: for m being Element of NAT holds rseq . m = H1(m) from SEQ_1:sch_1();
A72: for m being Element of NAT st m >= k holds
rseq . m <= e2 / 2
proof
let m be Element of NAT ; ::_thesis: ( m >= k implies rseq . m <= e2 / 2 )
A73: rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) rto_power p)) . i by A71;
assume A74: m >= k ; ::_thesis: rseq . m <= e2 / 2
then A75: for i being Element of NAT holds 0 <= ((seq_id ((vseq . m) - (vseq . n))) rto_power p) . i by A60, A69;
 (seq_id ((vseq . m) - (vseq . n))) rto_power p is summable by A60, A69, A74;
then A76: (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) rto_power p)) . i <= Sum ((seq_id ((vseq . m) - (vseq . n))) rto_power p) by A75, RSSPACE2:3;
 Sum ((seq_id ((vseq . m) - (vseq . n))) rto_power p) < e2 / 2 by A60, A69, A74;
hence  rseq . m <= e2 / 2 by A76, A73, XXREAL_0:2; ::_thesis: verum
end;
A77: lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . i by A40, A71;
 rseq is convergent by A40, A71;
hence  (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . i <= e2 / 2 by A77, A72, RSSPACE2:5; ::_thesis: verum
end;
now__::_thesis:_ex_e2_being_Element_of_REAL_st_
for_i_being_Element_of_NAT_holds_(Partial_Sums_(((seq_id_tseq)_-_(seq_id_(vseq_._n)))_rto_power_p))_._i_<_e2
take e2 = (e2 / 2) + 1; ::_thesis: for i being Element of NAT holds (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . i < e2
A78: e2 > e2 / 2 by XREAL_1:29;
let i be Element of NAT ; ::_thesis: (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . i < e2
 (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . i <= e2 / 2 by A70, NAT_1:2;
hence  (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) . i < e2 by A78, XXREAL_0:2; ::_thesis: verum
end;
then A79: Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p) is bounded_above by SEQ_2:def_3;
A80: Sum (((seq_id tseq) - (seq_id (vseq . n))) rto_power p) = lim (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) by SERIES_1:def_3;
A81: for i being Element of NAT holds 0 <= (((seq_id tseq) - (seq_id (vseq . n))) rto_power p) . i
proof
let i be Element of NAT ; ::_thesis: 0 <= (((seq_id tseq) - (seq_id (vseq . n))) rto_power p) . i
 (((seq_id tseq) - (seq_id (vseq . n))) rto_power p) . i = (abs (((seq_id tseq) - (seq_id (vseq . n))) . i)) to_power p by Def1;
hence  0 <= (((seq_id tseq) - (seq_id (vseq . n))) rto_power p) . i by A1, Lm1, COMPLEX1:46; ::_thesis: verum
end;
then  ((seq_id tseq) - (seq_id (vseq . n))) rto_power p is summable by A79, SERIES_1:17;
then  Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p) is convergent by SERIES_1:def_2;
then  lim (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) rto_power p)) <= e2 / 2 by A70, RSSPACE2:5;
hence  ( ((seq_id tseq) - (seq_id (vseq . n))) rto_power p is summable & Sum (((seq_id tseq) - (seq_id (vseq . n))) rto_power p) < e2 ) by A68, A81, A79, A80, SERIES_1:17, XXREAL_0:2; ::_thesis: verum
end;
hence  ex k being Element of NAT st
for n being Element of NAT st n >= k holds
( ((seq_id tseq) - (seq_id (vseq . n))) rto_power p is summable & Sum (((seq_id tseq) - (seq_id (vseq . n))) rto_power p) < e2 ) ; ::_thesis: verum
end;
 (seq_id tseq) rto_power p is summable
proof
consider m being Element of NAT  such that
A82: for n being Element of NAT st n >= m holds
( ((seq_id tseq) - (seq_id (vseq . n))) rto_power p is summable & Sum (((seq_id tseq) - (seq_id (vseq . n))) rto_power p) < 1 ) by A39;
A83: ((seq_id tseq) - (seq_id (vseq . m))) rto_power p is summable by A82;
set d = seq_id tseq;
set b = seq_id (vseq . m);
set a = (seq_id tseq) - (seq_id (vseq . m));
A84: ((seq_id tseq) - (seq_id (vseq . m))) + (seq_id (vseq . m)) = ((seq_id tseq) + (seq_id (vseq . m))) + (- (seq_id (vseq . m))) by SEQ_1:13
.= ((seq_id tseq) + (seq_id (vseq . m))) - (seq_id (vseq . m))
.= seq_id tseq by Lm10 ;
 (seq_id (vseq . m)) rto_power p is summable by A1, A3, Def2;
hence  (seq_id tseq) rto_power p is summable by A1, A83, A84, Lm11; ::_thesis: verum
end;
then reconsider tv = tseq as Point of lp by A1, A3, Th10;
 for e being Real st e > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e
proof
let e be Real; ::_thesis: ( e > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e )
assume A85: e > 0 ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e
set e1 = e to_power p;
consider m being Element of NAT  such that
A86: for n being Element of NAT st n >= m holds
( ((seq_id tseq) - (seq_id (vseq . n))) rto_power p is summable & Sum (((seq_id tseq) - (seq_id (vseq . n))) rto_power p) < e to_power p ) by A39, A85, POWER:34;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_m_holds_
||.((vseq_._n)_-_tv).||_<_e
let n be Element of NAT ; ::_thesis: ( n >= m implies ||.((vseq . n) - tv).|| < e )
assume A87: n >= m ; ::_thesis: ||.((vseq . n) - tv).|| < e
A88: Sum (((seq_id tseq) - (seq_id (vseq . n))) rto_power p) < e to_power p by A86, A87;
 for i being Element of NAT holds (((seq_id tseq) - (seq_id (vseq . n))) rto_power p) . i >= 0
proof
let i be Element of NAT ; ::_thesis: (((seq_id tseq) - (seq_id (vseq . n))) rto_power p) . i >= 0
 (((seq_id tseq) - (seq_id (vseq . n))) rto_power p) . i = (abs (((seq_id tseq) - (seq_id (vseq . n))) . i)) to_power p by Def1;
hence  (((seq_id tseq) - (seq_id (vseq . n))) rto_power p) . i >= 0 by A1, Lm1, COMPLEX1:46; ::_thesis: verum
end;
then A89: Sum (((seq_id tseq) - (seq_id (vseq . n))) rto_power p) >= 0 by A86, A87, SERIES_1:18;
A90: (e to_power p) to_power (1 / p) = e to_power (p * (1 / p)) by A85, POWER:33
.= e to_power 1 by A1, XCMPLX_1:106
.= e by POWER:25 ;
(Sum (((seq_id tv) - (seq_id (vseq . n))) rto_power p)) to_power (1 / p) = (Sum ((seq_id ((seq_id tv) - (seq_id (vseq . n)))) rto_power p)) to_power (1 / p) by RSSPACE:1
.= (Sum ((seq_id (tv - (vseq . n))) rto_power p)) to_power (1 / p) by A1, A3, Th10
.= the normF of lp . (tv - (vseq . n)) by A3, Def3
.= ||.(tv + (- (vseq . n))).||
.= ||.(- ((vseq . n) - tv)).|| by RLVECT_1:33
.= ||.((vseq . n) - tv).|| by NORMSP_1:2 ;
hence  ||.((vseq . n) - tv).|| < e by A2, A89, A88, A90, Th1; ::_thesis: verum
end;
hence  ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e ; ::_thesis: verum
end;
hence  vseq is convergent by NORMSP_1:def_6; ::_thesis: verum
end;

definition
let p be Real;
assume A1: 1 <= p ;
func l_Space^ p ->  RealBanachSpace equals :: LP_SPACE:def 4
 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) #);
coherence
 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) #) is RealBanachSpace
proof
set 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) #);
reconsider 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) #) as RealNormSpace by A1, Th9, Th14;
 for vseq being sequence of lp st vseq is Cauchy_sequence_by_Norm holds
vseq is convergent by A1, Th16;
hence  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) #) is RealBanachSpace by LOPBAN_1:def_15; ::_thesis: verum
end;
end;

:: deftheorem  defines l_Space^ LP_SPACE:def_4_:_
 for p being Real st 1 <= p holds
l_Space^ p = 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) #);