:: deftheorem defines is_differentiable_in PDIFF_7:def 1 :
for n being non zero Nat
for f being PartFunc of (REAL n),REAL
for x being Element of REAL n holds
( f is_differentiable_in x iff <>* f is_differentiable_in x );