let r be 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
A3: 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))]|)
A4: ( r (#) f1 is_differentiable_in t0 & r (#) f2 is_differentiable_in t0 & r (#) f3 is_differentiable_in t0 ) by A1, FDIFF_1:15;
A5: (r (#) f1) . t0 = r * (f1 . t0) by VALUED_1:6;
A6: (r (#) f2) . t0 = r * (f2 . t0) by VALUED_1:6;
A7: (r (#) f3) . t0 = r * (f3 . t0) by VALUED_1:6;
then 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 A4, A5, A6, A2, A3, Th94
.= - |[((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:15
.= - |[((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:15
.= - |[((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:15
.= - |[(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:74
.= - |[(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:74
.= - |[(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:74
.= - (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 A7, A6, A5, Lm6
.= - (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:78
.= - (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:78
.= - (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:78
.= - (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:217
.= - (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:219
.= - (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:217
.= - (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: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)) / ((1 / (r ^2)) "))]|) by XCMPLX_1:217
.= - (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:219
.= - (r * ((1 / (r ^2)) * |[((diff (f1,t0)) / ((f1 . t0) ^2)),((diff (f2,t0)) / ((f2 . t0) ^2)),((diff (f3,t0)) / ((f3 . t0) ^2))]|)) by Lm6
.= - ((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:74
.= - (((r / r) / r) * |[((diff (f1,t0)) / ((f1 . t0) ^2)),((diff (f2,t0)) / ((f2 . t0) ^2)),((diff (f3,t0)) / ((f3 . t0) ^2))]|) by XCMPLX_1:78
.= - ((1 / r) * |[((diff (f1,t0)) / ((f1 . t0) ^2)),((diff (f2,t0)) / ((f2 . t0) ^2)),((diff (f3,t0)) / ((f3 . t0) ^2))]|) by A3, 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