let r be Real; :: thesis: for s being Real_Sequence st s is summable holds
( r (#) s is summable & Sum (r (#) s) = r * (Sum s) )
let s be Real_Sequence; :: thesis: ( s is summable implies ( r (#) s is summable & Sum (r (#) s) = r * (Sum s) ) )
assume s is summable ; :: thesis: ( r (#) s is summable & Sum (r (#) s) = r * (Sum s) )
then A1: Partial_Sums s is convergent ;
then r (#) (Partial_Sums s) is convergent ;
then Partial_Sums (r (#) s) is convergent by Th9;
hence r (#) s is summable ; :: thesis: Sum (r (#) s) = r * (Sum s)
thus Sum (r (#) s) = lim (r (#) (Partial_Sums s)) by Th9
.= r * (Sum s) by A1, SEQ_2:8 ; :: thesis: verum