let n, m be non zero Nat; :: thesis: for g being PartFunc of (REAL m),(REAL n)
for y0 being Element of REAL m
for r being Real st g is_differentiable_in y0 holds
( r (#) g is_differentiable_in y0 & diff ((r (#) g),y0) = r (#) (diff (g,y0)) )
let g be PartFunc of (REAL m),(REAL n); :: thesis: for y0 being Element of REAL m
for r being Real st g is_differentiable_in y0 holds
( r (#) g is_differentiable_in y0 & diff ((r (#) g),y0) = r (#) (diff (g,y0)) )
let y0 be Element of REAL m; :: thesis: for r being Real st g is_differentiable_in y0 holds
( r (#) g is_differentiable_in y0 & diff ((r (#) g),y0) = r (#) (diff (g,y0)) )
let r be Real; :: thesis: ( g is_differentiable_in y0 implies ( r (#) g is_differentiable_in y0 & diff ((r (#) g),y0) = r (#) (diff (g,y0)) ) )
assume A1: g is_differentiable_in y0 ; :: thesis: ( r (#) g is_differentiable_in y0 & diff ((r (#) g),y0) = r (#) (diff (g,y0)) )
reconsider f = g as PartFunc of (REAL-NS m),(REAL-NS n) by Th1;
reconsider x0 = y0 as Point of (REAL-NS m) by REAL_NS1:def 4;
f is_differentiable_in x0 by A1, Th2;
then A2: ( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) ) by NDIFF_1:37;
r (#) f = r (#) g by Th6;
hence r (#) g is_differentiable_in y0 by A2, Th2; :: thesis: diff ((r (#) g),y0) = r (#) (diff (g,y0))
then diff ((r (#) g),y0) = diff ((r (#) f),x0) by Th3, Th6;
hence diff ((r (#) g),y0) = r (#) (diff (g,y0)) by A2, Th9, Th3, A1; :: thesis: verum