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