let m be non empty Element of NAT ; :: thesis: for f being PartFunc of (REAL m),REAL
for x0 being Element of REAL m holds
( f is_continuous_in x0 iff <>* f is_continuous_in x0 )
let f be PartFunc of (REAL m),REAL; :: thesis: for x0 being Element of REAL m holds
( f is_continuous_in x0 iff <>* f is_continuous_in x0 )
let x0 be Element of REAL m; :: thesis: ( f is_continuous_in x0 iff <>* f is_continuous_in x0 )
set g = <>* f;

hereby :: thesis: ( <>* f is_continuous_in x0 implies f is_continuous_in x0 )

assume P1: f is_continuous_in x0 ; :: thesis: <>* f is_continuous_in x0
then P2: x0 in dom f by XDef60;
then P3: x0 in dom (<>* f) by LMXTh0;

now :: 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 ) )

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
P5: ( 0 < s & ( for x1 being Element of REAL m st x1 in dom f & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) by P1, XDef60;
take s = 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 P5; :: 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 P6: ( x1 in dom (<>* f) & |.(x1 - x0).| < s ) ; :: thesis: |.(((<>* f) /. x1) - ((<>* f) /. x0)).| < r
then P8: x1 in dom f by LMXTh0;
then P7: |.((f /. x1) - (f /. x0)).| < r by P5, P6;
( (<>* f) /. x1 = <*(f /. x1)*> & (<>* f) /. x0 = <*(f /. x0)*> ) by P2, P8, XTh30;
then ((<>* f) /. x1) - ((<>* f) /. x0) = <*((f /. x1) - (f /. x0))*> by RVSUM_1:29;
hence |.(((<>* f) /. x1) - ((<>* f) /. x0)).| < r by P7, XTh30D; :: thesis: verum

end;

end;

hence <>* f is_continuous_in x0 by P3, PDIFF_7:36; :: thesis: verum

end;

assume A1: <>* f is_continuous_in x0 ; :: thesis: f is_continuous_in x0
then x0 in dom (<>* f) by PDIFF_7:36;
then P2: x0 in dom f by LMXTh0;

now :: 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 ) )

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
P4: ( 0 < s & ( for x1 being Element of REAL m st x1 in dom (<>* f) & |.(x1 - x0).| < s holds
|.(((<>* f) /. x1) - ((<>* f) /. x0)).| < r ) ) by A1, PDIFF_7:36;
take s = 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 P4; :: 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 P5: ( x1 in dom f & |.(x1 - x0).| < s ) ; :: thesis: |.((f /. x1) - (f /. x0)).| < r
then x1 in dom (<>* f) by LMXTh0;
then P6: |.(((<>* f) /. x1) - ((<>* f) /. x0)).| < r by P4, P5;
( (<>* f) /. x1 = <*(f /. x1)*> & (<>* f) /. x0 = <*(f /. x0)*> ) by P2, P5, XTh30;
then ((<>* f) /. x1) - ((<>* f) /. x0) = <*((f /. x1) - (f /. x0))*> by RVSUM_1:29;
hence |.((f /. x1) - (f /. x0)).| < r by P6, XTh30D; :: thesis: verum

end;

end;

hence f is_continuous_in x0 by P2, XDef60; :: thesis: verum