begin
theorem Lm1:
Lm3:
for p being Element of REAL 3
for r being real number holds r * p = |[(r * (p . 1)),(r * (p . 2)),(r * (p . 3))]|
Lm4:
for p1, p2 being Element of REAL 3 holds p1 + p2 = |[((p1 . 1) + (p2 . 1)),((p1 . 2) + (p2 . 2)),((p1 . 3) + (p2 . 3))]|
LmTh2:
for p being Element of REAL 3 holds
( (- p) . 1 = - (p . 1) & (- p) . 2 = - (p . 2) & (- p) . 3 = - (p . 3) )
theorem
Lm7:
for p1, p2 being Element of REAL 3 holds p1 - p2 = |[((p1 . 1) - (p2 . 1)),((p1 . 2) - (p2 . 2)),((p1 . 3) - (p2 . 3))]|
Lm8:
for p1, p2 being Element of REAL 3 holds |(p1,p2)| = (((p1 . 1) * (p2 . 1)) + ((p1 . 2) * (p2 . 2))) + ((p1 . 3) * (p2 . 3))
LmA8:
for r, x, y, z being Element of REAL holds r * |[x,y,z]| = |[(r * x),(r * y),(r * z)]|
LmA26:
for p1, p2 being Element of REAL 3 holds p1 + (- p2) = |[((p1 . 1) - (p2 . 1)),((p1 . 2) - (p2 . 2)),((p1 . 3) - (p2 . 3))]|
LmA31:
for x1, x2, x3, y1, y2, y3 being Element of REAL holds |[x1,x2,x3]| + |[y1,y2,y3]| = |[(x1 + y1),(x2 + y2),(x3 + y3)]|
LmB30:
for p1, p2 being Element of REAL 3 holds |(p1,p2)| = (((p1 . 1) * (p2 . 1)) + ((p1 . 2) * (p2 . 2))) + ((p1 . 3) * (p2 . 3))
LmAA30:
for r being Element of REAL
for p1, p2 being Element of REAL 3 holds |((r * p1),p2)| = r * |(p1,p2)|
LmB3:
for p1, p2, q1, q2 being Element of REAL 3 holds (p1 + p2) + (q1 + q2) = (p1 + q1) + (p2 + q2)
LmA62:
for p1, p2, q1, q2 being Element of REAL 3 holds (p1 + p2) - (q1 + q2) = (p1 - q1) + (p2 - q2)
LmA63:
for x1, x2, x3, y1, y2, y3 being Element of REAL holds |[x1,x2,x3]| - |[y1,y2,y3]| = |[(x1 - y1),(x2 - y2),(x3 - y3)]|
definition
func <e1> -> Element of
REAL 3
equals
|[1,0 ,0 ]|;
coherence
|[1,0 ,0 ]| is Element of REAL 3
;
func <e2> -> Element of
REAL 3
equals
|[0 ,1,0 ]|;
coherence
|[0 ,1,0 ]| is Element of REAL 3
;
func <e3> -> Element of
REAL 3
equals
|[0 ,0 ,1]|;
coherence
|[0 ,0 ,1]| is Element of REAL 3
;
end;
:: deftheorem defines <e1> EUCLID_8:def 1 :
:: deftheorem defines <e2> EUCLID_8:def 2 :
:: deftheorem defines <e3> EUCLID_8:def 3 :
LmTh8:
for x, y, z being Element of REAL
for p being Element of REAL 3 st p = |[x,y,z]| holds
|(p,p)| = ((x ^2 ) + (y ^2 )) + (z ^2 )
:: deftheorem defines <X> EUCLID_8:def 4 :
for
p1,
p2 being
Element of
REAL 3 holds
p1 <X> p2 = |[(((p1 . 2) * (p2 . 3)) - ((p1 . 3) * (p2 . 2))),(((p1 . 3) * (p2 . 1)) - ((p1 . 1) * (p2 . 3))),(((p1 . 1) * (p2 . 2)) - ((p1 . 2) * (p2 . 1)))]|;
Lm11:
for x1, x2, x3, y1, y2, y3 being Element of REAL holds |[x1,x2,x3]| <X> |[y1,y2,y3]| = |[((x2 * y3) - (x3 * y2)),((x3 * y1) - (x1 * y3)),((x1 * y2) - (x2 * y1))]|
Lm12:
for r being Element of REAL
for p1, p2 being Element of REAL 3 holds
( (r * p1) <X> p2 = r * (p1 <X> p2) & (r * p1) <X> p2 = p1 <X> (r * p2) )
theorem
begin
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem ThA11:
theorem ThA12:
theorem ThA13:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem ThA7:
theorem Th29:
theorem ThA8:
theorem
theorem
theorem
theorem ThA18:
theorem
theorem
theorem
definition
let f1,
f2,
f3 be
PartFunc of
REAL ,
REAL ;
func VFunc f1,
f2,
f3 -> Function of
REAL ,
(REAL 3) means :
Def1:
for
t being
Real holds
it . t = |[(f1 . t),(f2 . t),(f3 . t)]|;
existence
ex b1 being Function of REAL ,(REAL 3) st
for t being Real holds b1 . t = |[(f1 . t),(f2 . t),(f3 . t)]|
uniqueness
for b1, b2 being Function of REAL ,(REAL 3) st ( for t being Real holds b1 . t = |[(f1 . t),(f2 . t),(f3 . t)]| ) & ( for t being Real holds b2 . t = |[(f1 . t),(f2 . t),(f3 . t)]| ) holds
b1 = b2
end;
:: deftheorem Def1 defines VFunc EUCLID_8:def 5 :
theorem
theorem Th34:
theorem Th35:
theorem Th36:
theorem
theorem Th39:
theorem
theorem Th44:
theorem
for
p,
q being
Element of
REAL 3
for
f1,
f2,
f3,
g1,
g2,
g3 being
PartFunc of
REAL ,
REAL for
t1,
t2 being
Real st
p = (VFunc f1,f2,f3) . t1 &
q = (VFunc g1,g2,g3) . t2 &
p = q holds
(
f1 . t1 = g1 . t2 &
f2 . t1 = g2 . t2 &
f3 . t1 = g3 . t2 )
theorem
for
f1,
g1,
f2,
g2,
f3,
g3 being
PartFunc of
REAL ,
REAL for
t1,
t2 being
Real st
f1 . t1 = g1 . t2 &
f2 . t1 = g2 . t2 &
f3 . t1 = g3 . t2 holds
(VFunc f1,f2,f3) . t1 = (VFunc g1,g2,g3) . t2
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th23:
theorem
theorem Th52:
theorem Th53:
theorem
theorem
theorem Th80:
theorem
theorem
theorem
theorem
theorem
theorem Th88:
theorem Th81:
theorem
theorem Th92:
theorem Th93:
theorem ThA41:
theorem
theorem
theorem
theorem Th128:
theorem Th129:
for
x1,
x2,
x3,
y1,
y2,
y3 being
Element of
REAL holds
|[x1,x2,x3]| <X> |[y1,y2,y3]| = |[((x2 * y3) - (x3 * y2)),((x3 * y1) - (x1 * y3)),((x1 * y2) - (x2 * y1))]|
theorem
theorem Th137:
theorem Th138:
theorem
theorem
:: deftheorem defines |{ EUCLID_8:def 6 :
theorem
theorem
theorem
theorem ThA52:
theorem
theorem
begin
definition
let f1,
f2,
f3 be
PartFunc of
REAL ,
REAL ;
let t0 be
Real;
func VFuncdiff f1,
f2,
f3,
t0 -> Element of
REAL 3
equals
|[(diff f1,t0),(diff f2,t0),(diff f3,t0)]|;
coherence
|[(diff f1,t0),(diff f2,t0),(diff f3,t0)]| is Element of REAL 3
;
end;
:: deftheorem defines VFuncdiff EUCLID_8:def 7 :
for
f1,
f2,
f3 being
PartFunc of
REAL ,
REAL for
t0 being
Real holds
VFuncdiff f1,
f2,
f3,
t0 = |[(diff f1,t0),(diff f2,t0),(diff f3,t0)]|;
theorem
theorem Th57:
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 holds
VFuncdiff (f1 + g1),
(f2 + g2),
(f3 + g3),
t0 = (VFuncdiff f1,f2,f3,t0) + (VFuncdiff g1,g2,g3,t0)
theorem Th58:
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 holds
VFuncdiff (f1 - g1),
(f2 - g2),
(f3 - g3),
t0 = (VFuncdiff f1,f2,f3,t0) - (VFuncdiff g1,g2,g3,t0)
theorem Th59:
theorem Th60:
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 holds
VFuncdiff (f1 (#) g1),
(f2 (#) g2),
(f3 (#) g3),
t0 = |[((g1 . t0) * (diff f1,t0)),((g2 . t0) * (diff f2,t0)),((g3 . t0) * (diff f3,t0))]| + |[((f1 . t0) * (diff g1,t0)),((f2 . t0) * (diff g2,t0)),((f3 . t0) * (diff g3,t0))]|
theorem Th61:
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 f1 . t0 &
g2 is_differentiable_in f2 . t0 &
g3 is_differentiable_in f3 . t0 holds
VFuncdiff (g1 * f1),
(g2 * f2),
(g3 * f3),
t0 = |[((diff g1,(f1 . t0)) * (diff f1,t0)),((diff g2,(f2 . t0)) * (diff f2,t0)),((diff g3,(f3 . t0)) * (diff f3,t0))]|
theorem
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 (f1 / g1),
(f2 / g2),
(f3 / g3),
t0 = |[((((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 ))]|
theorem Th63:
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 holds
VFuncdiff (f1 ^ ),
(f2 ^ ),
(f3 ^ ),
t0 = - |[((diff f1,t0) / ((f1 . t0) ^2 )),((diff f2,t0) / ((f2 . t0) ^2 )),((diff f3,t0) / ((f3 . t0) ^2 ))]|
theorem
theorem
for
r being
Element of
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 holds
VFuncdiff (r (#) (f1 + g1)),
(r (#) (f2 + g2)),
(r (#) (f3 + g3)),
t0 = (r * (VFuncdiff f1,f2,f3,t0)) + (r * (VFuncdiff g1,g2,g3,t0))
theorem
for
r being
Element of
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 holds
VFuncdiff (r (#) (f1 - g1)),
(r (#) (f2 - g2)),
(r (#) (f3 - g3)),
t0 = (r * (VFuncdiff f1,f2,f3,t0)) - (r * (VFuncdiff g1,g2,g3,t0))
theorem
for
r being
Element of
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 holds
VFuncdiff ((r (#) f1) (#) g1),
((r (#) f2) (#) g2),
((r (#) f3) (#) g3),
t0 = (r * |[((g1 . t0) * (diff f1,t0)),((g2 . t0) * (diff f2,t0)),((g3 . t0) * (diff f3,t0))]|) + (r * |[((f1 . t0) * (diff g1,t0)),((f2 . t0) * (diff g2,t0)),((f3 . t0) * (diff g3,t0))]|)
theorem
for
r being
Element of
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 f1 . t0 &
g2 is_differentiable_in f2 . t0 &
g3 is_differentiable_in f3 . t0 holds
VFuncdiff ((r (#) g1) * f1),
((r (#) g2) * f2),
((r (#) g3) * f3),
t0 = r * |[((diff g1,(f1 . t0)) * (diff f1,t0)),((diff g2,(f2 . t0)) * (diff f2,t0)),((diff g3,(f3 . t0)) * (diff f3,t0))]|
theorem
for
r being
Element of
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 ))]|
theorem
for
r being
Element of
REAL 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 ))]|)
theorem
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 holds
VFuncdiff ((f2 (#) g3) - (f3 (#) g2)),
((f3 (#) g1) - (f1 (#) g3)),
((f1 (#) g2) - (f2 (#) g1)),
t0 = |[(((f2 . t0) * (diff g3,t0)) - ((f3 . t0) * (diff g2,t0))),(((f3 . t0) * (diff g1,t0)) - ((f1 . t0) * (diff g3,t0))),(((f1 . t0) * (diff g2,t0)) - ((f2 . t0) * (diff g1,t0)))]| + |[(((diff f2,t0) * (g3 . t0)) - ((diff f3,t0) * (g2 . t0))),(((diff f3,t0) * (g1 . t0)) - ((diff f1,t0) * (g3 . t0))),(((diff f1,t0) * (g2 . t0)) - ((diff f2,t0) * (g1 . t0)))]|
theorem
for
f1,
f2,
f3,
g1,
g2,
g3,
h1,
h2,
h3 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 &
h1 is_differentiable_in t0 &
h2 is_differentiable_in t0 &
h3 is_differentiable_in t0 holds
VFuncdiff (h1 (#) ((f2 (#) g3) - (f3 (#) g2))),
(h2 (#) ((f3 (#) g1) - (f1 (#) g3))),
(h3 (#) ((f1 (#) g2) - (f2 (#) g1))),
t0 = (|[((diff h1,t0) * (((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0)))),((diff h2,t0) * (((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0)))),((diff h3,t0) * (((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))))]| + |[((h1 . t0) * (((diff f2,t0) * (g3 . t0)) - ((diff f3,t0) * (g2 . t0)))),((h2 . t0) * (((diff f3,t0) * (g1 . t0)) - ((diff f1,t0) * (g3 . t0)))),((h3 . t0) * (((diff f1,t0) * (g2 . t0)) - ((diff f2,t0) * (g1 . t0))))]|) + |[((h1 . t0) * (((f2 . t0) * (diff g3,t0)) - ((f3 . t0) * (diff g2,t0)))),((h2 . t0) * (((f3 . t0) * (diff g1,t0)) - ((f1 . t0) * (diff g3,t0)))),((h3 . t0) * (((f1 . t0) * (diff g2,t0)) - ((f2 . t0) * (diff g1,t0))))]|
theorem
for
f1,
f2,
f3,
g1,
g2,
g3,
h1,
h2,
h3 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 &
h1 is_differentiable_in t0 &
h2 is_differentiable_in t0 &
h3 is_differentiable_in t0 holds
VFuncdiff (((h2 (#) f2) (#) g3) - ((h3 (#) f3) (#) g2)),
(((h3 (#) f3) (#) g1) - ((h1 (#) f1) (#) g3)),
(((h1 (#) f1) (#) g2) - ((h2 (#) f2) (#) g1)),
t0 = (|[((((h2 . t0) * (f2 . t0)) * (diff g3,t0)) - (((h3 . t0) * (f3 . t0)) * (diff g2,t0))),((((h3 . t0) * (f3 . t0)) * (diff g1,t0)) - (((h1 . t0) * (f1 . t0)) * (diff g3,t0))),((((h1 . t0) * (f1 . t0)) * (diff g2,t0)) - (((h2 . t0) * (f2 . t0)) * (diff g1,t0)))]| + |[((((h2 . t0) * (diff f2,t0)) * (g3 . t0)) - (((h3 . t0) * (diff f3,t0)) * (g2 . t0))),((((h3 . t0) * (diff f3,t0)) * (g1 . t0)) - (((h1 . t0) * (diff f1,t0)) * (g3 . t0))),((((h1 . t0) * (diff f1,t0)) * (g2 . t0)) - (((h2 . t0) * (diff f2,t0)) * (g1 . t0)))]|) + |[((((diff h2,t0) * (f2 . t0)) * (g3 . t0)) - (((diff h3,t0) * (f3 . t0)) * (g2 . t0))),((((diff h3,t0) * (f3 . t0)) * (g1 . t0)) - (((diff h1,t0) * (f1 . t0)) * (g3 . t0))),((((diff h1,t0) * (f1 . t0)) * (g2 . t0)) - (((diff h2,t0) * (f2 . t0)) * (g1 . t0)))]|
theorem
for
f1,
f2,
f3,
g1,
g2,
g3,
h1,
h2,
h3 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 &
h1 is_differentiable_in t0 &
h2 is_differentiable_in t0 &
h3 is_differentiable_in t0 holds
VFuncdiff ((h2 (#) ((f1 (#) g2) - (f2 (#) g1))) - (h3 (#) ((f3 (#) g1) - (f1 (#) g3)))),
((h3 (#) ((f2 (#) g3) - (f3 (#) g2))) - (h1 (#) ((f1 (#) g2) - (f2 (#) g1)))),
((h1 (#) ((f3 (#) g1) - (f1 (#) g3))) - (h2 (#) ((f2 (#) g3) - (f3 (#) g2)))),
t0 = (|[(((h2 . t0) * (((f1 . t0) * (diff g2,t0)) - ((f2 . t0) * (diff g1,t0)))) - ((h3 . t0) * (((f3 . t0) * (diff g1,t0)) - ((f1 . t0) * (diff g3,t0))))),(((h3 . t0) * (((f2 . t0) * (diff g3,t0)) - ((f3 . t0) * (diff g2,t0)))) - ((h1 . t0) * (((f1 . t0) * (diff g2,t0)) - ((f2 . t0) * (diff g1,t0))))),(((h1 . t0) * (((f3 . t0) * (diff g1,t0)) - ((f1 . t0) * (diff g3,t0)))) - ((h2 . t0) * (((f2 . t0) * (diff g3,t0)) - ((f3 . t0) * (diff g2,t0)))))]| + |[(((h2 . t0) * (((diff f1,t0) * (g2 . t0)) - ((diff f2,t0) * (g1 . t0)))) - ((h3 . t0) * (((diff f3,t0) * (g1 . t0)) - ((diff f1,t0) * (g3 . t0))))),(((h3 . t0) * (((diff f2,t0) * (g3 . t0)) - ((diff f3,t0) * (g2 . t0)))) - ((h1 . t0) * (((diff f1,t0) * (g2 . t0)) - ((diff f2,t0) * (g1 . t0))))),(((h1 . t0) * (((diff f3,t0) * (g1 . t0)) - ((diff f1,t0) * (g3 . t0)))) - ((h2 . t0) * (((diff f2,t0) * (g3 . t0)) - ((diff f3,t0) * (g2 . t0)))))]|) + |[(((diff h2,t0) * (((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0)))) - ((diff h3,t0) * (((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0))))),(((diff h3,t0) * (((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0)))) - ((diff h1,t0) * (((f1 . t0) * (g2 . t0)) - ((f2 . t0) * (g1 . t0))))),(((diff h1,t0) * (((f3 . t0) * (g1 . t0)) - ((f1 . t0) * (g3 . t0)))) - ((diff h2,t0) * (((f2 . t0) * (g3 . t0)) - ((f3 . t0) * (g2 . t0)))))]|