let X be set ; :: thesis: for f being PartFunc of REAL ,REAL st X c= dom f & f | X is continuous holds
( (abs f) | X is continuous & (- f) | X is continuous )
let f be PartFunc of REAL ,REAL ; :: thesis: ( X c= dom f & f | X is continuous implies ( (abs f) | X is continuous & (- f) | X is continuous ) )
assume Z: X c= dom f ; :: thesis: ( not f | X is continuous or ( (abs f) | X is continuous & (- f) | X is continuous ) )
assume A1: f | X is continuous ; :: thesis: ( (abs f) | X is continuous & (- f) | X is continuous )
thus (abs f) | X is continuous :: thesis: (- f) | X is continuous

proof

let r be real number ; :: according to FCONT_1:def 2 :: thesis: ( r in dom ((abs f) | X) implies (abs f) | X is_continuous_in r )
assume A3: r in dom ((abs f) | X) ; :: thesis: (abs f) | X is_continuous_in r
then ( r in dom (abs f) & r in X ) by RELAT_1:86;
then ( r in dom f & r in X ) by VALUED_1:def 11;
then B3: r in dom (f | X) by RELAT_1:86;
then A4: f | X is_continuous_in r by A1, Def2;
thus (abs f) | X is_continuous_in r :: thesis: verum

proof

let s1 be Real_Sequence; :: according to FCONT_1:def 1 :: thesis: ( rng s1 c= dom ((abs f) | X) & s1 is convergent & lim s1 = r implies ( ((abs f) | X) /* s1 is convergent & ((abs f) | X) . r = lim (((abs f) | X) /* s1) ) )
assume A6: ( rng s1 c= dom ((abs f) | X) & s1 is convergent & lim s1 = r ) ; :: thesis: ( ((abs f) | X) /* s1 is convergent & ((abs f) | X) . r = lim (((abs f) | X) /* s1) )
then rng s1 c= (dom (abs f)) /\ X by RELAT_1:90;
then rng s1 c= (dom f) /\ X by VALUED_1:def 11;
then A7: rng s1 c= dom (f | X) by RELAT_1:90;
then A8: ( (f | X) /* s1 is convergent & (f | X) . r = lim ((f | X) /* s1) ) by A4, A6, Def1;

now

let n be Element of NAT ; :: thesis: (abs ((f | X) /* s1)) . n = (((abs f) | X) /* s1) . n
A9: s1 . n in rng s1 by VALUED_0:28;
then s1 . n in dom (f | X) by A7;
then s1 . n in (dom f) /\ X by RELAT_1:90;
then A10: ( s1 . n in dom f & s1 . n in X ) by XBOOLE_0:def 4;
thus (abs ((f | X) /* s1)) . n = abs (((f | X) /* s1) . n) by SEQ_1:16
.= abs ((f | X) . (s1 . n)) by A7, FUNCT_2:185
.= abs (f . (s1 . n)) by A7, A9, FUNCT_1:70
.= (abs f) . (s1 . n) by VALUED_1:18
.= ((abs f) | X) . (s1 . n) by A10, FUNCT_1:72
.= (((abs f) | X) /* s1) . n by A6, FUNCT_2:185 ; :: thesis: verum

end;

then A11: abs ((f | X) /* s1) = ((abs f) | X) /* s1 by FUNCT_2:113;
hence ((abs f) | X) /* s1 is convergent by A8, SEQ_4:26; :: thesis: ((abs f) | X) . r = lim (((abs f) | X) /* s1)
abs ((f | X) . r) = abs (f . r) by B3, FUNCT_1:70
.= (abs f) . r by VALUED_1:18
.= ((abs f) | X) . r by A3, FUNCT_1:70 ;
hence ((abs f) | X) . r = lim (((abs f) | X) /* s1) by A8, A11, SEQ_4:27; :: thesis: verum

end;

end;

thus (- f) | X is continuous by A1, Th21, Z; :: thesis: verum