let n be Element of NAT ; :: thesis: for x0 being Real

for f being PartFunc of REAL,(REAL n) holds

( f is_continuous_in x0 iff ( x0 in dom f & ( for N1 being Subset of (REAL n) st ex r being Real st

( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N1 ) holds

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: for f being PartFunc of REAL,(REAL n) holds

( f is_continuous_in x0 iff ( x0 in dom f & ( for N1 being Subset of (REAL n) st ex r being Real st

( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N1 ) holds

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,(REAL n); :: thesis: ( f is_continuous_in x0 iff ( x0 in dom f & ( for N1 being Subset of (REAL n) st ex r being Real st

( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N1 ) holds

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 Subset of (REAL n) st ex r being Real st

( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N1 ) holds

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 Subset of (REAL n) st ex r being Real st

( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N1 ) holds

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 )

( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N1 ) holds

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: f is_continuous_in x0

reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def 4;

hence f is_continuous_in x0 ; :: thesis: verum

for f being PartFunc of REAL,(REAL n) holds

( f is_continuous_in x0 iff ( x0 in dom f & ( for N1 being Subset of (REAL n) st ex r being Real st

( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N1 ) holds

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: for f being PartFunc of REAL,(REAL n) holds

( f is_continuous_in x0 iff ( x0 in dom f & ( for N1 being Subset of (REAL n) st ex r being Real st

( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N1 ) holds

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,(REAL n); :: thesis: ( f is_continuous_in x0 iff ( x0 in dom f & ( for N1 being Subset of (REAL n) st ex r being Real st

( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N1 ) holds

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 Subset of (REAL n) st ex r being Real st

( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N1 ) holds

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 Subset of (REAL n) st ex r being Real st

( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N1 ) holds

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 A7:
( x0 in dom f & ( for N1 being Subset of (REAL n) st ex r being Real st
assume
f is_continuous_in x0
; :: thesis: ( x0 in dom f & ( for N1 being Subset of (REAL n) st ex r being Real st

( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N1 ) holds

ex N being Neighbourhood of x0 st

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

f /. x1 in N1 ) )

then consider g being PartFunc of REAL,(REAL-NS n) such that

A1: ( f = g & g is_continuous_in x0 ) ;

thus x0 in dom f by A1; :: thesis: for N1 being Subset of (REAL n) st ex r being Real st

( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N1 ) holds

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 Subset of (REAL n); :: thesis: ( ex r being Real st

( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N01 ) implies ex N being Neighbourhood of x0 st

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

f /. x1 in N01 )

assume A2: ex r being Real st

( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N01 ) ; :: 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

A3: 0 < r and

A4: { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } = N01 by A2;

f /. x0 = g /. x0 by A1, REAL_NS1:def 4;

then A5: { p where p is Point of (REAL-NS n) : ||.(p - (g /. x0)).|| < r } = N01 by A4, Th4;

{ p where p is Point of (REAL-NS n) : ||.(p - (g /. x0)).|| < r } is Neighbourhood of g /. x0 by A3, NFCONT_1:3;

then consider N being Neighbourhood of x0 such that

A6: for x1 being Real st x1 in dom g & x1 in N holds

g /. x1 in N01 by A5, A1, NFCONT_3:9;

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 ( x1 in dom f & x1 in N ) ; :: thesis: f /. x1 in N01

then g /. x1 in N01 by A1, A6;

hence f /. x1 in N01 by A1, REAL_NS1:def 4; :: thesis: verum

end;( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N1 ) holds

ex N being Neighbourhood of x0 st

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

f /. x1 in N1 ) )

then consider g being PartFunc of REAL,(REAL-NS n) such that

A1: ( f = g & g is_continuous_in x0 ) ;

thus x0 in dom f by A1; :: thesis: for N1 being Subset of (REAL n) st ex r being Real st

( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N1 ) holds

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 Subset of (REAL n); :: thesis: ( ex r being Real st

( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N01 ) implies ex N being Neighbourhood of x0 st

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

f /. x1 in N01 )

assume A2: ex r being Real st

( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N01 ) ; :: 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

A3: 0 < r and

A4: { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } = N01 by A2;

f /. x0 = g /. x0 by A1, REAL_NS1:def 4;

then A5: { p where p is Point of (REAL-NS n) : ||.(p - (g /. x0)).|| < r } = N01 by A4, Th4;

{ p where p is Point of (REAL-NS n) : ||.(p - (g /. x0)).|| < r } is Neighbourhood of g /. x0 by A3, NFCONT_1:3;

then consider N being Neighbourhood of x0 such that

A6: for x1 being Real st x1 in dom g & x1 in N holds

g /. x1 in N01 by A5, A1, NFCONT_3:9;

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 ( x1 in dom f & x1 in N ) ; :: thesis: f /. x1 in N01

then g /. x1 in N01 by A1, A6;

hence f /. x1 in N01 by A1, REAL_NS1:def 4; :: thesis: verum

( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N1 ) holds

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: f is_continuous_in x0

reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def 4;

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

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

g /. x1 in N1

then
g is_continuous_in x0
by A7, NFCONT_3:9;for x1 being Real st x1 in dom g & x1 in N holds

g /. x1 in N1

let N1 be Neighbourhood of g /. x0; :: thesis: ex N being Neighbourhood of x0 st

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

g /. x1 in N1

consider r being Real such that

A8: 0 < r and

A9: { p where p is Point of (REAL-NS n) : ||.(p - (g /. x0)).|| < r } c= N1 by NFCONT_1:def 1;

reconsider rr = r as Real ;

A10: 0 < rr by A8;

set N01 = { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } ;

f /. x0 = g /. x0 by REAL_NS1:def 4;

then A11: { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } = { p where p is Point of (REAL-NS n) : ||.(p - (g /. x0)).|| < r } by Th4;

then consider N being Neighbourhood of x0 such that

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

f /. x1 in { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } by A7, A10;

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

g /. x1 in N1

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

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

then f /. x1 in { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } by A12;

then g /. x1 in { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } by REAL_NS1:def 4;

hence g /. x1 in N1 by A9, A11; :: thesis: verum

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

g /. x1 in N1

consider r being Real such that

A8: 0 < r and

A9: { p where p is Point of (REAL-NS n) : ||.(p - (g /. x0)).|| < r } c= N1 by NFCONT_1:def 1;

reconsider rr = r as Real ;

A10: 0 < rr by A8;

set N01 = { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } ;

f /. x0 = g /. x0 by REAL_NS1:def 4;

then A11: { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } = { p where p is Point of (REAL-NS n) : ||.(p - (g /. x0)).|| < r } by Th4;

now :: thesis: for x being object st x in { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } holds

x in REAL n

then
{ p where p is Element of REAL n : |.(p - (f /. x0)).| < r } is Subset of (REAL n)
by TARSKI:def 3;x in REAL n

let x be object ; :: thesis: ( x in { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } implies x in REAL n )

assume x in { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } ; :: thesis: x in REAL n

then ex p being Element of REAL n st

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

hence x in REAL n ; :: thesis: verum

end;assume x in { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } ; :: thesis: x in REAL n

then ex p being Element of REAL n st

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

hence x in REAL n ; :: thesis: verum

then consider N being Neighbourhood of x0 such that

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

f /. x1 in { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } by A7, A10;

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

g /. x1 in N1

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

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

then f /. x1 in { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } by A12;

then g /. x1 in { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } by REAL_NS1:def 4;

hence g /. x1 in N1 by A9, A11; :: thesis: verum

hence f is_continuous_in x0 ; :: thesis: verum