let x0, r be Real; :: thesis: for n being non zero Element of NAT
for f being PartFunc of REAL,(REAL n) st f is_differentiable_in x0 holds
( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) )
let n be non zero Element of NAT ; :: thesis: for f being PartFunc of REAL,(REAL n) st f is_differentiable_in x0 holds
( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) )
let f be PartFunc of REAL,(REAL n); :: thesis: ( f is_differentiable_in x0 implies ( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) ) )
assume f is_differentiable_in x0 ; :: thesis: ( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) )
then consider g being PartFunc of REAL,(REAL-NS n) such that
A1: ( f = g & g is_differentiable_in x0 ) ;
A2: ( r (#) g is_differentiable_in x0 & diff ((r (#) g),x0) = r * (diff (g,x0)) ) by A1, NDIFF_3:16;
reconsider r = r as Real ;
A3: r (#) f = r (#) g by A1, NFCONT_4:6;
A4: diff (f,x0) = diff (g,x0) by A1, Th3;
diff ((r (#) f),x0) = diff ((r (#) g),x0) by A1, Th3, NFCONT_4:6;
hence ( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) ) by A3, A2, A4, REAL_NS1:3; :: thesis: verum