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 A1: X c= dom f ; :: thesis: ( not f | X is continuous or ( (abs f) | X is continuous & (- f) | X is continuous ) )
assume A2: 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; :: 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) by RELAT_1:57;
then A4: r in dom f by VALUED_1:def 11;
r in X by A3;
then A5: r in dom (f | X) by A4, RELAT_1:57;
then A6: f | X is_continuous_in r by A2;
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 that
A7: rng s1 c= dom ((abs f) | X) and
A8: ( s1 is convergent & lim s1 = r ) ; :: thesis: ( ((abs f) | X) /* s1 is convergent & ((abs f) | X) . r = lim (((abs f) | X) /* s1) )
rng s1 c= (dom (abs f)) /\ X by A7, RELAT_1:61;
then rng s1 c= (dom f) /\ X by VALUED_1:def 11;
then A9: rng s1 c= dom (f | X) by RELAT_1:61;

now :: thesis: for n being Element of NAT holds (abs ((f | X) /* s1)) . n = (((abs f) | X) /* s1) . n

let n be Element of NAT ; :: thesis: (abs ((f | X) /* s1)) . n = (((abs f) | X) /* s1) . n
A10: s1 . n in rng s1 by VALUED_0:28;
then s1 . n in dom (f | X) by A9;
then s1 . n in (dom f) /\ X by RELAT_1:61;
then A11: s1 . n in X by XBOOLE_0:def 4;
thus (abs ((f | X) /* s1)) . n = |.(((f | X) /* s1) . n).| by SEQ_1:12
.= |.((f | X) . (s1 . n)).| by A9, FUNCT_2:108
.= |.(f . (s1 . n)).| by A9, A10, FUNCT_1:47
.= (abs f) . (s1 . n) by VALUED_1:18
.= ((abs f) | X) . (s1 . n) by A11, FUNCT_1:49
.= (((abs f) | X) /* s1) . n by A7, FUNCT_2:108 ; :: thesis: verum

end;

then A12: abs ((f | X) /* s1) = ((abs f) | X) /* s1 by FUNCT_2:63;
A13: |.((f | X) . r).| = |.(f . r).| by A5, FUNCT_1:47
.= (abs f) . r by VALUED_1:18
.= ((abs f) | X) . r by A3, FUNCT_1:47 ;
A14: (f | X) /* s1 is convergent by A6, A8, A9;
hence ((abs f) | X) /* s1 is convergent by A12, SEQ_4:13; :: thesis: ((abs f) | X) . r = lim (((abs f) | X) /* s1)
(f | X) . r = lim ((f | X) /* s1) by A6, A8, A9;
hence ((abs f) | X) . r = lim (((abs f) | X) /* s1) by A14, A12, A13, SEQ_4:14; :: thesis: verum

end;

end;

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