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 that
A1: f = <>* g and
A2: x = <*y*> and
A3: f is_differentiable_in x ; :: thesis: (diff f,x) . <*1*> = <*(diff g,y)*>
g is_differentiable_in y by A1, A2, A3, Th7;
hence (diff f,x) . <*1*> = <*(diff g,y)*> by A1, A2, Th8; :: thesis: verum