let n be non empty Element of NAT ; :: thesis: for i being Element of NAT
for r being Real
for g being PartFunc of REAL n, REAL
for y being Element of REAL n st g is_partial_differentiable_in y,i holds
( r (#) g is_partial_differentiable_in y,i & partdiff (r (#) g),y,i = r * (partdiff g,y,i) )
let i be Element of NAT ; :: thesis: for r being Real
for g being PartFunc of REAL n, REAL
for y being Element of REAL n st g is_partial_differentiable_in y,i holds
( r (#) g is_partial_differentiable_in y,i & partdiff (r (#) g),y,i = r * (partdiff g,y,i) )
let r be Real; :: thesis: for g being PartFunc of REAL n, REAL
for y being Element of REAL n st g is_partial_differentiable_in y,i holds
( r (#) g is_partial_differentiable_in y,i & partdiff (r (#) g),y,i = r * (partdiff g,y,i) )
let g be PartFunc of REAL n, REAL ; :: thesis: for y being Element of REAL n st g is_partial_differentiable_in y,i holds
( r (#) g is_partial_differentiable_in y,i & partdiff (r (#) g),y,i = r * (partdiff g,y,i) )
let y be Element of REAL n; :: thesis: ( g is_partial_differentiable_in y,i implies ( r (#) g is_partial_differentiable_in y,i & partdiff (r (#) g),y,i = r * (partdiff g,y,i) ) )
assume A1: g is_partial_differentiable_in y,i ; :: thesis: ( r (#) g is_partial_differentiable_in y,i & partdiff (r (#) g),y,i = r * (partdiff g,y,i) )
A2: ( the carrier of (REAL-NS n) = REAL n & the carrier of (REAL-NS 1) = REAL 1 ) by REAL_NS1:def 4;
then reconsider f = <>* g as PartFunc of (REAL-NS n),(REAL-NS 1) ;
reconsider x = y as Point of (REAL-NS n) by REAL_NS1:def 4;
A3: dom (r (#) f) = dom (((proj 1,1) " ) * g) by VFUNCT_1:def 4;
A4: rng g c= dom ((proj 1,1) " ) by Th2;
then A5: dom (((proj 1,1) " ) * g) = dom g by RELAT_1:46;
dom (r (#) f) = dom g by A3, A4, RELAT_1:46;
then A6: dom (r (#) f) = dom (r (#) g) by VALUED_1:def 5;
A7: rng (r (#) g) c= dom ((proj 1,1) " ) by Th2;
then A8: dom (((proj 1,1) " ) * (r (#) g)) = dom (r (#) g) by RELAT_1:46;
A9: dom (r (#) f) = dom (<>* (r (#) g)) by A6, A7, RELAT_1:46;

now

let x be Element of the carrier of (REAL-NS n); :: thesis: ( x in dom (r (#) f) implies (r (#) f) . x = (<>* (r (#) g)) . x )
assume A10: x in dom (r (#) f) ; :: thesis: (r (#) f) . x = (<>* (r (#) g)) . x
then A11: x in dom f by VFUNCT_1:def 4;
A12: x in dom g by A5, A10, VFUNCT_1:def 4;
then A13: x in dom (r (#) g) by VALUED_1:def 5;
(r (#) f) . x = (r (#) f) /. x by A10, PARTFUN1:def 8;
then A14: (r (#) f) . x = r * (f /. x) by A10, VFUNCT_1:def 4;
A15: (<>* (r (#) g)) . x = ((proj 1,1) " ) . ((r (#) g) . x) by A6, A8, A10, FUNCT_1:22;
f /. x = (((proj 1,1) " ) * g) . x by A11, PARTFUN1:def 8;
then A16: f /. x = ((proj 1,1) " ) . (g . x) by A12, FUNCT_1:23;
consider I being Function of REAL , REAL 1 such that
A17: ( I is bijective & (proj 1,1) " = I ) by Th2;
r * (f /. x) = I . (r * (g . x)) by A16, A17, Th3;
hence (r (#) f) . x = (<>* (r (#) g)) . x by A13, A14, A15, A17, VALUED_1:def 5; :: thesis: verum

end;

then A18: r (#) f = <>* (r (#) g) by A2, A9, PARTFUN1:34;
A19: f is_partial_differentiable_in x,i by A1, Th14;
then A20: r (#) f is_partial_differentiable_in x,i by Th32;
reconsider One = <*1*> as VECTOR of (REAL-NS 1) by A2, FINSEQ_2:118;
A21: (partdiff f,x,i) . One = <*(partdiff g,y,i)*> by A19, Th15;
reconsider Pd = <*(partdiff g,y,i)*> as Element of REAL 1 by FINSEQ_2:118;
<*(partdiff (r (#) g),y,i)*> = (partdiff (r (#) f),x,i) . <*1*> by A18, A20, Th15
.= (r * (partdiff f,x,i)) . <*1*> by A19, Th32
.= r * ((partdiff f,x,i) . One) by LOPBAN_1:42
.= r * Pd by A21, REAL_NS1:3
.= <*(r * (partdiff g,y,i))*> by RVSUM_1:69 ;
then partdiff (r (#) g),y,i = <*(r * (partdiff g,y,i))*> . 1 by FINSEQ_1:57;
hence ( r (#) g is_partial_differentiable_in y,i & partdiff (r (#) g),y,i = r * (partdiff g,y,i) ) by A18, A20, Th14, FINSEQ_1:57; :: thesis: verum