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;

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 by FINSEQ_1:40;

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:40; :: thesis: verum

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

A17:
(partdiff (f,x,i)) . One = <*(partdiff (g,y,i))*>
by A5, Th15;(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;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

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 by FINSEQ_1:40;

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:40; :: thesis: verum