let r be Real; for f1, f2, f3, g1, g2, g3 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 & g1 is_differentiable_in t0 & g2 is_differentiable_in t0 & g3 is_differentiable_in t0 & g1 . t0 <> 0 & g2 . t0 <> 0 & g3 . t0 <> 0 holds
VFuncdiff (((r (#) f1) / g1),((r (#) f2) / g2),((r (#) f3) / g3),t0) = r * |[((((diff (f1,t0)) * (g1 . t0)) - ((diff (g1,t0)) * (f1 . t0))) / ((g1 . t0) ^2)),((((diff (f2,t0)) * (g2 . t0)) - ((diff (g2,t0)) * (f2 . t0))) / ((g2 . t0) ^2)),((((diff (f3,t0)) * (g3 . t0)) - ((diff (g3,t0)) * (f3 . t0))) / ((g3 . t0) ^2))]|
let f1, f2, f3, g1, g2, g3 be PartFunc of REAL,REAL; for t0 being Real st f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 & g1 is_differentiable_in t0 & g2 is_differentiable_in t0 & g3 is_differentiable_in t0 & g1 . t0 <> 0 & g2 . t0 <> 0 & g3 . t0 <> 0 holds
VFuncdiff (((r (#) f1) / g1),((r (#) f2) / g2),((r (#) f3) / g3),t0) = r * |[((((diff (f1,t0)) * (g1 . t0)) - ((diff (g1,t0)) * (f1 . t0))) / ((g1 . t0) ^2)),((((diff (f2,t0)) * (g2 . t0)) - ((diff (g2,t0)) * (f2 . t0))) / ((g2 . t0) ^2)),((((diff (f3,t0)) * (g3 . t0)) - ((diff (g3,t0)) * (f3 . t0))) / ((g3 . t0) ^2))]|
let t0 be Real; ( f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 & g1 is_differentiable_in t0 & g2 is_differentiable_in t0 & g3 is_differentiable_in t0 & g1 . t0 <> 0 & g2 . t0 <> 0 & g3 . t0 <> 0 implies VFuncdiff (((r (#) f1) / g1),((r (#) f2) / g2),((r (#) f3) / g3),t0) = r * |[((((diff (f1,t0)) * (g1 . t0)) - ((diff (g1,t0)) * (f1 . t0))) / ((g1 . t0) ^2)),((((diff (f2,t0)) * (g2 . t0)) - ((diff (g2,t0)) * (f2 . t0))) / ((g2 . t0) ^2)),((((diff (f3,t0)) * (g3 . t0)) - ((diff (g3,t0)) * (f3 . t0))) / ((g3 . t0) ^2))]| )
assume that
A1:
( f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 )
and
A2:
( g1 is_differentiable_in t0 & g2 is_differentiable_in t0 & g3 is_differentiable_in t0 )
and
A3:
( g1 . t0 <> 0 & g2 . t0 <> 0 & g3 . t0 <> 0 )
; VFuncdiff (((r (#) f1) / g1),((r (#) f2) / g2),((r (#) f3) / g3),t0) = r * |[((((diff (f1,t0)) * (g1 . t0)) - ((diff (g1,t0)) * (f1 . t0))) / ((g1 . t0) ^2)),((((diff (f2,t0)) * (g2 . t0)) - ((diff (g2,t0)) * (f2 . t0))) / ((g2 . t0) ^2)),((((diff (f3,t0)) * (g3 . t0)) - ((diff (g3,t0)) * (f3 . t0))) / ((g3 . 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;
then VFuncdiff (((r (#) f1) / g1),((r (#) f2) / g2),((r (#) f3) / g3),t0) =
|[((((diff ((r (#) f1),t0)) * (g1 . t0)) - ((diff (g1,t0)) * ((r (#) f1) . t0))) / ((g1 . t0) ^2)),(diff (((r (#) f2) / g2),t0)),(diff (((r (#) f3) / g3),t0))]|
by A2, A3, FDIFF_2:14
.=
|[((((diff ((r (#) f1),t0)) * (g1 . t0)) - ((diff (g1,t0)) * ((r (#) f1) . t0))) / ((g1 . t0) ^2)),((((diff ((r (#) f2),t0)) * (g2 . t0)) - ((diff (g2,t0)) * ((r (#) f2) . t0))) / ((g2 . t0) ^2)),(diff (((r (#) f3) / g3),t0))]|
by A2, A3, A4, FDIFF_2:14
.=
|[((((diff ((r (#) f1),t0)) * (g1 . t0)) - ((diff (g1,t0)) * ((r (#) f1) . t0))) / ((g1 . t0) ^2)),((((diff ((r (#) f2),t0)) * (g2 . t0)) - ((diff (g2,t0)) * ((r (#) f2) . t0))) / ((g2 . t0) ^2)),((((diff ((r (#) f3),t0)) * (g3 . t0)) - ((diff (g3,t0)) * ((r (#) f3) . t0))) / ((g3 . t0) ^2))]|
by A2, A3, A4, FDIFF_2:14
.=
|[((((r * (diff (f1,t0))) * (g1 . t0)) - ((diff (g1,t0)) * ((r (#) f1) . t0))) / ((g1 . t0) ^2)),((((diff ((r (#) f2),t0)) * (g2 . t0)) - ((diff (g2,t0)) * ((r (#) f2) . t0))) / ((g2 . t0) ^2)),((((diff ((r (#) f3),t0)) * (g3 . t0)) - ((diff (g3,t0)) * ((r (#) f3) . t0))) / ((g3 . t0) ^2))]|
by A1, FDIFF_1:15
.=
|[((((r * (diff (f1,t0))) * (g1 . t0)) - ((diff (g1,t0)) * ((r (#) f1) . t0))) / ((g1 . t0) ^2)),((((r * (diff (f2,t0))) * (g2 . t0)) - ((diff (g2,t0)) * ((r (#) f2) . t0))) / ((g2 . t0) ^2)),((((diff ((r (#) f3),t0)) * (g3 . t0)) - ((diff (g3,t0)) * ((r (#) f3) . t0))) / ((g3 . t0) ^2))]|
by A1, FDIFF_1:15
.=
|[((((r * (diff (f1,t0))) * (g1 . t0)) - ((diff (g1,t0)) * ((r (#) f1) . t0))) / ((g1 . t0) ^2)),((((r * (diff (f2,t0))) * (g2 . t0)) - ((diff (g2,t0)) * ((r (#) f2) . t0))) / ((g2 . t0) ^2)),((((r * (diff (f3,t0))) * (g3 . t0)) - ((diff (g3,t0)) * ((r (#) f3) . t0))) / ((g3 . t0) ^2))]|
by A1, FDIFF_1:15
.=
|[((((r * (diff (f1,t0))) * (g1 . t0)) - ((diff (g1,t0)) * (r * (f1 . t0)))) / ((g1 . t0) ^2)),((((r * (diff (f2,t0))) * (g2 . t0)) - ((diff (g2,t0)) * ((r (#) f2) . t0))) / ((g2 . t0) ^2)),((((r * (diff (f3,t0))) * (g3 . t0)) - ((diff (g3,t0)) * ((r (#) f3) . t0))) / ((g3 . t0) ^2))]|
by VALUED_1:6
.=
|[((((r * (diff (f1,t0))) * (g1 . t0)) - ((diff (g1,t0)) * (r * (f1 . t0)))) / ((g1 . t0) ^2)),((((r * (diff (f2,t0))) * (g2 . t0)) - ((diff (g2,t0)) * (r * (f2 . t0)))) / ((g2 . t0) ^2)),((((r * (diff (f3,t0))) * (g3 . t0)) - ((diff (g3,t0)) * ((r (#) f3) . t0))) / ((g3 . t0) ^2))]|
by VALUED_1:6
.=
|[((((r * (diff (f1,t0))) * (g1 . t0)) - ((diff (g1,t0)) * (r * (f1 . t0)))) / ((g1 . t0) ^2)),((((r * (diff (f2,t0))) * (g2 . t0)) - ((diff (g2,t0)) * (r * (f2 . t0)))) / ((g2 . t0) ^2)),((((r * (diff (f3,t0))) * (g3 . t0)) - ((diff (g3,t0)) * (r * (f3 . t0)))) / ((g3 . t0) ^2))]|
by VALUED_1:6
.=
|[((r * (((diff (f1,t0)) * (g1 . t0)) - ((diff (g1,t0)) * (f1 . t0)))) / ((g1 . t0) ^2)),((r * (((diff (f2,t0)) * (g2 . t0)) - ((diff (g2,t0)) * (f2 . t0)))) / ((g2 . t0) ^2)),((r * (((diff (f3,t0)) * (g3 . t0)) - ((diff (g3,t0)) * (f3 . t0)))) / ((g3 . t0) ^2))]|
.=
|[(r * ((((diff (f1,t0)) * (g1 . t0)) - ((diff (g1,t0)) * (f1 . t0))) / ((g1 . t0) ^2))),((r * (((diff (f2,t0)) * (g2 . t0)) - ((diff (g2,t0)) * (f2 . t0)))) / ((g2 . t0) ^2)),((r * (((diff (f3,t0)) * (g3 . t0)) - ((diff (g3,t0)) * (f3 . t0)))) / ((g3 . t0) ^2))]|
by XCMPLX_1:74
.=
|[(r * ((((diff (f1,t0)) * (g1 . t0)) - ((diff (g1,t0)) * (f1 . t0))) / ((g1 . t0) ^2))),(r * ((((diff (f2,t0)) * (g2 . t0)) - ((diff (g2,t0)) * (f2 . t0))) / ((g2 . t0) ^2))),((r * (((diff (f3,t0)) * (g3 . t0)) - ((diff (g3,t0)) * (f3 . t0)))) / ((g3 . t0) ^2))]|
by XCMPLX_1:74
.=
|[(r * ((((diff (f1,t0)) * (g1 . t0)) - ((diff (g1,t0)) * (f1 . t0))) / ((g1 . t0) ^2))),(r * ((((diff (f2,t0)) * (g2 . t0)) - ((diff (g2,t0)) * (f2 . t0))) / ((g2 . t0) ^2))),(r * ((((diff (f3,t0)) * (g3 . t0)) - ((diff (g3,t0)) * (f3 . t0))) / ((g3 . t0) ^2)))]|
by XCMPLX_1:74
.=
r * |[((((diff (f1,t0)) * (g1 . t0)) - ((diff (g1,t0)) * (f1 . t0))) / ((g1 . t0) ^2)),((((diff (f2,t0)) * (g2 . t0)) - ((diff (g2,t0)) * (f2 . t0))) / ((g2 . t0) ^2)),((((diff (f3,t0)) * (g3 . t0)) - ((diff (g3,t0)) * (f3 . t0))) / ((g3 . t0) ^2))]|
by Lm6
;
hence
VFuncdiff (((r (#) f1) / g1),((r (#) f2) / g2),((r (#) f3) / g3),t0) = r * |[((((diff (f1,t0)) * (g1 . t0)) - ((diff (g1,t0)) * (f1 . t0))) / ((g1 . t0) ^2)),((((diff (f2,t0)) * (g2 . t0)) - ((diff (g2,t0)) * (f2 . t0))) / ((g2 . t0) ^2)),((((diff (f3,t0)) * (g3 . t0)) - ((diff (g3,t0)) * (f3 . t0))) / ((g3 . t0) ^2))]|
; verum