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

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