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

(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