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