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

( (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

thus
(- f) | X is continuous
by A1, A2, Th20; :: thesis: verum
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

end;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;

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;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

then A12:
abs ((f | X) /* s1) = ((abs f) | X) /* s1
by FUNCT_2:63;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;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

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