let m be non zero Element of NAT ; :: thesis: 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); :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: verum