let n be natural number ; :: thesis: for x0 being real number
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 number ; :: 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 by Th2;
A3: x0 is Real by XREAL_0:def 1;
hence (#Z n) * f is_differentiable_in x0 by A1, A2, 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, A3, FDIFF_2:13
.= (n * ((f . x0) #Z (n - 1))) * (diff f,x0) by Th2 ; :: thesis: verum