let x0 be Real; :: 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 A1: x0 in dom f ; :: thesis: ( not f is_continuous_in x0 or ( abs f is_continuous_in x0 & - f is_continuous_in x0 ) )

assume A2: f is_continuous_in x0 ; :: thesis: ( abs f is_continuous_in x0 & - f is_continuous_in x0 )

thus - f is_continuous_in x0 by A1, A2, Th8; :: thesis: verum

( 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 A1: x0 in dom f ; :: thesis: ( not f is_continuous_in x0 or ( abs f is_continuous_in x0 & - f is_continuous_in x0 ) )

assume A2: f is_continuous_in x0 ; :: thesis: ( abs f is_continuous_in x0 & - f is_continuous_in x0 )

now :: thesis: for s1 being Real_Sequence st rng s1 c= dom (abs f) & s1 is convergent & lim s1 = x0 holds

( (abs f) /* s1 is convergent & (abs f) . x0 = lim ((abs f) /* s1) )

hence
abs f is_continuous_in x0
; :: thesis: - f is_continuous_in x0( (abs f) /* s1 is convergent & (abs f) . x0 = lim ((abs f) /* s1) )

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 that

A3: rng s1 c= dom (abs f) and

A4: ( s1 is convergent & lim s1 = x0 ) ; :: thesis: ( (abs f) /* s1 is convergent & (abs f) . x0 = lim ((abs f) /* s1) )

A5: rng s1 c= dom f by A3, VALUED_1:def 11;

then A6: f . x0 = lim (f /* s1) by A2, A4;

A7: f /* s1 is convergent by A2, A4, A5;

then abs (f /* s1) is convergent by SEQ_4:13;

hence (abs f) /* s1 is convergent by A5, RFUNCT_2:10; :: thesis: (abs f) . x0 = lim ((abs f) /* s1)

thus (abs f) . x0 = |.(f . x0).| by VALUED_1:18

.= lim (abs (f /* s1)) by A7, A6, SEQ_4:14

.= lim ((abs f) /* s1) by A5, RFUNCT_2:10 ; :: thesis: verum

end;assume that

A3: rng s1 c= dom (abs f) and

A4: ( s1 is convergent & lim s1 = x0 ) ; :: thesis: ( (abs f) /* s1 is convergent & (abs f) . x0 = lim ((abs f) /* s1) )

A5: rng s1 c= dom f by A3, VALUED_1:def 11;

then A6: f . x0 = lim (f /* s1) by A2, A4;

A7: f /* s1 is convergent by A2, A4, A5;

then abs (f /* s1) is convergent by SEQ_4:13;

hence (abs f) /* s1 is convergent by A5, RFUNCT_2:10; :: thesis: (abs f) . x0 = lim ((abs f) /* s1)

thus (abs f) . x0 = |.(f . x0).| by VALUED_1:18

.= lim (abs (f /* s1)) by A7, A6, SEQ_4:14

.= lim ((abs f) /* s1) by A5, RFUNCT_2:10 ; :: thesis: verum

thus - f is_continuous_in x0 by A1, A2, Th8; :: thesis: verum