let n be Nat; :: thesis: for x0 being Real
for f being PartFunc of REAL,REAL st f is_differentiable_in x0 holds
( (#Z n) * f is_differentiable_in x0 & diff (((#Z n) * f),x0) = (n * ((f . x0) #Z (n - 1))) * (diff (f,x0)) )
let x0 be Real; :: thesis: for f being PartFunc of REAL,REAL st f is_differentiable_in x0 holds
( (#Z n) * f is_differentiable_in x0 & diff (((#Z n) * f),x0) = (n * ((f . x0) #Z (n - 1))) * (diff (f,x0)) )
let f be PartFunc of REAL,REAL; :: thesis: ( f is_differentiable_in x0 implies ( (#Z n) * f is_differentiable_in x0 & diff (((#Z n) * f),x0) = (n * ((f . x0) #Z (n - 1))) * (diff (f,x0)) ) )
assume A1: f is_differentiable_in x0 ; :: thesis: ( (#Z n) * f is_differentiable_in x0 & diff (((#Z n) * f),x0) = (n * ((f . x0) #Z (n - 1))) * (diff (f,x0)) )
A2: ( #Z n is_differentiable_in f . x0 & x0 is Real ) by Th2;
hence (#Z n) * f is_differentiable_in x0 by A1, FDIFF_2:13; :: thesis: diff (((#Z n) * f),x0) = (n * ((f . x0) #Z (n - 1))) * (diff (f,x0))
thus diff (((#Z n) * f),x0) = (diff ((#Z n),(f . x0))) * (diff (f,x0)) by A1, A2, FDIFF_2:13
.= (n * ((f . x0) #Z (n - 1))) * (diff (f,x0)) by Th2 ; :: thesis: verum