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

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 V41() by A7, SERIES_1:16;

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 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 V41() by A7, SERIES_1:16;

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

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

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

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

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

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

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