let n, m be non empty Element of 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 AS: 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 DPREP010;
reconsider x0 = y0 as Point of (REAL-NS m) by REAL_NS1:def 4;
f is_differentiable_in x0 by AS, DPREP020;
then P2: ( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) ) by NDIFF_1:42;
r (#) f = r (#) g by DPREP060;
hence r (#) g is_differentiable_in y0 by P2, DPREP020; :: thesis: diff ((r (#) g),y0) = r (#) (diff (g,y0))
then diff ((r (#) g),y0) = diff ((r (#) f),x0) by DPREP030, DPREP060;
hence diff ((r (#) g),y0) = r (#) (diff (g,y0)) by P2, DPREP090, DPREP030, AS; :: thesis: verum