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,() 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 ;
reconsider r = r as Real ;
A3: r (#) f = r (#) g by ;
A4: diff (f,x0) = diff (g,x0) by ;
diff ((r (#) f),x0) = diff ((r (#) g),x0) by ;
hence ( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) ) by ; :: thesis: verum