let f be PartFunc of REAL ,REAL ; :: thesis: for r being Real st f is convergent_in+infty holds
( r (#) f is convergent_in+infty & lim_in+infty (r (#) f) = r * (lim_in+infty f) )
let r be Real; :: thesis: ( f is convergent_in+infty implies ( r (#) f is convergent_in+infty & lim_in+infty (r (#) f) = r * (lim_in+infty f) ) )
assume A1: f is convergent_in+infty ; :: thesis: ( r (#) f is convergent_in+infty & lim_in+infty (r (#) f) = r * (lim_in+infty f) )

A2: now

let seq be Real_Sequence; :: thesis: ( seq is divergent_to+infty & rng seq c= dom (r (#) f) implies ( (r (#) f) /* seq is convergent & lim ((r (#) f) /* seq) = r * (lim_in+infty f) ) )
assume that
A3: seq is divergent_to+infty and
A4: rng seq c= dom (r (#) f) ; :: thesis: ( (r (#) f) /* seq is convergent & lim ((r (#) f) /* seq) = r * (lim_in+infty f) )
A5: rng seq c= dom f by A4, VALUED_1:def 5;
then A6: lim (f /* seq) = lim_in+infty f by A1, A3, Def12;
lim_in+infty f = lim_in+infty f ;
then A7: f /* seq is convergent by A1, A3, A5, Def12;
then r (#) (f /* seq) is convergent by SEQ_2:21;
hence (r (#) f) /* seq is convergent by A5, RFUNCT_2:24; :: thesis: lim ((r (#) f) /* seq) = r * (lim_in+infty f)
thus lim ((r (#) f) /* seq) = lim (r (#) (f /* seq)) by A5, RFUNCT_2:24
.= r * (lim_in+infty f) by A7, A6, SEQ_2:22 ; :: thesis: verum

end;

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

proof

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

end;

hence r (#) f is convergent_in+infty by A2, Def6; :: thesis: lim_in+infty (r (#) f) = r * (lim_in+infty f)
hence lim_in+infty (r (#) f) = r * (lim_in+infty f) by A2, Def12; :: thesis: verum