theorem Th8: :: PDIFF_1:8

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