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 f .: N c= 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 f .: N c= 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 f .: N c= N1 ) ) )
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def 4;

hereby :: 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 f .: N c= N1 ) implies f is_continuous_in x0 )

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 f .: N c= N1 ) )
then A1: g is_continuous_in x0 ;
hence x0 in dom f ; :: 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 f .: N c= N1
thus 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 f .: N c= N1 :: thesis: verum

proof

let N1 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 } = N1 ) implies ex N being Neighbourhood of x0 st f .: N c= N1 )
given r being Real such that A2: ( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N1 ) ; :: thesis: ex N being Neighbourhood of x0 st f .: N c= N1
f /. x0 = g /. x0 by REAL_NS1:def 4;
then A3: { 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;
N1 is Neighbourhood of g /. x0 by A2, A3, NFCONT_1:3;
then consider N being Neighbourhood of x0 such that
A4: g .: N c= N1 by A1, NFCONT_3:10;
take N ; :: thesis: f .: N c= N1
thus f .: N c= N1 by A4; :: thesis: verum

end;

end;

assume A5: ( 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 f .: N c= N1 ) ) ; :: thesis: f is_continuous_in x0

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

let N1 be Neighbourhood of g /. x0; :: thesis: ex N being Neighbourhood of x0 st g .: N c= N1
consider r being Real such that
A6: 0 < r and
A7: { 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 ;
A8: 0 < rr by A6;
set N01 = { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } ;
f /. x0 = g /. x0 by REAL_NS1:def 4;
then A9: { 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
A10: f .: N c= { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } by A5, A8;
take N = N; :: thesis: g .: N c= N1
thus g .: N c= N1 by A7, A9, A10; :: thesis: verum

end;

then g is_continuous_in x0 by A5, NFCONT_3:10;
hence f is_continuous_in x0 ; :: thesis: verum