theorem Th7: :: PDIFF_1:7

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