let S be RealNormSpace; :: thesis: for f being PartFunc of REAL, the carrier of S

for x0 being Real holds

( f is_continuous_in x0 iff ( x0 in dom f & ( 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 ) ) )

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

( f is_continuous_in x0 iff ( x0 in dom f & ( 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 ) ) )

let x0 be Real; :: thesis: ( f is_continuous_in x0 iff ( x0 in dom f & ( 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 ) ) )

thus ( f is_continuous_in x0 implies ( x0 in dom f & ( 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 ) ) ) :: thesis: ( x0 in dom f & ( 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 ) implies f is_continuous_in x0 )

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

f /. x1 in N1 ) ) ; :: thesis: f is_continuous_in x0

for x0 being Real holds

( f is_continuous_in x0 iff ( x0 in dom f & ( 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 ) ) )

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

( f is_continuous_in x0 iff ( x0 in dom f & ( 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 ) ) )

let x0 be Real; :: thesis: ( f is_continuous_in x0 iff ( x0 in dom f & ( 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 ) ) )

thus ( f is_continuous_in x0 implies ( x0 in dom f & ( 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 ) ) ) :: thesis: ( x0 in dom f & ( 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 ) implies f is_continuous_in x0 )

proof

assume A8:
( x0 in dom f & ( for N1 being Neighbourhood of f /. x0 ex N being Neighbourhood of x0 st
assume A1:
f is_continuous_in x0
; :: thesis: ( x0 in dom f & ( 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 x0 in dom f ; :: 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

let N01 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 N01

consider r being Real such that

A2: 0 < r and

A3: { p where p is Point of S : ||.(p - (f /. x0)).|| < r } c= N01 by NFCONT_1:def 1;

set N1 = { p where p is Point of S : ||.(p - (f /. x0)).|| < r } ;

consider s being Real such that

A4: 0 < s and

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

||.((f /. x1) - (f /. x0)).|| < r by A1, A2, Th8;

reconsider N = ].(x0 - s),(x0 + s).[ as Neighbourhood of x0 by A4, RCOMP_1:def 6;

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

f /. x1 in N01

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

assume that

A6: x1 in dom f and

A7: x1 in N ; :: thesis: f /. x1 in N01

|.(x1 - x0).| < s by A7, RCOMP_1:1;

then ||.((f /. x1) - (f /. x0)).|| < r by A5, A6;

then f /. x1 in { p where p is Point of S : ||.(p - (f /. x0)).|| < r } ;

hence f /. x1 in N01 by A3; :: thesis: verum

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

f /. x1 in N1 ) )

hence x0 in dom f ; :: 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

let N01 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 N01

consider r being Real such that

A2: 0 < r and

A3: { p where p is Point of S : ||.(p - (f /. x0)).|| < r } c= N01 by NFCONT_1:def 1;

set N1 = { p where p is Point of S : ||.(p - (f /. x0)).|| < r } ;

consider s being Real such that

A4: 0 < s and

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

||.((f /. x1) - (f /. x0)).|| < r by A1, A2, Th8;

reconsider N = ].(x0 - s),(x0 + s).[ as Neighbourhood of x0 by A4, RCOMP_1:def 6;

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

f /. x1 in N01

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

assume that

A6: x1 in dom f and

A7: x1 in N ; :: thesis: f /. x1 in N01

|.(x1 - x0).| < s by A7, RCOMP_1:1;

then ||.((f /. x1) - (f /. x0)).|| < r by A5, A6;

then f /. x1 in { p where p is Point of S : ||.(p - (f /. x0)).|| < r } ;

hence f /. x1 in N01 by A3; :: thesis: verum

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

f /. x1 in N1 ) ) ; :: thesis: f is_continuous_in x0

now :: thesis: for r being Real st 0 < r holds

ex s being Real st

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

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

hence
f is_continuous_in x0
by A8, Th8; :: thesis: verumex s being Real st

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

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

let r be Real; :: thesis: ( 0 < r implies ex s being Real st

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

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

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

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

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

then reconsider N1 = { p where p is Point of S : ||.(p - (f /. x0)).|| < r } as Neighbourhood of f /. x0 by NFCONT_1:3;

consider N2 being Neighbourhood of x0 such that

A9: for x1 being Real st x1 in dom f & x1 in N2 holds

f /. x1 in N1 by A8;

consider s being Real 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 st x1 in dom f & |.(x1 - x0).| < s holds

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

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

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

||.((f /. x1) - (f /. x0)).|| < r ) ) by A10; :: thesis: verum

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

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

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

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

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

then reconsider N1 = { p where p is Point of S : ||.(p - (f /. x0)).|| < r } as Neighbourhood of f /. x0 by NFCONT_1:3;

consider N2 being Neighbourhood of x0 such that

A9: for x1 being Real st x1 in dom f & x1 in N2 holds

f /. x1 in N1 by A8;

consider s being Real 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 st x1 in dom f & |.(x1 - x0).| < s holds

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

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

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

proof

hence
( 0 < s & ( for x1 being Real st x1 in dom f & |.(x1 - x0).| < s holds
let x1 be Real; :: thesis: ( x1 in dom f & |.(x1 - x0).| < s implies ||.((f /. x1) - (f /. x0)).|| < r )

assume that

A12: x1 in dom f and

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

x1 in N2 by A11, A13, RCOMP_1:1;

then f /. x1 in N1 by A9, A12;

then ex p being Point of S st

( p = f /. x1 & ||.(p - (f /. x0)).|| < r ) ;

hence ||.((f /. x1) - (f /. x0)).|| < r ; :: thesis: verum

end;assume that

A12: x1 in dom f and

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

x1 in N2 by A11, A13, RCOMP_1:1;

then f /. x1 in N1 by A9, A12;

then ex p being Point of S st

( p = f /. x1 & ||.(p - (f /. x0)).|| < r ) ;

hence ||.((f /. x1) - (f /. x0)).|| < r ; :: thesis: verum

||.((f /. x1) - (f /. x0)).|| < r ) ) by A10; :: thesis: verum