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;
A5: b1 in the_set_of_RealSequences by RSSPACE:def 1;
A6: seq_id a1 = a by A4, RSSPACE:def 2;
A7: seq_id b1 = b by A5, RSSPACE:def 2;
A8: a1 in the_set_of_RealSequences_l^ p by A1, A2, A4, A6, Def2;
A9: b1 in the_set_of_RealSequences_l^ p by A1, A3, A5, A7, Def2;
reconsider a1 = a1 as VECTOR of Linear_Space_of_RealSequences by A8;
reconsider b1 = b1 as VECTOR of Linear_Space_of_RealSequences by A9;
the_set_of_RealSequences_l^ p is linearly-closed by A1, Th4;
then A10: a1 + b1 in the_set_of_RealSequences_l^ p by A8, A9, RLSUB_1:def 1;
seq_id (a1 + b1) = seq_id ((seq_id a1) + (seq_id b1)) by RSSPACE:4, RSSPACE:def 7
.= a + b by A6, A7, RSSPACE:3 ;
hence (a + b) rto_power p is summable by A1, A10, Def2; :: thesis: verum