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;

now :: thesis: for x being Real st x in X holds
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;

then g is_differentiable_on X by A2, NDIFF_3:def 5;
then g | X is continuous by NDIFF_3:23;
hence f | X is continuous by NFCONT_4:23; :: thesis: verum