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,() 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 ;
then A5: { p where p is Point of () : ||.(p - (g /. x0)).|| < r } = N01 by ;
{ p where p is Point of () : ||.(p - (g /. x0)).|| < r } is Neighbourhood of g /. x0 by ;
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 ;
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 ; :: 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:
reconsider g = f as PartFunc of REAL,() 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 () : ||.(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 () : ||.(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 ;
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 ; :: thesis: verum
end;
then g is_continuous_in x0 by ;
hence f is_continuous_in x0 ; :: thesis: verum