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 )

proof

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;

assume A7: ( 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: 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

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;

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

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;

then { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } is Subset of (REAL n) by TARSKI:def 3;
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;

then g is_continuous_in x0 by A7, NFCONT_3:9;
hence f is_continuous_in x0 ; :: thesis: verum