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
reconsider vq = v as Real_Sequence by FUNCT_2:66;
set up = (seq_id u) rto_power p;
set vp = (seq_id v) rto_power p;
set p1 = 1 / p;
A7: now :: thesis: for n being Nat holds
( ((seq_id v) rto_power p) . n = |.((seq_id v) . n).| to_power p & ((seq_id u) rto_power p) . n = |.((seq_id u) . n).| to_power p & 0 <= |.((seq_id v) . n).| & ( 0 < |.((seq_id v) . n).| or 0 = |.((seq_id v) . n).| ) & 0 <= ((seq_id v) rto_power p) . n & 0 <= |.((seq_id u) . n).| & ( 0 < |.((seq_id u) . n).| or 0 = |.((seq_id u) . n).| ) & 0 <= ((seq_id u) rto_power p) . n )
let n be Nat; :: thesis: ( ((seq_id v) rto_power p) . n = |.((seq_id v) . n).| to_power p & ((seq_id u) rto_power p) . n = |.((seq_id u) . n).| to_power p & 0 <= |.((seq_id v) . n).| & ( 0 < |.((seq_id v) . n).| or 0 = |.((seq_id v) . n).| ) & 0 <= ((seq_id v) rto_power p) . n & 0 <= |.((seq_id u) . n).| & ( 0 < |.((seq_id u) . n).| or 0 = |.((seq_id u) . n).| ) & 0 <= ((seq_id u) rto_power p) . n )
thus A8: ((seq_id v) rto_power p) . n = |.((seq_id v) . n).| to_power p by Def1; :: thesis: ( ((seq_id u) rto_power p) . n = |.((seq_id u) . n).| to_power p & 0 <= |.((seq_id v) . n).| & ( 0 < |.((seq_id v) . n).| or 0 = |.((seq_id v) . n).| ) & 0 <= ((seq_id v) rto_power p) . n & 0 <= |.((seq_id u) . n).| & ( 0 < |.((seq_id u) . n).| or 0 = |.((seq_id u) . n).| ) & 0 <= ((seq_id u) rto_power p) . n )
thus A9: ((seq_id u) rto_power p) . n = |.((seq_id u) . n).| to_power p by Def1; :: thesis: ( 0 <= |.((seq_id v) . n).| & ( 0 < |.((seq_id v) . n).| or 0 = |.((seq_id v) . n).| ) & 0 <= ((seq_id v) rto_power p) . n & 0 <= |.((seq_id u) . n).| & ( 0 < |.((seq_id u) . n).| or 0 = |.((seq_id u) . n).| ) & 0 <= ((seq_id u) rto_power p) . n )
thus 0 <= |.((seq_id v) . n).| by COMPLEX1:46; :: thesis: ( ( 0 < |.((seq_id v) . n).| or 0 = |.((seq_id v) . n).| ) & 0 <= ((seq_id v) rto_power p) . n & 0 <= |.((seq_id u) . n).| & ( 0 < |.((seq_id u) . n).| or 0 = |.((seq_id u) . n).| ) & 0 <= ((seq_id u) rto_power p) . n )
thus ( 0 < |.((seq_id v) . n).| or 0 = |.((seq_id v) . n).| ) by COMPLEX1:46; :: thesis: ( 0 <= ((seq_id v) rto_power p) . n & 0 <= |.((seq_id u) . n).| & ( 0 < |.((seq_id u) . n).| or 0 = |.((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 <= |.((seq_id u) . n).| & ( 0 < |.((seq_id u) . n).| or 0 = |.((seq_id u) . n).| ) & 0 <= ((seq_id u) rto_power p) . n )
thus 0 <= |.((seq_id u) . n).| by COMPLEX1:46; :: thesis: ( ( 0 < |.((seq_id u) . n).| or 0 = |.((seq_id u) . n).| ) & 0 <= ((seq_id u) rto_power p) . n )
thus ( 0 < |.((seq_id u) . n).| or 0 = |.((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 such that
A10: for n being object 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 ;
A12: Partial_Sums ((seq_id v) rto_power p) is V45() 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 Nat by A13;
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 ;
reconsider uq = u as Real_Sequence by FUNCT_2:66;
A17: (seq_id v) + (seq_id u) = seq_id (v + u) by RSSPACE:2;
(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 such that
A18: for n being object 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 ;
A19: Partial_Sums ((seq_id u) rto_power p) is V45() 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 Nat by A20;
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 ;
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 Nat holds
( ( for n being Nat holds
( ( 0 < |.((vq + uq) . n).| or 0 = |.((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 Nat; :: thesis: ( ( for n being Nat holds
( ( 0 < |.((vq + uq) . n).| or 0 = |.((vq + uq) . n).| ) & 0 <= ((vq + uq) rto_power p) . n ) ) & (Partial_Sums ((vq + uq) rto_power p)) . n < (q + q1) to_power p )
A25: n in NAT by ORDINAL1:def 12;
A26: 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 A27: ((Partial_Sums ((seq_id u) rto_power p)) . n) to_power (1 / p) < q1 by A22, A25;
NAT = dom (Partial_Sums ((seq_id v) rto_power p)) by SEQ_1:2;
then A28: (((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, A27, XREAL_1:8, A25;
((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, Th2;
then A29: ((Partial_Sums ((vq + uq) rto_power p)) . n) to_power (1 / p) < q + q1 by A28, XXREAL_0:2;
A30: 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 A31: (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, A31, POWER:def 2 ;
:: thesis: verum
end;
hereby :: thesis: (Partial_Sums ((vq + uq) rto_power p)) . n < (q + q1) to_power p
let n be Nat; :: thesis: ( ( 0 < |.((vq + uq) . n).| or 0 = |.((vq + uq) . n).| ) & 0 <= ((vq + uq) rto_power p) . n )
thus A33: ( 0 < |.((vq + uq) . n).| or 0 = |.((vq + uq) . n).| ) by COMPLEX1:46; :: thesis: 0 <= ((vq + uq) rto_power p) . n
((vq + uq) rto_power p) . n = |.((vq + uq) . n).| to_power p by Def1;
hence 0 <= ((vq + uq) rto_power p) . n by A1, A33, POWER:34, POWER:def 2; :: thesis: verum
end;
then A34: 0 <= ((vq + uq) rto_power p) . 0 ;
A35: (Partial_Sums ((vq + uq) rto_power p)) . 0 <= (Partial_Sums ((vq + uq) rto_power p)) . n by A32, SEQM_3:11, SERIES_1:16;
then 0 <= (Partial_Sums ((vq + uq) rto_power p)) . n by A34, 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, A29, A26, A30, A35, A34, Th1, SERIES_1:def 1; :: thesis: verum
end;
then for n being Nat holds
( Partial_Sums ((vq + uq) rto_power p) is bounded_above & 0 <= ((vq + uq) rto_power p) . n ) by SEQ_2:def 3;
hence (seq_id (v + u)) rto_power p is summable by A17, SERIES_1:17; :: thesis: verum
end;
thus 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 A37: 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;
A38: now :: thesis: for n being Nat holds
( 0 <= |.((seq_id v) . n).| & ( 0 < |.((seq_id v) . n).| or 0 = |.((seq_id v) . n).| ) & 0 <= ((seq_id v) rto_power p) . n )
let n be Nat; :: thesis: ( 0 <= |.((seq_id v) . n).| & ( 0 < |.((seq_id v) . n).| or 0 = |.((seq_id v) . n).| ) & 0 <= ((seq_id v) rto_power p) . n )
thus 0 <= |.((seq_id v) . n).| by COMPLEX1:46; :: thesis: ( ( 0 < |.((seq_id v) . n).| or 0 = |.((seq_id v) . n).| ) & 0 <= ((seq_id v) rto_power p) . n )
thus A39: ( 0 < |.((seq_id v) . n).| or 0 = |.((seq_id v) . n).| ) by COMPLEX1:46; :: thesis: 0 <= ((seq_id v) rto_power p) . n
((seq_id v) rto_power p) . n = |.((seq_id v) . n).| to_power p by Def1;
hence 0 <= ((seq_id v) rto_power p) . n by A1, A39, POWER:34, POWER:def 2; :: thesis: verum
end;
(seq_id v) rto_power p is summable by A1, A37, Def2;
then Partial_Sums ((seq_id v) rto_power p) is bounded_above by A38, SERIES_1:17;
then consider r being Real such that
A40: for n being object 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;
A41: seq_id (a * v) = a (#) (seq_id v) by RSSPACE:3;
A42: for n being Nat holds (Partial_Sums ((seq_id (a * v)) rto_power p)) . n = (|.a.| to_power p) * ((Partial_Sums ((seq_id v) rto_power p)) . n)
proof
let n be Nat; :: thesis: (Partial_Sums ((seq_id (a * v)) rto_power p)) . n = (|.a.| to_power p) * ((Partial_Sums ((seq_id v) rto_power p)) . n)
now :: thesis: for n being Nat holds ((seq_id (a * v)) rto_power p) . n = ((|.a.| to_power p) (#) ((seq_id v) rto_power p)) . n
let n be Nat; :: thesis: ((seq_id (a * v)) rto_power p) . n = ((|.a.| to_power p) (#) ((seq_id v) rto_power p)) . n
A43: |.a.| >= 0 by COMPLEX1:46;
A44: |.((seq_id v) . n).| >= 0 by COMPLEX1:46;
A45: (a (#) (seq_id v)) . n = a * ((seq_id v) . n) by SEQ_1:9;
((a (#) (seq_id v)) rto_power p) . n = |.((a (#) (seq_id v)) . n).| to_power p by Def1
.= (|.a.| * |.((seq_id v) . n).|) to_power p by A45, COMPLEX1:65
.= (|.a.| to_power p) * (|.((seq_id v) . n).| to_power p) by A1, A43, A44, Lm2 ;
hence ((seq_id (a * v)) rto_power p) . n = (|.a.| to_power p) * (((seq_id v) rto_power p) . n) by A41, Def1
.= ((|.a.| to_power p) (#) ((seq_id v) rto_power p)) . n by SEQ_1:9 ;
:: thesis: verum
end;
then for n being object st n in NAT holds
((seq_id (a * v)) rto_power p) . n = ((|.a.| to_power p) (#) ((seq_id v) rto_power p)) . n ;
then A46: (seq_id (a * v)) rto_power p = (|.a.| to_power p) (#) ((seq_id v) rto_power p) by FUNCT_2:12;
Partial_Sums ((|.a.| to_power p) (#) ((seq_id v) rto_power p)) = (|.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 = (|.a.| to_power p) * ((Partial_Sums ((seq_id v) rto_power p)) . n) by A46, SEQ_1:9; :: thesis: verum
end;
A47: ( 0 < |.a.| to_power p or 0 = |.a.| to_power p ) by A1, Lm1, COMPLEX1:46;
A48: 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)) & ( (|.a.| to_power p) * ((Partial_Sums ((seq_id v) rto_power p)) . n) < (|.a.| to_power p) * r or (|.a.| to_power p) * ((Partial_Sums ((seq_id v) rto_power p)) . n) = (|.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)) & ( (|.a.| to_power p) * ((Partial_Sums ((seq_id v) rto_power p)) . n) < (|.a.| to_power p) * r or (|.a.| to_power p) * ((Partial_Sums ((seq_id v) rto_power p)) . n) = (|.a.| to_power p) * r ) ) )
assume A49: n in dom (Partial_Sums ((seq_id v) rto_power p)) ; :: thesis: ( n in dom (Partial_Sums ((seq_id (a * v)) rto_power p)) & ( (|.a.| to_power p) * ((Partial_Sums ((seq_id v) rto_power p)) . n) < (|.a.| to_power p) * r or (|.a.| to_power p) * ((Partial_Sums ((seq_id v) rto_power p)) . n) = (|.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 A49, SEQ_1:1; :: thesis: ( (|.a.| to_power p) * ((Partial_Sums ((seq_id v) rto_power p)) . n) < (|.a.| to_power p) * r or (|.a.| to_power p) * ((Partial_Sums ((seq_id v) rto_power p)) . n) = (|.a.| to_power p) * r )
thus ( (|.a.| to_power p) * ((Partial_Sums ((seq_id v) rto_power p)) . n) < (|.a.| to_power p) * r or (|.a.| to_power p) * ((Partial_Sums ((seq_id v) rto_power p)) . n) = (|.a.| to_power p) * r ) by A40, A47, A49, XREAL_1:68; :: thesis: verum
end;
A50: 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 < (|.a.| to_power p) * r or (Partial_Sums ((seq_id (a * v)) rto_power p)) . n = (|.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 < (|.a.| to_power p) * r or (Partial_Sums ((seq_id (a * v)) rto_power p)) . n = (|.a.| to_power p) * r )
assume A51: n in dom (Partial_Sums ((seq_id (a * v)) rto_power p)) ; :: thesis: ( (Partial_Sums ((seq_id (a * v)) rto_power p)) . n < (|.a.| to_power p) * r or (Partial_Sums ((seq_id (a * v)) rto_power p)) . n = (|.a.| to_power p) * r )
reconsider n1 = n as Nat by A51;
n in NAT by A51, SEQ_1:1;
then n in dom (Partial_Sums ((seq_id v) rto_power p)) by SEQ_1:1;
then ( (|.a.| to_power p) * ((Partial_Sums ((seq_id v) rto_power p)) . n) < (|.a.| to_power p) * r or (|.a.| to_power p) * ((Partial_Sums ((seq_id v) rto_power p)) . n) = (|.a.| to_power p) * r ) by A48;
then ( (Partial_Sums ((seq_id (a * v)) rto_power p)) . n1 < (|.a.| to_power p) * r or (Partial_Sums ((seq_id (a * v)) rto_power p)) . n1 = (|.a.| to_power p) * r ) by A42;
hence ( (Partial_Sums ((seq_id (a * v)) rto_power p)) . n < (|.a.| to_power p) * r or (Partial_Sums ((seq_id (a * v)) rto_power p)) . n = (|.a.| to_power p) * r ) ; :: thesis: verum
end;
ex r1 being Real st
for n being object 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 = ((|.a.| to_power p) * r) + 1; :: thesis: for n being object 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 ;
for n being object 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
A52: (|.a.| to_power p) * r < ((|.a.| to_power p) * r) + 1 by XREAL_1:29;
let n be object ; :: 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 A50, A52, XXREAL_0:2; :: thesis: verum
end;
hence for n being object 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 A53: Partial_Sums ((seq_id (a * v)) rto_power p) is bounded_above by SEQ_2:def 1;
for n being Nat holds ((seq_id (a * v)) rto_power p) . n >= 0
proof
set b = a (#) (seq_id v);
let n be 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 = |.(a * ((seq_id v) . n)).| to_power p by Def1;
hence ((seq_id (a * v)) rto_power p) . n >= 0 by A1, A41, Lm1, COMPLEX1:46; :: thesis: verum
end;
hence (seq_id (a * v)) rto_power p is summable by A53, SERIES_1:17; :: thesis: verum
end;
hence a * v in the_set_of_RealSequences_l^ p by A1, Def2; :: thesis: verum
end;
hence the_set_of_RealSequences_l^ p is linearly-closed by A2, RLSUB_1:def 1; :: thesis: verum