let m be non zero Element of NAT ; :: thesis:
let Z be set ; :: thesis:
let f be PartFunc of (REAL m),REAL; :: thesis:
set g = <>* f;
assume A1: Z c= dom f ; :: thesis:

assume f is_continuous_on Z ; :: thesis:
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:

let x0 be Element of REAL m; :: thesis:
let r be Real; :: thesis:
assume A3: ( x0 in Z & 0 < r ) ; :: thesis:
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:
thus 0 < s by A4; :: thesis:

let x1 be Element of REAL m; :: thesis:
assume A5: ( x1 in Z & |.(x1 - x0).| < s ) ; :: thesis:
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:

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

let x0 be Element of REAL m; :: thesis:
let r be Real; :: thesis:
assume A9: ( x0 in Z & 0 < r ) ; :: thesis:
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:
thus 0 < s by A10; :: thesis:

let x1 be Element of REAL m; :: thesis:
assume A11: ( x1 in Z & |.(x1 - x0).| < s ) ; :: thesis:
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:

end;