let m be non zero Element of NAT ; for X being non empty Subset of (REAL m)
for f being PartFunc of (REAL m),REAL st X is open & X c= dom f & f is_continuously_differentiable_up_to_order 1,X holds
f is_continuous_on X
let X be non empty Subset of (REAL m); for f being PartFunc of (REAL m),REAL st X is open & X c= dom f & f is_continuously_differentiable_up_to_order 1,X holds
f is_continuous_on X
let f be PartFunc of (REAL m),REAL; ( X is open & X c= dom f & f is_continuously_differentiable_up_to_order 1,X implies f is_continuous_on X )
assume A1:
( X is open & X c= dom f & f is_continuously_differentiable_up_to_order 1,X )
; f is_continuous_on X
then A2:
f is_differentiable_on X
by Th2;
reconsider g = <>* f as PartFunc of (REAL m),(REAL 1) ;
A3:
g is_differentiable_on X
by A1, A2, PDIFF_9:53;
( the carrier of (REAL-NS m) = REAL m & the carrier of (REAL-NS 1) = REAL 1 )
by REAL_NS1:def 4;
then reconsider h = <>* f as PartFunc of (REAL-NS m),(REAL-NS 1) ;
h is_differentiable_on X
by A3, PDIFF_6:30;
then
h is_continuous_on X
by NDIFF_1:45;
then
g is_continuous_on X
by PDIFF_7:37;
hence
f is_continuous_on X
by PDIFF_9:44; verum