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 number st x0 in X & 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
abs ((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 number st x0 in X & 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) ) ) )
assume Z: X c= dom f ; :: thesis: ( f | X is continuous iff for x0, r being real number st x0 in X & 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) ) )
thus ( f | X is continuous implies for x0, r being real number st x0 in X & 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) ) ) :: thesis: ( ( for x0, r being real number st x0 in X & 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) ) ) implies f | X is continuous )

proof

assume A1: f | X is continuous ; :: thesis: for x0, r being real number st x0 in X & 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) )
let x0, r be real number ; :: thesis: ( x0 in X & 0 < r implies ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) ) )
assume A3: ( x0 in X & 0 < r ) ; :: thesis: ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) )
then x0 in dom (f | X) by Z, RELAT_1:91;
then f | X is_continuous_in x0 by A1, Def2;
then consider s being real number such that
A4: ( 0 < s & ( for x1 being real number st x1 in dom (f | X) & abs (x1 - x0) < s holds
abs (((f | X) . x1) - ((f | X) . x0)) < r ) ) by A3, Th3;
A5: dom (f | X) = (dom f) /\ X by RELAT_1:90
.= X by Z, XBOOLE_1:28 ;
take s ; :: thesis: ( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) )
thus 0 < s by A4; :: thesis: for x1 being real number st x1 in X & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r
let x1 be real number ; :: thesis: ( x1 in X & abs (x1 - x0) < s implies abs ((f . x1) - (f . x0)) < r )
assume A6: ( x1 in X & abs (x1 - x0) < s ) ; :: thesis: abs ((f . x1) - (f . x0)) < r
then abs ((f . x1) - (f . x0)) = abs (((f | X) . x1) - (f . x0)) by A5, FUNCT_1:70
.= abs (((f | X) . x1) - ((f | X) . x0)) by A3, A5, FUNCT_1:70 ;
hence abs ((f . x1) - (f . x0)) < r by A4, A5, A6; :: thesis: verum

end;

assume A8: for x0, r being real number st x0 in X & 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) ) ; :: thesis: f | X is continuous
A9: dom (f | X) = (dom f) /\ X by RELAT_1:90
.= X by Z, XBOOLE_1:28 ;

now

let x0 be real number ; :: thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 )
assume A10: x0 in dom (f | X) ; :: thesis: f | X is_continuous_in x0
B10: x0 in X by A10, RELAT_1:86;
for r being real number st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom (f | X) & abs (x1 - x0) < s holds
abs (((f | X) . x1) - ((f | X) . x0)) < r ) )

proof

let r be real number ; :: thesis: ( 0 < r implies ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom (f | X) & abs (x1 - x0) < s holds
abs (((f | X) . x1) - ((f | X) . x0)) < r ) ) )
assume 0 < r ; :: thesis: ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom (f | X) & abs (x1 - x0) < s holds
abs (((f | X) . x1) - ((f | X) . x0)) < r ) )
then consider s being real number such that
A11: ( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) ) by A8, B10;
take s ; :: thesis: ( 0 < s & ( for x1 being real number st x1 in dom (f | X) & abs (x1 - x0) < s holds
abs (((f | X) . x1) - ((f | X) . x0)) < r ) )
thus 0 < s by A11; :: thesis: for x1 being real number st x1 in dom (f | X) & abs (x1 - x0) < s holds
abs (((f | X) . x1) - ((f | X) . x0)) < r
let x1 be real number ; :: thesis: ( x1 in dom (f | X) & abs (x1 - x0) < s implies abs (((f | X) . x1) - ((f | X) . x0)) < r )
assume A12: ( x1 in dom (f | X) & abs (x1 - x0) < s ) ; :: thesis: abs (((f | X) . x1) - ((f | X) . x0)) < r
abs (((f | X) . x1) - ((f | X) . x0)) = abs (((f | X) . x1) - (f . x0)) by A10, FUNCT_1:70
.= abs ((f . x1) - (f . x0)) by A12, FUNCT_1:70 ;
hence abs (((f | X) . x1) - ((f | X) . x0)) < r by A9, A11, A12; :: thesis: verum

end;

hence f | X is_continuous_in x0 by Th3; :: thesis: verum

end;

hence f | X is continuous by Def2; :: thesis: verum