let r be Element of REAL ; :: thesis: for f1, f2, f3 being PartFunc of REAL ,REAL
for t0 being Real st f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 & f1 . t0 <> 0 & f2 . t0 <> 0 & f3 . t0 <> 0 & r <> 0 holds
VFuncdiff ((r (#) f1) ^ ),((r (#) f2) ^ ),((r (#) f3) ^ ),t0 = - ((1 / r) * |[((diff f1,t0) / ((f1 . t0) ^2 )),((diff f2,t0) / ((f2 . t0) ^2 )),((diff f3,t0) / ((f3 . t0) ^2 ))]|)
let f1, f2, f3 be PartFunc of REAL ,REAL ; :: thesis: for t0 being Real st f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 & f1 . t0 <> 0 & f2 . t0 <> 0 & f3 . t0 <> 0 & r <> 0 holds
VFuncdiff ((r (#) f1) ^ ),((r (#) f2) ^ ),((r (#) f3) ^ ),t0 = - ((1 / r) * |[((diff f1,t0) / ((f1 . t0) ^2 )),((diff f2,t0) / ((f2 . t0) ^2 )),((diff f3,t0) / ((f3 . t0) ^2 ))]|)
let t0 be Real; :: thesis: ( f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 & f1 . t0 <> 0 & f2 . t0 <> 0 & f3 . t0 <> 0 & r <> 0 implies VFuncdiff ((r (#) f1) ^ ),((r (#) f2) ^ ),((r (#) f3) ^ ),t0 = - ((1 / r) * |[((diff f1,t0) / ((f1 . t0) ^2 )),((diff f2,t0) / ((f2 . t0) ^2 )),((diff f3,t0) / ((f3 . t0) ^2 ))]|) )
assume that
A1: ( f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 ) and
A2: ( f1 . t0 <> 0 & f2 . t0 <> 0 & f3 . t0 <> 0 ) and
B0: r <> 0 ; :: thesis: VFuncdiff ((r (#) f1) ^ ),((r (#) f2) ^ ),((r (#) f3) ^ ),t0 = - ((1 / r) * |[((diff f1,t0) / ((f1 . t0) ^2 )),((diff f2,t0) / ((f2 . t0) ^2 )),((diff f3,t0) / ((f3 . t0) ^2 ))]|)
A3: ( r (#) f1 is_differentiable_in t0 & r (#) f2 is_differentiable_in t0 & r (#) f3 is_differentiable_in t0 ) by A1, FDIFF_1:23;
B1: (r (#) f1) . t0 = r * (f1 . t0) by VALUED_1:6;
B2: (r (#) f2) . t0 = r * (f2 . t0) by VALUED_1:6;
B3: (r (#) f3) . t0 = r * (f3 . t0) by VALUED_1:6;
VFuncdiff ((r (#) f1) ^ ),((r (#) f2) ^ ),((r (#) f3) ^ ),t0 = - |[((diff (r (#) f1),t0) / (((r (#) f1) . t0) ^2 )),((diff (r (#) f2),t0) / (((r (#) f2) . t0) ^2 )),((diff (r (#) f3),t0) / (((r (#) f3) . t0) ^2 ))]| by A3, B1, B2, B3, A2, B0, Th63
.= - |[((r * (diff f1,t0)) / (((r (#) f1) . t0) ^2 )),((diff (r (#) f2),t0) / (((r (#) f2) . t0) ^2 )),((diff (r (#) f3),t0) / (((r (#) f3) . t0) ^2 ))]| by A1, FDIFF_1:23
.= - |[((r * (diff f1,t0)) / (((r (#) f1) . t0) ^2 )),((r * (diff f2,t0)) / (((r (#) f2) . t0) ^2 )),((diff (r (#) f3),t0) / (((r (#) f3) . t0) ^2 ))]| by A1, FDIFF_1:23
.= - |[((r * (diff f1,t0)) / (((r (#) f1) . t0) ^2 )),((r * (diff f2,t0)) / (((r (#) f2) . t0) ^2 )),((r * (diff f3,t0)) / (((r (#) f3) . t0) ^2 ))]| by A1, FDIFF_1:23
.= - |[(r * ((diff f1,t0) / (((r (#) f1) . t0) ^2 ))),((r * (diff f2,t0)) / (((r (#) f2) . t0) ^2 )),((r * (diff f3,t0)) / (((r (#) f3) . t0) ^2 ))]| by XCMPLX_1:75
.= - |[(r * ((diff f1,t0) / (((r (#) f1) . t0) ^2 ))),(r * ((diff f2,t0) / (((r (#) f2) . t0) ^2 ))),((r * (diff f3,t0)) / (((r (#) f3) . t0) ^2 ))]| by XCMPLX_1:75
.= - |[(r * ((diff f1,t0) / (((r (#) f1) . t0) ^2 ))),(r * ((diff f2,t0) / (((r (#) f2) . t0) ^2 ))),(r * ((diff f3,t0) / (((r (#) f3) . t0) ^2 )))]| by XCMPLX_1:75
.= - (r * |[((diff f1,t0) / ((r ^2 ) * ((f1 . t0) ^2 ))),((diff f2,t0) / ((r ^2 ) * ((f2 . t0) ^2 ))),((diff f3,t0) / ((r ^2 ) * ((f3 . t0) ^2 )))]|) by B3, B2, B1, LmA8
.= - (r * |[(((diff f1,t0) / (r ^2 )) / ((f1 . t0) ^2 )),((diff f2,t0) / ((r ^2 ) * ((f2 . t0) ^2 ))),((diff f3,t0) / ((r ^2 ) * ((f3 . t0) ^2 )))]|) by XCMPLX_1:79
.= - (r * |[(((diff f1,t0) / (r ^2 )) / ((f1 . t0) ^2 )),(((diff f2,t0) / (r ^2 )) / ((f2 . t0) ^2 )),((diff f3,t0) / ((r ^2 ) * ((f3 . t0) ^2 )))]|) by XCMPLX_1:79
.= - (r * |[(((diff f1,t0) / (r ^2 )) / ((f1 . t0) ^2 )),(((diff f2,t0) / (r ^2 )) / ((f2 . t0) ^2 )),(((diff f3,t0) / (r ^2 )) / ((f3 . t0) ^2 ))]|) by XCMPLX_1:79
.= - (r * |[(((diff f1,t0) / ((f1 . t0) ^2 )) / (r ^2 )),(((diff f2,t0) / (r ^2 )) / ((f2 . t0) ^2 )),(((diff f3,t0) / (r ^2 )) / ((f3 . t0) ^2 ))]|) by XCMPLX_1:48
.= - (r * |[(((diff f1,t0) / ((f1 . t0) ^2 )) / (r ^2 )),(((diff f2,t0) / ((f2 . t0) ^2 )) / (r ^2 )),(((diff f3,t0) / (r ^2 )) / ((f3 . t0) ^2 ))]|) by XCMPLX_1:48
.= - (r * |[(((diff f1,t0) / ((f1 . t0) ^2 )) / (r ^2 )),(((diff f2,t0) / ((f2 . t0) ^2 )) / (r ^2 )),(((diff f3,t0) / ((f3 . t0) ^2 )) / (r ^2 ))]|) by XCMPLX_1:48
.= - (r * |[(((diff f1,t0) / ((f1 . t0) ^2 )) / ((1 / (r ^2 )) " )),(((diff f2,t0) / ((f2 . t0) ^2 )) / (r ^2 )),(((diff f3,t0) / ((f3 . t0) ^2 )) / (r ^2 ))]|) by XCMPLX_1:219
.= - (r * |[((1 / (r ^2 )) * ((diff f1,t0) / ((f1 . t0) ^2 ))),(((diff f2,t0) / ((f2 . t0) ^2 )) / (r ^2 )),(((diff f3,t0) / ((f3 . t0) ^2 )) / (r ^2 ))]|) by XCMPLX_1:221
.= - (r * |[((1 / (r ^2 )) * ((diff f1,t0) / ((f1 . t0) ^2 ))),(((diff f2,t0) / ((f2 . t0) ^2 )) / ((1 / (r ^2 )) " )),(((diff f3,t0) / ((f3 . t0) ^2 )) / (r ^2 ))]|) by XCMPLX_1:219
.= - (r * |[((1 / (r ^2 )) * ((diff f1,t0) / ((f1 . t0) ^2 ))),((1 / (r ^2 )) * ((diff f2,t0) / ((f2 . t0) ^2 ))),(((diff f3,t0) / ((f3 . t0) ^2 )) / (r ^2 ))]|) by XCMPLX_1:221
.= - (r * |[((1 / (r ^2 )) * ((diff f1,t0) / ((f1 . t0) ^2 ))),((1 / (r ^2 )) * ((diff f2,t0) / ((f2 . t0) ^2 ))),(((diff f3,t0) / ((f3 . t0) ^2 )) / ((1 / (r ^2 )) " ))]|) by XCMPLX_1:219
.= - (r * |[((1 / (r ^2 )) * ((diff f1,t0) / ((f1 . t0) ^2 ))),((1 / (r ^2 )) * ((diff f2,t0) / ((f2 . t0) ^2 ))),((1 / (r ^2 )) * ((diff f3,t0) / ((f3 . t0) ^2 )))]|) by XCMPLX_1:221
.= - (r * ((1 / (r ^2 )) * |[((diff f1,t0) / ((f1 . t0) ^2 )),((diff f2,t0) / ((f2 . t0) ^2 )),((diff f3,t0) / ((f3 . t0) ^2 ))]|)) by LmA8
.= - ((r * (1 / (r ^2 ))) * |[((diff f1,t0) / ((f1 . t0) ^2 )),((diff f2,t0) / ((f2 . t0) ^2 )),((diff f3,t0) / ((f3 . t0) ^2 ))]|) by EUCLID_4:4
.= - (((r * 1) / (r ^2 )) * |[((diff f1,t0) / ((f1 . t0) ^2 )),((diff f2,t0) / ((f2 . t0) ^2 )),((diff f3,t0) / ((f3 . t0) ^2 ))]|) by XCMPLX_1:75
.= - (((r / r) / r) * |[((diff f1,t0) / ((f1 . t0) ^2 )),((diff f2,t0) / ((f2 . t0) ^2 )),((diff f3,t0) / ((f3 . t0) ^2 ))]|) by XCMPLX_1:79
.= - ((1 / r) * |[((diff f1,t0) / ((f1 . t0) ^2 )),((diff f2,t0) / ((f2 . t0) ^2 )),((diff f3,t0) / ((f3 . t0) ^2 ))]|) by B0, XCMPLX_1:60 ;
hence VFuncdiff ((r (#) f1) ^ ),((r (#) f2) ^ ),((r (#) f3) ^ ),t0 = - ((1 / r) * |[((diff f1,t0) / ((f1 . t0) ^2 )),((diff f2,t0) / ((f2 . t0) ^2 )),((diff f3,t0) / ((f3 . t0) ^2 ))]|) ; :: thesis: verum