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) ) )
A1: the carrier of (REAL-NS n) = REAL n by REAL_NS1:def 4;
A2: rng g c= dom ((proj 1,1) " ) by Th2;
then A3: dom (((proj 1,1) " ) * g) = dom g by RELAT_1:46;
reconsider Pd = <*(partdiff g,y,i)*> as Element of REAL 1 by FINSEQ_2:118;
reconsider x = y as Point of (REAL-NS n) by REAL_NS1:def 4;
A4: 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) by REAL_NS1:def 4;
reconsider One = <*1*> as VECTOR of (REAL-NS 1) by A4, FINSEQ_2:118;
assume 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) )
then A5: f is_partial_differentiable_in x,i by Th14;
then A6: r (#) f is_partial_differentiable_in x,i by Th32;
dom (r (#) f) = dom (((proj 1,1) " ) * g) by VFUNCT_1:def 4;
then dom (r (#) f) = dom g by A2, RELAT_1:46;
then A7: dom (r (#) f) = dom (r (#) g) by VALUED_1:def 5;
A8: rng (r (#) g) c= dom ((proj 1,1) " ) by Th2;
then A9: dom (((proj 1,1) " ) * (r (#) g)) = dom (r (#) g) by RELAT_1:46;

A10: now

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

end;

A17: (partdiff f,x,i) . One = <*(partdiff g,y,i)*> by A5, Th15;
dom (r (#) f) = dom (<>* (r (#) g)) by A7, A8, RELAT_1:46;
then A18: r (#) f = <>* (r (#) g) by A1, A4, A10, PARTFUN1:34;
then <*(partdiff (r (#) g),y,i)*> = (partdiff (r (#) f),x,i) . <*1*> by A5, Th15, Th32
.= (r * (partdiff f,x,i)) . <*1*> by A5, Th32
.= r * ((partdiff f,x,i) . One) by LOPBAN_1:42
.= r * Pd by A17, 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, A6, Th14, FINSEQ_1:57; :: thesis: verum