:: deftheorem defines is_differentiable_in NDIFF_4:def 6 :
for n being non zero Element of NAT
for f being PartFunc of (REAL-NS n),REAL
for x being Point of (REAL-NS n) holds
( f is_differentiable_in x iff ex g being PartFunc of (REAL n),REAL ex y being Element of REAL n st
( f = g & x = y & g is_differentiable_in y ) );