let r, x0 be Real; :: thesis: for f being PartFunc of REAL,REAL st f is_convergent_in x0 holds
( r (#) f is_convergent_in x0 & lim ((r (#) f),x0) = r * (lim (f,x0)) )
let f be PartFunc of REAL,REAL; :: thesis: ( f is_convergent_in x0 implies ( r (#) f is_convergent_in x0 & lim ((r (#) f),x0) = r * (lim (f,x0)) ) )
assume A1: f is_convergent_in x0 ; :: thesis: ( r (#) f is_convergent_in x0 & lim ((r (#) f),x0) = r * (lim (f,x0)) )

A2: now :: thesis: for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom (r (#) f)) \ {x0} holds
( (r (#) f) /* seq is convergent & lim ((r (#) f) /* seq) = r * (lim (f,x0)) )

let seq be Real_Sequence; :: thesis: ( seq is convergent & lim seq = x0 & rng seq c= (dom (r (#) f)) \ {x0} implies ( (r (#) f) /* seq is convergent & lim ((r (#) f) /* seq) = r * (lim (f,x0)) ) )
assume that
A3: seq is convergent and
A4: lim seq = x0 and
A5: rng seq c= (dom (r (#) f)) \ {x0} ; :: thesis: ( (r (#) f) /* seq is convergent & lim ((r (#) f) /* seq) = r * (lim (f,x0)) )
A6: rng seq c= (dom f) \ {x0} by A5, VALUED_1:def 5;
then A7: r (#) (f /* seq) = (r (#) f) /* seq by RFUNCT_2:9, XBOOLE_1:1;
A8: f /* seq is convergent by A1, A3, A4, A6;
then r (#) (f /* seq) is convergent by SEQ_2:7;
hence (r (#) f) /* seq is convergent by A6, RFUNCT_2:9, XBOOLE_1:1; :: thesis: lim ((r (#) f) /* seq) = r * (lim (f,x0))
lim (f /* seq) = lim (f,x0) by A1, A3, A4, A6, Def4;
hence lim ((r (#) f) /* seq) = r * (lim (f,x0)) by A8, A7, SEQ_2:8; :: thesis: verum

end;

now :: thesis: for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (r (#) f) & g2 < r2 & x0 < g2 & g2 in dom (r (#) f) )

let r1, r2 be Real; :: thesis: ( r1 < x0 & x0 < r2 implies ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (r (#) f) & g2 < r2 & x0 < g2 & g2 in dom (r (#) f) ) )
assume that
A9: r1 < x0 and
A10: x0 < r2 ; :: thesis: ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (r (#) f) & g2 < r2 & x0 < g2 & g2 in dom (r (#) f) )
consider g1, g2 being Real such that
A11: r1 < g1 and
A12: g1 < x0 and
A13: g1 in dom f and
A14: g2 < r2 and
A15: x0 < g2 and
A16: g2 in dom f by A1, A9, A10;
take g1 = g1; :: thesis: ex g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (r (#) f) & g2 < r2 & x0 < g2 & g2 in dom (r (#) f) )
take g2 = g2; :: thesis: ( r1 < g1 & g1 < x0 & g1 in dom (r (#) f) & g2 < r2 & x0 < g2 & g2 in dom (r (#) f) )
thus ( r1 < g1 & g1 < x0 & g1 in dom (r (#) f) & g2 < r2 & x0 < g2 & g2 in dom (r (#) f) ) by A11, A12, A13, A14, A15, A16, VALUED_1:def 5; :: thesis: verum

end;

hence r (#) f is_convergent_in x0 by A2; :: thesis: lim ((r (#) f),x0) = r * (lim (f,x0))
hence lim ((r (#) f),x0) = r * (lim (f,x0)) by A2, Def4; :: thesis: verum