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 FUNCT_2:8;
seq_id a1 = a ;
then A6: a1 in the_set_of_RealSequences_l^ p by A1, A2, A4, Def2;
A7: b1 in the_set_of_RealSequences by FUNCT_2:8;
seq_id b1 = b ;
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
.= a + b ;
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