let f be PartFunc of REAL ,REAL ; :: thesis: ( f is total & ( for x1, x2 being real number holds f . (x1 + x2) = (f . x1) + (f . x2) ) & ex x0 being real number st f is_continuous_in x0 implies f | REAL is continuous )
assume that
A1: f is total and
A2: for x1, x2 being real number holds f . (x1 + x2) = (f . x1) + (f . x2) ; :: thesis: ( for x0 being real number holds not f is_continuous_in x0 or f | REAL is continuous )
given x0 being real number such that A3: f is_continuous_in x0 ; :: thesis: f | REAL is continuous
A4: dom f = REAL by A1, PARTFUN1:def 4;
A5: (f . x0) + 0 = f . (x0 + 0 )
.= (f . x0) + (f . 0 ) by A2 ;

A6: now

let x1 be real number ; :: thesis: - (f . x1) = f . (- x1)
0 = f . (x1 + (- x1)) by A5
.= (f . x1) + (f . (- x1)) by A2 ;
hence - (f . x1) = f . (- x1) ; :: thesis: verum

end;

A7: now

let x1, x2 be real number ; :: thesis: f . (x1 - x2) = (f . x1) - (f . x2)
thus f . (x1 - x2) = f . (x1 + (- x2))
.= (f . x1) + (f . (- x2)) by A2
.= (f . x1) + (- (f . x2)) by A6
.= (f . x1) - (f . x2) ; :: thesis: verum

end;

now

let x1, r be real number ; :: thesis: ( x1 in REAL & r > 0 implies ex s being real number st
( s > 0 & ( for x2 being real number st x2 in REAL & abs (x2 - x1) < s holds
abs ((f . x2) - (f . x1)) < r ) ) )
assume ( x1 in REAL & r > 0 ) ; :: thesis: ex s being real number st
( s > 0 & ( for x2 being real number st x2 in REAL & abs (x2 - x1) < s holds
abs ((f . x2) - (f . x1)) < r ) )
then consider s being real number such that
A8: ( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) ) by A3, Th3;
take s = s; :: thesis: ( s > 0 & ( for x2 being real number st x2 in REAL & abs (x2 - x1) < s holds
abs ((f . x2) - (f . x1)) < r ) )
thus s > 0 by A8; :: thesis: for x2 being real number st x2 in REAL & abs (x2 - x1) < s holds
abs ((f . x2) - (f . x1)) < r
let x2 be real number ; :: thesis: ( x2 in REAL & abs (x2 - x1) < s implies abs ((f . x2) - (f . x1)) < r )
assume A9: ( x2 in REAL & abs (x2 - x1) < s ) ; :: thesis: abs ((f . x2) - (f . x1)) < r
set y = x1 - x0;
(x1 - x0) + x0 = x1 ;
then A10: abs ((f . x2) - (f . x1)) = abs ((f . x2) - ((f . (x1 - x0)) + (f . x0))) by A2
.= abs (((f . x2) - (f . (x1 - x0))) - (f . x0))
.= abs ((f . (x2 - (x1 - x0))) - (f . x0)) by A7 ;
A11: x2 - (x1 - x0) is Real by XREAL_0:def 1;
abs ((x2 - (x1 - x0)) - x0) = abs (x2 - x1) ;
hence abs ((f . x2) - (f . x1)) < r by A4, A8, A9, A10, A11; :: thesis: verum

end;

hence f | REAL is continuous by A4, Th15; :: thesis: verum