let m, n be non zero Nat; :: thesis: for f being PartFunc of (REAL m),(REAL n)
for x0 being Element of REAL m holds
( f is_continuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in dom f & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) ) )
let f be PartFunc of (REAL m),(REAL n); :: thesis: for x0 being Element of REAL m holds
( f is_continuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in dom f & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) ) )
let x0 be Element of REAL m; :: thesis: ( f is_continuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in dom f & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) ) )
( the carrier of (REAL-NS m) = REAL m & the carrier of (REAL-NS n) = REAL n ) by REAL_NS1:def 4;
then reconsider g = f as PartFunc of (REAL-NS m),(REAL-NS n) ;
reconsider y0 = x0 as Point of (REAL-NS m) by REAL_NS1:def 4;

hereby :: thesis: ( x0 in dom f & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in dom f & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) implies f is_continuous_in x0 )

assume f is_continuous_in x0 ; :: thesis: ( x0 in dom f & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in dom f & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) )
then A1: g is_continuous_in y0 ;
then A2: ( y0 in dom g & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for y1 being Point of (REAL-NS m) st y1 in dom g & ||.(y1 - y0).|| < s holds
||.((g /. y1) - (g /. y0)).|| < r ) ) ) ) by NFCONT_1:7;
thus x0 in dom f by A1, NFCONT_1:7; :: thesis: for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in dom f & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) )
thus for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in dom f & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) :: thesis: verum

proof

let r be Real; :: thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Element of REAL m 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 Element of REAL m st x1 in dom f & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) )
then consider s being Real such that
A3: ( 0 < s & ( for y1 being Point of (REAL-NS m) st y1 in dom g & ||.(y1 - y0).|| < s holds
||.((g /. y1) - (g /. y0)).|| < r ) ) by A1, NFCONT_1:7;
take s ; :: thesis: ( 0 < s & ( for x1 being Element of REAL m st x1 in dom f & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) )
thus 0 < s by A3; :: thesis: for x1 being Element of REAL m st x1 in dom f & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r

hereby :: thesis: verum

let x1 be Element of REAL m; :: thesis: ( x1 in dom f & |.(x1 - x0).| < s implies |.((f /. x1) - (f /. x0)).| < r )
assume A4: ( x1 in dom f & |.(x1 - x0).| < s ) ; :: thesis: |.((f /. x1) - (f /. x0)).| < r
reconsider y1 = x1 as Point of (REAL-NS m) by REAL_NS1:def 4;
( y1 in dom g & ||.(y1 - y0).|| < s ) by A4, REAL_NS1:1, REAL_NS1:5;
then A5: ||.((g /. y1) - (g /. y0)).|| < r by A3;
( g /. y1 = f /. x1 & g /. y0 = f /. x0 ) by A2, Th30, A4;
hence |.((f /. x1) - (f /. x0)).| < r by A5, REAL_NS1:1, REAL_NS1:5; :: thesis: verum

end;

end;

end;

assume A6: ( x0 in dom f & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in dom f & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) ) ; :: thesis: f is_continuous_in x0
reconsider y0 = x0 as Point of (REAL-NS m) by REAL_NS1:def 4;
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for y1 being Point of (REAL-NS m) st y1 in dom g & ||.(y1 - y0).|| < s holds
||.((g /. y1) - (g /. y0)).|| < r ) )

proof

let r be Real; :: thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for y1 being Point of (REAL-NS m) st y1 in dom g & ||.(y1 - y0).|| < s holds
||.((g /. y1) - (g /. y0)).|| < r ) ) )
assume 0 < r ; :: thesis: ex s being Real st
( 0 < s & ( for y1 being Point of (REAL-NS m) st y1 in dom g & ||.(y1 - y0).|| < s holds
||.((g /. y1) - (g /. y0)).|| < r ) )
then consider s being Real such that
A7: ( 0 < s & ( for x1 being Element of REAL m st x1 in dom f & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) by A6;
take s ; :: thesis: ( 0 < s & ( for y1 being Point of (REAL-NS m) st y1 in dom g & ||.(y1 - y0).|| < s holds
||.((g /. y1) - (g /. y0)).|| < r ) )
thus 0 < s by A7; :: thesis: for y1 being Point of (REAL-NS m) st y1 in dom g & ||.(y1 - y0).|| < s holds
||.((g /. y1) - (g /. y0)).|| < r

hereby :: thesis: verum

let y1 be Point of (REAL-NS m); :: thesis: ( y1 in dom g & ||.(y1 - y0).|| < s implies ||.((g /. y1) - (g /. y0)).|| < r )
assume A8: ( y1 in dom g & ||.(y1 - y0).|| < s ) ; :: thesis: ||.((g /. y1) - (g /. y0)).|| < r
reconsider x1 = y1 as Element of REAL m by REAL_NS1:def 4;
( x1 in dom f & |.(x1 - x0).| < s ) by A8, REAL_NS1:1, REAL_NS1:5;
then A9: |.((f /. x1) - (f /. x0)).| < r by A7;
( g /. y1 = f /. x1 & g /. y0 = f /. x0 ) by A8, A6, Th30;
hence ||.((g /. y1) - (g /. y0)).|| < r by A9, REAL_NS1:1, REAL_NS1:5; :: thesis: verum

end;

end;

then g is_continuous_in y0 by A6, NFCONT_1:7;
hence f is_continuous_in x0 ; :: thesis: verum