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

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