let n be non zero Element of NAT ; :: thesis: for J being Function of (REAL-NS 1),REAL

for x0 being Point of (REAL-NS 1)

for y0 being Element of REAL

for g being PartFunc of REAL,(REAL-NS n)

for f being PartFunc of (REAL-NS 1),(REAL-NS n) st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J & g is_differentiable_in y0 holds

( f is_differentiable_in x0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )

let J be Function of (REAL-NS 1),REAL; :: thesis: for x0 being Point of (REAL-NS 1)

for y0 being Element of REAL

for g being PartFunc of REAL,(REAL-NS n)

for f being PartFunc of (REAL-NS 1),(REAL-NS n) st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J & g is_differentiable_in y0 holds

( f is_differentiable_in x0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )

let x0 be Point of (REAL-NS 1); :: thesis: for y0 being Element of REAL

for g being PartFunc of REAL,(REAL-NS n)

for f being PartFunc of (REAL-NS 1),(REAL-NS n) st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J & g is_differentiable_in y0 holds

( f is_differentiable_in x0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )

let y0 be Element of REAL ; :: thesis: for g being PartFunc of REAL,(REAL-NS n)

for f being PartFunc of (REAL-NS 1),(REAL-NS n) st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J & g is_differentiable_in y0 holds

( f is_differentiable_in x0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )

let g be PartFunc of REAL,(REAL-NS n); :: thesis: for f being PartFunc of (REAL-NS 1),(REAL-NS n) st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J & g is_differentiable_in y0 holds

( f is_differentiable_in x0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )

let f be PartFunc of (REAL-NS 1),(REAL-NS n); :: thesis: ( J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J & g is_differentiable_in y0 implies ( f is_differentiable_in x0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) ) )

assume A1: ( J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J & g is_differentiable_in y0 ) ; :: thesis: ( f is_differentiable_in x0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )

hence A2: f is_differentiable_in x0 by Th44; :: thesis: ( diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )

reconsider I = (proj (1,1)) " as Function of REAL,(REAL-NS 1) by PDIFF_1:2, REAL_NS1:def 4;

A3: J * I = id REAL by A1, Lm2, FUNCT_1:39;

f * I = g * (id REAL) by A1, A3, RELAT_1:36

.= g by FUNCT_2:17 ;

hence ( diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) ) by A1, Th42, A2; :: thesis: verum

for x0 being Point of (REAL-NS 1)

for y0 being Element of REAL

for g being PartFunc of REAL,(REAL-NS n)

for f being PartFunc of (REAL-NS 1),(REAL-NS n) st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J & g is_differentiable_in y0 holds

( f is_differentiable_in x0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )

let J be Function of (REAL-NS 1),REAL; :: thesis: for x0 being Point of (REAL-NS 1)

for y0 being Element of REAL

for g being PartFunc of REAL,(REAL-NS n)

for f being PartFunc of (REAL-NS 1),(REAL-NS n) st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J & g is_differentiable_in y0 holds

( f is_differentiable_in x0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )

let x0 be Point of (REAL-NS 1); :: thesis: for y0 being Element of REAL

for g being PartFunc of REAL,(REAL-NS n)

for f being PartFunc of (REAL-NS 1),(REAL-NS n) st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J & g is_differentiable_in y0 holds

( f is_differentiable_in x0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )

let y0 be Element of REAL ; :: thesis: for g being PartFunc of REAL,(REAL-NS n)

for f being PartFunc of (REAL-NS 1),(REAL-NS n) st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J & g is_differentiable_in y0 holds

( f is_differentiable_in x0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )

let g be PartFunc of REAL,(REAL-NS n); :: thesis: for f being PartFunc of (REAL-NS 1),(REAL-NS n) st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J & g is_differentiable_in y0 holds

( f is_differentiable_in x0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )

let f be PartFunc of (REAL-NS 1),(REAL-NS n); :: thesis: ( J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J & g is_differentiable_in y0 implies ( f is_differentiable_in x0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) ) )

assume A1: ( J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J & g is_differentiable_in y0 ) ; :: thesis: ( f is_differentiable_in x0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )

hence A2: f is_differentiable_in x0 by Th44; :: thesis: ( diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )

reconsider I = (proj (1,1)) " as Function of REAL,(REAL-NS 1) by PDIFF_1:2, REAL_NS1:def 4;

A3: J * I = id REAL by A1, Lm2, FUNCT_1:39;

f * I = g * (id REAL) by A1, A3, RELAT_1:36

.= g by FUNCT_2:17 ;

hence ( diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) ) by A1, Th42, A2; :: thesis: verum