let X be set ; :: thesis: for n being non zero Element of NAT

for f being PartFunc of REAL,(REAL n) st f is_differentiable_on X holds

f | X is continuous

let n be non zero Element of NAT ; :: thesis: for f being PartFunc of REAL,(REAL n) st f is_differentiable_on X holds

f | X is continuous

let f be PartFunc of REAL,(REAL n); :: thesis: ( f is_differentiable_on X implies f | X is continuous )

assume A1: f is_differentiable_on X ; :: thesis: f | X is continuous

reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def 4;

A2: X c= dom g by A1;

then g | X is continuous by NDIFF_3:23;

hence f | X is continuous by NFCONT_4:23; :: thesis: verum

for f being PartFunc of REAL,(REAL n) st f is_differentiable_on X holds

f | X is continuous

let n be non zero Element of NAT ; :: thesis: for f being PartFunc of REAL,(REAL n) st f is_differentiable_on X holds

f | X is continuous

let f be PartFunc of REAL,(REAL n); :: thesis: ( f is_differentiable_on X implies f | X is continuous )

assume A1: f is_differentiable_on X ; :: thesis: f | X is continuous

reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def 4;

A2: X c= dom g by A1;

now :: thesis: for x being Real st x in X holds

g | X is_differentiable_in x

then
g is_differentiable_on X
by A2, NDIFF_3:def 5;g | X is_differentiable_in x

let x be Real; :: thesis: ( x in X implies g | X is_differentiable_in x )

assume x in X ; :: thesis: g | X is_differentiable_in x

then f | X is_differentiable_in x by A1;

hence g | X is_differentiable_in x ; :: thesis: verum

end;assume x in X ; :: thesis: g | X is_differentiable_in x

then f | X is_differentiable_in x by A1;

hence g | X is_differentiable_in x ; :: thesis: verum

then g | X is continuous by NDIFF_3:23;

hence f | X is continuous by NFCONT_4:23; :: thesis: verum