let x0, r be Real; :: thesis:
let f be PartFunc of REAL , REAL ; :: thesis:
assume A1: f is_convergent_in x0 ; :: thesis:

A2: now

let r1, r2 be Real; :: thesis:
assume ( r1 < x0 & x0 < r2 ) ; :: thesis:
then consider g1, g2 being Real such that
A3: ( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) by A1, Def1;
take g1 = g1; :: thesis:
take g2 = g2; :: thesis:
thus ( r1 < g1 & g1 < x0 & g1 in dom (r (#) f) & g2 < r2 & x0 < g2 & g2 in dom (r (#) f) ) by A3, VALUED_1:def 5; :: thesis:

end;

A4: now

let seq be Real_Sequence; :: thesis:
A5: lim f,x0 = lim f,x0 ;
assume A6: ( seq is convergent & lim seq = x0 & rng seq c= (dom (r (#) f)) \ {x0} ) ; :: thesis:
then A7: rng seq c= (dom f) \ {x0} by VALUED_1:def 5;
then A8: ( f /* seq is convergent & lim (f /* seq) = lim f,x0 ) by A1, A5, A6, Def4;
then A9: r (#) (f /* seq) is convergent by SEQ_2:21;
A10: r (#) (f /* seq) = (r (#) f) /* seq by A7, RFUNCT_2:24, XBOOLE_1:1;
thus (r (#) f) /* seq is convergent by A7, A9, RFUNCT_2:24, XBOOLE_1:1; :: thesis:
thus lim ((r (#) f) /* seq) = r * (lim f,x0) by A8, A10, SEQ_2:22; :: thesis:

end;

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