let f be PartFunc of REAL,REAL; :: thesis:
let r be Real; :: thesis:
assume A1: f is convergent_in-infty ; :: thesis:

A2: now :: thesis:

let seq be Real_Sequence; :: thesis:
assume that
A3: seq is divergent_to-infty and
A4: rng seq c= dom (r (#) f) ; :: thesis:
A5: rng seq c= dom f by A4, VALUED_1:def 5;
then A6: lim (f /* seq) = lim_in-infty f by A1, A3, Def13;
A7: f /* seq is convergent by A1, A3, A5;
then r (#) (f /* seq) is convergent ;
hence (r (#) f) /* seq is convergent by A5, RFUNCT_2:9; :: thesis:
thus lim ((r (#) f) /* seq) = lim (r (#) (f /* seq)) by A5, RFUNCT_2:9
.= r * (lim_in-infty f) by A7, A6, SEQ_2:8 ; :: thesis:

end;

for r1 being Real ex g being Real st
( g < r1 & g in dom (r (#) f) )

let r1 be Real; :: thesis:
consider g being Real such that
A8: ( g < r1 & g in dom f ) by A1;
take g ; :: thesis:
thus ( g < r1 & g in dom (r (#) f) ) by A8, VALUED_1:def 5; :: thesis:

end;

hence r (#) f is convergent_in-infty by A2; :: thesis:
hence lim_in-infty (r (#) f) = r * (lim_in-infty f) by A2, Def13; :: thesis: