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

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