let f be PartFunc of REAL,REAL; :: thesis: for x0 being Real holds

( f is_continuous_in x0 iff for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st f .: N c= N1 )

let x0 be Real; :: thesis: ( f is_continuous_in x0 iff for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st f .: N c= N1 )

thus ( f is_continuous_in x0 implies for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st f .: N c= N1 ) :: thesis: ( ( for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st f .: N c= N1 ) implies f is_continuous_in x0 )

( f is_continuous_in x0 iff for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st f .: N c= N1 )

let x0 be Real; :: thesis: ( f is_continuous_in x0 iff for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st f .: N c= N1 )

thus ( f is_continuous_in x0 implies for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st f .: N c= N1 ) :: thesis: ( ( for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st f .: N c= N1 ) implies f is_continuous_in x0 )

proof

assume A3:
for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st f .: N c= N1
; :: thesis: f is_continuous_in x0
assume A1:
f is_continuous_in x0
; :: thesis: for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st f .: N c= N1

let N1 be Neighbourhood of f . x0; :: thesis: ex N being Neighbourhood of x0 st f .: N c= N1

consider N being Neighbourhood of x0 such that

A2: for x1 being Real st x1 in dom f & x1 in N holds

f . x1 in N1 by A1, Th4;

take N ; :: thesis: f .: N c= N1

end;let N1 be Neighbourhood of f . x0; :: thesis: ex N being Neighbourhood of x0 st f .: N c= N1

consider N being Neighbourhood of x0 such that

A2: for x1 being Real st x1 in dom f & x1 in N holds

f . x1 in N1 by A1, Th4;

take N ; :: thesis: f .: N c= N1

now :: thesis: for r being Real st r in f .: N holds

r in N1

hence
f .: N c= N1
; :: thesis: verumr in N1

let r be Real; :: thesis: ( r in f .: N implies r in N1 )

assume r in f .: N ; :: thesis: r in N1

then ex x being Element of REAL st

( x in dom f & x in N & r = f . x ) by PARTFUN2:59;

hence r in N1 by A2; :: thesis: verum

end;assume r in f .: N ; :: thesis: r in N1

then ex x being Element of REAL st

( x in dom f & x in N & r = f . x ) by PARTFUN2:59;

hence r in N1 by A2; :: thesis: verum

now :: thesis: for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st

for x1 being Real st x1 in dom f & x1 in N holds

f . x1 in N1

hence
f is_continuous_in x0
by Th4; :: thesis: verumfor x1 being Real 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 st x1 in dom f & x1 in N holds

f . x1 in N1

consider N being Neighbourhood of x0 such that

A4: f .: N c= N1 by A3;

take N = N; :: thesis: for x1 being Real st x1 in dom f & x1 in N holds

f . x1 in N1

let x1 be Real; :: thesis: ( x1 in dom f & x1 in N implies f . x1 in N1 )

assume ( x1 in dom f & x1 in N ) ; :: thesis: f . x1 in N1

then f . x1 in f .: N by FUNCT_1:def 6;

hence f . x1 in N1 by A4; :: thesis: verum

end;for x1 being Real st x1 in dom f & x1 in N holds

f . x1 in N1

consider N being Neighbourhood of x0 such that

A4: f .: N c= N1 by A3;

take N = N; :: thesis: for x1 being Real st x1 in dom f & x1 in N holds

f . x1 in N1

let x1 be Real; :: thesis: ( x1 in dom f & x1 in N implies f . x1 in N1 )

assume ( x1 in dom f & x1 in N ) ; :: thesis: f . x1 in N1

then f . x1 in f .: N by FUNCT_1:def 6;

hence f . x1 in N1 by A4; :: thesis: verum