theorem Th10: :: PDIFF_1:10

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*> & f is_differentiable_in x holds
(diff (f,x)) . <*1*> = <*(diff (g,y))*>