let S be RealNormSpace; :: thesis: for f being PartFunc of REAL, the carrier of S st f is total & ( for x1, x2 being Real holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being Real st f is_continuous_in x0 holds
f | REAL is continuous
let f be PartFunc of REAL, the carrier of S; :: thesis: ( f is total & ( for x1, x2 being Real holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being Real st f is_continuous_in x0 implies f | REAL is continuous )
assume that
A1: f is total and
A2: for x1, x2 being Real holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ; :: thesis: ( for x0 being Real holds not f is_continuous_in x0 or f | REAL is continuous )
A3: dom f = REAL by A1, PARTFUN1:def 2;
given x0 being Real such that A4: f is_continuous_in x0 ; :: thesis: f | REAL is continuous
reconsider z0 = 0 as Real ;
(f /. z0) + (f /. z0) = f /. (z0 + z0) by A2;
then (f /. z0) + ((f /. z0) - (f /. z0)) = (f /. z0) - (f /. z0) by RLVECT_1:28;
then (f /. z0) + (0. S) = (f /. z0) - (f /. z0) by RLVECT_1:15;
then A5: (f /. z0) + (0. S) = 0. S by RLVECT_1:15;

A6: now :: thesis: for x1 being Real holds - (f /. x1) = f /. (- x1)

let x1 be Real; :: thesis: - (f /. x1) = f /. (- x1)
0. S = f /. (x1 + (- x1)) by A5, RLVECT_1:4;
then 0. S = (f /. x1) + (f /. (- x1)) by A2;
hence - (f /. x1) = f /. (- x1) by RLVECT_1:def 10; :: thesis: verum

end;

A7: now :: thesis: for x1, x2 being Real holds f /. (x1 - x2) = (f /. x1) - (f /. x2)

let x1, x2 be Real; :: thesis: f /. (x1 - x2) = (f /. x1) - (f /. x2)
f /. (x1 - x2) = f /. (x1 + (- x2)) ;
then f /. (x1 - x2) = (f /. x1) + (f /. (- x2)) by A2;
hence f /. (x1 - x2) = (f /. x1) - (f /. x2) by A6; :: thesis: verum

end;

now :: thesis: for x1, r being Real st x1 in REAL & r > 0 holds
ex s being Real st
( s > 0 & ( for x2 being Real st x2 in REAL & |.(x2 - x1).| < s holds
||.((f /. x2) - (f /. x1)).|| < r ) )

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

end;

hence f | REAL is continuous by A3, Th17; :: thesis: verum