let n be non zero Nat; :: thesis: for i being 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 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:27;
reconsider d = partdiff (g,y,i) as Element of REAL by XREAL_0:def 1;
reconsider Pd = <*d*> as Element of REAL 1 by FINSEQ_2:98;
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 = <*jj*> as VECTOR of (REAL-NS 1) by A4, FINSEQ_2:98;
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:27;
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:27;

A10: now :: thesis: for x being Element of (REAL-NS n) st x in dom (r (#) f) holds
(r (#) f) . x = (<>* (r (#) g)) . x

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:12;
(r (#) f) . x = (r (#) f) /. x by A12, PARTFUN1:def 6;
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 6;
then f /. x = ((proj (1,1)) ") . (g . x) by A15, FUNCT_1:13;
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:27;
then A18: r (#) f = <>* (r (#) g) by A1, A4, A10, PARTFUN1:5;
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:36
.= r * Pd by A17, REAL_NS1:3
.= <*(r * (partdiff (g,y,i)))*> by RVSUM_1:47 ;
then partdiff ((r (#) g),y,i) = <*(r * (partdiff (g,y,i)))*> . 1 ;
hence ( r (#) g is_partial_differentiable_in y,i & partdiff ((r (#) g),y,i) = r * (partdiff (g,y,i)) ) by A18, A6, Th14; :: thesis: verum