let r be real number ; :: 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 by Def2;
then r (#) (Partial_Sums s) is convergent by SEQ_2:21;
then Partial_Sums (r (#) s) is convergent by Th12;
hence r (#) s is summable by Def2; :: thesis: Sum (r (#) s) = r * (Sum s)
thus Sum (r (#) s) = lim (r (#) (Partial_Sums s)) by Th12
.= r * (Sum s) by A1, SEQ_2:22 ; :: thesis: verum