let m be non zero Element of NAT ; :: thesis: for Z being set
for f being PartFunc of (REAL m),REAL st Z c= dom f holds
( f is_continuous_on Z iff for x0 being Element of REAL m
for r being Real st x0 in Z & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in Z & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) )
let Z be set ; :: thesis: for f being PartFunc of (REAL m),REAL st Z c= dom f holds
( f is_continuous_on Z iff for x0 being Element of REAL m
for r being Real st x0 in Z & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in Z & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) )
let f be PartFunc of (REAL m),REAL; :: thesis: ( Z c= dom f implies ( f is_continuous_on Z iff for x0 being Element of REAL m
for r being Real st x0 in Z & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in Z & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) )
set g = <>* f;
assume A1: Z c= dom f ; :: thesis: ( f is_continuous_on Z iff for x0 being Element of REAL m
for r being Real st x0 in Z & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in Z & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) )

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

assume f is_continuous_on Z ; :: thesis: for x0 being Element of REAL m
for r being Real st x0 in Z & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in Z & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) )
then A2: <>* f is_continuous_on Z by A1, Th44;
thus for x0 being Element of REAL m
for r being Real st x0 in Z & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in Z & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) :: thesis: verum

proof

let x0 be Element of REAL m; :: thesis: for r being Real st x0 in Z & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in Z & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) )
let r be Real; :: thesis: ( x0 in Z & 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in Z & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) )
assume A3: ( x0 in Z & 0 < r ) ; :: thesis: ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in Z & |.(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 Z & |.(x1 - x0).| < s holds
|.(((<>* f) /. x1) - ((<>* f) /. x0)).| < r ) ) by A2, PDIFF_7:38;
take s ; :: thesis: ( 0 < s & ( for x1 being Element of REAL m st x1 in Z & |.(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 Z & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r

hereby :: thesis: verum

let x1 be Element of REAL m; :: thesis: ( x1 in Z & |.(x1 - x0).| < s implies |.((f /. x1) - (f /. x0)).| < r )
assume A5: ( x1 in Z & |.(x1 - x0).| < s ) ; :: thesis: |.((f /. x1) - (f /. x0)).| < r
then A6: |.(((<>* f) /. x1) - ((<>* f) /. x0)).| < r by A4;
( (<>* f) /. x1 = <*(f /. x1)*> & (<>* f) /. x0 = <*(f /. x0)*> ) by A5, A1, A3, Th6;
then ((<>* f) /. x1) - ((<>* f) /. x0) = <*((f /. x1) - (f /. x0))*> by RVSUM_1:29;
hence |.((f /. x1) - (f /. x0)).| < r by A6, Lm1; :: thesis: verum

end;

end;

end;

assume A7: for x0 being Element of REAL m
for r being Real st x0 in Z & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in Z & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ; :: thesis: f is_continuous_on Z
A8: Z c= dom (<>* f) by A1, Th3;
for y0 being Element of REAL m
for r being Real st y0 in Z & 0 < r holds
ex s being Real st
( 0 < s & ( for y1 being Element of REAL m st y1 in Z & |.(y1 - y0).| < s holds
|.(((<>* f) /. y1) - ((<>* f) /. y0)).| < r ) )

proof

let x0 be Element of REAL m; :: thesis: for r being Real st x0 in Z & 0 < r holds
ex s being Real st
( 0 < s & ( for y1 being Element of REAL m st y1 in Z & |.(y1 - x0).| < s holds
|.(((<>* f) /. y1) - ((<>* f) /. x0)).| < r ) )
let r be Real; :: thesis: ( x0 in Z & 0 < r implies ex s being Real st
( 0 < s & ( for y1 being Element of REAL m st y1 in Z & |.(y1 - x0).| < s holds
|.(((<>* f) /. y1) - ((<>* f) /. x0)).| < r ) ) )
assume A9: ( x0 in Z & 0 < r ) ; :: thesis: ex s being Real st
( 0 < s & ( for y1 being Element of REAL m st y1 in Z & |.(y1 - x0).| < s holds
|.(((<>* f) /. y1) - ((<>* f) /. x0)).| < r ) )
then consider s being Real such that
A10: ( 0 < s & ( for x1 being Element of REAL m st x1 in Z & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) by A7;
take s ; :: thesis: ( 0 < s & ( for y1 being Element of REAL m st y1 in Z & |.(y1 - x0).| < s holds
|.(((<>* f) /. y1) - ((<>* f) /. x0)).| < r ) )
thus 0 < s by A10; :: thesis: for y1 being Element of REAL m st y1 in Z & |.(y1 - x0).| < s holds
|.(((<>* f) /. y1) - ((<>* f) /. x0)).| < r

hereby :: thesis: verum

let x1 be Element of REAL m; :: thesis: ( x1 in Z & |.(x1 - x0).| < s implies |.(((<>* f) /. x1) - ((<>* f) /. x0)).| < r )
assume A11: ( x1 in Z & |.(x1 - x0).| < s ) ; :: thesis: |.(((<>* f) /. x1) - ((<>* f) /. x0)).| < r
then A12: |.((f /. x1) - (f /. x0)).| < r by A10;
( (<>* f) /. x1 = <*(f /. x1)*> & (<>* f) /. x0 = <*(f /. x0)*> ) by A1, A11, A9, 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;

then <>* f is_continuous_on Z by A8, PDIFF_7:38;
hence f is_continuous_on Z by Th44; :: thesis: verum