let f be PartFunc of REAL,REAL; :: thesis: for x0 being real number holds
( f is_continuous_in x0 iff for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom f & x1 in N holds
f . x1 in N1 )
let x0 be real number ; :: thesis: ( f is_continuous_in x0 iff for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom f & x1 in N holds
f . x1 in N1 )
thus ( f is_continuous_in x0 implies for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom f & x1 in N holds
f . x1 in N1 ) :: thesis: ( ( for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom f & x1 in N holds
f . x1 in N1 ) implies f is_continuous_in x0 )

proof

assume A1: f is_continuous_in x0 ; :: thesis: for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom f & x1 in N holds
f . x1 in N1
let N1 be Neighbourhood of f . x0; :: thesis: ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom f & x1 in N holds
f . x1 in N1
consider r being real number such that
A2: 0 < r and
A3: N1 = ].((f . x0) - r),((f . x0) + r).[ by RCOMP_1:def 6;
consider s being real number such that
A4: 0 < s and
A5: for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r by A1, A2, Th3;
reconsider N = ].(x0 - s),(x0 + s).[ as Neighbourhood of x0 by A4, RCOMP_1:def 6;
take N ; :: thesis: for x1 being real number st x1 in dom f & x1 in N holds
f . x1 in N1
let x1 be real number ; :: thesis: ( x1 in dom f & x1 in N implies f . x1 in N1 )
assume that
A6: x1 in dom f and
A7: x1 in N ; :: thesis: f . x1 in N1
abs (x1 - x0) < s by A7, RCOMP_1:1;
then abs ((f . x1) - (f . x0)) < r by A5, A6;
hence f . x1 in N1 by A3, RCOMP_1:1; :: thesis: verum

end;

assume A8: for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom f & x1 in N holds
f . x1 in N1 ; :: thesis: f is_continuous_in x0

now

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 & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) ) )
assume 0 < r ; :: thesis: ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) )
then reconsider N1 = ].((f . x0) - r),((f . x0) + r).[ as Neighbourhood of f . x0 by RCOMP_1:def 6;
consider N2 being Neighbourhood of x0 such that
A9: for x1 being real number st x1 in dom f & x1 in N2 holds
f . x1 in N1 by A8;
consider s being real number such that
A10: 0 < s and
A11: N2 = ].(x0 - s),(x0 + s).[ by RCOMP_1:def 6;
take s = s; :: thesis: ( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) )
for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r

proof

let x1 be real number ; :: thesis: ( x1 in dom f & abs (x1 - x0) < s implies abs ((f . x1) - (f . x0)) < r )
assume that
A12: x1 in dom f and
A13: abs (x1 - x0) < s ; :: thesis: abs ((f . x1) - (f . x0)) < r
x1 in N2 by A11, A13, RCOMP_1:1;
then f . x1 in N1 by A9, A12;
hence abs ((f . x1) - (f . x0)) < r by RCOMP_1:1; :: thesis: verum

end;

hence ( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) ) by A10; :: thesis: verum

end;

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