REAL is V11() V38() V133() V134() V135() V139() set
NAT is V133() V134() V135() V136() V137() V138() V139() Element of K19(REAL)
K19(REAL) is set
K20(REAL,REAL) is Relation-like complex-yielding V124() V125() set
K19(K20(REAL,REAL)) is set
COMPLEX is V11() V38() V133() V139() set
RAT is V11() V38() V133() V134() V135() V136() V139() set
INT is V11() V38() V133() V134() V135() V136() V137() V139() set
K20(COMPLEX,COMPLEX) is Relation-like complex-yielding set
K19(K20(COMPLEX,COMPLEX)) is set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is Relation-like complex-yielding set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is set
K20(K20(REAL,REAL),REAL) is Relation-like complex-yielding V124() V125() set
K19(K20(K20(REAL,REAL),REAL)) is set
K20(RAT,RAT) is Relation-like RAT -valued complex-yielding V124() V125() set
K19(K20(RAT,RAT)) is set
K20(K20(RAT,RAT),RAT) is Relation-like RAT -valued complex-yielding V124() V125() set
K19(K20(K20(RAT,RAT),RAT)) is set
K20(INT,INT) is Relation-like RAT -valued INT -valued complex-yielding V124() V125() set
K19(K20(INT,INT)) is set
K20(K20(INT,INT),INT) is Relation-like RAT -valued INT -valued complex-yielding V124() V125() set
K19(K20(K20(INT,INT),INT)) is set
K20(NAT,NAT) is Relation-like RAT -valued INT -valued complex-yielding V124() V125() V126() set
K20(K20(NAT,NAT),NAT) is Relation-like RAT -valued INT -valued complex-yielding V124() V125() V126() set
K19(K20(K20(NAT,NAT),NAT)) is set
omega is V133() V134() V135() V136() V137() V138() V139() set
K19(omega) is set
K19(NAT) is set
K376() is V51() V79() L8()
the U1 of K376() is set
K381() is V51() V79() V101() V102() V103() V105() V155() V156() V157() V158() V159() V160() L8()
K382() is V51() V79() V103() V105() V158() V159() V160() M13(K381())
K383() is V51() V79() V101() V103() V105() V158() V159() V160() V161() M16(K381(),K382())
K385() is V51() V79() V101() V103() V105() L8()
K386() is V51() V79() V101() V103() V105() V161() M13(K385())
0 is Relation-like non-empty empty-yielding RAT -valued V9() V11() FinSequence-like FinSequence-membered complex-yielding V124() V125() V126() V133() V134() V135() V136() V137() V138() V139() set
1 is V11() ordinal natural real V33() V34() V35() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
{0,1} is V11() set
K20(1,1) is Relation-like RAT -valued INT -valued complex-yielding V124() V125() V126() set
K19(K20(1,1)) is set
K20(K20(1,1),1) is Relation-like RAT -valued INT -valued complex-yielding V124() V125() V126() set
K19(K20(K20(1,1),1)) is set
K20(K20(1,1),REAL) is Relation-like complex-yielding V124() V125() set
K19(K20(K20(1,1),REAL)) is set
2 is V11() ordinal natural real V33() V34() V35() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
K20(2,2) is Relation-like RAT -valued INT -valued complex-yielding V124() V125() V126() set
K20(K20(2,2),REAL) is Relation-like complex-yielding V124() V125() set
K19(K20(K20(2,2),REAL)) is set
TOP-REAL 2 is V51() V77() V145() V146() V163() V190() V191() V192() V193() V194() V195() V196() V202() L16()
the U1 of (TOP-REAL 2) is set
3 is V11() ordinal natural real V33() V34() V35() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
TOP-REAL 3 is V51() V77() V145() V146() V163() V190() V191() V192() V193() V194() V195() V196() V202() L16()
the U1 of (TOP-REAL 3) is set
K604() is L13()
the U1 of K604() is set
K473() is V177() L14()
K609() is V163() L13()
the U1 of K609() is set
K20( the U1 of (TOP-REAL 2), the U1 of K609()) is Relation-like set
K19(K20( the U1 of (TOP-REAL 2), the U1 of K609())) is set
0 is Relation-like non-empty empty-yielding RAT -valued V9() V11() ordinal natural real V33() V34() V35() FinSequence-like FinSequence-membered ext-real non negative complex-yielding V124() V125() V126() V133() V134() V135() V136() V137() V138() V139() Element of NAT
sqrt 0 is real V33() ext-real Element of REAL
sqrt 1 is real V33() ext-real Element of REAL
K20(NAT,REAL) is Relation-like complex-yielding V124() V125() set
K19(K20(NAT,REAL)) is set
3 -tuples_on REAL is V9() V11() FinSequence-membered FinSequenceSet of REAL
REAL 3 is V9() V11() FinSequence-membered FinSequenceSet of REAL
f1 is real set
f2 is real set
f3 is real set
<*f1,f2,f3*> is Relation-like NAT -defined V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() set
g1 is real V33() ext-real Element of REAL
g2 is real V33() ext-real Element of REAL
g3 is real V33() ext-real Element of REAL
<*g1,g2,g3*> is Relation-like NAT -defined V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() set
f1 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
f1 . 1 is real V33() ext-real Element of REAL
f1 . 2 is real V33() ext-real Element of REAL
f1 . 3 is real V33() ext-real Element of REAL
((f1 . 1),(f1 . 2),(f1 . 3)) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
f2 is real V33() ext-real Element of REAL
f3 is real V33() ext-real Element of REAL
g1 is real V33() ext-real Element of REAL
<*f2,f3,g1*> is Relation-like NAT -defined V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() set
f1 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
f1 . 1 is real V33() ext-real Element of REAL
f1 . 2 is real V33() ext-real Element of REAL
f1 . 3 is real V33() ext-real Element of REAL
f2 is real set
f2 * f1 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
K354(f2) is Relation-like V6() V26( REAL , REAL ) complex-yielding V124() V125() Element of K19(K20(REAL,REAL))
K157() is Relation-like V6() V26(K20(REAL,REAL), REAL ) complex-yielding V124() V125() Element of K19(K20(K20(REAL,REAL),REAL))
id REAL is Relation-like REAL -defined REAL -valued total complex-yielding V124() V125() Element of K19(K20(REAL,REAL))
K175(K157(),f2,(id REAL)) is set
f1 (#) K354(f2) is Relation-like NAT -defined FinSequence-like complex-yielding V124() V125() set
f2 * (f1 . 1) is real V33() ext-real Element of REAL
f2 * (f1 . 2) is real V33() ext-real Element of REAL
f2 * (f1 . 3) is real V33() ext-real Element of REAL
((f2 * (f1 . 1)),(f2 * (f1 . 2)),(f2 * (f1 . 3))) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
(f2 * f1) . 1 is real V33() ext-real Element of REAL
(f2 * f1) . 2 is real V33() ext-real Element of REAL
(f2 * f1) . 3 is real V33() ext-real Element of REAL
f1 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
f1 . 1 is real V33() ext-real Element of REAL
f1 . 2 is real V33() ext-real Element of REAL
f1 . 3 is real V33() ext-real Element of REAL
f2 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
f1 + f2 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
K155() is Relation-like V6() V26(K20(REAL,REAL), REAL ) complex-yielding V124() V125() Element of K19(K20(K20(REAL,REAL),REAL))
K173(K155(),f1,f2) is set
f2 . 1 is real V33() ext-real Element of REAL
(f1 . 1) + (f2 . 1) is real V33() ext-real Element of REAL
f2 . 2 is real V33() ext-real Element of REAL
(f1 . 2) + (f2 . 2) is real V33() ext-real Element of REAL
f2 . 3 is real V33() ext-real Element of REAL
(f1 . 3) + (f2 . 3) is real V33() ext-real Element of REAL
(((f1 . 1) + (f2 . 1)),((f1 . 2) + (f2 . 2)),((f1 . 3) + (f2 . 3))) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
(f1 + f2) . 1 is real V33() ext-real Element of REAL
(f1 + f2) . 2 is real V33() ext-real Element of REAL
(f1 + f2) . 3 is real V33() ext-real Element of REAL
f1 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
- f1 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
K101(1) is V11() V33() set
K101(1) (#) f1 is Relation-like V6() set
K153() is Relation-like V6() V26( REAL , REAL ) complex-yielding V124() V125() Element of K19(K20(REAL,REAL))
f1 (#) K153() is Relation-like NAT -defined FinSequence-like complex-yielding V124() V125() set
(- f1) . 1 is real V33() ext-real Element of REAL
f1 . 1 is real V33() ext-real Element of REAL
- (f1 . 1) is real V33() ext-real Element of REAL
(- f1) . 2 is real V33() ext-real Element of REAL
f1 . 2 is real V33() ext-real Element of REAL
- (f1 . 2) is real V33() ext-real Element of REAL
(- f1) . 3 is real V33() ext-real Element of REAL
f1 . 3 is real V33() ext-real Element of REAL
- (f1 . 3) is real V33() ext-real Element of REAL
- 1 is V11() real V33() V34() V35() ext-real Element of INT
(- 1) * (f1 . 1) is real V33() ext-real Element of REAL
(- 1) * (f1 . 2) is real V33() ext-real Element of REAL
(- 1) * (f1 . 3) is real V33() ext-real Element of REAL
(((- 1) * (f1 . 1)),((- 1) * (f1 . 2)),((- 1) * (f1 . 3))) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
((- (f1 . 1)),(- (f1 . 2)),(- (f1 . 3))) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
f1 is Relation-like NAT -defined REAL -valued V6() V38() FinSequence-like FinSubsequence-like complex-yielding V124() V125() FinSequence of REAL
len f1 is ordinal natural real V33() V34() V35() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
f1 . 1 is real V33() ext-real Element of REAL
f1 . 2 is real V33() ext-real Element of REAL
f1 . 3 is real V33() ext-real Element of REAL
f2 is real V33() ext-real Element of REAL
f3 is real V33() ext-real Element of REAL
g1 is real V33() ext-real Element of REAL
<*f2,f3,g1*> is Relation-like NAT -defined V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() set
f1 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
f1 . 1 is real V33() ext-real Element of REAL
f1 . 2 is real V33() ext-real Element of REAL
f1 . 3 is real V33() ext-real Element of REAL
f2 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
f1 - f2 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
- f2 is Relation-like V6() complex-yielding set
K101(1) is V11() V33() set
K101(1) (#) f2 is Relation-like V6() set
K153() is Relation-like V6() V26( REAL , REAL ) complex-yielding V124() V125() Element of K19(K20(REAL,REAL))
f2 (#) K153() is Relation-like NAT -defined FinSequence-like complex-yielding V124() V125() set
f1 + (- f2) is Relation-like V6() set
K156() is Relation-like V6() V26(K20(REAL,REAL), REAL ) complex-yielding V124() V125() Element of K19(K20(K20(REAL,REAL),REAL))
K155() is Relation-like V6() V26(K20(REAL,REAL), REAL ) complex-yielding V124() V125() Element of K19(K20(K20(REAL,REAL),REAL))
id REAL is Relation-like REAL -defined REAL -valued total complex-yielding V124() V125() Element of K19(K20(REAL,REAL))
K220(REAL,K155(),(id REAL),K153()) is Relation-like V6() V26(K20(REAL,REAL), REAL ) complex-yielding V124() V125() Element of K19(K20(K20(REAL,REAL),REAL))
K173(K156(),f1,f2) is set
f2 . 1 is real V33() ext-real Element of REAL
(f1 . 1) - (f2 . 1) is real V33() ext-real Element of REAL
f2 . 2 is real V33() ext-real Element of REAL
(f1 . 2) - (f2 . 2) is real V33() ext-real Element of REAL
f2 . 3 is real V33() ext-real Element of REAL
(f1 . 3) - (f2 . 3) is real V33() ext-real Element of REAL
(((f1 . 1) - (f2 . 1)),((f1 . 2) - (f2 . 2)),((f1 . 3) - (f2 . 3))) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
- f2 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
(- f2) . 1 is real V33() ext-real Element of REAL
- (f2 . 1) is real V33() ext-real Element of REAL
(- f2) . 2 is real V33() ext-real Element of REAL
- (f2 . 2) is real V33() ext-real Element of REAL
(- f2) . 3 is real V33() ext-real Element of REAL
- (f2 . 3) is real V33() ext-real Element of REAL
f1 + (- f2) is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
K173(K155(),f1,(- f2)) is set
(f1 . 1) + (- (f2 . 1)) is real V33() ext-real Element of REAL
(f1 . 2) + (- (f2 . 2)) is real V33() ext-real Element of REAL
(f1 . 3) + (- (f2 . 3)) is real V33() ext-real Element of REAL
(((f1 . 1) + (- (f2 . 1))),((f1 . 2) + (- (f2 . 2))),((f1 . 3) + (- (f2 . 3)))) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
f1 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
f1 . 1 is real V33() ext-real Element of REAL
f1 . 2 is real V33() ext-real Element of REAL
f1 . 3 is real V33() ext-real Element of REAL
f2 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
|(f1,f2)| is real V33() ext-real Element of REAL
mlt (f1,f2) is Relation-like NAT -defined REAL -valued V6() V38() FinSequence-like FinSubsequence-like complex-yielding V124() V125() FinSequence of REAL
K157() is Relation-like V6() V26(K20(REAL,REAL), REAL ) complex-yielding V124() V125() Element of K19(K20(K20(REAL,REAL),REAL))
K173(K157(),f1,f2) is set
Sum (mlt (f1,f2)) is real V33() ext-real Element of REAL
f2 . 1 is real V33() ext-real Element of REAL
(f1 . 1) * (f2 . 1) is real V33() ext-real Element of REAL
f2 . 2 is real V33() ext-real Element of REAL
(f1 . 2) * (f2 . 2) is real V33() ext-real Element of REAL
((f1 . 1) * (f2 . 1)) + ((f1 . 2) * (f2 . 2)) is real V33() ext-real Element of REAL
f2 . 3 is real V33() ext-real Element of REAL
(f1 . 3) * (f2 . 3) is real V33() ext-real Element of REAL
(((f1 . 1) * (f2 . 1)) + ((f1 . 2) * (f2 . 2))) + ((f1 . 3) * (f2 . 3)) is real V33() ext-real Element of REAL
f3 is Relation-like NAT -defined REAL -valued V6() V38() FinSequence-like FinSubsequence-like complex-yielding V124() V125() FinSequence of REAL
len f3 is ordinal natural real V33() V34() V35() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
<*(f1 . 1),(f1 . 2),(f1 . 3)*> is Relation-like NAT -defined V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() set
len <*(f1 . 1),(f1 . 2),(f1 . 3)*> is ordinal natural real V33() V34() V35() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
g1 is Relation-like NAT -defined REAL -valued V6() V38() FinSequence-like FinSubsequence-like complex-yielding V124() V125() FinSequence of REAL
len g1 is ordinal natural real V33() V34() V35() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
<*(f2 . 1),(f2 . 2),(f2 . 3)*> is Relation-like NAT -defined V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() set
len <*(f2 . 1),(f2 . 2),(f2 . 3)*> is ordinal natural real V33() V34() V35() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
f3 . 1 is real V33() ext-real Element of REAL
g1 . 1 is real V33() ext-real Element of REAL
(f3 . 1) * (g1 . 1) is real V33() ext-real Element of REAL
f3 . 2 is real V33() ext-real Element of REAL
g1 . 2 is real V33() ext-real Element of REAL
(f3 . 2) * (g1 . 2) is real V33() ext-real Element of REAL
f3 . 3 is real V33() ext-real Element of REAL
g1 . 3 is real V33() ext-real Element of REAL
(f3 . 3) * (g1 . 3) is real V33() ext-real Element of REAL
<*((f3 . 1) * (g1 . 1)),((f3 . 2) * (g1 . 2)),((f3 . 3) * (g1 . 3))*> is Relation-like NAT -defined V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() set
Sum <*((f3 . 1) * (g1 . 1)),((f3 . 2) * (g1 . 2)),((f3 . 3) * (g1 . 3))*> is real V33() set
(f1 . 3) * (g1 . 3) is real V33() ext-real Element of REAL
(((f1 . 1) * (f2 . 1)) + ((f1 . 2) * (f2 . 2))) + ((f1 . 3) * (g1 . 3)) is real V33() ext-real Element of REAL
f1 is real V33() ext-real Element of REAL
f2 is real V33() ext-real Element of REAL
f1 * f2 is real V33() ext-real Element of REAL
f3 is real V33() ext-real Element of REAL
f1 * f3 is real V33() ext-real Element of REAL
g1 is real V33() ext-real Element of REAL
(f2,f3,g1) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
f1 * (f2,f3,g1) is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
K354(f1) is Relation-like V6() V26( REAL , REAL ) complex-yielding V124() V125() Element of K19(K20(REAL,REAL))
K157() is Relation-like V6() V26(K20(REAL,REAL), REAL ) complex-yielding V124() V125() Element of K19(K20(K20(REAL,REAL),REAL))
id REAL is Relation-like REAL -defined REAL -valued total complex-yielding V124() V125() Element of K19(K20(REAL,REAL))
K175(K157(),f1,(id REAL)) is set
(f2,f3,g1) (#) K354(f1) is Relation-like NAT -defined FinSequence-like complex-yielding V124() V125() set
f1 * g1 is real V33() ext-real Element of REAL
((f1 * f2),(f1 * f3),(f1 * g1)) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
(f2,f3,g1) . 1 is real V33() ext-real Element of REAL
f1 * ((f2,f3,g1) . 1) is real V33() ext-real Element of REAL
(f2,f3,g1) . 2 is real V33() ext-real Element of REAL
f1 * ((f2,f3,g1) . 2) is real V33() ext-real Element of REAL
(f2,f3,g1) . 3 is real V33() ext-real Element of REAL
f1 * ((f2,f3,g1) . 3) is real V33() ext-real Element of REAL
((f1 * ((f2,f3,g1) . 1)),(f1 * ((f2,f3,g1) . 2)),(f1 * ((f2,f3,g1) . 3))) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
((f1 * f2),(f1 * ((f2,f3,g1) . 2)),(f1 * ((f2,f3,g1) . 3))) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
((f1 * f2),(f1 * f3),(f1 * ((f2,f3,g1) . 3))) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
f1 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
f1 . 1 is real V33() ext-real Element of REAL
f1 . 2 is real V33() ext-real Element of REAL
f1 . 3 is real V33() ext-real Element of REAL
f2 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
- f2 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
K101(1) is V11() V33() set
K101(1) (#) f2 is Relation-like V6() set
K153() is Relation-like V6() V26( REAL , REAL ) complex-yielding V124() V125() Element of K19(K20(REAL,REAL))
f2 (#) K153() is Relation-like NAT -defined FinSequence-like complex-yielding V124() V125() set
f1 + (- f2) is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
K155() is Relation-like V6() V26(K20(REAL,REAL), REAL ) complex-yielding V124() V125() Element of K19(K20(K20(REAL,REAL),REAL))
K173(K155(),f1,(- f2)) is set
f2 . 1 is real V33() ext-real Element of REAL
(f1 . 1) - (f2 . 1) is real V33() ext-real Element of REAL
f2 . 2 is real V33() ext-real Element of REAL
(f1 . 2) - (f2 . 2) is real V33() ext-real Element of REAL
f2 . 3 is real V33() ext-real Element of REAL
(f1 . 3) - (f2 . 3) is real V33() ext-real Element of REAL
(((f1 . 1) - (f2 . 1)),((f1 . 2) - (f2 . 2)),((f1 . 3) - (f2 . 3))) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
- 1 is V11() real V33() V34() V35() ext-real Element of INT
(- 1) * (f2 . 1) is real V33() ext-real Element of REAL
(- 1) * (f2 . 2) is real V33() ext-real Element of REAL
(- 1) * (f2 . 3) is real V33() ext-real Element of REAL
(((- 1) * (f2 . 1)),((- 1) * (f2 . 2)),((- 1) * (f2 . 3))) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
- (f2 . 1) is real V33() ext-real Element of REAL
- (f2 . 2) is real V33() ext-real Element of REAL
- (f2 . 3) is real V33() ext-real Element of REAL
((- (f2 . 1)),(- (f2 . 2)),(- (f2 . 3))) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
(- f2) . 1 is real V33() ext-real Element of REAL
(f1 . 1) + ((- f2) . 1) is real V33() ext-real Element of REAL
(- f2) . 2 is real V33() ext-real Element of REAL
(f1 . 2) + ((- f2) . 2) is real V33() ext-real Element of REAL
(- f2) . 3 is real V33() ext-real Element of REAL
(f1 . 3) + ((- f2) . 3) is real V33() ext-real Element of REAL
(((f1 . 1) + ((- f2) . 1)),((f1 . 2) + ((- f2) . 2)),((f1 . 3) + ((- f2) . 3))) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
(f1 . 1) + (- (f2 . 1)) is real V33() ext-real Element of REAL
(((f1 . 1) + (- (f2 . 1))),((f1 . 2) + ((- f2) . 2)),((f1 . 3) + ((- f2) . 3))) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
(f1 . 2) + (- (f2 . 2)) is real V33() ext-real Element of REAL
(((f1 . 1) + (- (f2 . 1))),((f1 . 2) + (- (f2 . 2))),((f1 . 3) + ((- f2) . 3))) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
(f1 . 3) + (- (f2 . 3)) is real V33() ext-real Element of REAL
(((f1 . 1) + (- (f2 . 1))),((f1 . 2) + (- (f2 . 2))),((f1 . 3) + (- (f2 . 3)))) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
f1 is real V33() ext-real Element of REAL
f2 is real V33() ext-real Element of REAL
f3 is real V33() ext-real Element of REAL
(f1,f2,f3) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
g1 is real V33() ext-real Element of REAL
f1 + g1 is real V33() ext-real Element of REAL
g2 is real V33() ext-real Element of REAL
f2 + g2 is real V33() ext-real Element of REAL
g3 is real V33() ext-real Element of REAL
(g1,g2,g3) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
(f1,f2,f3) + (g1,g2,g3) is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
K155() is Relation-like V6() V26(K20(REAL,REAL), REAL ) complex-yielding V124() V125() Element of K19(K20(K20(REAL,REAL),REAL))
K173(K155(),(f1,f2,f3),(g1,g2,g3)) is set
f3 + g3 is real V33() ext-real Element of REAL
((f1 + g1),(f2 + g2),(f3 + g3)) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
(g1,g2,g3) . 1 is real V33() ext-real Element of REAL
(g1,g2,g3) . 2 is real V33() ext-real Element of REAL
(g1,g2,g3) . 3 is real V33() ext-real Element of REAL
(f1,f2,f3) . 1 is real V33() ext-real Element of REAL
((f1,f2,f3) . 1) + ((g1,g2,g3) . 1) is real V33() ext-real Element of REAL
(f1,f2,f3) . 2 is real V33() ext-real Element of REAL
((f1,f2,f3) . 2) + ((g1,g2,g3) . 2) is real V33() ext-real Element of REAL
(f1,f2,f3) . 3 is real V33() ext-real Element of REAL
((f1,f2,f3) . 3) + ((g1,g2,g3) . 3) is real V33() ext-real Element of REAL
f1 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
f2 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
f1 + f2 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
K155() is Relation-like V6() V26(K20(REAL,REAL), REAL ) complex-yielding V124() V125() Element of K19(K20(K20(REAL,REAL),REAL))
K173(K155(),f1,f2) is set
f3 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
f1 + f3 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
K173(K155(),f1,f3) is set
g1 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
f3 + g1 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
K173(K155(),f3,g1) is set
(f1 + f2) + (f3 + g1) is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
K173(K155(),(f1 + f2),(f3 + g1)) is set
f2 + g1 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
K173(K155(),f2,g1) is set
(f1 + f3) + (f2 + g1) is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
K173(K155(),(f1 + f3),(f2 + g1)) is set
(f1 + f2) + f3 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
K173(K155(),(f1 + f2),f3) is set
((f1 + f2) + f3) + g1 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
K173(K155(),((f1 + f2) + f3),g1) is set
(f1 + f3) + f2 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
K173(K155(),(f1 + f3),f2) is set
((f1 + f3) + f2) + g1 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
K173(K155(),((f1 + f3) + f2),g1) is set
f1 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
f2 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
f1 + f2 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
K155() is Relation-like V6() V26(K20(REAL,REAL), REAL ) complex-yielding V124() V125() Element of K19(K20(K20(REAL,REAL),REAL))
K173(K155(),f1,f2) is set
f3 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
f1 - f3 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
- f3 is Relation-like V6() complex-yielding set
K101(1) is V11() V33() set
K101(1) (#) f3 is Relation-like V6() set
K153() is Relation-like V6() V26( REAL , REAL ) complex-yielding V124() V125() Element of K19(K20(REAL,REAL))
f3 (#) K153() is Relation-like NAT -defined FinSequence-like complex-yielding V124() V125() set
f1 + (- f3) is Relation-like V6() set
K156() is Relation-like V6() V26(K20(REAL,REAL), REAL ) complex-yielding V124() V125() Element of K19(K20(K20(REAL,REAL),REAL))
id REAL is Relation-like REAL -defined REAL -valued total complex-yielding V124() V125() Element of K19(K20(REAL,REAL))
K220(REAL,K155(),(id REAL),K153()) is Relation-like V6() V26(K20(REAL,REAL), REAL ) complex-yielding V124() V125() Element of K19(K20(K20(REAL,REAL),REAL))
K173(K156(),f1,f3) is set
g1 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
f3 + g1 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
K173(K155(),f3,g1) is set
(f1 + f2) - (f3 + g1) is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
- (f3 + g1) is Relation-like V6() complex-yielding set
K101(1) (#) (f3 + g1) is Relation-like V6() set
(f3 + g1) (#) K153() is Relation-like NAT -defined FinSequence-like complex-yielding V124() V125() set
(f1 + f2) + (- (f3 + g1)) is Relation-like V6() set
K173(K156(),(f1 + f2),(f3 + g1)) is set
f2 - g1 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
- g1 is Relation-like V6() complex-yielding set
K101(1) (#) g1 is Relation-like V6() set
g1 (#) K153() is Relation-like NAT -defined FinSequence-like complex-yielding V124() V125() set
f2 + (- g1) is Relation-like V6() set
K173(K156(),f2,g1) is set
(f1 - f3) + (f2 - g1) is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
K173(K155(),(f1 - f3),(f2 - g1)) is set
(f1 + f2) - f3 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
(f1 + f2) + (- f3) is Relation-like V6() set
K173(K156(),(f1 + f2),f3) is set
((f1 + f2) - f3) - g1 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
((f1 + f2) - f3) + (- g1) is Relation-like V6() set
K173(K156(),((f1 + f2) - f3),g1) is set
- f3 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
- g1 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
(- f3) + (- g1) is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
K173(K155(),(- f3),(- g1)) is set
(f1 + f2) + ((- f3) + (- g1)) is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
K173(K155(),(f1 + f2),((- f3) + (- g1))) is set
f1 is real V33() ext-real Element of REAL
f2 is real V33() ext-real Element of REAL
f3 is real V33() ext-real Element of REAL
(f1,f2,f3) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
g1 is real V33() ext-real Element of REAL
f1 - g1 is real V33() ext-real Element of REAL
g2 is real V33() ext-real Element of REAL
f2 - g2 is real V33() ext-real Element of REAL
g3 is real V33() ext-real Element of REAL
(g1,g2,g3) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
(f1,f2,f3) - (g1,g2,g3) is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
- (g1,g2,g3) is Relation-like V6() complex-yielding set
K101(1) is V11() V33() set
K101(1) (#) (g1,g2,g3) is Relation-like V6() set
K153() is Relation-like V6() V26( REAL , REAL ) complex-yielding V124() V125() Element of K19(K20(REAL,REAL))
(g1,g2,g3) (#) K153() is Relation-like NAT -defined FinSequence-like complex-yielding V124() V125() set
(f1,f2,f3) + (- (g1,g2,g3)) is Relation-like V6() set
K156() is Relation-like V6() V26(K20(REAL,REAL), REAL ) complex-yielding V124() V125() Element of K19(K20(K20(REAL,REAL),REAL))
K155() is Relation-like V6() V26(K20(REAL,REAL), REAL ) complex-yielding V124() V125() Element of K19(K20(K20(REAL,REAL),REAL))
id REAL is Relation-like REAL -defined REAL -valued total complex-yielding V124() V125() Element of K19(K20(REAL,REAL))
K220(REAL,K155(),(id REAL),K153()) is Relation-like V6() V26(K20(REAL,REAL), REAL ) complex-yielding V124() V125() Element of K19(K20(K20(REAL,REAL),REAL))
K173(K156(),(f1,f2,f3),(g1,g2,g3)) is set
f3 - g3 is real V33() ext-real Element of REAL
((f1 - g1),(f2 - g2),(f3 - g3)) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
(g1,g2,g3) . 1 is real V33() ext-real Element of REAL
(g1,g2,g3) . 2 is real V33() ext-real Element of REAL
(g1,g2,g3) . 3 is real V33() ext-real Element of REAL
(f1,f2,f3) . 1 is real V33() ext-real Element of REAL
((f1,f2,f3) . 1) - ((g1,g2,g3) . 1) is real V33() ext-real Element of REAL
(f1,f2,f3) . 2 is real V33() ext-real Element of REAL
((f1,f2,f3) . 2) - ((g1,g2,g3) . 2) is real V33() ext-real Element of REAL
(f1,f2,f3) . 3 is real V33() ext-real Element of REAL
((f1,f2,f3) . 3) - ((g1,g2,g3) . 3) is real V33() ext-real Element of REAL
(1,0,0) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
(0,1,0) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
(0,0,1) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
() is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
() is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
() is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
f1 is real V33() ext-real Element of REAL
f1 ^2 is real V33() ext-real Element of REAL
K100(f1,f1) is V33() set
f2 is real V33() ext-real Element of REAL
f2 ^2 is real V33() ext-real Element of REAL
K100(f2,f2) is V33() set
(f1 ^2) + (f2 ^2) is real V33() ext-real Element of REAL
f3 is real V33() ext-real Element of REAL
(f1,f2,f3) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
f3 ^2 is real V33() ext-real Element of REAL
K100(f3,f3) is V33() set
((f1 ^2) + (f2 ^2)) + (f3 ^2) is real V33() ext-real Element of REAL
g1 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
|(g1,g1)| is real V33() ext-real Element of REAL
mlt (g1,g1) is Relation-like NAT -defined REAL -valued V6() V38() FinSequence-like FinSubsequence-like complex-yielding V124() V125() FinSequence of REAL
K157() is Relation-like V6() V26(K20(REAL,REAL), REAL ) complex-yielding V124() V125() Element of K19(K20(K20(REAL,REAL),REAL))
K173(K157(),g1,g1) is set
Sum (mlt (g1,g1)) is real V33() ext-real Element of REAL
g1 . 1 is real V33() ext-real Element of REAL
g1 . 2 is real V33() ext-real Element of REAL
g1 . 3 is real V33() ext-real Element of REAL
f1 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
f1 . 2 is real V33() ext-real Element of REAL
f2 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
f2 . 3 is real V33() ext-real Element of REAL
(f1 . 2) * (f2 . 3) is real V33() ext-real Element of REAL
f1 . 3 is real V33() ext-real Element of REAL
f2 . 2 is real V33() ext-real Element of REAL
(f1 . 3) * (f2 . 2) is real V33() ext-real Element of REAL
((f1 . 2) * (f2 . 3)) - ((f1 . 3) * (f2 . 2)) is real V33() ext-real Element of REAL
f2 . 1 is real V33() ext-real Element of REAL
(f1 . 3) * (f2 . 1) is real V33() ext-real Element of REAL
f1 . 1 is real V33() ext-real Element of REAL
(f1 . 1) * (f2 . 3) is real V33() ext-real Element of REAL
((f1 . 3) * (f2 . 1)) - ((f1 . 1) * (f2 . 3)) is real V33() ext-real Element of REAL
(f1 . 1) * (f2 . 2) is real V33() ext-real Element of REAL
(f1 . 2) * (f2 . 1) is real V33() ext-real Element of REAL
((f1 . 1) * (f2 . 2)) - ((f1 . 2) * (f2 . 1)) is real V33() ext-real Element of REAL
((((f1 . 2) * (f2 . 3)) - ((f1 . 3) * (f2 . 2))),(((f1 . 3) * (f2 . 1)) - ((f1 . 1) * (f2 . 3))),(((f1 . 1) * (f2 . 2)) - ((f1 . 2) * (f2 . 1)))) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
f1 is real V33() ext-real Element of REAL
f2 is real V33() ext-real Element of REAL
f3 is real V33() ext-real Element of REAL
(f1,f2,f3) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
g1 is real V33() ext-real Element of REAL
f3 * g1 is real V33() ext-real Element of REAL
f2 * g1 is real V33() ext-real Element of REAL
g2 is real V33() ext-real Element of REAL
f3 * g2 is real V33() ext-real Element of REAL
f1 * g2 is real V33() ext-real Element of REAL
(f1 * g2) - (f2 * g1) is real V33() ext-real Element of REAL
g3 is real V33() ext-real Element of REAL
(g1,g2,g3) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
((f1,f2,f3),(g1,g2,g3)) is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
(f1,f2,f3) . 2 is real V33() ext-real Element of REAL
(g1,g2,g3) . 3 is real V33() ext-real Element of REAL
((f1,f2,f3) . 2) * ((g1,g2,g3) . 3) is real V33() ext-real Element of REAL
(f1,f2,f3) . 3 is real V33() ext-real Element of REAL
(g1,g2,g3) . 2 is real V33() ext-real Element of REAL
((f1,f2,f3) . 3) * ((g1,g2,g3) . 2) is real V33() ext-real Element of REAL
(((f1,f2,f3) . 2) * ((g1,g2,g3) . 3)) - (((f1,f2,f3) . 3) * ((g1,g2,g3) . 2)) is real V33() ext-real Element of REAL
(g1,g2,g3) . 1 is real V33() ext-real Element of REAL
((f1,f2,f3) . 3) * ((g1,g2,g3) . 1) is real V33() ext-real Element of REAL
(f1,f2,f3) . 1 is real V33() ext-real Element of REAL
((f1,f2,f3) . 1) * ((g1,g2,g3) . 3) is real V33() ext-real Element of REAL
(((f1,f2,f3) . 3) * ((g1,g2,g3) . 1)) - (((f1,f2,f3) . 1) * ((g1,g2,g3) . 3)) is real V33() ext-real Element of REAL
((f1,f2,f3) . 1) * ((g1,g2,g3) . 2) is real V33() ext-real Element of REAL
((f1,f2,f3) . 2) * ((g1,g2,g3) . 1) is real V33() ext-real Element of REAL
(((f1,f2,f3) . 1) * ((g1,g2,g3) . 2)) - (((f1,f2,f3) . 2) * ((g1,g2,g3) . 1)) is real V33() ext-real Element of REAL
(((((f1,f2,f3) . 2) * ((g1,g2,g3) . 3)) - (((f1,f2,f3) . 3) * ((g1,g2,g3) . 2))),((((f1,f2,f3) . 3) * ((g1,g2,g3) . 1)) - (((f1,f2,f3) . 1) * ((g1,g2,g3) . 3))),((((f1,f2,f3) . 1) * ((g1,g2,g3) . 2)) - (((f1,f2,f3) . 2) * ((g1,g2,g3) . 1)))) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
f2 * g3 is real V33() ext-real Element of REAL
(f2 * g3) - (f3 * g2) is real V33() ext-real Element of REAL
f1 * g3 is real V33() ext-real Element of REAL
(f3 * g1) - (f1 * g3) is real V33() ext-real Element of REAL
(((f2 * g3) - (f3 * g2)),((f3 * g1) - (f1 * g3)),((f1 * g2) - (f2 * g1))) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
f1 is real V33() ext-real Element of REAL
f2 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
f1 * f2 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
K354(f1) is Relation-like V6() V26( REAL , REAL ) complex-yielding V124() V125() Element of K19(K20(REAL,REAL))
K157() is Relation-like V6() V26(K20(REAL,REAL), REAL ) complex-yielding V124() V125() Element of K19(K20(K20(REAL,REAL),REAL))
id REAL is Relation-like REAL -defined REAL -valued total complex-yielding V124() V125() Element of K19(K20(REAL,REAL))
K175(K157(),f1,(id REAL)) is set
f2 (#) K354(f1) is Relation-like NAT -defined FinSequence-like complex-yielding V124() V125() set
f3 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
((f1 * f2),f3) is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
(f1 * f2) . 2 is real V33() ext-real Element of REAL
f3 . 3 is real V33() ext-real Element of REAL
((f1 * f2) . 2) * (f3 . 3) is real V33() ext-real Element of REAL
(f1 * f2) . 3 is real V33() ext-real Element of REAL
f3 . 2 is real V33() ext-real Element of REAL
((f1 * f2) . 3) * (f3 . 2) is real V33() ext-real Element of REAL
(((f1 * f2) . 2) * (f3 . 3)) - (((f1 * f2) . 3) * (f3 . 2)) is real V33() ext-real Element of REAL
f3 . 1 is real V33() ext-real Element of REAL
((f1 * f2) . 3) * (f3 . 1) is real V33() ext-real Element of REAL
(f1 * f2) . 1 is real V33() ext-real Element of REAL
((f1 * f2) . 1) * (f3 . 3) is real V33() ext-real Element of REAL
(((f1 * f2) . 3) * (f3 . 1)) - (((f1 * f2) . 1) * (f3 . 3)) is real V33() ext-real Element of REAL
((f1 * f2) . 1) * (f3 . 2) is real V33() ext-real Element of REAL
((f1 * f2) . 2) * (f3 . 1) is real V33() ext-real Element of REAL
(((f1 * f2) . 1) * (f3 . 2)) - (((f1 * f2) . 2) * (f3 . 1)) is real V33() ext-real Element of REAL
(((((f1 * f2) . 2) * (f3 . 3)) - (((f1 * f2) . 3) * (f3 . 2))),((((f1 * f2) . 3) * (f3 . 1)) - (((f1 * f2) . 1) * (f3 . 3))),((((f1 * f2) . 1) * (f3 . 2)) - (((f1 * f2) . 2) * (f3 . 1)))) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
(f2,f3) is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
f2 . 2 is real V33() ext-real Element of REAL
(f2 . 2) * (f3 . 3) is real V33() ext-real Element of REAL
f2 . 3 is real V33() ext-real Element of REAL
(f2 . 3) * (f3 . 2) is real V33() ext-real Element of REAL
((f2 . 2) * (f3 . 3)) - ((f2 . 3) * (f3 . 2)) is real V33() ext-real Element of REAL
(f2 . 3) * (f3 . 1) is real V33() ext-real Element of REAL
f2 . 1 is real V33() ext-real Element of REAL
(f2 . 1) * (f3 . 3) is real V33() ext-real Element of REAL
((f2 . 3) * (f3 . 1)) - ((f2 . 1) * (f3 . 3)) is real V33() ext-real Element of REAL
(f2 . 1) * (f3 . 2) is real V33() ext-real Element of REAL
(f2 . 2) * (f3 . 1) is real V33() ext-real Element of REAL
((f2 . 1) * (f3 . 2)) - ((f2 . 2) * (f3 . 1)) is real V33() ext-real Element of REAL
((((f2 . 2) * (f3 . 3)) - ((f2 . 3) * (f3 . 2))),(((f2 . 3) * (f3 . 1)) - ((f2 . 1) * (f3 . 3))),(((f2 . 1) * (f3 . 2)) - ((f2 . 2) * (f3 . 1)))) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
f1 * (f2,f3) is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
(f2,f3) (#) K354(f1) is Relation-like NAT -defined FinSequence-like complex-yielding V124() V125() set
f1 * f3 is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
f3 (#) K354(f1) is Relation-like NAT -defined FinSequence-like complex-yielding V124() V125() set
(f2,(f1 * f3)) is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
(f1 * f3) . 3 is real V33() ext-real Element of REAL
(f2 . 2) * ((f1 * f3) . 3) is real V33() ext-real Element of REAL
(f1 * f3) . 2 is real V33() ext-real Element of REAL
(f2 . 3) * ((f1 * f3) . 2) is real V33() ext-real Element of REAL
((f2 . 2) * ((f1 * f3) . 3)) - ((f2 . 3) * ((f1 * f3) . 2)) is real V33() ext-real Element of REAL
(f1 * f3) . 1 is real V33() ext-real Element of REAL
(f2 . 3) * ((f1 * f3) . 1) is real V33() ext-real Element of REAL
(f2 . 1) * ((f1 * f3) . 3) is real V33() ext-real Element of REAL
((f2 . 3) * ((f1 * f3) . 1)) - ((f2 . 1) * ((f1 * f3) . 3)) is real V33() ext-real Element of REAL
(f2 . 1) * ((f1 * f3) . 2) is real V33() ext-real Element of REAL
(f2 . 2) * ((f1 * f3) . 1) is real V33() ext-real Element of REAL
((f2 . 1) * ((f1 * f3) . 2)) - ((f2 . 2) * ((f1 * f3) . 1)) is real V33() ext-real Element of REAL
((((f2 . 2) * ((f1 * f3) . 3)) - ((f2 . 3) * ((f1 * f3) . 2))),(((f2 . 3) * ((f1 * f3) . 1)) - ((f2 . 1) * ((f1 * f3) . 3))),(((f2 . 1) * ((f1 * f3) . 2)) - ((f2 . 2) * ((f1 * f3) . 1)))) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
(f2,f3) . 1 is real V33() ext-real Element of REAL
(f2,f3) . 2 is real V33() ext-real Element of REAL
(f2,f3) . 3 is real V33() ext-real Element of REAL
f1 * (f2 . 1) is real V33() ext-real Element of REAL
f1 * (f2 . 2) is real V33() ext-real Element of REAL
f1 * (f2 . 3) is real V33() ext-real Element of REAL
((f1 * (f2 . 1)),(f1 * (f2 . 2)),(f1 * (f2 . 3))) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
(((f1 * (f2 . 1)),(f1 * (f2 . 2)),(f1 * (f2 . 3))),f3) is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
((f1 * (f2 . 1)),(f1 * (f2 . 2)),(f1 * (f2 . 3))) . 2 is real V33() ext-real Element of REAL
(((f1 * (f2 . 1)),(f1 * (f2 . 2)),(f1 * (f2 . 3))) . 2) * (f3 . 3) is real V33() ext-real Element of REAL
((f1 * (f2 . 1)),(f1 * (f2 . 2)),(f1 * (f2 . 3))) . 3 is real V33() ext-real Element of REAL
(((f1 * (f2 . 1)),(f1 * (f2 . 2)),(f1 * (f2 . 3))) . 3) * (f3 . 2) is real V33() ext-real Element of REAL
((((f1 * (f2 . 1)),(f1 * (f2 . 2)),(f1 * (f2 . 3))) . 2) * (f3 . 3)) - ((((f1 * (f2 . 1)),(f1 * (f2 . 2)),(f1 * (f2 . 3))) . 3) * (f3 . 2)) is real V33() ext-real Element of REAL
(((f1 * (f2 . 1)),(f1 * (f2 . 2)),(f1 * (f2 . 3))) . 3) * (f3 . 1) is real V33() ext-real Element of REAL
((f1 * (f2 . 1)),(f1 * (f2 . 2)),(f1 * (f2 . 3))) . 1 is real V33() ext-real Element of REAL
(((f1 * (f2 . 1)),(f1 * (f2 . 2)),(f1 * (f2 . 3))) . 1) * (f3 . 3) is real V33() ext-real Element of REAL
((((f1 * (f2 . 1)),(f1 * (f2 . 2)),(f1 * (f2 . 3))) . 3) * (f3 . 1)) - ((((f1 * (f2 . 1)),(f1 * (f2 . 2)),(f1 * (f2 . 3))) . 1) * (f3 . 3)) is real V33() ext-real Element of REAL
(((f1 * (f2 . 1)),(f1 * (f2 . 2)),(f1 * (f2 . 3))) . 1) * (f3 . 2) is real V33() ext-real Element of REAL
(((f1 * (f2 . 1)),(f1 * (f2 . 2)),(f1 * (f2 . 3))) . 2) * (f3 . 1) is real V33() ext-real Element of REAL
((((f1 * (f2 . 1)),(f1 * (f2 . 2)),(f1 * (f2 . 3))) . 1) * (f3 . 2)) - ((((f1 * (f2 . 1)),(f1 * (f2 . 2)),(f1 * (f2 . 3))) . 2) * (f3 . 1)) is real V33() ext-real Element of REAL
((((((f1 * (f2 . 1)),(f1 * (f2 . 2)),(f1 * (f2 . 3))) . 2) * (f3 . 3)) - ((((f1 * (f2 . 1)),(f1 * (f2 . 2)),(f1 * (f2 . 3))) . 3) * (f3 . 2))),(((((f1 * (f2 . 1)),(f1 * (f2 . 2)),(f1 * (f2 . 3))) . 3) * (f3 . 1)) - ((((f1 * (f2 . 1)),(f1 * (f2 . 2)),(f1 * (f2 . 3))) . 1) * (f3 . 3))),(((((f1 * (f2 . 1)),(f1 * (f2 . 2)),(f1 * (f2 . 3))) . 1) * (f3 . 2)) - ((((f1 * (f2 . 1)),(f1 * (f2 . 2)),(f1 * (f2 . 3))) . 2) * (f3 . 1)))) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
((f3 . 1),(f3 . 2),(f3 . 3)) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
(((f1 * (f2 . 1)),(f1 * (f2 . 2)),(f1 * (f2 . 3))),((f3 . 1),(f3 . 2),(f3 . 3))) is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
((f3 . 1),(f3 . 2),(f3 . 3)) . 3 is real V33() ext-real Element of REAL
(((f1 * (f2 . 1)),(f1 * (f2 . 2)),(f1 * (f2 . 3))) . 2) * (((f3 . 1),(f3 . 2),(f3 . 3)) . 3) is real V33() ext-real Element of REAL
((f3 . 1),(f3 . 2),(f3 . 3)) . 2 is real V33() ext-real Element of REAL
(((f1 * (f2 . 1)),(f1 * (f2 . 2)),(f1 * (f2 . 3))) . 3) * (((f3 . 1),(f3 . 2),(f3 . 3)) . 2) is real V33() ext-real Element of REAL
((((f1 * (f2 . 1)),(f1 * (f2 . 2)),(f1 * (f2 . 3))) . 2) * (((f3 . 1),(f3 . 2),(f3 . 3)) . 3)) - ((((f1 * (f2 . 1)),(f1 * (f2 . 2)),(f1 * (f2 . 3))) . 3) * (((f3 . 1),(f3 . 2),(f3 . 3)) . 2)) is real V33() ext-real Element of REAL
((f3 . 1),(f3 . 2),(f3 . 3)) . 1 is real V33() ext-real Element of REAL
(((f1 * (f2 . 1)),(f1 * (f2 . 2)),(f1 * (f2 . 3))) . 3) * (((f3 . 1),(f3 . 2),(f3 . 3)) . 1) is real V33() ext-real Element of REAL
(((f1 * (f2 . 1)),(f1 * (f2 . 2)),(f1 * (f2 . 3))) . 1) * (((f3 . 1),(f3 . 2),(f3 . 3)) . 3) is real V33() ext-real Element of REAL
((((f1 * (f2 . 1)),(f1 * (f2 . 2)),(f1 * (f2 . 3))) . 3) * (((f3 . 1),(f3 . 2),(f3 . 3)) . 1)) - ((((f1 * (f2 . 1)),(f1 * (f2 . 2)),(f1 * (f2 . 3))) . 1) * (((f3 . 1),(f3 . 2),(f3 . 3)) . 3)) is real V33() ext-real Element of REAL
(((f1 * (f2 . 1)),(f1 * (f2 . 2)),(f1 * (f2 . 3))) . 1) * (((f3 . 1),(f3 . 2),(f3 . 3)) . 2) is real V33() ext-real Element of REAL
(((f1 * (f2 . 1)),(f1 * (f2 . 2)),(f1 * (f2 . 3))) . 2) * (((f3 . 1),(f3 . 2),(f3 . 3)) . 1) is real V33() ext-real Element of REAL
((((f1 * (f2 . 1)),(f1 * (f2 . 2)),(f1 * (f2 . 3))) . 1) * (((f3 . 1),(f3 . 2),(f3 . 3)) . 2)) - ((((f1 * (f2 . 1)),(f1 * (f2 . 2)),(f1 * (f2 . 3))) . 2) * (((f3 . 1),(f3 . 2),(f3 . 3)) . 1)) is real V33() ext-real Element of REAL
((((((f1 * (f2 . 1)),(f1 * (f2 . 2)),(f1 * (f2 . 3))) . 2) * (((f3 . 1),(f3 . 2),(f3 . 3)) . 3)) - ((((f1 * (f2 . 1)),(f1 * (f2 . 2)),(f1 * (f2 . 3))) . 3) * (((f3 . 1),(f3 . 2),(f3 . 3)) . 2))),(((((f1 * (f2 . 1)),(f1 * (f2 . 2)),(f1 * (f2 . 3))) . 3) * (((f3 . 1),(f3 . 2),(f3 . 3)) . 1)) - ((((f1 * (f2 . 1)),(f1 * (f2 . 2)),(f1 * (f2 . 3))) . 1) * (((f3 . 1),(f3 . 2),(f3 . 3)) . 3))),(((((f1 * (f2 . 1)),(f1 * (f2 . 2)),(f1 * (f2 . 3))) . 1) * (((f3 . 1),(f3 . 2),(f3 . 3)) . 2)) - ((((f1 * (f2 . 1)),(f1 * (f2 . 2)),(f1 * (f2 . 3))) . 2) * (((f3 . 1),(f3 . 2),(f3 . 3)) . 1)))) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
(f1 * (f2 . 2)) * (f3 . 3) is real V33() ext-real Element of REAL
(f1 * (f2 . 3)) * (f3 . 2) is real V33() ext-real Element of REAL
((f1 * (f2 . 2)) * (f3 . 3)) - ((f1 * (f2 . 3)) * (f3 . 2)) is real V33() ext-real Element of REAL
(f1 * (f2 . 3)) * (f3 . 1) is real V33() ext-real Element of REAL
(f1 * (f2 . 1)) * (f3 . 3) is real V33() ext-real Element of REAL
((f1 * (f2 . 3)) * (f3 . 1)) - ((f1 * (f2 . 1)) * (f3 . 3)) is real V33() ext-real Element of REAL
(f1 * (f2 . 1)) * (f3 . 2) is real V33() ext-real Element of REAL
(f1 * (f2 . 2)) * (f3 . 1) is real V33() ext-real Element of REAL
((f1 * (f2 . 1)) * (f3 . 2)) - ((f1 * (f2 . 2)) * (f3 . 1)) is real V33() ext-real Element of REAL
((((f1 * (f2 . 2)) * (f3 . 3)) - ((f1 * (f2 . 3)) * (f3 . 2))),(((f1 * (f2 . 3)) * (f3 . 1)) - ((f1 * (f2 . 1)) * (f3 . 3))),(((f1 * (f2 . 1)) * (f3 . 2)) - ((f1 * (f2 . 2)) * (f3 . 1)))) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
f1 * ((f2,f3) . 1) is real V33() ext-real Element of REAL
f1 * ((f2,f3) . 2) is real V33() ext-real Element of REAL
f1 * ((f2,f3) . 3) is real V33() ext-real Element of REAL
((f1 * ((f2,f3) . 1)),(f1 * ((f2,f3) . 2)),(f1 * ((f2,f3) . 3))) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
f1 * (f3 . 3) is real V33() ext-real Element of REAL
(f2 . 2) * (f1 * (f3 . 3)) is real V33() ext-real Element of REAL
f1 * (f3 . 2) is real V33() ext-real Element of REAL
(f2 . 3) * (f1 * (f3 . 2)) is real V33() ext-real Element of REAL
((f2 . 2) * (f1 * (f3 . 3))) - ((f2 . 3) * (f1 * (f3 . 2))) is real V33() ext-real Element of REAL
f1 * (f3 . 1) is real V33() ext-real Element of REAL
(f2 . 3) * (f1 * (f3 . 1)) is real V33() ext-real Element of REAL
(f2 . 1) * (f1 * (f3 . 3)) is real V33() ext-real Element of REAL
((f2 . 3) * (f1 * (f3 . 1))) - ((f2 . 1) * (f1 * (f3 . 3))) is real V33() ext-real Element of REAL
(f2 . 1) * (f1 * (f3 . 2)) is real V33() ext-real Element of REAL
(f2 . 2) * (f1 * (f3 . 1)) is real V33() ext-real Element of REAL
((f2 . 1) * (f1 * (f3 . 2))) - ((f2 . 2) * (f1 * (f3 . 1))) is real V33() ext-real Element of REAL
((((f2 . 2) * (f1 * (f3 . 3))) - ((f2 . 3) * (f1 * (f3 . 2)))),(((f2 . 3) * (f1 * (f3 . 1))) - ((f2 . 1) * (f1 * (f3 . 3)))),(((f2 . 1) * (f1 * (f3 . 2))) - ((f2 . 2) * (f1 * (f3 . 1))))) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
((f2 . 1),(f2 . 2),(f2 . 3)) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
((f1 * (f3 . 1)),(f1 * (f3 . 2)),(f1 * (f3 . 3))) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
(((f2 . 1),(f2 . 2),(f2 . 3)),((f1 * (f3 . 1)),(f1 * (f3 . 2)),(f1 * (f3 . 3)))) is Relation-like NAT -defined REAL -valued V6() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
((f2 . 1),(f2 . 2),(f2 . 3)) . 2 is real V33() ext-real Element of REAL
((f1 * (f3 . 1)),(f1 * (f3 . 2)),(f1 * (f3 . 3))) . 3 is real V33() ext-real Element of REAL
(((f2 . 1),(f2 . 2),(f2 . 3)) . 2) * (((f1 * (f3 . 1)),(f1 * (f3 . 2)),(f1 * (f3 . 3))) . 3) is real V33() ext-real Element of REAL
((f2 . 1),(f2 . 2),(f2 . 3)) . 3 is real V33() ext-real Element of REAL
((f1 * (f3 . 1)),(f1 * (f3 . 2)),(f1 * (f3 . 3))) . 2 is real V33() ext-real Element of REAL
(((f2 . 1),(f2 . 2),(f2 . 3)) . 3) * (((f1 * (f3 . 1)),(f1 * (f3 . 2)),(f1 * (f3 . 3))) . 2) is real V33() ext-real Element of REAL
((((f2 . 1),(f2 . 2),(f2 . 3)) . 2) * (((f1 * (f3 . 1)),(f1 * (f3 . 2)),(f1 * (f3 . 3))) . 3)) - ((((f2 . 1),(f2 . 2),(f2 . 3)) . 3) * (((f1 * (f3 . 1)),(f1 * (f3 . 2)),(f1 * (f3 . 3))) . 2)) is real V33() ext-real Element of REAL
((f1 * (f3 . 1)),(f1 * (f3 . 2)),(f1 * (f3 . 3))) . 1 is real V33() ext-real Element of REAL
(((f2 . 1),(f2 . 2),(f2 . 3)) . 3) * (((f1 * (f3 . 1)),(f1 * (f3 . 2)),(f1 * (f3 . 3))) . 1) is real V33() ext-real Element of REAL
((f2 . 1),(f2 . 2),(f2 . 3)) . 1 is real V33() ext-real Element of REAL
(((f2 . 1),(f2 . 2),(f2 . 3)) . 1) * (((f1 * (f3 . 1)),(f1 * (f3 . 2)),(f1 * (f3 . 3))) . 3) is real V33() ext-real Element of REAL
((((f2 . 1),(f2 . 2),(f2 . 3)) . 3) * (((f1 * (f3 . 1)),(f1 * (f3 . 2)),(f1 * (f3 . 3))) . 1)) - ((((f2 . 1),(f2 . 2),(f2 . 3)) . 1) * (((f1 * (f3 . 1)),(f1 * (f3 . 2)),(f1 * (f3 . 3))) . 3)) is real V33() ext-real Element of REAL
(((f2 . 1),(f2 . 2),(f2 . 3)) . 1) * (((f1 * (f3 . 1)),(f1 * (f3 . 2)),(f1 * (f3 . 3))) . 2) is real V33() ext-real Element of REAL
(((f2 . 1),(f2 . 2),(f2 . 3)) . 2) * (((f1 * (f3 . 1)),(f1 * (f3 . 2)),(f1 * (f3 . 3))) . 1) is real V33() ext-real Element of REAL
((((f2 . 1),(f2 . 2),(f2 . 3)) . 1) * (((f1 * (f3 . 1)),(f1 * (f3 . 2)),(f1 * (f3 . 3))) . 2)) - ((((f2 . 1),(f2 . 2),(f2 . 3)) . 2) * (((f1 * (f3 . 1)),(f1 * (f3 . 2)),(f1 * (f3 . 3))) . 1)) is real V33() ext-real Element of REAL
((((((f2 . 1),(f2 . 2),(f2 . 3)) . 2) * (((f1 * (f3 . 1)),(f1 * (f3 . 2)),(f1 * (f3 . 3))) . 3)) - ((((f2 . 1),(f2 . 2),(f2 . 3)) . 3) * (((f1 * (f3 . 1)),(f1 * (f3 . 2)),(f1 * (f3 . 3))) . 2))),(((((f2 . 1),(f2 . 2),(f2 . 3)) . 3) * (((f1 * (f3 . 1)),(f1 * (f3 . 2)),(f1 * (f3 . 3))) . 1)) - ((((f2 . 1),(f2 . 2),(f2 . 3)) . 1) * (((f1 * (f3 . 1)),(f1 * (f3 . 2)),(f1 * (f3 . 3))) . 3))),(((((f2 . 1),(f2 . 2),(f2 . 3)) . 1) * (((f1 * (f3 . 1)),(f1 * (f3 . 2)),(f1 * (f3 . 3))) . 2)) - ((((f2 . 1),(f2 . 2),(f2 . 3)) . 2) * (((f1 * (f3 . 1)),(f1 * (f3 . 2)),(f1 * (f3 . 3))) . 1)))) is Relation-like NAT -defined REAL -valued V6() V11() V38() V45(3) FinSequence-like FinSubsequence-like complex-yielding V124() V125() Element of REAL 3
(f2,((f1 * (f3 . 1)),(f1 * (f3 . 2)),(f1 * (f3 . 3)))) is Relation-like NAT -defined REAL -valued V6() V38() V45(3)