let x0 be real number ; :: thesis: for f being PartFunc of REAL ,REAL st x0 in dom f & f is_continuous_in x0 holds
( abs f is_continuous_in x0 & - f is_continuous_in x0 )
let f be PartFunc of REAL ,REAL ; :: thesis: ( x0 in dom f & f is_continuous_in x0 implies ( abs f is_continuous_in x0 & - f is_continuous_in x0 ) )
assume Z: x0 in dom f ; :: thesis: ( not f is_continuous_in x0 or ( abs f is_continuous_in x0 & - f is_continuous_in x0 ) )
assume A1: f is_continuous_in x0 ; :: thesis: ( abs f is_continuous_in x0 & - f is_continuous_in x0 )

now

let s1 be Real_Sequence; :: thesis: ( rng s1 c= dom (abs f) & s1 is convergent & lim s1 = x0 implies ( (abs f) /* s1 is convergent & (abs f) . x0 = lim ((abs f) /* s1) ) )
assume A3: ( rng s1 c= dom (abs f) & s1 is convergent & lim s1 = x0 ) ; :: thesis: ( (abs f) /* s1 is convergent & (abs f) . x0 = lim ((abs f) /* s1) )
then A4: rng s1 c= dom f by VALUED_1:def 11;
then A5: ( f /* s1 is convergent & f . x0 = lim (f /* s1) ) by A1, A3, Def1;
then abs (f /* s1) is convergent by SEQ_4:26;
hence (abs f) /* s1 is convergent by A4, RFUNCT_2:25; :: thesis: (abs f) . x0 = lim ((abs f) /* s1)
thus (abs f) . x0 = abs (f . x0) by VALUED_1:18
.= lim (abs (f /* s1)) by A5, SEQ_4:27
.= lim ((abs f) /* s1) by A4, RFUNCT_2:25 ; :: thesis: verum

end;

hence abs f is_continuous_in x0 by Def1; :: thesis: - f is_continuous_in x0
thus - f is_continuous_in x0 by A1, Th8, Z; :: thesis: verum