theorem :: PDIFF_1:9

for f being PartFunc of (REAL-NS 1),(REAL-NS 1)
for g being PartFunc of REAL,REAL
for x being Point of (REAL-NS 1)
for y being Real st f = <>* g & x = <*y*> holds
( f is_differentiable_in x iff g is_differentiable_in y ) by Th7, Th8;