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 A3: ( v in the_set_of_RealSequences_l^ p & u in the_set_of_RealSequences_l^ p ) ; :: thesis: v + u in the_set_of_RealSequences_l^ p
A4: (seq_id (v + u)) rto_power p is summable

proof

A5: (seq_id v) rto_power p is summable by A1, A3, Def2;
A6: (seq_id u) rto_power p is summable by A1, A3, Def2;
A7: 1 / p > 0 by A1, XREAL_1:141;
set p1 = 1 / p;
set vp = (seq_id v) rto_power p;
set up = (seq_id u) rto_power p;
A8: p * (1 / p) = (p * 1) / p by XCMPLX_1:75
.= 1 by A1, XCMPLX_1:60 ;

A9: now

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 A10: ((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 A11: ((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:132; :: 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:132; :: 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, A10, POWER:39, 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:132; :: 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:132; :: thesis: 0 <= ((seq_id u) rto_power p) . n
hence 0 <= ((seq_id u) rto_power p) . n by A1, A11, POWER:39, POWER:def 2; :: thesis: verum

end;

then A12: Partial_Sums ((seq_id u) rto_power p) is non-decreasing by SERIES_1:19;
Partial_Sums ((seq_id u) rto_power p) is bounded_above by A6, A9, SERIES_1:20;
then consider r1 being real number such that
A13: 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;

A14: now

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 A15: 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 A15, SEQ_1:4;
A16: (Partial_Sums ((seq_id u) rto_power p)) . 0 <= (Partial_Sums ((seq_id u) rto_power p)) . n1 by A12, SEQM_3:21;
0 <= ((seq_id u) rto_power p) . 0 by A9;
then 0 <= (Partial_Sums ((seq_id u) rto_power p)) . 0 by SERIES_1:def 1;
hence ((Partial_Sums ((seq_id u) rto_power p)) . n) to_power (1 / p) < r1 to_power (1 / p) by A7, A13, A15, A16, Th1; :: thesis: verum

end;

A17: Partial_Sums ((seq_id v) rto_power p) is non-decreasing by A9, SERIES_1:19;
Partial_Sums ((seq_id v) rto_power p) is bounded_above by A5, A9, SERIES_1:20;
then consider r being real number such that
A18: 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;
reconsider r = r as Real by XREAL_0:def 1;

now

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 A19: 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 A19, SEQ_1:4;
A20: (Partial_Sums ((seq_id v) rto_power p)) . 0 <= (Partial_Sums ((seq_id v) rto_power p)) . n1 by A17, SEQM_3:21;
0 <= ((seq_id v) rto_power p) . 0 by A9;
then 0 <= (Partial_Sums ((seq_id v) rto_power p)) . 0 by SERIES_1:def 1;
hence ((Partial_Sums ((seq_id v) rto_power p)) . n) to_power (1 / p) < r to_power (1 / p) by A7, A18, A19, A20, Th1; :: thesis: verum

end;

then consider q being Real such that
A21: 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 ;
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 by A14;
set g = q + q1;
v in the_set_of_RealSequences by A1, A3, Def2;
then reconsider vq = v as Real_Sequence by RSSPACE:def 1;
u in the_set_of_RealSequences by A1, A3, Def2;
then reconsider uq = u as Real_Sequence by RSSPACE:def 1;
A23: (seq_id v) rto_power p = vq rto_power p by RSSPACE:3;
A24: (seq_id u) rto_power p = uq rto_power p by RSSPACE:3;

now

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 )
NAT = dom (Partial_Sums ((seq_id u) rto_power p)) by SEQ_1:4;
then A25: ((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:4;
then A26: (((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 A21, A25, XREAL_1:10;
((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, A23, A24, Th2;
then A27: ((Partial_Sums ((vq + uq) rto_power p)) . n) to_power (1 / p) < q + q1 by A26, XXREAL_0:2;

A28: now

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:38
.= (Partial_Sums ((vq + uq) rto_power p)) . n by A8, POWER:30 ;
:: thesis: verum

end;

A29: now

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 A7, 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 )
A32: ((vq + uq) rto_power p) . n = (abs ((vq + uq) . n)) to_power p by Def1;
thus ( 0 < abs ((vq + uq) . n) or 0 = abs ((vq + uq) . n) ) by COMPLEX1:132; :: thesis: 0 <= ((vq + uq) rto_power p) . n
hence 0 <= ((vq + uq) rto_power p) . n by A1, A32, POWER:39, POWER:def 2; :: thesis: verum

end;

then A33: Partial_Sums ((vq + uq) rto_power p) is non-decreasing by SERIES_1:19;

A34: now

A35: (Partial_Sums ((vq + uq) rto_power p)) . 0 <= (Partial_Sums ((vq + uq) rto_power p)) . n by A33, SEQM_3:21;
A36: 0 <= ((vq + uq) rto_power p) . 0 by A31;
hence 0 <= (Partial_Sums ((vq + uq) rto_power p)) . 0 by SERIES_1:def 1; :: thesis: 0 <= (Partial_Sums ((vq + uq) rto_power p)) . n
thus 0 <= (Partial_Sums ((vq + uq) rto_power p)) . n by A35, A36, SERIES_1:def 1; :: thesis: verum

end;

then ((Partial_Sums ((vq + uq) rto_power p)) . n) to_power (1 / p) >= 0 by A7, Lm1;
hence (Partial_Sums ((vq + uq) rto_power p)) . n < (q + q1) to_power p by A1, A27, A28, A29, A34, Th1; :: thesis: verum

end;

then A37: 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;
A38: seq_id v = vq by RSSPACE:3;
A39: seq_id u = uq by RSSPACE:3;
(seq_id v) + (seq_id u) = seq_id ((seq_id v) + (seq_id u)) by RSSPACE:3
.= seq_id (v + u) by RSSPACE:4, RSSPACE:def 7 ;
hence (seq_id (v + u)) rto_power p is summable by A37, A38, A39, SERIES_1:20; :: thesis: verum

end;

v + u = (seq_id v) + (seq_id u) by RSSPACE:4, RSSPACE:def 7
.= seq_id ((seq_id v) + (seq_id u)) by RSSPACE:3
.= seq_id (v + u) by RSSPACE:4, 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, A4, 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 A40: 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;
A41: (seq_id v) rto_power p is summable by A1, A40, Def2;

now

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 )
A42: ((seq_id v) rto_power p) . n = (abs ((seq_id v) . n)) to_power p by Def1;
thus 0 <= abs ((seq_id v) . n) by COMPLEX1:132; :: thesis: ( ( 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) or 0 = abs ((seq_id v) . n) ) by COMPLEX1:132; :: thesis: 0 <= ((seq_id v) rto_power p) . n
hence 0 <= ((seq_id v) rto_power p) . n by A1, A42, POWER:39, POWER:def 2; :: thesis: verum

end;

then A43: Partial_Sums ((seq_id v) rto_power p) is bounded_above by A41, SERIES_1:20;
A44: seq_id (a * v) = seq_id (a (#) (seq_id v)) by RSSPACE:5, RSSPACE:def 7
.= a (#) (seq_id v) by RSSPACE:3 ;
A45: 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

A46: now

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
A47: abs a >= 0 by COMPLEX1:132;
A48: abs ((seq_id v) . n) >= 0 by COMPLEX1:132;
A49: (a (#) (seq_id v)) . n = a * ((seq_id v) . n) by SEQ_1:13;
((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 A49, COMPLEX1:151
.= ((abs a) to_power p) * ((abs ((seq_id v) . n)) to_power p) by A1, A47, A48, Lm2 ;
hence ((seq_id (a * v)) rto_power p) . n = ((abs a) to_power p) * (((seq_id v) rto_power p) . n) by A44, Def1
.= (((abs a) to_power p) (#) ((seq_id v) rto_power p)) . n by SEQ_1:13 ;
:: thesis: verum

end;

A50: (seq_id (a * v)) rto_power p = ((abs a) to_power p) (#) ((seq_id v) rto_power p)

proof

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 by A46;
hence (seq_id (a * v)) rto_power p = ((abs a) to_power p) (#) ((seq_id v) rto_power p) by FUNCT_2:18; :: thesis: verum

end;

A51: 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:12;
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)
thus (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 A50, A51, SEQ_1:13; :: thesis: verum

end;

consider r being real number such that
A52: 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 A43, SEQ_2:def 1;
A53: ( 0 < (abs a) to_power p or 0 = (abs a) to_power p ) by A1, Lm1, COMPLEX1:132;

A54: now

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 A55: 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:3;
hence n in dom (Partial_Sums ((seq_id (a * v)) rto_power p)) by A55, SEQ_1:3; :: 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 A52, A53, A55, XREAL_1:70; :: thesis: verum

end;

A56: 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 A57: 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 )
n in NAT by A57, SEQ_1:3;
then n in dom (Partial_Sums ((seq_id v) rto_power p)) by SEQ_1:3;
then A58: ( ((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 A54;
reconsider n1 = n as Element of NAT by A57, SEQ_1:3;
( (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 A45, A58;
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;

A59: 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

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 A60: n in dom (Partial_Sums ((seq_id (a * v)) rto_power p)) ; :: thesis: (Partial_Sums ((seq_id (a * v)) rto_power p)) . n < r1
((abs a) to_power p) * r < (((abs a) to_power p) * r) + 1 by XREAL_1:31;
hence (Partial_Sums ((seq_id (a * v)) rto_power p)) . n < r1 by A56, A60, 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;

A61: for n being Element of NAT holds ((seq_id (a * v)) rto_power p) . n >= 0

proof

let n be Element of NAT ; :: thesis: ((seq_id (a * v)) rto_power p) . n >= 0
A62: (a (#) (seq_id v)) . n = a * ((seq_id v) . n) by SEQ_1:13;
set b = a (#) (seq_id v);
((a (#) (seq_id v)) rto_power p) . n = (abs (a * ((seq_id v) . n))) to_power p by A62, Def1;
hence ((seq_id (a * v)) rto_power p) . n >= 0 by A1, A44, Lm1, COMPLEX1:132; :: thesis: verum

end;

Partial_Sums ((seq_id (a * v)) rto_power p) is bounded_above by A59, SEQ_2:def 1;
hence (seq_id (a * v)) rto_power p is summable by A61, SERIES_1:20; :: 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