let n be non empty Element of NAT ; :: thesis: for f being PartFunc of REAL,(REAL n)
for x0 being Real st f is_differentiable_in x0 holds
f is_continuous_in x0
let f be PartFunc of REAL,(REAL n); :: thesis: for x0 being Real st f is_differentiable_in x0 holds
f is_continuous_in x0
let x0 be Real; :: thesis: ( f is_differentiable_in x0 implies f is_continuous_in x0 )
assume f is_differentiable_in x0 ; :: thesis: f is_continuous_in x0
then consider g being PartFunc of REAL,(REAL-NS n) such that
A1: ( f = g & g is_differentiable_in x0 ) by Def1;
g is_continuous_in x0 by A1, NDIFF_3:22;
hence f is_continuous_in x0 by A1, NFCONT_4:def 1; :: thesis: verum