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

( 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