let X be set ; :: thesis: for f being PartFunc of REAL,REAL st X c= dom f holds

( f | X is continuous iff for x0, r being Real st x0 in X & 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Real st x1 in X & |.(x1 - x0).| < s holds

|.((f . x1) - (f . x0)).| < r ) ) )

let f be PartFunc of REAL,REAL; :: thesis: ( X c= dom f implies ( f | X is continuous iff for x0, r being Real st x0 in X & 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Real st x1 in X & |.(x1 - x0).| < s holds

|.((f . x1) - (f . x0)).| < r ) ) ) )

assume A1: X c= dom f ; :: thesis: ( f | X is continuous iff for x0, r being Real st x0 in X & 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Real st x1 in X & |.(x1 - x0).| < s holds

|.((f . x1) - (f . x0)).| < r ) ) )

thus ( f | X is continuous implies for x0, r being Real st x0 in X & 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Real st x1 in X & |.(x1 - x0).| < s holds

|.((f . x1) - (f . x0)).| < r ) ) ) :: thesis: ( ( for x0, r being Real st x0 in X & 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Real st x1 in X & |.(x1 - x0).| < s holds

|.((f . x1) - (f . x0)).| < r ) ) ) implies f | X is continuous )

ex s being Real st

( 0 < s & ( for x1 being Real st x1 in X & |.(x1 - x0).| < s holds

|.((f . x1) - (f . x0)).| < r ) ) ; :: thesis: f | X is continuous

( f | X is continuous iff for x0, r being Real st x0 in X & 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Real st x1 in X & |.(x1 - x0).| < s holds

|.((f . x1) - (f . x0)).| < r ) ) )

let f be PartFunc of REAL,REAL; :: thesis: ( X c= dom f implies ( f | X is continuous iff for x0, r being Real st x0 in X & 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Real st x1 in X & |.(x1 - x0).| < s holds

|.((f . x1) - (f . x0)).| < r ) ) ) )

assume A1: X c= dom f ; :: thesis: ( f | X is continuous iff for x0, r being Real st x0 in X & 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Real st x1 in X & |.(x1 - x0).| < s holds

|.((f . x1) - (f . x0)).| < r ) ) )

thus ( f | X is continuous implies for x0, r being Real st x0 in X & 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Real st x1 in X & |.(x1 - x0).| < s holds

|.((f . x1) - (f . x0)).| < r ) ) ) :: thesis: ( ( for x0, r being Real st x0 in X & 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Real st x1 in X & |.(x1 - x0).| < s holds

|.((f . x1) - (f . x0)).| < r ) ) ) implies f | X is continuous )

proof

assume A10:
for x0, r being Real st x0 in X & 0 < r holds
assume A2:
f | X is continuous
; :: thesis: for x0, r being Real st x0 in X & 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Real st x1 in X & |.(x1 - x0).| < s holds

|.((f . x1) - (f . x0)).| < r ) )

let x0, r be Real; :: thesis: ( x0 in X & 0 < r implies ex s being Real st

( 0 < s & ( for x1 being Real st x1 in X & |.(x1 - x0).| < s holds

|.((f . x1) - (f . x0)).| < r ) ) )

assume that

A3: x0 in X and

A4: 0 < r ; :: thesis: ex s being Real st

( 0 < s & ( for x1 being Real st x1 in X & |.(x1 - x0).| < s holds

|.((f . x1) - (f . x0)).| < r ) )

x0 in dom (f | X) by A1, A3, RELAT_1:62;

then f | X is_continuous_in x0 by A2;

then consider s being Real such that

A5: 0 < s and

A6: for x1 being Real st x1 in dom (f | X) & |.(x1 - x0).| < s holds

|.(((f | X) . x1) - ((f | X) . x0)).| < r by A4, Th3;

take s ; :: thesis: ( 0 < s & ( for x1 being Real st x1 in X & |.(x1 - x0).| < s holds

|.((f . x1) - (f . x0)).| < r ) )

thus 0 < s by A5; :: thesis: for x1 being Real st x1 in X & |.(x1 - x0).| < s holds

|.((f . x1) - (f . x0)).| < r

let x1 be Real; :: thesis: ( x1 in X & |.(x1 - x0).| < s implies |.((f . x1) - (f . x0)).| < r )

assume that

A7: x1 in X and

A8: |.(x1 - x0).| < s ; :: thesis: |.((f . x1) - (f . x0)).| < r

A9: dom (f | X) = (dom f) /\ X by RELAT_1:61

.= X by A1, XBOOLE_1:28 ;

then |.((f . x1) - (f . x0)).| = |.(((f | X) . x1) - (f . x0)).| by A7, FUNCT_1:47

.= |.(((f | X) . x1) - ((f | X) . x0)).| by A3, A9, FUNCT_1:47 ;

hence |.((f . x1) - (f . x0)).| < r by A6, A9, A7, A8; :: thesis: verum

end;ex s being Real st

( 0 < s & ( for x1 being Real st x1 in X & |.(x1 - x0).| < s holds

|.((f . x1) - (f . x0)).| < r ) )

let x0, r be Real; :: thesis: ( x0 in X & 0 < r implies ex s being Real st

( 0 < s & ( for x1 being Real st x1 in X & |.(x1 - x0).| < s holds

|.((f . x1) - (f . x0)).| < r ) ) )

assume that

A3: x0 in X and

A4: 0 < r ; :: thesis: ex s being Real st

( 0 < s & ( for x1 being Real st x1 in X & |.(x1 - x0).| < s holds

|.((f . x1) - (f . x0)).| < r ) )

x0 in dom (f | X) by A1, A3, RELAT_1:62;

then f | X is_continuous_in x0 by A2;

then consider s being Real such that

A5: 0 < s and

A6: for x1 being Real st x1 in dom (f | X) & |.(x1 - x0).| < s holds

|.(((f | X) . x1) - ((f | X) . x0)).| < r by A4, Th3;

take s ; :: thesis: ( 0 < s & ( for x1 being Real st x1 in X & |.(x1 - x0).| < s holds

|.((f . x1) - (f . x0)).| < r ) )

thus 0 < s by A5; :: thesis: for x1 being Real st x1 in X & |.(x1 - x0).| < s holds

|.((f . x1) - (f . x0)).| < r

let x1 be Real; :: thesis: ( x1 in X & |.(x1 - x0).| < s implies |.((f . x1) - (f . x0)).| < r )

assume that

A7: x1 in X and

A8: |.(x1 - x0).| < s ; :: thesis: |.((f . x1) - (f . x0)).| < r

A9: dom (f | X) = (dom f) /\ X by RELAT_1:61

.= X by A1, XBOOLE_1:28 ;

then |.((f . x1) - (f . x0)).| = |.(((f | X) . x1) - (f . x0)).| by A7, FUNCT_1:47

.= |.(((f | X) . x1) - ((f | X) . x0)).| by A3, A9, FUNCT_1:47 ;

hence |.((f . x1) - (f . x0)).| < r by A6, A9, A7, A8; :: thesis: verum

ex s being Real st

( 0 < s & ( for x1 being Real st x1 in X & |.(x1 - x0).| < s holds

|.((f . x1) - (f . x0)).| < r ) ) ; :: thesis: f | X is continuous

now :: thesis: for x0 being Real st x0 in dom (f | X) holds

f | X is_continuous_in x0

hence
f | X is continuous
; :: thesis: verumf | X is_continuous_in x0

let x0 be Real; :: thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 )

assume A11: x0 in dom (f | X) ; :: thesis: f | X is_continuous_in x0

A12: x0 in X by A11;

for r being Real st 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Real st x1 in dom (f | X) & |.(x1 - x0).| < s holds

|.(((f | X) . x1) - ((f | X) . x0)).| < r ) )

end;assume A11: x0 in dom (f | X) ; :: thesis: f | X is_continuous_in x0

A12: x0 in X by A11;

for r being Real st 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Real st x1 in dom (f | X) & |.(x1 - x0).| < s holds

|.(((f | X) . x1) - ((f | X) . x0)).| < r ) )

proof

hence
f | X is_continuous_in x0
by Th3; :: thesis: verum
let r be Real; :: thesis: ( 0 < r implies ex s being Real st

( 0 < s & ( for x1 being Real st x1 in dom (f | X) & |.(x1 - x0).| < s holds

|.(((f | X) . x1) - ((f | X) . x0)).| < r ) ) )

assume 0 < r ; :: thesis: ex s being Real st

( 0 < s & ( for x1 being Real st x1 in dom (f | X) & |.(x1 - x0).| < s holds

|.(((f | X) . x1) - ((f | X) . x0)).| < r ) )

then consider s being Real such that

A13: 0 < s and

A14: for x1 being Real st x1 in X & |.(x1 - x0).| < s holds

|.((f . x1) - (f . x0)).| < r by A10, A12;

take s ; :: thesis: ( 0 < s & ( for x1 being Real st x1 in dom (f | X) & |.(x1 - x0).| < s holds

|.(((f | X) . x1) - ((f | X) . x0)).| < r ) )

thus 0 < s by A13; :: thesis: for x1 being Real st x1 in dom (f | X) & |.(x1 - x0).| < s holds

|.(((f | X) . x1) - ((f | X) . x0)).| < r

let x1 be Real; :: thesis: ( x1 in dom (f | X) & |.(x1 - x0).| < s implies |.(((f | X) . x1) - ((f | X) . x0)).| < r )

assume that

A15: x1 in dom (f | X) and

A16: |.(x1 - x0).| < s ; :: thesis: |.(((f | X) . x1) - ((f | X) . x0)).| < r

|.(((f | X) . x1) - ((f | X) . x0)).| = |.(((f | X) . x1) - (f . x0)).| by A11, FUNCT_1:47

.= |.((f . x1) - (f . x0)).| by A15, FUNCT_1:47 ;

hence |.(((f | X) . x1) - ((f | X) . x0)).| < r by A14, A15, A16; :: thesis: verum

end;( 0 < s & ( for x1 being Real st x1 in dom (f | X) & |.(x1 - x0).| < s holds

|.(((f | X) . x1) - ((f | X) . x0)).| < r ) ) )

assume 0 < r ; :: thesis: ex s being Real st

( 0 < s & ( for x1 being Real st x1 in dom (f | X) & |.(x1 - x0).| < s holds

|.(((f | X) . x1) - ((f | X) . x0)).| < r ) )

then consider s being Real such that

A13: 0 < s and

A14: for x1 being Real st x1 in X & |.(x1 - x0).| < s holds

|.((f . x1) - (f . x0)).| < r by A10, A12;

take s ; :: thesis: ( 0 < s & ( for x1 being Real st x1 in dom (f | X) & |.(x1 - x0).| < s holds

|.(((f | X) . x1) - ((f | X) . x0)).| < r ) )

thus 0 < s by A13; :: thesis: for x1 being Real st x1 in dom (f | X) & |.(x1 - x0).| < s holds

|.(((f | X) . x1) - ((f | X) . x0)).| < r

let x1 be Real; :: thesis: ( x1 in dom (f | X) & |.(x1 - x0).| < s implies |.(((f | X) . x1) - ((f | X) . x0)).| < r )

assume that

A15: x1 in dom (f | X) and

A16: |.(x1 - x0).| < s ; :: thesis: |.(((f | X) . x1) - ((f | X) . x0)).| < r

|.(((f | X) . x1) - ((f | X) . x0)).| = |.(((f | X) . x1) - (f . x0)).| by A11, FUNCT_1:47

.= |.((f . x1) - (f . x0)).| by A15, FUNCT_1:47 ;

hence |.(((f | X) . x1) - ((f | X) . x0)).| < r by A14, A15, A16; :: thesis: verum