let m be non zero 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 A1: f is_continuous_in x0 ; :: thesis: <>* f is_continuous_in x0
then A2: x0 in dom f by Th36;
then A3: x0 in dom (<>* f) by Th3;

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
A4: ( 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, Th36;
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 A4; :: 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 A5: ( x1 in dom (<>* f) & |.(x1 - x0).| < s ) ; :: thesis: |.(((<>* f) /. x1) - ((<>* f) /. x0)).| < r
then A6: x1 in dom f by Th3;
then A7: |.((f /. x1) - (f /. x0)).| < r by A4, A5;
( (<>* f) /. x1 = <*(f /. x1)*> & (<>* f) /. x0 = <*(f /. x0)*> ) by A2, A6, Th6;
then ((<>* f) /. x1) - ((<>* f) /. x0) = <*((f /. x1) - (f /. x0))*> by RVSUM_1:29;
hence |.(((<>* f) /. x1) - ((<>* f) /. x0)).| < r by A7, Lm1; :: thesis: verum

end;

end;

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

end;

assume A8: <>* f is_continuous_in x0 ; :: thesis: f is_continuous_in x0
then x0 in dom (<>* f) by PDIFF_7:36;
then A9: x0 in dom f by Th3;

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
A10: ( 0 < s & ( for x1 being Element of REAL m st x1 in dom (<>* f) & |.(x1 - x0).| < s holds
|.(((<>* f) /. x1) - ((<>* f) /. x0)).| < r ) ) by A8, 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 A10; :: 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 A11: ( x1 in dom f & |.(x1 - x0).| < s ) ; :: thesis: |.((f /. x1) - (f /. x0)).| < r
then x1 in dom (<>* f) by Th3;
then A12: |.(((<>* f) /. x1) - ((<>* f) /. x0)).| < r by A10, A11;
( (<>* f) /. x1 = <*(f /. x1)*> & (<>* f) /. x0 = <*(f /. x0)*> ) by A9, A11, Th6;
then ((<>* f) /. x1) - ((<>* f) /. x0) = <*((f /. x1) - (f /. x0))*> by RVSUM_1:29;
hence |.((f /. x1) - (f /. x0)).| < r by A12, Lm1; :: thesis: verum

end;

end;

hence f is_continuous_in x0 by A9, Th36; :: thesis: verum