let f be PartFunc of (REAL-NS 1),(REAL-NS 1); :: thesis: for g being PartFunc of REAL ,REAL
for x being Point of (REAL-NS 1)
for y being Element of REAL st f = <>* g & x = <*y*> & f is_differentiable_in x holds
(diff f,x) . <*1*> = <*(diff g,y)*>
let g be PartFunc of REAL ,REAL ; :: thesis: for x being Point of (REAL-NS 1)
for y being Element of REAL st f = <>* g & x = <*y*> & f is_differentiable_in x holds
(diff f,x) . <*1*> = <*(diff g,y)*>
let x be Point of (REAL-NS 1); :: thesis: for y being Element of REAL st f = <>* g & x = <*y*> & f is_differentiable_in x holds
(diff f,x) . <*1*> = <*(diff g,y)*>
let y be Element of REAL ; :: thesis: ( f = <>* g & x = <*y*> & f is_differentiable_in x implies (diff f,x) . <*1*> = <*(diff g,y)*> )
assume A1: ( f = <>* g & x = <*y*> & f is_differentiable_in x ) ; :: thesis: (diff f,x) . <*1*> = <*(diff g,y)*>
then g is_differentiable_in y by Th7;
hence (diff f,x) . <*1*> = <*(diff g,y)*> by A1, Th8; :: thesis: verum