theorem Th44: :: NDIFF_4:44

for n being non zero Element of NAT
for J being Function of (REAL-NS 1),REAL
for x0 being Point of (REAL-NS 1)
for y0 being Element of REAL
for g being PartFunc of REAL,(REAL-NS n)
for f being PartFunc of (REAL-NS 1),(REAL-NS n) st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds
( f is_differentiable_in x0 iff g is_differentiable_in y0 )