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