let f be PartFunc of REAL,REAL; :: 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

A5: (f . x0) + 0 = f . (x0 + 0)

.= (f . x0) + (f . 0) by A2 ;

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

A5: (f . x0) + 0 = f . (x0 + 0)

.= (f . x0) + (f . 0) by A2 ;

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

let x1 be Real; :: 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;0 = f . (x1 + (- x1)) by A5

.= (f . x1) + (f . (- x1)) by A2 ;

hence - (f . x1) = f . (- x1) ; :: thesis: verum

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)

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

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

hence
f | REAL is continuous
by A3, Th14; :: thesis: verumex 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, Th3;

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)).|

.= |.((f . (x2 - (x1 - x0))) - (f . x0)).| by A7 ;

hence |.((f . x2) - (f . x1)).| < r by A3, A10, A11, A12; :: thesis: verum

end;( 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, Th3;

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)).|

.= |.((f . (x2 - (x1 - x0))) - (f . x0)).| by A7 ;

hence |.((f . x2) - (f . x1)).| < r by A3, A10, A11, A12; :: thesis: verum