let x0 be Real; :: thesis: for f being PartFunc of REAL,REAL st f is_right_convergent_in x0 holds
( abs f is_right_convergent_in x0 & lim_right ((abs f),x0) = |.(lim_right (f,x0)).| )
let f be PartFunc of REAL,REAL; :: thesis: ( f is_right_convergent_in x0 implies ( abs f is_right_convergent_in x0 & lim_right ((abs f),x0) = |.(lim_right (f,x0)).| ) )
assume A1: f is_right_convergent_in x0 ; :: thesis: ( abs f is_right_convergent_in x0 & lim_right ((abs f),x0) = |.(lim_right (f,x0)).| )

A2: now :: thesis: for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom (abs f)) /\ (right_open_halfline x0) holds
( (abs f) /* seq is convergent & lim ((abs f) /* seq) = |.(lim_right (f,x0)).| )

let seq be Real_Sequence; :: thesis: ( seq is convergent & lim seq = x0 & rng seq c= (dom (abs f)) /\ (right_open_halfline x0) implies ( (abs f) /* seq is convergent & lim ((abs f) /* seq) = |.(lim_right (f,x0)).| ) )
assume that
A3: seq is convergent and
A4: lim seq = x0 and
A5: rng seq c= (dom (abs f)) /\ (right_open_halfline x0) ; :: thesis: ( (abs f) /* seq is convergent & lim ((abs f) /* seq) = |.(lim_right (f,x0)).| )
A6: rng seq c= (dom f) /\ (right_open_halfline x0) by A5, VALUED_1:def 11;
(dom f) /\ (right_open_halfline x0) c= dom f by XBOOLE_1:17;
then rng seq c= dom f by A6, XBOOLE_1:1;
then A7: abs (f /* seq) = (abs f) /* seq by RFUNCT_2:10;
A8: f /* seq is convergent by A1, A3, A4, A6;
hence (abs f) /* seq is convergent by A7; :: thesis: lim ((abs f) /* seq) = |.(lim_right (f,x0)).|
lim (f /* seq) = lim_right (f,x0) by A1, A3, A4, A6, Def8;
hence lim ((abs f) /* seq) = |.(lim_right (f,x0)).| by A8, A7, SEQ_4:14; :: thesis: verum

end;

now :: thesis: for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom (abs f) )

let r be Real; :: thesis: ( x0 < r implies ex g being Real st
( g < r & x0 < g & g in dom (abs f) ) )
assume x0 < r ; :: thesis: ex g being Real st
( g < r & x0 < g & g in dom (abs f) )
then consider g being Real such that
A9: g < r and
A10: x0 < g and
A11: g in dom f by A1;
take g = g; :: thesis: ( g < r & x0 < g & g in dom (abs f) )
thus ( g < r & x0 < g & g in dom (abs f) ) by A9, A10, A11, VALUED_1:def 11; :: thesis: verum

end;

hence abs f is_right_convergent_in x0 by A2; :: thesis: lim_right ((abs f),x0) = |.(lim_right (f,x0)).|
hence lim_right ((abs f),x0) = |.(lim_right (f,x0)).| by A2, Def8; :: thesis: verum