:: RLVECT_4 semantic presentation

REAL is non empty V5() V26() set
NAT is non empty V17() V18() V19() Element of K32(REAL)
K32(REAL) is set
NAT is non empty V17() V18() V19() set
K32(NAT) is set
K32(NAT) is set
COMPLEX is non empty V5() V26() set
RAT is non empty V5() V26() set
INT is non empty V5() V26() set
2 is non empty V17() V18() V19() V23() V24() V25() V41() Element of NAT
{} is set
the empty V17() V18() V19() V21() V22() V23() V24() V25() V26() V30() V41() set is empty V17() V18() V19() V21() V22() V23() V24() V25() V26() V30() V41() set
1 is non empty V17() V18() V19() V23() V24() V25() V41() Element of NAT
0 is V17() V18() V19() V23() V24() V25() V41() Element of NAT
- 1 is V24() V25() V41() Element of REAL
K107(0) is V24() V25() V41() set
F₁() is non empty set
F₂() is non empty set
F₃() is Element of F₁()
F₄() is Element of F₁()
F₅() is Element of F₁()
K33(F₁(),F₂()) is set
K32(K33(F₁(),F₂())) is set
F₆() is Element of F₂()
F₇() is Element of F₂()
F₈() is Element of F₂()
V is Element of F₁()
F₉(V) is Element of F₂()
v is Element of F₂()
w is Element of F₂()
u is Element of F₂()
V is V7() V10(F₁()) V11(F₂()) Function-like quasi_total Element of K32(K33(F₁(),F₂()))
V . F₃() is Element of F₂()
V . F₄() is Element of F₂()
V . F₅() is Element of F₂()
v is Element of F₁()
V . v is Element of F₂()
F₉(v) is Element of F₂()
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
v is Element of the carrier of V
{v} is V26() Element of K32( the carrier of V)
K32( the carrier of V) is set
w is V24() V25() V41() Element of REAL
K33( the carrier of V,REAL) is set
K32(K33( the carrier of V,REAL)) is set
u is V7() V10( the carrier of V) V11( REAL ) Function-like quasi_total Element of K32(K33( the carrier of V,REAL))
u . v is V24() V25() V41() Element of REAL
Funcs ( the carrier of V,REAL) is non empty FUNCTION_DOMAIN of the carrier of V, REAL
b is Element of the carrier of V
a is V7() V10( the carrier of V) V11( REAL ) Function-like quasi_total Element of Funcs ( the carrier of V,REAL)
a . b is V24() V25() V41() Element of REAL
b is V7() V10( the carrier of V) V11( REAL ) Function-like quasi_total Linear_Combination of V
Carrier b is Element of K32( the carrier of V)
c is set
b . c is set
c is V7() V10( the carrier of V) V11( REAL ) Function-like quasi_total Linear_Combination of {v}
c . v is V24() V25() V41() Element of REAL
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
v is Element of the carrier of V
w is Element of the carrier of V
{v,w} is V26() Element of K32( the carrier of V)
K32( the carrier of V) is set
u is V24() V25() V41() Element of REAL
a is V24() V25() V41() Element of REAL
K33( the carrier of V,REAL) is set
K32(K33( the carrier of V,REAL)) is set
b is V7() V10( the carrier of V) V11( REAL ) Function-like quasi_total Element of K32(K33( the carrier of V,REAL))
b . v is V24() V25() V41() Element of REAL
b . w is V24() V25() V41() Element of REAL
Funcs ( the carrier of V,REAL) is non empty FUNCTION_DOMAIN of the carrier of V, REAL
r3 is Element of the carrier of V
c is V7() V10( the carrier of V) V11( REAL ) Function-like quasi_total Element of Funcs ( the carrier of V,REAL)
c . r3 is V24() V25() V41() Element of REAL
r3 is V7() V10( the carrier of V) V11( REAL ) Function-like quasi_total Linear_Combination of V
Carrier r3 is Element of K32( the carrier of V)
r4 is set
r3 . r4 is set
r4 is V7() V10( the carrier of V) V11( REAL ) Function-like quasi_total Linear_Combination of {v,w}
r4 . v is V24() V25() V41() Element of REAL
r4 . w is V24() V25() V41() Element of REAL
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
v is Element of the carrier of V
w is Element of the carrier of V
u is Element of the carrier of V
{v,w,u} is V26() Element of K32( the carrier of V)
K32( the carrier of V) is set
a is V24() V25() V41() Element of REAL
b is V24() V25() V41() Element of REAL
c is V24() V25() V41() Element of REAL
K33( the carrier of V,REAL) is set
K32(K33( the carrier of V,REAL)) is set
r3 is V7() V10( the carrier of V) V11( REAL ) Function-like quasi_total Element of K32(K33( the carrier of V,REAL))
r3 . v is V24() V25() V41() Element of REAL
r3 . w is V24() V25() V41() Element of REAL
r3 . u is V24() V25() V41() Element of REAL
Funcs ( the carrier of V,REAL) is non empty FUNCTION_DOMAIN of the carrier of V, REAL
t is Element of the carrier of V
r4 is V7() V10( the carrier of V) V11( REAL ) Function-like quasi_total Element of Funcs ( the carrier of V,REAL)
r4 . t is V24() V25() V41() Element of REAL
t is V7() V10( the carrier of V) V11( REAL ) Function-like quasi_total Linear_Combination of V
Carrier t is Element of K32( the carrier of V)
a4 is set
t . a4 is set
a4 is V7() V10( the carrier of V) V11( REAL ) Function-like quasi_total Linear_Combination of {v,w,u}
a4 . v is V24() V25() V41() Element of REAL
a4 . w is V24() V25() V41() Element of REAL
a4 . u is V24() V25() V41() Element of REAL
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
v is Element of the carrier of V
v - v is Element of the carrier of V
- v is Element of the carrier of V
K196(V,v,(- v)) is Element of the carrier of V
w is Element of the carrier of V
v + w is Element of the carrier of V
(v + w) - v is Element of the carrier of V
K196(V,(v + w),(- v)) is Element of the carrier of V
w + v is Element of the carrier of V
(w + v) - v is Element of the carrier of V
K196(V,(w + v),(- v)) is Element of the carrier of V
(v - v) + w is Element of the carrier of V
w - v is Element of the carrier of V
K196(V,w,(- v)) is Element of the carrier of V
(w - v) + v is Element of the carrier of V
v + (w - v) is Element of the carrier of V
w + (v - v) is Element of the carrier of V
v - w is Element of the carrier of V
- w is Element of the carrier of V
K196(V,v,(- w)) is Element of the carrier of V
v - (v - w) is Element of the carrier of V
- (v - w) is Element of the carrier of V
K196(V,v,(- (v - w))) is Element of the carrier of V
0. V is V52(V) Element of the carrier of V
(0. V) + w is Element of the carrier of V
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
v is Element of the carrier of V
w is Element of the carrier of V
v - w is Element of the carrier of V
- w is Element of the carrier of V
K196(V,v,(- w)) is Element of the carrier of V
u is Element of the carrier of V
u - w is Element of the carrier of V
K196(V,u,(- w)) is Element of the carrier of V
- (v - w) is Element of the carrier of V
w - u is Element of the carrier of V
- u is Element of the carrier of V
K196(V,w,(- u)) is Element of the carrier of V
w - v is Element of the carrier of V
- v is Element of the carrier of V
K196(V,w,(- v)) is Element of the carrier of V
V is V24() V25() V41() Element of REAL
- V is V24() V25() V41() Element of REAL
v is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of v is non empty set
w is Element of the carrier of v
V * w is Element of the carrier of v
- (V * w) is Element of the carrier of v
(- V) * w is Element of the carrier of v
- w is Element of the carrier of v
V * (- w) is Element of the carrier of v
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
v is Element of the carrier of V
w is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
v + w is Element of K32( the carrier of V)
K32( the carrier of V) is set
u is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
v + u is Element of K32( the carrier of V)
a is set
b is Element of the carrier of V
v + b is Element of the carrier of V
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
v is Element of the carrier of V
w is Element of the carrier of V
u is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
w + u is Element of K32( the carrier of V)
K32( the carrier of V) is set
v + u is Element of K32( the carrier of V)
a is Coset of u
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
v is Element of the carrier of V
w is Element of the carrier of V
u is Element of the carrier of V
{v,w,u} is V26() Element of K32( the carrier of V)
K32( the carrier of V) is set
a is V7() V10( the carrier of V) V11( REAL ) Function-like quasi_total Linear_Combination of {v,w,u}
Sum a is Element of the carrier of V
a . v is V24() V25() V41() Element of REAL
(a . v) * v is Element of the carrier of V
a . w is V24() V25() V41() Element of REAL
(a . w) * w is Element of the carrier of V
((a . v) * v) + ((a . w) * w) is Element of the carrier of V
a . u is V24() V25() V41() Element of REAL
(a . u) * u is Element of the carrier of V
(((a . v) * v) + ((a . w) * w)) + ((a . u) * u) is Element of the carrier of V
Carrier a is Element of K32( the carrier of V)
r4 is Element of the carrier of V
a . r4 is V24() V25() V41() Element of REAL
the Element of Carrier a is Element of Carrier a
a . the Element of Carrier a is set
ZeroLC V is V7() V10( the carrier of V) V11( REAL ) Function-like quasi_total Linear_Combination of V
0. V is V52(V) Element of the carrier of V
((a . v) * v) + (0. V) is Element of the carrier of V
(((a . v) * v) + ((a . w) * w)) + (0. V) is Element of the carrier of V
{u} is V26() Element of K32( the carrier of V)
r4 is set
a . r4 is set
<*u*> is V7() V10( NAT ) V11( the carrier of V) Function-like FinSequence-like FinSequence of the carrier of V
a (#) <*u*> is V7() V10( NAT ) V11( the carrier of V) Function-like FinSequence-like FinSequence of the carrier of V
<*((a . u) * u)*> is V7() V10( NAT ) V11( the carrier of V) Function-like FinSequence-like FinSequence of the carrier of V
rng <*u*> is set
Sum <*((a . u) * u)*> is Element of the carrier of V
0. V is V52(V) Element of the carrier of V
(0. V) + ((a . u) * u) is Element of the carrier of V
(0. V) + (0. V) is Element of the carrier of V
((0. V) + (0. V)) + ((a . u) * u) is Element of the carrier of V
((a . v) * v) + (0. V) is Element of the carrier of V
(((a . v) * v) + (0. V)) + ((a . u) * u) is Element of the carrier of V
{w} is V26() Element of K32( the carrier of V)
r4 is set
a . r4 is set
<*w*> is V7() V10( NAT ) V11( the carrier of V) Function-like FinSequence-like FinSequence of the carrier of V
a (#) <*w*> is V7() V10( NAT ) V11( the carrier of V) Function-like FinSequence-like FinSequence of the carrier of V
<*((a . w) * w)*> is V7() V10( NAT ) V11( the carrier of V) Function-like FinSequence-like FinSequence of the carrier of V
rng <*w*> is set
Sum <*((a . w) * w)*> is Element of the carrier of V
0. V is V52(V) Element of the carrier of V
(0. V) + ((a . w) * w) is Element of the carrier of V
((0. V) + ((a . w) * w)) + (0. V) is Element of the carrier of V
(((a . v) * v) + ((a . w) * w)) + (0. V) is Element of the carrier of V
{w,u} is V26() Element of K32( the carrier of V)
r4 is set
a . r4 is set
<*w,u*> is V7() V10( NAT ) V11( the carrier of V) Function-like FinSequence-like FinSequence of the carrier of V
a (#) <*w,u*> is V7() V10( NAT ) V11( the carrier of V) Function-like FinSequence-like FinSequence of the carrier of V
<*((a . w) * w),((a . u) * u)*> is V7() V10( NAT ) V11( the carrier of V) Function-like FinSequence-like FinSequence of the carrier of V
rng <*w,u*> is set
Sum <*((a . w) * w),((a . u) * u)*> is Element of the carrier of V
((a . w) * w) + ((a . u) * u) is Element of the carrier of V
0. V is V52(V) Element of the carrier of V
(0. V) + ((a . w) * w) is Element of the carrier of V
((0. V) + ((a . w) * w)) + ((a . u) * u) is Element of the carrier of V
{v} is V26() Element of K32( the carrier of V)
r4 is set
a . r4 is set
<*v*> is V7() V10( NAT ) V11( the carrier of V) Function-like FinSequence-like FinSequence of the carrier of V
a (#) <*v*> is V7() V10( NAT ) V11( the carrier of V) Function-like FinSequence-like FinSequence of the carrier of V
<*((a . v) * v)*> is V7() V10( NAT ) V11( the carrier of V) Function-like FinSequence-like FinSequence of the carrier of V
rng <*v*> is set
Sum <*((a . v) * v)*> is Element of the carrier of V
0. V is V52(V) Element of the carrier of V
((a . v) * v) + (0. V) is Element of the carrier of V
(((a . v) * v) + (0. V)) + (0. V) is Element of the carrier of V
(((a . v) * v) + ((a . w) * w)) + (0. V) is Element of the carrier of V
{v,u} is V26() Element of K32( the carrier of V)
r4 is set
a . r4 is set
<*v,u*> is V7() V10( NAT ) V11( the carrier of V) Function-like FinSequence-like FinSequence of the carrier of V
a (#) <*v,u*> is V7() V10( NAT ) V11( the carrier of V) Function-like FinSequence-like FinSequence of the carrier of V
<*((a . v) * v),((a . u) * u)*> is V7() V10( NAT ) V11( the carrier of V) Function-like FinSequence-like FinSequence of the carrier of V
rng <*v,u*> is set
Sum <*((a . v) * v),((a . u) * u)*> is Element of the carrier of V
((a . v) * v) + ((a . u) * u) is Element of the carrier of V
0. V is V52(V) Element of the carrier of V
((a . v) * v) + (0. V) is Element of the carrier of V
(((a . v) * v) + (0. V)) + ((a . u) * u) is Element of the carrier of V
{v,w} is V26() Element of K32( the carrier of V)
r4 is set
a . r4 is set
<*v,w*> is V7() V10( NAT ) V11( the carrier of V) Function-like FinSequence-like FinSequence of the carrier of V
a (#) <*v,w*> is V7() V10( NAT ) V11( the carrier of V) Function-like FinSequence-like FinSequence of the carrier of V
<*((a . v) * v),((a . w) * w)*> is V7() V10( NAT ) V11( the carrier of V) Function-like FinSequence-like FinSequence of the carrier of V
rng <*v,w*> is set
Sum <*((a . v) * v),((a . w) * w)*> is Element of the carrier of V
0. V is V52(V) Element of the carrier of V
(((a . v) * v) + ((a . w) * w)) + (0. V) is Element of the carrier of V
r4 is set
<*v,w,u*> is V7() V10( NAT ) V11( the carrier of V) Function-like FinSequence-like FinSequence of the carrier of V
a (#) <*v,w,u*> is V7() V10( NAT ) V11( the carrier of V) Function-like FinSequence-like FinSequence of the carrier of V
<*((a . v) * v),((a . w) * w),((a . u) * u)*> is V7() V10( NAT ) V11( the carrier of V) Function-like FinSequence-like FinSequence of the carrier of V
rng <*v,w,u*> is set
Sum <*((a . v) * v),((a . w) * w),((a . u) * u)*> is Element of the carrier of V
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
0. V is V52(V) Element of the carrier of V
v is Element of the carrier of V
w is Element of the carrier of V
u is Element of the carrier of V
{v,w,u} is V26() Element of K32( the carrier of V)
K32( the carrier of V) is set
a is V24() V25() V41() Element of REAL
a * v is Element of the carrier of V
b is V24() V25() V41() Element of REAL
b * w is Element of the carrier of V
(a * v) + (b * w) is Element of the carrier of V
c is V24() V25() V41() Element of REAL
c * u is Element of the carrier of V
((a * v) + (b * w)) + (c * u) is Element of the carrier of V
K33( the carrier of V,REAL) is set
K32(K33( the carrier of V,REAL)) is set
r3 is V7() V10( the carrier of V) V11( REAL ) Function-like quasi_total Element of K32(K33( the carrier of V,REAL))
r3 . v is V24() V25() V41() Element of REAL
r3 . w is V24() V25() V41() Element of REAL
r3 . u is V24() V25() V41() Element of REAL
Funcs ( the carrier of V,REAL) is non empty FUNCTION_DOMAIN of the carrier of V, REAL
t is Element of the carrier of V
r4 is V7() V10( the carrier of V) V11( REAL ) Function-like quasi_total Element of Funcs ( the carrier of V,REAL)
r4 . t is V24() V25() V41() Element of REAL
t is V7() V10( the carrier of V) V11( REAL ) Function-like quasi_total Linear_Combination of V
Carrier t is Element of K32( the carrier of V)
a4 is set
t . a4 is set
a4 is V7() V10( the carrier of V) V11( REAL ) Function-like quasi_total Linear_Combination of {v,w,u}
Sum a4 is Element of the carrier of V
Carrier a4 is Element of K32( the carrier of V)
1 * v is Element of the carrier of V
(- 1) * w is Element of the carrier of V
(1 * v) + ((- 1) * w) is Element of the carrier of V
0 * u is Element of the carrier of V
((1 * v) + ((- 1) * w)) + (0 * u) is Element of the carrier of V
(- 1) * v is Element of the carrier of V
v + ((- 1) * v) is Element of the carrier of V
(v + ((- 1) * v)) + (0 * u) is Element of the carrier of V
- v is Element of the carrier of V
v + (- v) is Element of the carrier of V
(v + (- v)) + (0 * u) is Element of the carrier of V
(v + (- v)) + (0. V) is Element of the carrier of V
1 * v is Element of the carrier of V
0 * w is Element of the carrier of V
(1 * v) + (0 * w) is Element of the carrier of V
(- 1) * u is Element of the carrier of V
((1 * v) + (0 * w)) + ((- 1) * u) is Element of the carrier of V
v + (0 * w) is Element of the carrier of V
(- 1) * v is Element of the carrier of V
(v + (0 * w)) + ((- 1) * v) is Element of the carrier of V
v + (0. V) is Element of the carrier of V
(v + (0. V)) + ((- 1) * v) is Element of the carrier of V
- v is Element of the carrier of V
(v + (0. V)) + (- v) is Element of the carrier of V
v + (- v) is Element of the carrier of V
0 * v is Element of the carrier of V
1 * w is Element of the carrier of V
(0 * v) + (1 * w) is Element of the carrier of V
(- 1) * u is Element of the carrier of V
((0 * v) + (1 * w)) + ((- 1) * u) is Element of the carrier of V
- w is Element of the carrier of V
((0 * v) + (1 * w)) + (- w) is Element of the carrier of V
(0. V) + (1 * w) is Element of the carrier of V
((0. V) + (1 * w)) + (- w) is Element of the carrier of V
(0. V) + w is Element of the carrier of V
((0. V) + w) + (- w) is Element of the carrier of V
w + (- w) is Element of the carrier of V
a is V7() V10( the carrier of V) V11( REAL ) Function-like quasi_total Linear_Combination of {v,w,u}
Sum a is Element of the carrier of V
Carrier a is Element of K32( the carrier of V)
a . v is V24() V25() V41() Element of REAL
(a . v) * v is Element of the carrier of V
a . w is V24() V25() V41() Element of REAL
(a . w) * w is Element of the carrier of V
((a . v) * v) + ((a . w) * w) is Element of the carrier of V
a . u is V24() V25() V41() Element of REAL
(a . u) * u is Element of the carrier of V
(((a . v) * v) + ((a . w) * w)) + ((a . u) * u) is Element of the carrier of V
b is set
V is set
v is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of v is non empty set
w is Element of the carrier of v
{w} is V26() Element of K32( the carrier of v)
K32( the carrier of v) is set
Lin {w} is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of v
u is V7() V10( the carrier of v) V11( REAL ) Function-like quasi_total Linear_Combination of {w}
Sum u is Element of the carrier of v
u . w is V24() V25() V41() Element of REAL
(u . w) * w is Element of the carrier of v
u is V24() V25() V41() Element of REAL
u * w is Element of the carrier of v
K33( the carrier of v,REAL) is set
K32(K33( the carrier of v,REAL)) is set
a is V7() V10( the carrier of v) V11( REAL ) Function-like quasi_total Element of K32(K33( the carrier of v,REAL))
a . w is V24() V25() V41() Element of REAL
Funcs ( the carrier of v,REAL) is non empty FUNCTION_DOMAIN of the carrier of v, REAL
c is Element of the carrier of v
b is V7() V10( the carrier of v) V11( REAL ) Function-like quasi_total Element of Funcs ( the carrier of v,REAL)
b . c is V24() V25() V41() Element of REAL
c is V7() V10( the carrier of v) V11( REAL ) Function-like quasi_total Linear_Combination of v
Carrier c is Element of K32( the carrier of v)
r3 is set
c . r3 is set
r3 is V7() V10( the carrier of v) V11( REAL ) Function-like quasi_total Linear_Combination of {w}
Sum r3 is Element of the carrier of v
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
v is Element of the carrier of V
{v} is V26() Element of K32( the carrier of V)
K32( the carrier of V) is set
Lin {v} is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
V is set
v is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of v is non empty set
w is Element of the carrier of v
u is Element of the carrier of v
{u} is V26() Element of K32( the carrier of v)
K32( the carrier of v) is set
Lin {u} is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of v
w + (Lin {u}) is Element of K32( the carrier of v)
a is Element of the carrier of v
w + a is Element of the carrier of v
b is V24() V25() V41() Element of REAL
b * u is Element of the carrier of v
a is V24() V25() V41() Element of REAL
a * u is Element of the carrier of v
w + (a * u) is Element of the carrier of v
V is set
v is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of v is non empty set
w is Element of the carrier of v
u is Element of the carrier of v
{w,u} is V26() Element of K32( the carrier of v)
K32( the carrier of v) is set
Lin {w,u} is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of v
{w} is V26() Element of K32( the carrier of v)
a is V24() V25() V41() Element of REAL
a * w is Element of the carrier of v
0. v is V52(v) Element of the carrier of v
(a * w) + (0. v) is Element of the carrier of v
0 * u is Element of the carrier of v
(a * w) + (0 * u) is Element of the carrier of v
a is V7() V10( the carrier of v) V11( REAL ) Function-like quasi_total Linear_Combination of {w,u}
Sum a is Element of the carrier of v
a . w is V24() V25() V41() Element of REAL
(a . w) * w is Element of the carrier of v
a . u is V24() V25() V41() Element of REAL
(a . u) * u is Element of the carrier of v
((a . w) * w) + ((a . u) * u) is Element of the carrier of v
a is V24() V25() V41() Element of REAL
a * w is Element of the carrier of v
b is V24() V25() V41() Element of REAL
b * u is Element of the carrier of v
(a * w) + (b * u) is Element of the carrier of v
a is V24() V25() V41() Element of REAL
a * w is Element of the carrier of v
b is V24() V25() V41() Element of REAL
b * u is Element of the carrier of v
(a * w) + (b * u) is Element of the carrier of v
a + b is V24() V25() V41() Element of REAL
(a + b) * w is Element of the carrier of v
{w} is V26() Element of K32( the carrier of v)
Lin {w} is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of v
K33( the carrier of v,REAL) is set
K32(K33( the carrier of v,REAL)) is set
c is V7() V10( the carrier of v) V11( REAL ) Function-like quasi_total Element of K32(K33( the carrier of v,REAL))
c . w is V24() V25() V41() Element of REAL
c . u is V24() V25() V41() Element of REAL
Funcs ( the carrier of v,REAL) is non empty FUNCTION_DOMAIN of the carrier of v, REAL
r4 is Element of the carrier of v
r3 is V7() V10( the carrier of v) V11( REAL ) Function-like quasi_total Element of Funcs ( the carrier of v,REAL)
r3 . r4 is V24() V25() V41() Element of REAL
r4 is V7() V10( the carrier of v) V11( REAL ) Function-like quasi_total Linear_Combination of v
Carrier r4 is Element of K32( the carrier of v)
t is set
r4 . t is set
t is V7() V10( the carrier of v) V11( REAL ) Function-like quasi_total Linear_Combination of {w,u}
Sum t is Element of the carrier of v
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
v is Element of the carrier of V
w is Element of the carrier of V
{v,w} is V26() Element of K32( the carrier of V)
K32( the carrier of V) is set
Lin {v,w} is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
V is set
v is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of v is non empty set
w is Element of the carrier of v
u is Element of the carrier of v
a is Element of the carrier of v
{u,a} is V26() Element of K32( the carrier of v)
K32( the carrier of v) is set
Lin {u,a} is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of v
w + (Lin {u,a}) is Element of K32( the carrier of v)
b is Element of the carrier of v
w + b is Element of the carrier of v
c is V24() V25() V41() Element of REAL
c * u is Element of the carrier of v
r3 is V24() V25() V41() Element of REAL
r3 * a is Element of the carrier of v
(c * u) + (r3 * a) is Element of the carrier of v
w + (c * u) is Element of the carrier of v
(w + (c * u)) + (r3 * a) is Element of the carrier of v
b is V24() V25() V41() Element of REAL
b * u is Element of the carrier of v
w + (b * u) is Element of the carrier of v
c is V24() V25() V41() Element of REAL
c * a is Element of the carrier of v
(w + (b * u)) + (c * a) is Element of the carrier of v
(b * u) + (c * a) is Element of the carrier of v
w + ((b * u) + (c * a)) is Element of the carrier of v
V is set
v is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of v is non empty set
w is Element of the carrier of v
u is Element of the carrier of v
a is Element of the carrier of v
{w,u,a} is V26() Element of K32( the carrier of v)
K32( the carrier of v) is set
Lin {w,u,a} is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of v
b is V7() V10( the carrier of v) V11( REAL ) Function-like quasi_total Linear_Combination of {w,u,a}
Sum b is Element of the carrier of v
b . w is V24() V25() V41() Element of REAL
(b . w) * w is Element of the carrier of v
b . u is V24() V25() V41() Element of REAL
(b . u) * u is Element of the carrier of v
((b . w) * w) + ((b . u) * u) is Element of the carrier of v
b . a is V24() V25() V41() Element of REAL
(b . a) * a is Element of the carrier of v
(((b . w) * w) + ((b . u) * u)) + ((b . a) * a) is Element of the carrier of v
{w,a} is V26() Element of K32( the carrier of v)
{w,w,u} is V26() Element of K32( the carrier of v)
{a,a,w} is V26() Element of K32( the carrier of v)
{w,u} is V26() Element of K32( the carrier of v)
b is V24() V25() V41() Element of REAL
b * w is Element of the carrier of v
c is V24() V25() V41() Element of REAL
c * u is Element of the carrier of v
(b * w) + (c * u) is Element of the carrier of v
0. v is V52(v) Element of the carrier of v
((b * w) + (c * u)) + (0. v) is Element of the carrier of v
0 * a is Element of the carrier of v
((b * w) + (c * u)) + (0 * a) is Element of the carrier of v
b is V24() V25() V41() Element of REAL
b * w is Element of the carrier of v
c is V24() V25() V41() Element of REAL
c * a is Element of the carrier of v
(b * w) + (c * a) is Element of the carrier of v
0. v is V52(v) Element of the carrier of v
(b * w) + (0. v) is Element of the carrier of v
((b * w) + (0. v)) + (c * a) is Element of the carrier of v
0 * u is Element of the carrier of v
(b * w) + (0 * u) is Element of the carrier of v
((b * w) + (0 * u)) + (c * a) is Element of the carrier of v
{w,u} is V26() Element of K32( the carrier of v)
b is V24() V25() V41() Element of REAL
b * w is Element of the carrier of v
c is V24() V25() V41() Element of REAL
c * u is Element of the carrier of v
(b * w) + (c * u) is Element of the carrier of v
r3 is V24() V25() V41() Element of REAL
r3 * a is Element of the carrier of v
((b * w) + (c * u)) + (r3 * a) is Element of the carrier of v
b is V24() V25() V41() Element of REAL
b * w is Element of the carrier of v
c is V24() V25() V41() Element of REAL
c * u is Element of the carrier of v
(b * w) + (c * u) is Element of the carrier of v
r3 is V24() V25() V41() Element of REAL
r3 * a is Element of the carrier of v
((b * w) + (c * u)) + (r3 * a) is Element of the carrier of v
b is V24() V25() V41() Element of REAL
b * w is Element of the carrier of v
c is V24() V25() V41() Element of REAL
c * u is Element of the carrier of v
(b * w) + (c * u) is Element of the carrier of v
r3 is V24() V25() V41() Element of REAL
r3 * a is Element of the carrier of v
((b * w) + (c * u)) + (r3 * a) is Element of the carrier of v
{w,a} is V26() Element of K32( the carrier of v)
b + c is V24() V25() V41() Element of REAL
(b + c) * w is Element of the carrier of v
((b + c) * w) + (r3 * a) is Element of the carrier of v
{w,w,u} is V26() Element of K32( the carrier of v)
{u,w} is V26() Element of K32( the carrier of v)
r3 * w is Element of the carrier of v
(b * w) + (r3 * w) is Element of the carrier of v
(c * u) + ((b * w) + (r3 * w)) is Element of the carrier of v
b + r3 is V24() V25() V41() Element of REAL
(b + r3) * w is Element of the carrier of v
(c * u) + ((b + r3) * w) is Element of the carrier of v
{u,u,w} is V26() Element of K32( the carrier of v)
{w,u} is V26() Element of K32( the carrier of v)
r3 * u is Element of the carrier of v
(c * u) + (r3 * u) is Element of the carrier of v
(b * w) + ((c * u) + (r3 * u)) is Element of the carrier of v
c + r3 is V24() V25() V41() Element of REAL
(c + r3) * u is Element of the carrier of v
(b * w) + ((c + r3) * u) is Element of the carrier of v
K33( the carrier of v,REAL) is set
K32(K33( the carrier of v,REAL)) is set
r4 is V7() V10( the carrier of v) V11( REAL ) Function-like quasi_total Element of K32(K33( the carrier of v,REAL))
r4 . w is V24() V25() V41() Element of REAL
r4 . u is V24() V25() V41() Element of REAL
r4 . a is V24() V25() V41() Element of REAL
Funcs ( the carrier of v,REAL) is non empty FUNCTION_DOMAIN of the carrier of v, REAL
a4 is Element of the carrier of v
t is V7() V10( the carrier of v) V11( REAL ) Function-like quasi_total Element of Funcs ( the carrier of v,REAL)
t . a4 is V24() V25() V41() Element of REAL
a4 is V7() V10( the carrier of v) V11( REAL ) Function-like quasi_total Linear_Combination of v
Carrier a4 is Element of K32( the carrier of v)
a3 is set
a4 . a3 is set
a3 is V7() V10( the carrier of v) V11( REAL ) Function-like quasi_total Linear_Combination of {w,u,a}
Sum a3 is Element of the carrier of v
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
v is Element of the carrier of V
w is Element of the carrier of V
u is Element of the carrier of V
{v,w,u} is V26() Element of K32( the carrier of V)
K32( the carrier of V) is set
Lin {v,w,u} is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
V is set
v is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of v is non empty set
w is Element of the carrier of v
u is Element of the carrier of v
a is Element of the carrier of v
b is Element of the carrier of v
{u,a,b} is V26() Element of K32( the carrier of v)
K32( the carrier of v) is set
Lin {u,a,b} is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of v
w + (Lin {u,a,b}) is Element of K32( the carrier of v)
c is Element of the carrier of v
w + c is Element of the carrier of v
r3 is V24() V25() V41() Element of REAL
r3 * u is Element of the carrier of v
r4 is V24() V25() V41() Element of REAL
r4 * a is Element of the carrier of v
(r3 * u) + (r4 * a) is Element of the carrier of v
t is V24() V25() V41() Element of REAL
t * b is Element of the carrier of v
((r3 * u) + (r4 * a)) + (t * b) is Element of the carrier of v
w + (r3 * u) is Element of the carrier of v
(w + (r3 * u)) + (r4 * a) is Element of the carrier of v
((w + (r3 * u)) + (r4 * a)) + (t * b) is Element of the carrier of v
w + ((r3 * u) + (r4 * a)) is Element of the carrier of v
(w + ((r3 * u) + (r4 * a))) + (t * b) is Element of the carrier of v
c is V24() V25() V41() Element of REAL
c * u is Element of the carrier of v
w + (c * u) is Element of the carrier of v
r3 is V24() V25() V41() Element of REAL
r3 * a is Element of the carrier of v
(w + (c * u)) + (r3 * a) is Element of the carrier of v
r4 is V24() V25() V41() Element of REAL
r4 * b is Element of the carrier of v
((w + (c * u)) + (r3 * a)) + (r4 * b) is Element of the carrier of v
(c * u) + (r3 * a) is Element of the carrier of v
((c * u) + (r3 * a)) + (r4 * b) is Element of the carrier of v
w + (((c * u) + (r3 * a)) + (r4 * b)) is Element of the carrier of v
w + ((c * u) + (r3 * a)) is Element of the carrier of v
(w + ((c * u) + (r3 * a))) + (r4 * b) is Element of the carrier of v
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
v is Element of the carrier of V
w is Element of the carrier of V
{v,w} is V26() Element of K32( the carrier of V)
K32( the carrier of V) is set
w - v is Element of the carrier of V
- v is Element of the carrier of V
K196(V,w,(- v)) is Element of the carrier of V
{v,(w - v)} is V26() Element of K32( the carrier of V)
u is V24() V25() V41() Element of REAL
u * v is Element of the carrier of V
a is V24() V25() V41() Element of REAL
a * (w - v) is Element of the carrier of V
(u * v) + (a * (w - v)) is Element of the carrier of V
0. V is V52(V) Element of the carrier of V
a * w is Element of the carrier of V
a * v is Element of the carrier of V
(a * w) - (a * v) is Element of the carrier of V
- (a * v) is Element of the carrier of V
K196(V,(a * w),(- (a * v))) is Element of the carrier of V
(u * v) + ((a * w) - (a * v)) is Element of the carrier of V
(u * v) + (a * w) is Element of the carrier of V
((u * v) + (a * w)) - (a * v) is Element of the carrier of V
K196(V,((u * v) + (a * w)),(- (a * v))) is Element of the carrier of V
(u * v) - (a * v) is Element of the carrier of V
K196(V,(u * v),(- (a * v))) is Element of the carrier of V
((u * v) - (a * v)) + (a * w) is Element of the carrier of V
u - a is V24() V25() V41() Element of REAL
(u - a) * v is Element of the carrier of V
((u - a) * v) + (a * w) is Element of the carrier of V
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
v is Element of the carrier of V
w is Element of the carrier of V
{v,w} is V26() Element of K32( the carrier of V)
K32( the carrier of V) is set
w + v is Element of the carrier of V
{v,(w + v)} is V26() Element of K32( the carrier of V)
u is V24() V25() V41() Element of REAL
u * v is Element of the carrier of V
a is V24() V25() V41() Element of REAL
a * (w + v) is Element of the carrier of V
(u * v) + (a * (w + v)) is Element of the carrier of V
0. V is V52(V) Element of the carrier of V
a * v is Element of the carrier of V
a * w is Element of the carrier of V
(a * v) + (a * w) is Element of the carrier of V
(u * v) + ((a * v) + (a * w)) is Element of the carrier of V
(u * v) + (a * v) is Element of the carrier of V
((u * v) + (a * v)) + (a * w) is Element of the carrier of V
u + a is V24() V25() V41() Element of REAL
(u + a) * v is Element of the carrier of V
((u + a) * v) + (a * w) is Element of the carrier of V
V is V24() V25() V41() Element of REAL
v is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of v is non empty set
w is Element of the carrier of v
u is Element of the carrier of v
{w,u} is V26() Element of K32( the carrier of v)
K32( the carrier of v) is set
V * u is Element of the carrier of v
{w,(V * u)} is V26() Element of K32( the carrier of v)
a is V24() V25() V41() Element of REAL
a * w is Element of the carrier of v
b is V24() V25() V41() Element of REAL
b * (V * u) is Element of the carrier of v
(a * w) + (b * (V * u)) is Element of the carrier of v
0. v is V52(v) Element of the carrier of v
b * V is V24() V25() V41() Element of REAL
(b * V) * u is Element of the carrier of v
(a * w) + ((b * V) * u) is Element of the carrier of v
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
v is Element of the carrier of V
w is Element of the carrier of V
{v,w} is V26() Element of K32( the carrier of V)
K32( the carrier of V) is set
- w is Element of the carrier of V
{v,(- w)} is V26() Element of K32( the carrier of V)
(- 1) * w is Element of the carrier of V
V is V24() V25() V41() Element of REAL
v is V24() V25() V41() Element of REAL
w is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of w is non empty set
u is Element of the carrier of w
V * u is Element of the carrier of w
v * u is Element of the carrier of w
{(V * u),(v * u)} is V26() Element of K32( the carrier of w)
K32( the carrier of w) is set
0. w is V52(w) Element of the carrier of w
0. w is V52(w) Element of the carrier of w
v * (V * u) is Element of the carrier of w
- V is V24() V25() V41() Element of REAL
(- V) * (v * u) is Element of the carrier of w
(v * (V * u)) + ((- V) * (v * u)) is Element of the carrier of w
V * v is V24() V25() V41() Element of REAL
(V * v) * u is Element of the carrier of w
((V * v) * u) + ((- V) * (v * u)) is Element of the carrier of w
V * (v * u) is Element of the carrier of w
((V * v) * u) - (V * (v * u)) is Element of the carrier of w
- (V * (v * u)) is Element of the carrier of w
K196(w,((V * v) * u),(- (V * (v * u)))) is Element of the carrier of w
((V * v) * u) - ((V * v) * u) is Element of the carrier of w
- ((V * v) * u) is Element of the carrier of w
K196(w,((V * v) * u),(- ((V * v) * u))) is Element of the carrier of w
0. w is V52(w) Element of the carrier of w
V is V24() V25() V41() Element of REAL
v is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of v is non empty set
w is Element of the carrier of v
V * w is Element of the carrier of v
{w,(V * w)} is V26() Element of K32( the carrier of v)
K32( the carrier of v) is set
1 * w is Element of the carrier of v
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
v is Element of the carrier of V
w is Element of the carrier of V
u is Element of the carrier of V
{v,w,u} is V26() Element of K32( the carrier of V)
K32( the carrier of V) is set
u - v is Element of the carrier of V
- v is Element of the carrier of V
K196(V,u,(- v)) is Element of the carrier of V
{v,w,(u - v)} is V26() Element of K32( the carrier of V)
a is V24() V25() V41() Element of REAL
a * v is Element of the carrier of V
b is V24() V25() V41() Element of REAL
b * w is Element of the carrier of V
(a * v) + (b * w) is Element of the carrier of V
c is V24() V25() V41() Element of REAL
c * (u - v) is Element of the carrier of V
((a * v) + (b * w)) + (c * (u - v)) is Element of the carrier of V
0. V is V52(V) Element of the carrier of V
c * u is Element of the carrier of V
c * v is Element of the carrier of V
(c * u) - (c * v) is Element of the carrier of V
- (c * v) is Element of the carrier of V
K196(V,(c * u),(- (c * v))) is Element of the carrier of V
((a * v) + (b * w)) + ((c * u) - (c * v)) is Element of the carrier of V
(b * w) + ((c * u) - (c * v)) is Element of the carrier of V
(a * v) + ((b * w) + ((c * u) - (c * v))) is Element of the carrier of V
(b * w) + (c * u) is Element of the carrier of V
((b * w) + (c * u)) - (c * v) is Element of the carrier of V
K196(V,((b * w) + (c * u)),(- (c * v))) is Element of the carrier of V
(a * v) + (((b * w) + (c * u)) - (c * v)) is Element of the carrier of V
(b * w) - (c * v) is Element of the carrier of V
K196(V,(b * w),(- (c * v))) is Element of the carrier of V
((b * w) - (c * v)) + (c * u) is Element of the carrier of V
(a * v) + (((b * w) - (c * v)) + (c * u)) is Element of the carrier of V
(a * v) + ((b * w) - (c * v)) is Element of the carrier of V
((a * v) + ((b * w) - (c * v))) + (c * u) is Element of the carrier of V
((a * v) + (b * w)) - (c * v) is Element of the carrier of V
K196(V,((a * v) + (b * w)),(- (c * v))) is Element of the carrier of V
(((a * v) + (b * w)) - (c * v)) + (c * u) is Element of the carrier of V
(a * v) - (c * v) is Element of the carrier of V
K196(V,(a * v),(- (c * v))) is Element of the carrier of V
((a * v) - (c * v)) + (b * w) is Element of the carrier of V
(((a * v) - (c * v)) + (b * w)) + (c * u) is Element of the carrier of V
a - c is V24() V25() V41() Element of REAL
(a - c) * v is Element of the carrier of V
((a - c) * v) + (b * w) is Element of the carrier of V
(((a - c) * v) + (b * w)) + (c * u) is Element of the carrier of V
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
v is Element of the carrier of V
w is Element of the carrier of V
w - v is Element of the carrier of V
- v is Element of the carrier of V
K196(V,w,(- v)) is Element of the carrier of V
u is Element of the carrier of V
{v,w,u} is V26() Element of K32( the carrier of V)
K32( the carrier of V) is set
u - v is Element of the carrier of V
K196(V,u,(- v)) is Element of the carrier of V
{v,(w - v),(u - v)} is V26() Element of K32( the carrier of V)
a is V24() V25() V41() Element of REAL
a * v is Element of the carrier of V
b is V24() V25() V41() Element of REAL
b * (w - v) is Element of the carrier of V
(a * v) + (b * (w - v)) is Element of the carrier of V
c is V24() V25() V41() Element of REAL
c * (u - v) is Element of the carrier of V
((a * v) + (b * (w - v))) + (c * (u - v)) is Element of the carrier of V
0. V is V52(V) Element of the carrier of V
b * w is Element of the carrier of V
b * v is Element of the carrier of V
(b * w) - (b * v) is Element of the carrier of V
- (b * v) is Element of the carrier of V
K196(V,(b * w),(- (b * v))) is Element of the carrier of V
(a * v) + ((b * w) - (b * v)) is Element of the carrier of V
((a * v) + ((b * w) - (b * v))) + (c * (u - v)) is Element of the carrier of V
(b * w) + (- (b * v)) is Element of the carrier of V
(a * v) + ((b * w) + (- (b * v))) is Element of the carrier of V
c * u is Element of the carrier of V
c * v is Element of the carrier of V
(c * u) - (c * v) is Element of the carrier of V
- (c * v) is Element of the carrier of V
K196(V,(c * u),(- (c * v))) is Element of the carrier of V
((a * v) + ((b * w) + (- (b * v)))) + ((c * u) - (c * v)) is Element of the carrier of V
(a * v) + (- (b * v)) is Element of the carrier of V
((a * v) + (- (b * v))) + (b * w) is Element of the carrier of V
(- (c * v)) + (c * u) is Element of the carrier of V
(((a * v) + (- (b * v))) + (b * w)) + ((- (c * v)) + (c * u)) is Element of the carrier of V
(b * w) + ((- (c * v)) + (c * u)) is Element of the carrier of V
((a * v) + (- (b * v))) + ((b * w) + ((- (c * v)) + (c * u))) is Element of the carrier of V
(b * w) + (c * u) is Element of the carrier of V
(- (c * v)) + ((b * w) + (c * u)) is Element of the carrier of V
((a * v) + (- (b * v))) + ((- (c * v)) + ((b * w) + (c * u))) is Element of the carrier of V
((a * v) + (- (b * v))) + (- (c * v)) is Element of the carrier of V
(((a * v) + (- (b * v))) + (- (c * v))) + ((b * w) + (c * u)) is Element of the carrier of V
b * (- v) is Element of the carrier of V
(a * v) + (b * (- v)) is Element of the carrier of V
((a * v) + (b * (- v))) + (- (c * v)) is Element of the carrier of V
(((a * v) + (b * (- v))) + (- (c * v))) + ((b * w) + (c * u)) is Element of the carrier of V
- b is V24() V25() V41() Element of REAL
(- b) * v is Element of the carrier of V
(a * v) + ((- b) * v) is Element of the carrier of V
((a * v) + ((- b) * v)) + (- (c * v)) is Element of the carrier of V
(((a * v) + ((- b) * v)) + (- (c * v))) + ((b * w) + (c * u)) is Element of the carrier of V
c * (- v) is Element of the carrier of V
((a * v) + ((- b) * v)) + (c * (- v)) is Element of the carrier of V
(((a * v) + ((- b) * v)) + (c * (- v))) + ((b * w) + (c * u)) is Element of the carrier of V
- c is V24() V25() V41() Element of REAL
(- c) * v is Element of the carrier of V
((a * v) + ((- b) * v)) + ((- c) * v) is Element of the carrier of V
(((a * v) + ((- b) * v)) + ((- c) * v)) + ((b * w) + (c * u)) is Element of the carrier of V
a + (- b) is V24() V25() V41() Element of REAL
(a + (- b)) * v is Element of the carrier of V
((a + (- b)) * v) + ((- c) * v) is Element of the carrier of V
(((a + (- b)) * v) + ((- c) * v)) + ((b * w) + (c * u)) is Element of the carrier of V
(a + (- b)) + (- c) is V24() V25() V41() Element of REAL
((a + (- b)) + (- c)) * v is Element of the carrier of V
(((a + (- b)) + (- c)) * v) + ((b * w) + (c * u)) is Element of the carrier of V
(((a + (- b)) + (- c)) * v) + (b * w) is Element of the carrier of V
((((a + (- b)) + (- c)) * v) + (b * w)) + (c * u) is Element of the carrier of V
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
v is Element of the carrier of V
w is Element of the carrier of V
u is Element of the carrier of V
{v,w,u} is V26() Element of K32( the carrier of V)
K32( the carrier of V) is set
u + v is Element of the carrier of V
{v,w,(u + v)} is V26() Element of K32( the carrier of V)
a is V24() V25() V41() Element of REAL
a * v is Element of the carrier of V
b is V24() V25() V41() Element of REAL
b * w is Element of the carrier of V
(a * v) + (b * w) is Element of the carrier of V
c is V24() V25() V41() Element of REAL
c * (u + v) is Element of the carrier of V
((a * v) + (b * w)) + (c * (u + v)) is Element of the carrier of V
0. V is V52(V) Element of the carrier of V
c * v is Element of the carrier of V
c * u is Element of the carrier of V
(c * v) + (c * u) is Element of the carrier of V
((a * v) + (b * w)) + ((c * v) + (c * u)) is Element of the carrier of V
(b * w) + ((c * v) + (c * u)) is Element of the carrier of V
(a * v) + ((b * w) + ((c * v) + (c * u))) is Element of the carrier of V
(b * w) + (c * u) is Element of the carrier of V
(c * v) + ((b * w) + (c * u)) is Element of the carrier of V
(a * v) + ((c * v) + ((b * w) + (c * u))) is Element of the carrier of V
(a * v) + (c * v) is Element of the carrier of V
((a * v) + (c * v)) + ((b * w) + (c * u)) is Element of the carrier of V
a + c is V24() V25() V41() Element of REAL
(a + c) * v is Element of the carrier of V
((a + c) * v) + ((b * w) + (c * u)) is Element of the carrier of V
((a + c) * v) + (b * w) is Element of the carrier of V
(((a + c) * v) + (b * w)) + (c * u) is Element of the carrier of V
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
v is Element of the carrier of V
w is Element of the carrier of V
w + v is Element of the carrier of V
u is Element of the carrier of V
{v,w,u} is V26() Element of K32( the carrier of V)
K32( the carrier of V) is set
u + v is Element of the carrier of V
{v,(w + v),(u + v)} is V26() Element of K32( the carrier of V)
a is V24() V25() V41() Element of REAL
a * v is Element of the carrier of V
b is V24() V25() V41() Element of REAL
b * (w + v) is Element of the carrier of V
(a * v) + (b * (w + v)) is Element of the carrier of V
c is V24() V25() V41() Element of REAL
c * (u + v) is Element of the carrier of V
((a * v) + (b * (w + v))) + (c * (u + v)) is Element of the carrier of V
0. V is V52(V) Element of the carrier of V
b * v is Element of the carrier of V
b * w is Element of the carrier of V
(b * v) + (b * w) is Element of the carrier of V
(a * v) + ((b * v) + (b * w)) is Element of the carrier of V
((a * v) + ((b * v) + (b * w))) + (c * (u + v)) is Element of the carrier of V
(a * v) + (b * v) is Element of the carrier of V
((a * v) + (b * v)) + (b * w) is Element of the carrier of V
(((a * v) + (b * v)) + (b * w)) + (c * (u + v)) is Element of the carrier of V
a + b is V24() V25() V41() Element of REAL
(a + b) * v is Element of the carrier of V
((a + b) * v) + (b * w) is Element of the carrier of V
(((a + b) * v) + (b * w)) + (c * (u + v)) is Element of the carrier of V
c * v is Element of the carrier of V
c * u is Element of the carrier of V
(c * v) + (c * u) is Element of the carrier of V
(((a + b) * v) + (b * w)) + ((c * v) + (c * u)) is Element of the carrier of V
(b * w) + ((c * v) + (c * u)) is Element of the carrier of V
((a + b) * v) + ((b * w) + ((c * v) + (c * u))) is Element of the carrier of V
(b * w) + (c * u) is Element of the carrier of V
(c * v) + ((b * w) + (c * u)) is Element of the carrier of V
((a + b) * v) + ((c * v) + ((b * w) + (c * u))) is Element of the carrier of V
((a + b) * v) + (c * v) is Element of the carrier of V
(((a + b) * v) + (c * v)) + ((b * w) + (c * u)) is Element of the carrier of V
(a + b) + c is V24() V25() V41() Element of REAL
((a + b) + c) * v is Element of the carrier of V
(((a + b) + c) * v) + ((b * w) + (c * u)) is Element of the carrier of V
(((a + b) + c) * v) + (b * w) is Element of the carrier of V
((((a + b) + c) * v) + (b * w)) + (c * u) is Element of the carrier of V
V is V24() V25() V41() Element of REAL
v is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of v is non empty set
w is Element of the carrier of v
u is Element of the carrier of v
a is Element of the carrier of v
{w,u,a} is V26() Element of K32( the carrier of v)
K32( the carrier of v) is set
V * a is Element of the carrier of v
{w,u,(V * a)} is V26() Element of K32( the carrier of v)
b is V24() V25() V41() Element of REAL
b * w is Element of the carrier of v
c is V24() V25() V41() Element of REAL
c * u is Element of the carrier of v
(b * w) + (c * u) is Element of the carrier of v
r3 is V24() V25() V41() Element of REAL
r3 * (V * a) is Element of the carrier of v
((b * w) + (c * u)) + (r3 * (V * a)) is Element of the carrier of v
0. v is V52(v) Element of the carrier of v
r3 * V is V24() V25() V41() Element of REAL
(r3 * V) * a is Element of the carrier of v
((b * w) + (c * u)) + ((r3 * V) * a) is Element of the carrier of v
V is V24() V25() V41() Element of REAL
v is V24() V25() V41() Element of REAL
w is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of w is non empty set
u is Element of the carrier of w
a is Element of the carrier of w
V * a is Element of the carrier of w
b is Element of the carrier of w
{u,a,b} is V26() Element of K32( the carrier of w)
K32( the carrier of w) is set
v * b is Element of the carrier of w
{u,(V * a),(v * b)} is V26() Element of K32( the carrier of w)
c is V24() V25() V41() Element of REAL
c * u is Element of the carrier of w
r3 is V24() V25() V41() Element of REAL
r3 * (V * a) is Element of the carrier of w
(c * u) + (r3 * (V * a)) is Element of the carrier of w
r4 is V24() V25() V41() Element of REAL
r4 * (v * b) is Element of the carrier of w
((c * u) + (r3 * (V * a))) + (r4 * (v * b)) is Element of the carrier of w
0. w is V52(w) Element of the carrier of w
r3 * V is V24() V25() V41() Element of REAL
(r3 * V) * a is Element of the carrier of w
(c * u) + ((r3 * V) * a) is Element of the carrier of w
((c * u) + ((r3 * V) * a)) + (r4 * (v * b)) is Element of the carrier of w
r4 * v is V24() V25() V41() Element of REAL
(r4 * v) * b is Element of the carrier of w
((c * u) + ((r3 * V) * a)) + ((r4 * v) * b) is Element of the carrier of w
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
v is Element of the carrier of V
w is Element of the carrier of V
u is Element of the carrier of V
{v,w,u} is V26() Element of K32( the carrier of V)
K32( the carrier of V) is set
- u is Element of the carrier of V
{v,w,(- u)} is V26() Element of K32( the carrier of V)
(- 1) * u is Element of the carrier of V
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
v is Element of the carrier of V
w is Element of the carrier of V
- w is Element of the carrier of V
u is Element of the carrier of V
{v,w,u} is V26() Element of K32( the carrier of V)
K32( the carrier of V) is set
- u is Element of the carrier of V
{v,(- w),(- u)} is V26() Element of K32( the carrier of V)
(- 1) * u is Element of the carrier of V
(- 1) * w is Element of the carrier of V
V is V24() V25() V41() Element of REAL
v is V24() V25() V41() Element of REAL
w is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of w is non empty set
u is Element of the carrier of w
V * u is Element of the carrier of w
v * u is Element of the carrier of w
a is Element of the carrier of w
{(V * u),(v * u),a} is V26() Element of K32( the carrier of w)
K32( the carrier of w) is set
{(V * u),(v * u)} is V26() Element of K32( the carrier of w)
V is V24() V25() V41() Element of REAL
v is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of v is non empty set
w is Element of the carrier of v
V * w is Element of the carrier of v
u is Element of the carrier of v
{w,(V * w),u} is V26() Element of K32( the carrier of v)
K32( the carrier of v) is set
1 * w is Element of the carrier of v
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
0. V is V52(V) Element of the carrier of V
v is Element of the carrier of V
{v} is V26() Element of K32( the carrier of V)
K32( the carrier of V) is set
Lin {v} is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
w is Element of the carrier of V
{w} is V26() Element of K32( the carrier of V)
Lin {w} is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
u is V24() V25() V41() Element of REAL
u * w is Element of the carrier of V
a is Element of the carrier of V
b is V24() V25() V41() Element of REAL
b * v is Element of the carrier of V
b * u is V24() V25() V41() Element of REAL
(b * u) * w is Element of the carrier of V
b is V24() V25() V41() Element of REAL
b * w is Element of the carrier of V
u " is V24() V25() V41() Element of REAL
(u ") * v is Element of the carrier of V
(u ") * u is V24() V25() V41() Element of REAL
((u ") * u) * w is Element of the carrier of V
1 * w is Element of the carrier of V
b * (u ") is V24() V25() V41() Element of REAL
(b * (u ")) * v is Element of the carrier of V
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
v is Element of the carrier of V
w is Element of the carrier of V
{v,w} is V26() Element of K32( the carrier of V)
K32( the carrier of V) is set
Lin {v,w} is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
u is Element of the carrier of V
a is Element of the carrier of V
{u,a} is V26() Element of K32( the carrier of V)
Lin {u,a} is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
b is V24() V25() V41() Element of REAL
b * u is Element of the carrier of V
c is V24() V25() V41() Element of REAL
c * a is Element of the carrier of V
(b * u) + (c * a) is Element of the carrier of V
r3 is V24() V25() V41() Element of REAL
r3 * u is Element of the carrier of V
r4 is V24() V25() V41() Element of REAL
r4 * a is Element of the carrier of V
(r3 * u) + (r4 * a) is Element of the carrier of V
b * r4 is V24() V25() V41() Element of REAL
c * r3 is V24() V25() V41() Element of REAL
(b * r4) - (c * r3) is V24() V25() V41() Element of REAL
0. V is V52(V) Element of the carrier of V
0 * a is Element of the carrier of V
(0. V) + (0 * a) is Element of the carrier of V
(0. V) + (0. V) is Element of the carrier of V
b " is V24() V25() V41() Element of REAL
(b ") * b is V24() V25() V41() Element of REAL
((b ") * b) * r4 is V24() V25() V41() Element of REAL
(b ") * (c * r3) is V24() V25() V41() Element of REAL
1 * r4 is V24() V25() V41() Element of REAL
(b ") * c is V24() V25() V41() Element of REAL
r3 * ((b ") * c) is V24() V25() V41() Element of REAL
(r3 * ((b ") * c)) * a is Element of the carrier of V
(r3 * u) + ((r3 * ((b ") * c)) * a) is Element of the carrier of V
((b ") * c) * a is Element of the carrier of V
r3 * (((b ") * c) * a) is Element of the carrier of V
(r3 * u) + (r3 * (((b ") * c) * a)) is Element of the carrier of V
u + (((b ") * c) * a) is Element of the carrier of V
r3 * 1 is V24() V25() V41() Element of REAL
(r3 * 1) * (u + (((b ") * c) * a)) is Element of the carrier of V
r3 * ((b ") * b) is V24() V25() V41() Element of REAL
(r3 * ((b ") * b)) * (u + (((b ") * c) * a)) is Element of the carrier of V
r3 * (b ") is V24() V25() V41() Element of REAL
(r3 * (b ")) * b is V24() V25() V41() Element of REAL
((r3 * (b ")) * b) * (u + (((b ") * c) * a)) is Element of the carrier of V
b * (u + (((b ") * c) * a)) is Element of the carrier of V
(r3 * (b ")) * (b * (u + (((b ") * c) * a))) is Element of the carrier of V
b * (((b ") * c) * a) is Element of the carrier of V
(b * u) + (b * (((b ") * c) * a)) is Element of the carrier of V
(r3 * (b ")) * ((b * u) + (b * (((b ") * c) * a))) is Element of the carrier of V
b * ((b ") * c) is V24() V25() V41() Element of REAL
(b * ((b ") * c)) * a is Element of the carrier of V
(b * u) + ((b * ((b ") * c)) * a) is Element of the carrier of V
(r3 * (b ")) * ((b * u) + ((b * ((b ") * c)) * a)) is Element of the carrier of V
b * (b ") is V24() V25() V41() Element of REAL
(b * (b ")) * c is V24() V25() V41() Element of REAL
((b * (b ")) * c) * a is Element of the carrier of V
(b * u) + (((b * (b ")) * c) * a) is Element of the carrier of V
(r3 * (b ")) * ((b * u) + (((b * (b ")) * c) * a)) is Element of the carrier of V
1 * c is V24() V25() V41() Element of REAL
(1 * c) * a is Element of the carrier of V
(b * u) + ((1 * c) * a) is Element of the carrier of V
(r3 * (b ")) * ((b * u) + ((1 * c) * a)) is Element of the carrier of V
(r3 * (b ")) * ((b * u) + (c * a)) is Element of the carrier of V
c " is V24() V25() V41() Element of REAL
(c ") * (b * r4) is V24() V25() V41() Element of REAL
(c ") * (c * r3) is V24() V25() V41() Element of REAL
(c ") * c is V24() V25() V41() Element of REAL
((c ") * c) * r3 is V24() V25() V41() Element of REAL
1 * r3 is V24() V25() V41() Element of REAL
(c ") * b is V24() V25() V41() Element of REAL
r4 * ((c ") * b) is V24() V25() V41() Element of REAL
(r4 * ((c ") * b)) * u is Element of the carrier of V
((r4 * ((c ") * b)) * u) + (r4 * a) is Element of the carrier of V
((c ") * b) * u is Element of the carrier of V
r4 * (((c ") * b) * u) is Element of the carrier of V
(r4 * (((c ") * b) * u)) + (r4 * a) is Element of the carrier of V
(((c ") * b) * u) + a is Element of the carrier of V
r4 * 1 is V24() V25() V41() Element of REAL
(r4 * 1) * ((((c ") * b) * u) + a) is Element of the carrier of V
r4 * ((c ") * c) is V24() V25() V41() Element of REAL
(r4 * ((c ") * c)) * ((((c ") * b) * u) + a) is Element of the carrier of V
r4 * (c ") is V24() V25() V41() Element of REAL
(r4 * (c ")) * c is V24() V25() V41() Element of REAL
((r4 * (c ")) * c) * ((((c ") * b) * u) + a) is Element of the carrier of V
c * ((((c ") * b) * u) + a) is Element of the carrier of V
(r4 * (c ")) * (c * ((((c ") * b) * u) + a)) is Element of the carrier of V
c * (((c ") * b) * u) is Element of the carrier of V
(c * (((c ") * b) * u)) + (c * a) is Element of the carrier of V
(r4 * (c ")) * ((c * (((c ") * b) * u)) + (c * a)) is Element of the carrier of V
c * ((c ") * b) is V24() V25() V41() Element of REAL
(c * ((c ") * b)) * u is Element of the carrier of V
((c * ((c ") * b)) * u) + (c * a) is Element of the carrier of V
(r4 * (c ")) * (((c * ((c ") * b)) * u) + (c * a)) is Element of the carrier of V
c * (c ") is V24() V25() V41() Element of REAL
(c * (c ")) * b is V24() V25() V41() Element of REAL
((c * (c ")) * b) * u is Element of the carrier of V
(((c * (c ")) * b) * u) + (c * a) is Element of the carrier of V
(r4 * (c ")) * ((((c * (c ")) * b) * u) + (c * a)) is Element of the carrier of V
1 * b is V24() V25() V41() Element of REAL
(1 * b) * u is Element of the carrier of V
((1 * b) * u) + (c * a) is Element of the carrier of V
(r4 * (c ")) * (((1 * b) * u) + (c * a)) is Element of the carrier of V
(r4 * (c ")) * ((b * u) + (c * a)) is Element of the carrier of V
c " is V24() V25() V41() Element of REAL
(c ") * v is Element of the carrier of V
(c ") * (b * u) is Element of the carrier of V
(c ") * (c * a) is Element of the carrier of V
((c ") * (b * u)) + ((c ") * (c * a)) is Element of the carrier of V
(c ") * b is V24() V25() V41() Element of REAL
((c ") * b) * u is Element of the carrier of V
(((c ") * b) * u) + ((c ") * (c * a)) is Element of the carrier of V
(c ") * c is V24() V25() V41() Element of REAL
((c ") * c) * a is Element of the carrier of V
(((c ") * b) * u) + (((c ") * c) * a) is Element of the carrier of V
1 * a is Element of the carrier of V
(((c ") * b) * u) + (1 * a) is Element of the carrier of V
(((c ") * b) * u) + a is Element of the carrier of V
((c ") * v) - (((c ") * b) * u) is Element of the carrier of V
- (((c ") * b) * u) is Element of the carrier of V
K196(V,((c ") * v),(- (((c ") * b) * u))) is Element of the carrier of V
((c ") * v) - ((c ") * (b * u)) is Element of the carrier of V
- ((c ") * (b * u)) is Element of the carrier of V
K196(V,((c ") * v),(- ((c ") * (b * u)))) is Element of the carrier of V
v - (b * u) is Element of the carrier of V
- (b * u) is Element of the carrier of V
K196(V,v,(- (b * u))) is Element of the carrier of V
(c ") * (v - (b * u)) is Element of the carrier of V
r4 * ((c ") * (v - (b * u))) is Element of the carrier of V
(r3 * u) + (r4 * ((c ") * (v - (b * u)))) is Element of the carrier of V
r4 * (c ") is V24() V25() V41() Element of REAL
(r4 * (c ")) * (v - (b * u)) is Element of the carrier of V
(r3 * u) + ((r4 * (c ")) * (v - (b * u))) is Element of the carrier of V
(r4 * (c ")) * v is Element of the carrier of V
(r4 * (c ")) * (b * u) is Element of the carrier of V
((r4 * (c ")) * v) - ((r4 * (c ")) * (b * u)) is Element of the carrier of V
- ((r4 * (c ")) * (b * u)) is Element of the carrier of V
K196(V,((r4 * (c ")) * v),(- ((r4 * (c ")) * (b * u)))) is Element of the carrier of V
(r3 * u) + (((r4 * (c ")) * v) - ((r4 * (c ")) * (b * u))) is Element of the carrier of V
(r3 * u) + ((r4 * (c ")) * v) is Element of the carrier of V
((r3 * u) + ((r4 * (c ")) * v)) - ((r4 * (c ")) * (b * u)) is Element of the carrier of V
K196(V,((r3 * u) + ((r4 * (c ")) * v)),(- ((r4 * (c ")) * (b * u)))) is Element of the carrier of V
((r4 * (c ")) * v) + (r3 * u) is Element of the carrier of V
(r4 * (c ")) * b is V24() V25() V41() Element of REAL
((r4 * (c ")) * b) * u is Element of the carrier of V
(((r4 * (c ")) * v) + (r3 * u)) - (((r4 * (c ")) * b) * u) is Element of the carrier of V
- (((r4 * (c ")) * b) * u) is Element of the carrier of V
K196(V,(((r4 * (c ")) * v) + (r3 * u)),(- (((r4 * (c ")) * b) * u))) is Element of the carrier of V
(r3 * u) - (((r4 * (c ")) * b) * u) is Element of the carrier of V
K196(V,(r3 * u),(- (((r4 * (c ")) * b) * u))) is Element of the carrier of V
((r4 * (c ")) * v) + ((r3 * u) - (((r4 * (c ")) * b) * u)) is Element of the carrier of V
r3 - ((r4 * (c ")) * b) is V24() V25() V41() Element of REAL
(r3 - ((r4 * (c ")) * b)) * u is Element of the carrier of V
((r4 * (c ")) * v) + ((r3 - ((r4 * (c ")) * b)) * u) is Element of the carrier of V
c * w is Element of the carrier of V
c * ((r4 * (c ")) * v) is Element of the carrier of V
c * ((r3 - ((r4 * (c ")) * b)) * u) is Element of the carrier of V
(c * ((r4 * (c ")) * v)) + (c * ((r3 - ((r4 * (c ")) * b)) * u)) is Element of the carrier of V
c * (r4 * (c ")) is V24() V25() V41() Element of REAL
(c * (r4 * (c "))) * v is Element of the carrier of V
((c * (r4 * (c "))) * v) + (c * ((r3 - ((r4 * (c ")) * b)) * u)) is Element of the carrier of V
c * (c ") is V24() V25() V41() Element of REAL
r4 * (c * (c ")) is V24() V25() V41() Element of REAL
(r4 * (c * (c "))) * v is Element of the carrier of V
((r4 * (c * (c "))) * v) + (c * ((r3 - ((r4 * (c ")) * b)) * u)) is Element of the carrier of V
r4 * 1 is V24() V25() V41() Element of REAL
(r4 * 1) * v is Element of the carrier of V
((r4 * 1) * v) + (c * ((r3 - ((r4 * (c ")) * b)) * u)) is Element of the carrier of V
r4 * v is Element of the carrier of V
c * (r3 - ((r4 * (c ")) * b)) is V24() V25() V41() Element of REAL
(c * (r3 - ((r4 * (c ")) * b))) * u is Element of the carrier of V
(r4 * v) + ((c * (r3 - ((r4 * (c ")) * b))) * u) is Element of the carrier of V
r4 * b is V24() V25() V41() Element of REAL
(c * (c ")) * (r4 * b) is V24() V25() V41() Element of REAL
(c * r3) - ((c * (c ")) * (r4 * b)) is V24() V25() V41() Element of REAL
((c * r3) - ((c * (c ")) * (r4 * b))) * u is Element of the carrier of V
(r4 * v) + (((c * r3) - ((c * (c ")) * (r4 * b))) * u) is Element of the carrier of V
1 * (r4 * b) is V24() V25() V41() Element of REAL
(c * r3) - (1 * (r4 * b)) is V24() V25() V41() Element of REAL
((c * r3) - (1 * (r4 * b))) * u is Element of the carrier of V
(r4 * v) + (((c * r3) - (1 * (r4 * b))) * u) is Element of the carrier of V
- ((b * r4) - (c * r3)) is V24() V25() V41() Element of REAL
(- ((b * r4) - (c * r3))) * u is Element of the carrier of V
(r4 * v) + ((- ((b * r4) - (c * r3))) * u) is Element of the carrier of V
((b * r4) - (c * r3)) * u is Element of the carrier of V
- (((b * r4) - (c * r3)) * u) is Element of the carrier of V
(r4 * v) + (- (((b * r4) - (c * r3)) * u)) is Element of the carrier of V
(c * w) - (r4 * v) is Element of the carrier of V
- (r4 * v) is Element of the carrier of V
K196(V,(c * w),(- (r4 * v))) is Element of the carrier of V
- ((c * w) - (r4 * v)) is Element of the carrier of V
- (c * w) is Element of the carrier of V
(r4 * v) + (- (c * w)) is Element of the carrier of V
((b * r4) - (c * r3)) " is V24() V25() V41() Element of REAL
(((b * r4) - (c * r3)) ") * ((b * r4) - (c * r3)) is V24() V25() V41() Element of REAL
((((b * r4) - (c * r3)) ") * ((b * r4) - (c * r3))) * u is Element of the carrier of V
(((b * r4) - (c * r3)) ") * ((r4 * v) + (- (c * w))) is Element of the carrier of V
1 * u is Element of the carrier of V
(((b * r4) - (c * r3)) ") * (r4 * v) is Element of the carrier of V
(((b * r4) - (c * r3)) ") * (- (c * w)) is Element of the carrier of V
((((b * r4) - (c * r3)) ") * (r4 * v)) + ((((b * r4) - (c * r3)) ") * (- (c * w))) is Element of the carrier of V
(((b * r4) - (c * r3)) ") * r4 is V24() V25() V41() Element of REAL
((((b * r4) - (c * r3)) ") * r4) * v is Element of the carrier of V
(((((b * r4) - (c * r3)) ") * r4) * v) + ((((b * r4) - (c * r3)) ") * (- (c * w))) is Element of the carrier of V
- c is V24() V25() V41() Element of REAL
(- c) * w is Element of the carrier of V
(((b * r4) - (c * r3)) ") * ((- c) * w) is Element of the carrier of V
(((((b * r4) - (c * r3)) ") * r4) * v) + ((((b * r4) - (c * r3)) ") * ((- c) * w)) is Element of the carrier of V
(((b * r4) - (c * r3)) ") * (- c) is V24() V25() V41() Element of REAL
((((b * r4) - (c * r3)) ") * (- c)) * w is Element of the carrier of V
(((((b * r4) - (c * r3)) ") * r4) * v) + (((((b * r4) - (c * r3)) ") * (- c)) * w) is Element of the carrier of V
- (((b * r4) - (c * r3)) ") is V24() V25() V41() Element of REAL
(- (((b * r4) - (c * r3)) ")) * c is V24() V25() V41() Element of REAL
((- (((b * r4) - (c * r3)) ")) * c) * w is Element of the carrier of V
(((((b * r4) - (c * r3)) ") * r4) * v) + (((- (((b * r4) - (c * r3)) ")) * c) * w) is Element of the carrier of V
(- (((b * r4) - (c * r3)) ")) * (c * w) is Element of the carrier of V
(((((b * r4) - (c * r3)) ") * r4) * v) + ((- (((b * r4) - (c * r3)) ")) * (c * w)) is Element of the carrier of V
(((b * r4) - (c * r3)) ") * (c * w) is Element of the carrier of V
- ((((b * r4) - (c * r3)) ") * (c * w)) is Element of the carrier of V
(((((b * r4) - (c * r3)) ") * r4) * v) + (- ((((b * r4) - (c * r3)) ") * (c * w))) is Element of the carrier of V
(((b * r4) - (c * r3)) ") * c is V24() V25() V41() Element of REAL
((((b * r4) - (c * r3)) ") * c) * w is Element of the carrier of V
- (((((b * r4) - (c * r3)) ") * c) * w) is Element of the carrier of V
(((((b * r4) - (c * r3)) ") * r4) * v) + (- (((((b * r4) - (c * r3)) ") * c) * w)) is Element of the carrier of V
((((b * r4) - (c * r3)) ") * (r4 * v)) - (((((b * r4) - (c * r3)) ") * c) * w) is Element of the carrier of V
K196(V,((((b * r4) - (c * r3)) ") * (r4 * v)),(- (((((b * r4) - (c * r3)) ") * c) * w))) is Element of the carrier of V
((c ") * b) * (((((b * r4) - (c * r3)) ") * (r4 * v)) - (((((b * r4) - (c * r3)) ") * c) * w)) is Element of the carrier of V
((c ") * v) - (((c ") * b) * (((((b * r4) - (c * r3)) ") * (r4 * v)) - (((((b * r4) - (c * r3)) ") * c) * w))) is Element of the carrier of V
- (((c ") * b) * (((((b * r4) - (c * r3)) ") * (r4 * v)) - (((((b * r4) - (c * r3)) ") * c) * w))) is Element of the carrier of V
K196(V,((c ") * v),(- (((c ") * b) * (((((b * r4) - (c * r3)) ") * (r4 * v)) - (((((b * r4) - (c * r3)) ") * c) * w))))) is Element of the carrier of V
((((b * r4) - (c * r3)) ") * (r4 * v)) - ((((b * r4) - (c * r3)) ") * (c * w)) is Element of the carrier of V
K196(V,((((b * r4) - (c * r3)) ") * (r4 * v)),(- ((((b * r4) - (c * r3)) ") * (c * w)))) is Element of the carrier of V
((c ") * b) * (((((b * r4) - (c * r3)) ") * (r4 * v)) - ((((b * r4) - (c * r3)) ") * (c * w))) is Element of the carrier of V
((c ") * v) - (((c ") * b) * (((((b * r4) - (c * r3)) ") * (r4 * v)) - ((((b * r4) - (c * r3)) ") * (c * w)))) is Element of the carrier of V
- (((c ") * b) * (((((b * r4) - (c * r3)) ") * (r4 * v)) - ((((b * r4) - (c * r3)) ") * (c * w)))) is Element of the carrier of V
K196(V,((c ") * v),(- (((c ") * b) * (((((b * r4) - (c * r3)) ") * (r4 * v)) - ((((b * r4) - (c * r3)) ") * (c * w)))))) is Element of the carrier of V
(r4 * v) - (c * w) is Element of the carrier of V
K196(V,(r4 * v),(- (c * w))) is Element of the carrier of V
(((b * r4) - (c * r3)) ") * ((r4 * v) - (c * w)) is Element of the carrier of V
((c ") * b) * ((((b * r4) - (c * r3)) ") * ((r4 * v) - (c * w))) is Element of the carrier of V
((c ") * v) - (((c ") * b) * ((((b * r4) - (c * r3)) ") * ((r4 * v) - (c * w)))) is Element of the carrier of V
- (((c ") * b) * ((((b * r4) - (c * r3)) ") * ((r4 * v) - (c * w)))) is Element of the carrier of V
K196(V,((c ") * v),(- (((c ") * b) * ((((b * r4) - (c * r3)) ") * ((r4 * v) - (c * w)))))) is Element of the carrier of V
b * (c ") is V24() V25() V41() Element of REAL
(b * (c ")) * (((b * r4) - (c * r3)) ") is V24() V25() V41() Element of REAL
((b * (c ")) * (((b * r4) - (c * r3)) ")) * ((r4 * v) - (c * w)) is Element of the carrier of V
((c ") * v) - (((b * (c ")) * (((b * r4) - (c * r3)) ")) * ((r4 * v) - (c * w))) is Element of the carrier of V
- (((b * (c ")) * (((b * r4) - (c * r3)) ")) * ((r4 * v) - (c * w))) is Element of the carrier of V
K196(V,((c ") * v),(- (((b * (c ")) * (((b * r4) - (c * r3)) ")) * ((r4 * v) - (c * w))))) is Element of the carrier of V
(((b * r4) - (c * r3)) ") * (c ") is V24() V25() V41() Element of REAL
b * ((((b * r4) - (c * r3)) ") * (c ")) is V24() V25() V41() Element of REAL
(b * ((((b * r4) - (c * r3)) ") * (c "))) * ((r4 * v) - (c * w)) is Element of the carrier of V
((c ") * v) - ((b * ((((b * r4) - (c * r3)) ") * (c "))) * ((r4 * v) - (c * w))) is Element of the carrier of V
- ((b * ((((b * r4) - (c * r3)) ") * (c "))) * ((r4 * v) - (c * w))) is Element of the carrier of V
K196(V,((c ") * v),(- ((b * ((((b * r4) - (c * r3)) ") * (c "))) * ((r4 * v) - (c * w))))) is Element of the carrier of V
((((b * r4) - (c * r3)) ") * (c ")) * ((r4 * v) - (c * w)) is Element of the carrier of V
b * (((((b * r4) - (c * r3)) ") * (c ")) * ((r4 * v) - (c * w))) is Element of the carrier of V
((c ") * v) - (b * (((((b * r4) - (c * r3)) ") * (c ")) * ((r4 * v) - (c * w)))) is Element of the carrier of V
- (b * (((((b * r4) - (c * r3)) ") * (c ")) * ((r4 * v) - (c * w)))) is Element of the carrier of V
K196(V,((c ") * v),(- (b * (((((b * r4) - (c * r3)) ") * (c ")) * ((r4 * v) - (c * w)))))) is Element of the carrier of V
(c ") * ((r4 * v) - (c * w)) is Element of the carrier of V
(((b * r4) - (c * r3)) ") * ((c ") * ((r4 * v) - (c * w))) is Element of the carrier of V
b * ((((b * r4) - (c * r3)) ") * ((c ") * ((r4 * v) - (c * w)))) is Element of the carrier of V
((c ") * v) - (b * ((((b * r4) - (c * r3)) ") * ((c ") * ((r4 * v) - (c * w))))) is Element of the carrier of V
- (b * ((((b * r4) - (c * r3)) ") * ((c ") * ((r4 * v) - (c * w))))) is Element of the carrier of V
K196(V,((c ") * v),(- (b * ((((b * r4) - (c * r3)) ") * ((c ") * ((r4 * v) - (c * w))))))) is Element of the carrier of V
(c ") * (r4 * v) is Element of the carrier of V
(c ") * (c * w) is Element of the carrier of V
((c ") * (r4 * v)) - ((c ") * (c * w)) is Element of the carrier of V
- ((c ") * (c * w)) is Element of the carrier of V
K196(V,((c ") * (r4 * v)),(- ((c ") * (c * w)))) is Element of the carrier of V
(((b * r4) - (c * r3)) ") * (((c ") * (r4 * v)) - ((c ") * (c * w))) is Element of the carrier of V
b * ((((b * r4) - (c * r3)) ") * (((c ") * (r4 * v)) - ((c ") * (c * w)))) is Element of the carrier of V
((c ") * v) - (b * ((((b * r4) - (c * r3)) ") * (((c ") * (r4 * v)) - ((c ") * (c * w))))) is Element of the carrier of V
- (b * ((((b * r4) - (c * r3)) ") * (((c ") * (r4 * v)) - ((c ") * (c * w))))) is Element of the carrier of V
K196(V,((c ") * v),(- (b * ((((b * r4) - (c * r3)) ") * (((c ") * (r4 * v)) - ((c ") * (c * w))))))) is Element of the carrier of V
((c ") * c) * w is Element of the carrier of V
((c ") * (r4 * v)) - (((c ") * c) * w) is Element of the carrier of V
- (((c ") * c) * w) is Element of the carrier of V
K196(V,((c ") * (r4 * v)),(- (((c ") * c) * w))) is Element of the carrier of V
(((b * r4) - (c * r3)) ") * (((c ") * (r4 * v)) - (((c ") * c) * w)) is Element of the carrier of V
b * ((((b * r4) - (c * r3)) ") * (((c ") * (r4 * v)) - (((c ") * c) * w))) is Element of the carrier of V
((c ") * v) - (b * ((((b * r4) - (c * r3)) ") * (((c ") * (r4 * v)) - (((c ") * c) * w)))) is Element of the carrier of V
- (b * ((((b * r4) - (c * r3)) ") * (((c ") * (r4 * v)) - (((c ") * c) * w)))) is Element of the carrier of V
K196(V,((c ") * v),(- (b * ((((b * r4) - (c * r3)) ") * (((c ") * (r4 * v)) - (((c ") * c) * w)))))) is Element of the carrier of V
(c ") * r4 is V24() V25() V41() Element of REAL
((c ") * r4) * v is Element of the carrier of V
(((c ") * r4) * v) - (((c ") * c) * w) is Element of the carrier of V
K196(V,(((c ") * r4) * v),(- (((c ") * c) * w))) is Element of the carrier of V
(((b * r4) - (c * r3)) ") * ((((c ") * r4) * v) - (((c ") * c) * w)) is Element of the carrier of V
b * ((((b * r4) - (c * r3)) ") * ((((c ") * r4) * v) - (((c ") * c) * w))) is Element of the carrier of V
((c ") * v) - (b * ((((b * r4) - (c * r3)) ") * ((((c ") * r4) * v) - (((c ") * c) * w)))) is Element of the carrier of V
- (b * ((((b * r4) - (c * r3)) ") * ((((c ") * r4) * v) - (((c ") * c) * w)))) is Element of the carrier of V
K196(V,((c ") * v),(- (b * ((((b * r4) - (c * r3)) ") * ((((c ") * r4) * v) - (((c ") * c) * w)))))) is Element of the carrier of V
1 * w is Element of the carrier of V
(((c ") * r4) * v) - (1 * w) is Element of the carrier of V
- (1 * w) is Element of the carrier of V
K196(V,(((c ") * r4) * v),(- (1 * w))) is Element of the carrier of V
(((b * r4) - (c * r3)) ") * ((((c ") * r4) * v) - (1 * w)) is Element of the carrier of V
b * ((((b * r4) - (c * r3)) ") * ((((c ") * r4) * v) - (1 * w))) is Element of the carrier of V
((c ") * v) - (b * ((((b * r4) - (c * r3)) ") * ((((c ") * r4) * v) - (1 * w)))) is Element of the carrier of V
- (b * ((((b * r4) - (c * r3)) ") * ((((c ") * r4) * v) - (1 * w)))) is Element of the carrier of V
K196(V,((c ") * v),(- (b * ((((b * r4) - (c * r3)) ") * ((((c ") * r4) * v) - (1 * w)))))) is Element of the carrier of V
(((c ") * r4) * v) - w is Element of the carrier of V
- w is Element of the carrier of V
K196(V,(((c ") * r4) * v),(- w)) is Element of the carrier of V
(((b * r4) - (c * r3)) ") * ((((c ") * r4) * v) - w) is Element of the carrier of V
b * ((((b * r4) - (c * r3)) ") * ((((c ") * r4) * v) - w)) is Element of the carrier of V
((c ") * v) - (b * ((((b * r4) - (c * r3)) ") * ((((c ") * r4) * v) - w))) is Element of the carrier of V
- (b * ((((b * r4) - (c * r3)) ") * ((((c ") * r4) * v) - w))) is Element of the carrier of V
K196(V,((c ") * v),(- (b * ((((b * r4) - (c * r3)) ") * ((((c ") * r4) * v) - w))))) is Element of the carrier of V
(((b * r4) - (c * r3)) ") * (((c ") * r4) * v) is Element of the carrier of V
(((b * r4) - (c * r3)) ") * w is Element of the carrier of V
((((b * r4) - (c * r3)) ") * (((c ") * r4) * v)) - ((((b * r4) - (c * r3)) ") * w) is Element of the carrier of V
- ((((b * r4) - (c * r3)) ") * w) is Element of the carrier of V
K196(V,((((b * r4) - (c * r3)) ") * (((c ") * r4) * v)),(- ((((b * r4) - (c * r3)) ") * w))) is Element of the carrier of V
b * (((((b * r4) - (c * r3)) ") * (((c ") * r4) * v)) - ((((b * r4) - (c * r3)) ") * w)) is Element of the carrier of V
((c ") * v) - (b * (((((b * r4) - (c * r3)) ") * (((c ") * r4) * v)) - ((((b * r4) - (c * r3)) ") * w))) is Element of the carrier of V
- (b * (((((b * r4) - (c * r3)) ") * (((c ") * r4) * v)) - ((((b * r4) - (c * r3)) ") * w))) is Element of the carrier of V
K196(V,((c ") * v),(- (b * (((((b * r4) - (c * r3)) ") * (((c ") * r4) * v)) - ((((b * r4) - (c * r3)) ") * w))))) is Element of the carrier of V
b * ((((b * r4) - (c * r3)) ") * (((c ") * r4) * v)) is Element of the carrier of V
b * ((((b * r4) - (c * r3)) ") * w) is Element of the carrier of V
(b * ((((b * r4) - (c * r3)) ") * (((c ") * r4) * v))) - (b * ((((b * r4) - (c * r3)) ") * w)) is Element of the carrier of V
- (b * ((((b * r4) - (c * r3)) ") * w)) is Element of the carrier of V
K196(V,(b * ((((b * r4) - (c * r3)) ") * (((c ") * r4) * v))),(- (b * ((((b * r4) - (c * r3)) ") * w)))) is Element of the carrier of V
((c ") * v) - ((b * ((((b * r4) - (c * r3)) ") * (((c ") * r4) * v))) - (b * ((((b * r4) - (c * r3)) ") * w))) is Element of the carrier of V
- ((b * ((((b * r4) - (c * r3)) ") * (((c ") * r4) * v))) - (b * ((((b * r4) - (c * r3)) ") * w))) is Element of the carrier of V
K196(V,((c ") * v),(- ((b * ((((b * r4) - (c * r3)) ") * (((c ") * r4) * v))) - (b * ((((b * r4) - (c * r3)) ") * w))))) is Element of the carrier of V
((c ") * v) - (b * ((((b * r4) - (c * r3)) ") * (((c ") * r4) * v))) is Element of the carrier of V
- (b * ((((b * r4) - (c * r3)) ") * (((c ") * r4) * v))) is Element of the carrier of V
K196(V,((c ") * v),(- (b * ((((b * r4) - (c * r3)) ") * (((c ") * r4) * v))))) is Element of the carrier of V
(((c ") * v) - (b * ((((b * r4) - (c * r3)) ") * (((c ") * r4) * v)))) + (b * ((((b * r4) - (c * r3)) ") * w)) is Element of the carrier of V
b * (((b * r4) - (c * r3)) ") is V24() V25() V41() Element of REAL
(b * (((b * r4) - (c * r3)) ")) * w is Element of the carrier of V
(((c ") * v) - (b * ((((b * r4) - (c * r3)) ") * (((c ") * r4) * v)))) + ((b * (((b * r4) - (c * r3)) ")) * w) is Element of the carrier of V
(b * (((b * r4) - (c * r3)) ")) * (((c ") * r4) * v) is Element of the carrier of V
((c ") * v) - ((b * (((b * r4) - (c * r3)) ")) * (((c ") * r4) * v)) is Element of the carrier of V
- ((b * (((b * r4) - (c * r3)) ")) * (((c ") * r4) * v)) is Element of the carrier of V
K196(V,((c ") * v),(- ((b * (((b * r4) - (c * r3)) ")) * (((c ") * r4) * v)))) is Element of the carrier of V
(((c ") * v) - ((b * (((b * r4) - (c * r3)) ")) * (((c ") * r4) * v))) + ((b * (((b * r4) - (c * r3)) ")) * w) is Element of the carrier of V
(b * (((b * r4) - (c * r3)) ")) * ((c ") * r4) is V24() V25() V41() Element of REAL
((b * (((b * r4) - (c * r3)) ")) * ((c ") * r4)) * v is Element of the carrier of V
((c ") * v) - (((b * (((b * r4) - (c * r3)) ")) * ((c ") * r4)) * v) is Element of the carrier of V
- (((b * (((b * r4) - (c * r3)) ")) * ((c ") * r4)) * v) is Element of the carrier of V
K196(V,((c ") * v),(- (((b * (((b * r4) - (c * r3)) ")) * ((c ") * r4)) * v))) is Element of the carrier of V
(((c ") * v) - (((b * (((b * r4) - (c * r3)) ")) * ((c ") * r4)) * v)) + ((b * (((b * r4) - (c * r3)) ")) * w) is Element of the carrier of V
(c ") - ((b * (((b * r4) - (c * r3)) ")) * ((c ") * r4)) is V24() V25() V41() Element of REAL
((c ") - ((b * (((b * r4) - (c * r3)) ")) * ((c ") * r4))) * v is Element of the carrier of V
(((b * r4) - (c * r3)) ") * b is V24() V25() V41() Element of REAL
((((b * r4) - (c * r3)) ") * b) * w is Element of the carrier of V
(((c ") - ((b * (((b * r4) - (c * r3)) ")) * ((c ") * r4))) * v) + (((((b * r4) - (c * r3)) ") * b) * w) is Element of the carrier of V
b * ((((b * r4) - (c * r3)) ") * r4) is V24() V25() V41() Element of REAL
1 - (b * ((((b * r4) - (c * r3)) ") * r4)) is V24() V25() V41() Element of REAL
(c ") * (1 - (b * ((((b * r4) - (c * r3)) ") * r4))) is V24() V25() V41() Element of REAL
(((b * r4) - (c * r3)) ") * (b * r4) is V24() V25() V41() Element of REAL
((((b * r4) - (c * r3)) ") * ((b * r4) - (c * r3))) - ((((b * r4) - (c * r3)) ") * (b * r4)) is V24() V25() V41() Element of REAL
(c ") * (((((b * r4) - (c * r3)) ") * ((b * r4) - (c * r3))) - ((((b * r4) - (c * r3)) ") * (b * r4))) is V24() V25() V41() Element of REAL
((c ") * c) * (((b * r4) - (c * r3)) ") is V24() V25() V41() Element of REAL
- r3 is V24() V25() V41() Element of REAL
(((c ") * c) * (((b * r4) - (c * r3)) ")) * (- r3) is V24() V25() V41() Element of REAL
1 * (((b * r4) - (c * r3)) ") is V24() V25() V41() Element of REAL
(1 * (((b * r4) - (c * r3)) ")) * (- r3) is V24() V25() V41() Element of REAL
(((b * r4) - (c * r3)) ") * r3 is V24() V25() V41() Element of REAL
- ((((b * r4) - (c * r3)) ") * r3) is V24() V25() V41() Element of REAL
((((b * r4) - (c * r3)) ") * r3) * v is Element of the carrier of V
- (((((b * r4) - (c * r3)) ") * r3) * v) is Element of the carrier of V
(- (((((b * r4) - (c * r3)) ") * r3) * v)) + (((((b * r4) - (c * r3)) ") * b) * w) is Element of the carrier of V
- ((((b * r4) - (c * r3)) ") * c) is V24() V25() V41() Element of REAL
b " is V24() V25() V41() Element of REAL
((((b * r4) - (c * r3)) ") * c) * (b ") is V24() V25() V41() Element of REAL
(((((b * r4) - (c * r3)) ") * c) * (b ")) * r3 is V24() V25() V41() Element of REAL
(b ") + ((((((b * r4) - (c * r3)) ") * c) * (b ")) * r3) is V24() V25() V41() Element of REAL
(((b * r4) - (c * r3)) ") * (c * r3) is V24() V25() V41() Element of REAL
1 + ((((b * r4) - (c * r3)) ") * (c * r3)) is V24() V25() V41() Element of REAL
(b ") * (1 + ((((b * r4) - (c * r3)) ") * (c * r3))) is V24() V25() V41() Element of REAL
((((b * r4) - (c * r3)) ") * ((b * r4) - (c * r3))) + ((((b * r4) - (c * r3)) ") * (c * r3)) is V24() V25() V41() Element of REAL
(b ") * (((((b * r4) - (c * r3)) ") * ((b * r4) - (c * r3))) + ((((b * r4) - (c * r3)) ") * (c * r3))) is V24() V25() V41() Element of REAL
(b ") * b is V24() V25() V41() Element of REAL
((b ") * b) * r4 is V24() V25() V41() Element of REAL
(((b * r4) - (c * r3)) ") * (((b ") * b) * r4) is V24() V25() V41() Element of REAL
1 * r4 is V24() V25() V41() Element of REAL
(((b * r4) - (c * r3)) ") * (1 * r4) is V24() V25() V41() Element of REAL
(b ") * v is Element of the carrier of V
(b ") * (b * u) is Element of the carrier of V
(b ") * (c * a) is Element of the carrier of V
((b ") * (b * u)) + ((b ") * (c * a)) is Element of the carrier of V
((b ") * b) * u is Element of the carrier of V
(((b ") * b) * u) + ((b ") * (c * a)) is Element of the carrier of V
(1 * u) + ((b ") * (c * a)) is Element of the carrier of V
u + ((b ") * (c * a)) is Element of the carrier of V
c * (b ") is V24() V25() V41() Element of REAL
(c * (b ")) * a is Element of the carrier of V
u + ((c * (b ")) * a) is Element of the carrier of V
((b ") * v) - ((c * (b ")) * a) is Element of the carrier of V
- ((c * (b ")) * a) is Element of the carrier of V
K196(V,((b ") * v),(- ((c * (b ")) * a))) is Element of the carrier of V
r3 * ((b ") * v) is Element of the carrier of V
r3 * ((c * (b ")) * a) is Element of the carrier of V
(r3 * ((b ") * v)) - (r3 * ((c * (b ")) * a)) is Element of the carrier of V
- (r3 * ((c * (b ")) * a)) is Element of the carrier of V
K196(V,(r3 * ((b ") * v)),(- (r3 * ((c * (b ")) * a)))) is Element of the carrier of V
((r3 * ((b ") * v)) - (r3 * ((c * (b ")) * a))) + (r4 * a) is Element of the carrier of V
r3 * (b ") is V24() V25() V41() Element of REAL
(r3 * (b ")) * v is Element of the carrier of V
(b ") * c is V24() V25() V41() Element of REAL
((b ") * c) * a is Element of the carrier of V
r3 * (((b ") * c) * a) is Element of the carrier of V
((r3 * (b ")) * v) - (r3 * (((b ") * c) * a)) is Element of the carrier of V
- (r3 * (((b ") * c) * a)) is Element of the carrier of V
K196(V,((r3 * (b ")) * v),(- (r3 * (((b ") * c) * a)))) is Element of the carrier of V
(((r3 * (b ")) * v) - (r3 * (((b ") * c) * a))) + (r4 * a) is Element of the carrier of V
r3 * ((b ") * c) is V24() V25() V41() Element of REAL
(r3 * ((b ") * c)) * a is Element of the carrier of V
((r3 * (b ")) * v) - ((r3 * ((b ") * c)) * a) is Element of the carrier of V
- ((r3 * ((b ") * c)) * a) is Element of the carrier of V
K196(V,((r3 * (b ")) * v),(- ((r3 * ((b ") * c)) * a))) is Element of the carrier of V
(((r3 * (b ")) * v) - ((r3 * ((b ") * c)) * a)) + (r4 * a) is Element of the carrier of V
r3 * c is V24() V25() V41() Element of REAL
(b ") * (r3 * c) is V24() V25() V41() Element of REAL
((b ") * (r3 * c)) * a is Element of the carrier of V
((r3 * (b ")) * v) - (((b ") * (r3 * c)) * a) is Element of the carrier of V
- (((b ") * (r3 * c)) * a) is Element of the carrier of V
K196(V,((r3 * (b ")) * v),(- (((b ") * (r3 * c)) * a))) is Element of the carrier of V
(((r3 * (b ")) * v) - (((b ") * (r3 * c)) * a)) + (r4 * a) is Element of the carrier of V
(b ") * r3 is V24() V25() V41() Element of REAL
((b ") * r3) * v is Element of the carrier of V
(r3 * c) * a is Element of the carrier of V
(b ") * ((r3 * c) * a) is Element of the carrier of V
(((b ") * r3) * v) - ((b ") * ((r3 * c) * a)) is Element of the carrier of V
- ((b ") * ((r3 * c) * a)) is Element of the carrier of V
K196(V,(((b ") * r3) * v),(- ((b ") * ((r3 * c) * a)))) is Element of the carrier of V
((((b ") * r3) * v) - ((b ") * ((r3 * c) * a))) + (r4 * a) is Element of the carrier of V
r3 * v is Element of the carrier of V
(b ") * (r3 * v) is Element of the carrier of V
((b ") * (r3 * v)) - ((b ") * ((r3 * c) * a)) is Element of the carrier of V
K196(V,((b ") * (r3 * v)),(- ((b ") * ((r3 * c) * a)))) is Element of the carrier of V
(((b ") * (r3 * v)) - ((b ") * ((r3 * c) * a))) + (r4 * a) is Element of the carrier of V
b * w is Element of the carrier of V
b * (((b ") * (r3 * v)) - ((b ") * ((r3 * c) * a))) is Element of the carrier of V
b * (r4 * a) is Element of the carrier of V
(b * (((b ") * (r3 * v)) - ((b ") * ((r3 * c) * a)))) + (b * (r4 * a)) is Element of the carrier of V
(b * r4) * a is Element of the carrier of V
(b * (((b ") * (r3 * v)) - ((b ") * ((r3 * c) * a)))) + ((b * r4) * a) is Element of the carrier of V
b * ((b ") * (r3 * v)) is Element of the carrier of V
b * ((b ") * ((r3 * c) * a)) is Element of the carrier of V
(b * ((b ") * (r3 * v))) - (b * ((b ") * ((r3 * c) * a))) is Element of the carrier of V
- (b * ((b ") * ((r3 * c) * a))) is Element of the carrier of V
K196(V,(b * ((b ") * (r3 * v))),(- (b * ((b ") * ((r3 * c) * a))))) is Element of the carrier of V
((b * ((b ") * (r3 * v))) - (b * ((b ") * ((r3 * c) * a)))) + ((b * r4) * a) is Element of the carrier of V
b * (b ") is V24() V25() V41() Element of REAL
(b * (b ")) * (r3 * v) is Element of the carrier of V
((b * (b ")) * (r3 * v)) - (b * ((b ") * ((r3 * c) * a))) is Element of the carrier of V
K196(V,((b * (b ")) * (r3 * v)),(- (b * ((b ") * ((r3 * c) * a))))) is Element of the carrier of V
(((b * (b ")) * (r3 * v)) - (b * ((b ") * ((r3 * c) * a)))) + ((b * r4) * a) is Element of the carrier of V
(b * (b ")) * ((r3 * c) * a) is Element of the carrier of V
((b * (b ")) * (r3 * v)) - ((b * (b ")) * ((r3 * c) * a)) is Element of the carrier of V
- ((b * (b ")) * ((r3 * c) * a)) is Element of the carrier of V
K196(V,((b * (b ")) * (r3 * v)),(- ((b * (b ")) * ((r3 * c) * a)))) is Element of the carrier of V
(((b * (b ")) * (r3 * v)) - ((b * (b ")) * ((r3 * c) * a))) + ((b * r4) * a) is Element of the carrier of V
1 * (r3 * v) is Element of the carrier of V
(1 * (r3 * v)) - ((b * (b ")) * ((r3 * c) * a)) is Element of the carrier of V
K196(V,(1 * (r3 * v)),(- ((b * (b ")) * ((r3 * c) * a)))) is Element of the carrier of V
((1 * (r3 * v)) - ((b * (b ")) * ((r3 * c) * a))) + ((b * r4) * a) is Element of the carrier of V
1 * ((r3 * c) * a) is Element of the carrier of V
(1 * (r3 * v)) - (1 * ((r3 * c) * a)) is Element of the carrier of V
- (1 * ((r3 * c) * a)) is Element of the carrier of V
K196(V,(1 * (r3 * v)),(- (1 * ((r3 * c) * a)))) is Element of the carrier of V
((1 * (r3 * v)) - (1 * ((r3 * c) * a))) + ((b * r4) * a) is Element of the carrier of V
(r3 * v) - (1 * ((r3 * c) * a)) is Element of the carrier of V
K196(V,(r3 * v),(- (1 * ((r3 * c) * a)))) is Element of the carrier of V
((r3 * v) - (1 * ((r3 * c) * a))) + ((b * r4) * a) is Element of the carrier of V
(r3 * v) - ((r3 * c) * a) is Element of the carrier of V
- ((r3 * c) * a) is Element of the carrier of V
K196(V,(r3 * v),(- ((r3 * c) * a))) is Element of the carrier of V
((r3 * v) - ((r3 * c) * a)) + ((b * r4) * a) is Element of the carrier of V
((r3 * c) * a) - ((b * r4) * a) is Element of the carrier of V
- ((b * r4) * a) is Element of the carrier of V
K196(V,((r3 * c) * a),(- ((b * r4) * a))) is Element of the carrier of V
(r3 * v) - (((r3 * c) * a) - ((b * r4) * a)) is Element of the carrier of V
- (((r3 * c) * a) - ((b * r4) * a)) is Element of the carrier of V
K196(V,(r3 * v),(- (((r3 * c) * a) - ((b * r4) * a)))) is Element of the carrier of V
(r3 * c) - (b * r4) is V24() V25() V41() Element of REAL
((r3 * c) - (b * r4)) * a is Element of the carrier of V
- (((r3 * c) - (b * r4)) * a) is Element of the carrier of V
(r3 * v) + (- (((r3 * c) - (b * r4)) * a)) is Element of the carrier of V
- ((r3 * c) - (b * r4)) is V24() V25() V41() Element of REAL
(- ((r3 * c) - (b * r4))) * a is Element of the carrier of V
(r3 * v) + ((- ((r3 * c) - (b * r4))) * a) is Element of the carrier of V
((b * r4) - (c * r3)) * a is Element of the carrier of V
(r3 * v) + (((b * r4) - (c * r3)) * a) is Element of the carrier of V
(((b * r4) - (c * r3)) ") * (b * w) is Element of the carrier of V
(((b * r4) - (c * r3)) ") * (r3 * v) is Element of the carrier of V
(((b * r4) - (c * r3)) ") * (((b * r4) - (c * r3)) * a) is Element of the carrier of V
((((b * r4) - (c * r3)) ") * (r3 * v)) + ((((b * r4) - (c * r3)) ") * (((b * r4) - (c * r3)) * a)) is Element of the carrier of V
((((b * r4) - (c * r3)) ") * ((b * r4) - (c * r3))) * a is Element of the carrier of V
((((b * r4) - (c * r3)) ") * (r3 * v)) + (((((b * r4) - (c * r3)) ") * ((b * r4) - (c * r3))) * a) is Element of the carrier of V
((((b * r4) - (c * r3)) ") * (r3 * v)) + (1 * a) is Element of the carrier of V
((((b * r4) - (c * r3)) ") * (r3 * v)) + a is Element of the carrier of V
((((b * r4) - (c * r3)) ") * (b * w)) - ((((b * r4) - (c * r3)) ") * (r3 * v)) is Element of the carrier of V
- ((((b * r4) - (c * r3)) ") * (r3 * v)) is Element of the carrier of V
K196(V,((((b * r4) - (c * r3)) ") * (b * w)),(- ((((b * r4) - (c * r3)) ") * (r3 * v)))) is Element of the carrier of V
(((((b * r4) - (c * r3)) ") * b) * w) - ((((b * r4) - (c * r3)) ") * (r3 * v)) is Element of the carrier of V
K196(V,(((((b * r4) - (c * r3)) ") * b) * w),(- ((((b * r4) - (c * r3)) ") * (r3 * v)))) is Element of the carrier of V
(c * (b ")) * (- (((((b * r4) - (c * r3)) ") * r3) * v)) is Element of the carrier of V
(c * (b ")) * (((((b * r4) - (c * r3)) ") * b) * w) is Element of the carrier of V
((c * (b ")) * (- (((((b * r4) - (c * r3)) ") * r3) * v))) + ((c * (b ")) * (((((b * r4) - (c * r3)) ") * b) * w)) is Element of the carrier of V
((b ") * v) - (((c * (b ")) * (- (((((b * r4) - (c * r3)) ") * r3) * v))) + ((c * (b ")) * (((((b * r4) - (c * r3)) ") * b) * w))) is Element of the carrier of V
- (((c * (b ")) * (- (((((b * r4) - (c * r3)) ") * r3) * v))) + ((c * (b ")) * (((((b * r4) - (c * r3)) ") * b) * w))) is Element of the carrier of V
K196(V,((b ") * v),(- (((c * (b ")) * (- (((((b * r4) - (c * r3)) ") * r3) * v))) + ((c * (b ")) * (((((b * r4) - (c * r3)) ") * b) * w))))) is Element of the carrier of V
(c * (b ")) * ((((b * r4) - (c * r3)) ") * b) is V24() V25() V41() Element of REAL
((c * (b ")) * ((((b * r4) - (c * r3)) ") * b)) * w is Element of the carrier of V
((c * (b ")) * (- (((((b * r4) - (c * r3)) ") * r3) * v))) + (((c * (b ")) * ((((b * r4) - (c * r3)) ") * b)) * w) is Element of the carrier of V
((b ") * v) - (((c * (b ")) * (- (((((b * r4) - (c * r3)) ") * r3) * v))) + (((c * (b ")) * ((((b * r4) - (c * r3)) ") * b)) * w)) is Element of the carrier of V
- (((c * (b ")) * (- (((((b * r4) - (c * r3)) ") * r3) * v))) + (((c * (b ")) * ((((b * r4) - (c * r3)) ") * b)) * w)) is Element of the carrier of V
K196(V,((b ") * v),(- (((c * (b ")) * (- (((((b * r4) - (c * r3)) ") * r3) * v))) + (((c * (b ")) * ((((b * r4) - (c * r3)) ") * b)) * w)))) is Element of the carrier of V
((b ") * b) * (((b * r4) - (c * r3)) ") is V24() V25() V41() Element of REAL
c * (((b ") * b) * (((b * r4) - (c * r3)) ")) is V24() V25() V41() Element of REAL
(c * (((b ") * b) * (((b * r4) - (c * r3)) "))) * w is Element of the carrier of V
((c * (b ")) * (- (((((b * r4) - (c * r3)) ") * r3) * v))) + ((c * (((b ") * b) * (((b * r4) - (c * r3)) "))) * w) is Element of the carrier of V
((b ") * v) - (((c * (b ")) * (- (((((b * r4) - (c * r3)) ") * r3) * v))) + ((c * (((b ") * b) * (((b * r4) - (c * r3)) "))) * w)) is Element of the carrier of V
- (((c * (b ")) * (- (((((b * r4) - (c * r3)) ") * r3) * v))) + ((c * (((b ") * b) * (((b * r4) - (c * r3)) "))) * w)) is Element of the carrier of V
K196(V,((b ") * v),(- (((c * (b ")) * (- (((((b * r4) - (c * r3)) ") * r3) * v))) + ((c * (((b ") * b) * (((b * r4) - (c * r3)) "))) * w)))) is Element of the carrier of V
c * (1 * (((b * r4) - (c * r3)) ")) is V24() V25() V41() Element of REAL
(c * (1 * (((b * r4) - (c * r3)) "))) * w is Element of the carrier of V
((c * (b ")) * (- (((((b * r4) - (c * r3)) ") * r3) * v))) + ((c * (1 * (((b * r4) - (c * r3)) "))) * w) is Element of the carrier of V
((b ") * v) - (((c * (b ")) * (- (((((b * r4) - (c * r3)) ") * r3) * v))) + ((c * (1 * (((b * r4) - (c * r3)) "))) * w)) is Element of the carrier of V
- (((c * (b ")) * (- (((((b * r4) - (c * r3)) ") * r3) * v))) + ((c * (1 * (((b * r4) - (c * r3)) "))) * w)) is Element of the carrier of V
K196(V,((b ") * v),(- (((c * (b ")) * (- (((((b * r4) - (c * r3)) ") * r3) * v))) + ((c * (1 * (((b * r4) - (c * r3)) "))) * w)))) is Element of the carrier of V
(c * (b ")) * (- ((((b * r4) - (c * r3)) ") * (r3 * v))) is Element of the carrier of V
c * (((b * r4) - (c * r3)) ") is V24() V25() V41() Element of REAL
(c * (((b * r4) - (c * r3)) ")) * w is Element of the carrier of V
((c * (b ")) * (- ((((b * r4) - (c * r3)) ") * (r3 * v)))) + ((c * (((b * r4) - (c * r3)) ")) * w) is Element of the carrier of V
((b ") * v) - (((c * (b ")) * (- ((((b * r4) - (c * r3)) ") * (r3 * v)))) + ((c * (((b * r4) - (c * r3)) ")) * w)) is Element of the carrier of V
- (((c * (b ")) * (- ((((b * r4) - (c * r3)) ") * (r3 * v)))) + ((c * (((b * r4) - (c * r3)) ")) * w)) is Element of the carrier of V
K196(V,((b ") * v),(- (((c * (b ")) * (- ((((b * r4) - (c * r3)) ") * (r3 * v)))) + ((c * (((b * r4) - (c * r3)) ")) * w)))) is Element of the carrier of V
(- (((b * r4) - (c * r3)) ")) * (r3 * v) is Element of the carrier of V
(c * (b ")) * ((- (((b * r4) - (c * r3)) ")) * (r3 * v)) is Element of the carrier of V
((c * (b ")) * ((- (((b * r4) - (c * r3)) ")) * (r3 * v))) + ((c * (((b * r4) - (c * r3)) ")) * w) is Element of the carrier of V
((b ") * v) - (((c * (b ")) * ((- (((b * r4) - (c * r3)) ")) * (r3 * v))) + ((c * (((b * r4) - (c * r3)) ")) * w)) is Element of the carrier of V
- (((c * (b ")) * ((- (((b * r4) - (c * r3)) ")) * (r3 * v))) + ((c * (((b * r4) - (c * r3)) ")) * w)) is Element of the carrier of V
K196(V,((b ") * v),(- (((c * (b ")) * ((- (((b * r4) - (c * r3)) ")) * (r3 * v))) + ((c * (((b * r4) - (c * r3)) ")) * w)))) is Element of the carrier of V
(c * (b ")) * (- (((b * r4) - (c * r3)) ")) is V24() V25() V41() Element of REAL
((c * (b ")) * (- (((b * r4) - (c * r3)) "))) * (r3 * v) is Element of the carrier of V
(((c * (b ")) * (- (((b * r4) - (c * r3)) "))) * (r3 * v)) + ((c * (((b * r4) - (c * r3)) ")) * w) is Element of the carrier of V
((b ") * v) - ((((c * (b ")) * (- (((b * r4) - (c * r3)) "))) * (r3 * v)) + ((c * (((b * r4) - (c * r3)) ")) * w)) is Element of the carrier of V
- ((((c * (b ")) * (- (((b * r4) - (c * r3)) "))) * (r3 * v)) + ((c * (((b * r4) - (c * r3)) ")) * w)) is Element of the carrier of V
K196(V,((b ") * v),(- ((((c * (b ")) * (- (((b * r4) - (c * r3)) "))) * (r3 * v)) + ((c * (((b * r4) - (c * r3)) ")) * w)))) is Element of the carrier of V
(- 1) * (((b * r4) - (c * r3)) ") is V24() V25() V41() Element of REAL
((- 1) * (((b * r4) - (c * r3)) ")) * c is V24() V25() V41() Element of REAL
(((- 1) * (((b * r4) - (c * r3)) ")) * c) * (b ") is V24() V25() V41() Element of REAL
((((- 1) * (((b * r4) - (c * r3)) ")) * c) * (b ")) * (r3 * v) is Element of the carrier of V
(((((- 1) * (((b * r4) - (c * r3)) ")) * c) * (b ")) * (r3 * v)) + ((c * (((b * r4) - (c * r3)) ")) * w) is Element of the carrier of V
((b ") * v) - ((((((- 1) * (((b * r4) - (c * r3)) ")) * c) * (b ")) * (r3 * v)) + ((c * (((b * r4) - (c * r3)) ")) * w)) is Element of the carrier of V
- ((((((- 1) * (((b * r4) - (c * r3)) ")) * c) * (b ")) * (r3 * v)) + ((c * (((b * r4) - (c * r3)) ")) * w)) is Element of the carrier of V
K196(V,((b ") * v),(- ((((((- 1) * (((b * r4) - (c * r3)) ")) * c) * (b ")) * (r3 * v)) + ((c * (((b * r4) - (c * r3)) ")) * w)))) is Element of the carrier of V
(((- 1) * (((b * r4) - (c * r3)) ")) * c) * ((b ") * (r3 * v)) is Element of the carrier of V
((((- 1) * (((b * r4) - (c * r3)) ")) * c) * ((b ") * (r3 * v))) + ((c * (((b * r4) - (c * r3)) ")) * w) is Element of the carrier of V
((b ") * v) - (((((- 1) * (((b * r4) - (c * r3)) ")) * c) * ((b ") * (r3 * v))) + ((c * (((b * r4) - (c * r3)) ")) * w)) is Element of the carrier of V
- (((((- 1) * (((b * r4) - (c * r3)) ")) * c) * ((b ") * (r3 * v))) + ((c * (((b * r4) - (c * r3)) ")) * w)) is Element of the carrier of V
K196(V,((b ") * v),(- (((((- 1) * (((b * r4) - (c * r3)) ")) * c) * ((b ") * (r3 * v))) + ((c * (((b * r4) - (c * r3)) ")) * w)))) is Element of the carrier of V
c * ((b ") * (r3 * v)) is Element of the carrier of V
((- 1) * (((b * r4) - (c * r3)) ")) * (c * ((b ") * (r3 * v))) is Element of the carrier of V
(((- 1) * (((b * r4) - (c * r3)) ")) * (c * ((b ") * (r3 * v)))) + ((c * (((b * r4) - (c * r3)) ")) * w) is Element of the carrier of V
((b ") * v) - ((((- 1) * (((b * r4) - (c * r3)) ")) * (c * ((b ") * (r3 * v)))) + ((c * (((b * r4) - (c * r3)) ")) * w)) is Element of the carrier of V
- ((((- 1) * (((b * r4) - (c * r3)) ")) * (c * ((b ") * (r3 * v)))) + ((c * (((b * r4) - (c * r3)) ")) * w)) is Element of the carrier of V
K196(V,((b ") * v),(- ((((- 1) * (((b * r4) - (c * r3)) ")) * (c * ((b ") * (r3 * v)))) + ((c * (((b * r4) - (c * r3)) ")) * w)))) is Element of the carrier of V
(((b * r4) - (c * r3)) ") * (c * ((b ") * (r3 * v))) is Element of the carrier of V
(- 1) * ((((b * r4) - (c * r3)) ") * (c * ((b ") * (r3 * v)))) is Element of the carrier of V
((- 1) * ((((b * r4) - (c * r3)) ") * (c * ((b ") * (r3 * v))))) + ((c * (((b * r4) - (c * r3)) ")) * w) is Element of the carrier of V
((b ") * v) - (((- 1) * ((((b * r4) - (c * r3)) ") * (c * ((b ") * (r3 * v))))) + ((c * (((b * r4) - (c * r3)) ")) * w)) is Element of the carrier of V
- (((- 1) * ((((b * r4) - (c * r3)) ") * (c * ((b ") * (r3 * v))))) + ((c * (((b * r4) - (c * r3)) ")) * w)) is Element of the carrier of V
K196(V,((b ") * v),(- (((- 1) * ((((b * r4) - (c * r3)) ") * (c * ((b ") * (r3 * v))))) + ((c * (((b * r4) - (c * r3)) ")) * w)))) is Element of the carrier of V
- ((((b * r4) - (c * r3)) ") * (c * ((b ") * (r3 * v)))) is Element of the carrier of V
(- ((((b * r4) - (c * r3)) ") * (c * ((b ") * (r3 * v))))) + ((c * (((b * r4) - (c * r3)) ")) * w) is Element of the carrier of V
((b ") * v) - ((- ((((b * r4) - (c * r3)) ") * (c * ((b ") * (r3 * v))))) + ((c * (((b * r4) - (c * r3)) ")) * w)) is Element of the carrier of V
- ((- ((((b * r4) - (c * r3)) ") * (c * ((b ") * (r3 * v))))) + ((c * (((b * r4) - (c * r3)) ")) * w)) is Element of the carrier of V
K196(V,((b ") * v),(- ((- ((((b * r4) - (c * r3)) ") * (c * ((b ") * (r3 * v))))) + ((c * (((b * r4) - (c * r3)) ")) * w)))) is Element of the carrier of V
((((b * r4) - (c * r3)) ") * c) * ((b ") * (r3 * v)) is Element of the carrier of V
- (((((b * r4) - (c * r3)) ") * c) * ((b ") * (r3 * v))) is Element of the carrier of V
(- (((((b * r4) - (c * r3)) ") * c) * ((b ") * (r3 * v)))) + ((c * (((b * r4) - (c * r3)) ")) * w) is Element of the carrier of V
((b ") * v) - ((- (((((b * r4) - (c * r3)) ") * c) * ((b ") * (r3 * v)))) + ((c * (((b * r4) - (c * r3)) ")) * w)) is Element of the carrier of V
- ((- (((((b * r4) - (c * r3)) ") * c) * ((b ") * (r3 * v)))) + ((c * (((b * r4) - (c * r3)) ")) * w)) is Element of the carrier of V
K196(V,((b ") * v),(- ((- (((((b * r4) - (c * r3)) ") * c) * ((b ") * (r3 * v)))) + ((c * (((b * r4) - (c * r3)) ")) * w)))) is Element of the carrier of V
(((((b * r4) - (c * r3)) ") * c) * (b ")) * (r3 * v) is Element of the carrier of V
- ((((((b * r4) - (c * r3)) ") * c) * (b ")) * (r3 * v)) is Element of the carrier of V
(- ((((((b * r4) - (c * r3)) ") * c) * (b ")) * (r3 * v))) + ((c * (((b * r4) - (c * r3)) ")) * w) is Element of the carrier of V
((b ") * v) - ((- ((((((b * r4) - (c * r3)) ") * c) * (b ")) * (r3 * v))) + ((c * (((b * r4) - (c * r3)) ")) * w)) is Element of the carrier of V
- ((- ((((((b * r4) - (c * r3)) ") * c) * (b ")) * (r3 * v))) + ((c * (((b * r4) - (c * r3)) ")) * w)) is Element of the carrier of V
K196(V,((b ") * v),(- ((- ((((((b * r4) - (c * r3)) ") * c) * (b ")) * (r3 * v))) + ((c * (((b * r4) - (c * r3)) ")) * w)))) is Element of the carrier of V
((((((b * r4) - (c * r3)) ") * c) * (b ")) * r3) * v is Element of the carrier of V
- (((((((b * r4) - (c * r3)) ") * c) * (b ")) * r3) * v) is Element of the carrier of V
(- (((((((b * r4) - (c * r3)) ") * c) * (b ")) * r3) * v)) + ((c * (((b * r4) - (c * r3)) ")) * w) is Element of the carrier of V
((b ") * v) - ((- (((((((b * r4) - (c * r3)) ") * c) * (b ")) * r3) * v)) + ((c * (((b * r4) - (c * r3)) ")) * w)) is Element of the carrier of V
- ((- (((((((b * r4) - (c * r3)) ") * c) * (b ")) * r3) * v)) + ((c * (((b * r4) - (c * r3)) ")) * w)) is Element of the carrier of V
K196(V,((b ") * v),(- ((- (((((((b * r4) - (c * r3)) ") * c) * (b ")) * r3) * v)) + ((c * (((b * r4) - (c * r3)) ")) * w)))) is Element of the carrier of V
((b ") * v) - (- (((((((b * r4) - (c * r3)) ") * c) * (b ")) * r3) * v)) is Element of the carrier of V
- (- (((((((b * r4) - (c * r3)) ") * c) * (b ")) * r3) * v)) is Element of the carrier of V
K196(V,((b ") * v),(- (- (((((((b * r4) - (c * r3)) ") * c) * (b ")) * r3) * v)))) is Element of the carrier of V
(((b ") * v) - (- (((((((b * r4) - (c * r3)) ") * c) * (b ")) * r3) * v))) - ((c * (((b * r4) - (c * r3)) ")) * w) is Element of the carrier of V
- ((c * (((b * r4) - (c * r3)) ")) * w) is Element of the carrier of V
K196(V,(((b ") * v) - (- (((((((b * r4) - (c * r3)) ") * c) * (b ")) * r3) * v))),(- ((c * (((b * r4) - (c * r3)) ")) * w))) is Element of the carrier of V
((b ") * v) + (((((((b * r4) - (c * r3)) ") * c) * (b ")) * r3) * v) is Element of the carrier of V
(((b ") * v) + (((((((b * r4) - (c * r3)) ") * c) * (b ")) * r3) * v)) - ((c * (((b * r4) - (c * r3)) ")) * w) is Element of the carrier of V
K196(V,(((b ") * v) + (((((((b * r4) - (c * r3)) ") * c) * (b ")) * r3) * v)),(- ((c * (((b * r4) - (c * r3)) ")) * w))) is Element of the carrier of V
(- ((((b * r4) - (c * r3)) ") * c)) * w is Element of the carrier of V
(((((b * r4) - (c * r3)) ") * r4) * v) + ((- ((((b * r4) - (c * r3)) ") * c)) * w) is Element of the carrier of V
(- ((((b * r4) - (c * r3)) ") * r3)) * v is Element of the carrier of V
((- ((((b * r4) - (c * r3)) ") * r3)) * v) + (((((b * r4) - (c * r3)) ") * b) * w) is Element of the carrier of V
a is Element of the carrier of V
b is V24() V25() V41() Element of REAL
b * u is Element of the carrier of V
r6 is V24() V25() V41() Element of REAL
r6 * a is Element of the carrier of V
(b * u) + (r6 * a) is Element of the carrier of V
b * (((((b * r4) - (c * r3)) ") * r4) * v) is Element of the carrier of V
b * ((- ((((b * r4) - (c * r3)) ") * c)) * w) is Element of the carrier of V
(b * (((((b * r4) - (c * r3)) ") * r4) * v)) + (b * ((- ((((b * r4) - (c * r3)) ") * c)) * w)) is Element of the carrier of V
r6 * (((- ((((b * r4) - (c * r3)) ") * r3)) * v) + (((((b * r4) - (c * r3)) ") * b) * w)) is Element of the carrier of V
((b * (((((b * r4) - (c * r3)) ") * r4) * v)) + (b * ((- ((((b * r4) - (c * r3)) ") * c)) * w))) + (r6 * (((- ((((b * r4) - (c * r3)) ") * r3)) * v) + (((((b * r4) - (c * r3)) ") * b) * w))) is Element of the carrier of V
r6 * ((- ((((b * r4) - (c * r3)) ") * r3)) * v) is Element of the carrier of V
r6 * (((((b * r4) - (c * r3)) ") * b) * w) is Element of the carrier of V
(r6 * ((- ((((b * r4) - (c * r3)) ") * r3)) * v)) + (r6 * (((((b * r4) - (c * r3)) ") * b) * w)) is Element of the carrier of V
((b * (((((b * r4) - (c * r3)) ") * r4) * v)) + (b * ((- ((((b * r4) - (c * r3)) ") * c)) * w))) + ((r6 * ((- ((((b * r4) - (c * r3)) ") * r3)) * v)) + (r6 * (((((b * r4) - (c * r3)) ") * b) * w))) is Element of the carrier of V
b * ((((b * r4) - (c * r3)) ") * r4) is V24() V25() V41() Element of REAL
(b * ((((b * r4) - (c * r3)) ") * r4)) * v is Element of the carrier of V
((b * ((((b * r4) - (c * r3)) ") * r4)) * v) + (b * ((- ((((b * r4) - (c * r3)) ") * c)) * w)) is Element of the carrier of V
(((b * ((((b * r4) - (c * r3)) ") * r4)) * v) + (b * ((- ((((b * r4) - (c * r3)) ") * c)) * w))) + ((r6 * ((- ((((b * r4) - (c * r3)) ") * r3)) * v)) + (r6 * (((((b * r4) - (c * r3)) ") * b) * w))) is Element of the carrier of V
b * (- ((((b * r4) - (c * r3)) ") * c)) is V24() V25() V41() Element of REAL
(b * (- ((((b * r4) - (c * r3)) ") * c))) * w is Element of the carrier of V
((b * ((((b * r4) - (c * r3)) ") * r4)) * v) + ((b * (- ((((b * r4) - (c * r3)) ") * c))) * w) is Element of the carrier of V
(((b * ((((b * r4) - (c * r3)) ") * r4)) * v) + ((b * (- ((((b * r4) - (c * r3)) ") * c))) * w)) + ((r6 * ((- ((((b * r4) - (c * r3)) ") * r3)) * v)) + (r6 * (((((b * r4) - (c * r3)) ") * b) * w))) is Element of the carrier of V
r6 * (- ((((b * r4) - (c * r3)) ") * r3)) is V24() V25() V41() Element of REAL
(r6 * (- ((((b * r4) - (c * r3)) ") * r3))) * v is Element of the carrier of V
((r6 * (- ((((b * r4) - (c * r3)) ") * r3))) * v) + (r6 * (((((b * r4) - (c * r3)) ") * b) * w)) is Element of the carrier of V
(((b * ((((b * r4) - (c * r3)) ") * r4)) * v) + ((b * (- ((((b * r4) - (c * r3)) ") * c))) * w)) + (((r6 * (- ((((b * r4) - (c * r3)) ") * r3))) * v) + (r6 * (((((b * r4) - (c * r3)) ") * b) * w))) is Element of the carrier of V
r6 * ((((b * r4) - (c * r3)) ") * b) is V24() V25() V41() Element of REAL
(r6 * ((((b * r4) - (c * r3)) ") * b)) * w is Element of the carrier of V
((r6 * (- ((((b * r4) - (c * r3)) ") * r3))) * v) + ((r6 * ((((b * r4) - (c * r3)) ") * b)) * w) is Element of the carrier of V
(((b * ((((b * r4) - (c * r3)) ") * r4)) * v) + ((b * (- ((((b * r4) - (c * r3)) ") * c))) * w)) + (((r6 * (- ((((b * r4) - (c * r3)) ") * r3))) * v) + ((r6 * ((((b * r4) - (c * r3)) ") * b)) * w)) is Element of the carrier of V
((b * (- ((((b * r4) - (c * r3)) ") * c))) * w) + (((r6 * (- ((((b * r4) - (c * r3)) ") * r3))) * v) + ((r6 * ((((b * r4) - (c * r3)) ") * b)) * w)) is Element of the carrier of V
((b * ((((b * r4) - (c * r3)) ") * r4)) * v) + (((b * (- ((((b * r4) - (c * r3)) ") * c))) * w) + (((r6 * (- ((((b * r4) - (c * r3)) ") * r3))) * v) + ((r6 * ((((b * r4) - (c * r3)) ") * b)) * w))) is Element of the carrier of V
((b * (- ((((b * r4) - (c * r3)) ") * c))) * w) + ((r6 * ((((b * r4) - (c * r3)) ") * b)) * w) is Element of the carrier of V
((r6 * (- ((((b * r4) - (c * r3)) ") * r3))) * v) + (((b * (- ((((b * r4) - (c * r3)) ") * c))) * w) + ((r6 * ((((b * r4) - (c * r3)) ") * b)) * w)) is Element of the carrier of V
((b * ((((b * r4) - (c * r3)) ") * r4)) * v) + (((r6 * (- ((((b * r4) - (c * r3)) ") * r3))) * v) + (((b * (- ((((b * r4) - (c * r3)) ") * c))) * w) + ((r6 * ((((b * r4) - (c * r3)) ") * b)) * w))) is Element of the carrier of V
((b * ((((b * r4) - (c * r3)) ") * r4)) * v) + ((r6 * (- ((((b * r4) - (c * r3)) ") * r3))) * v) is Element of the carrier of V
(((b * ((((b * r4) - (c * r3)) ") * r4)) * v) + ((r6 * (- ((((b * r4) - (c * r3)) ") * r3))) * v)) + (((b * (- ((((b * r4) - (c * r3)) ") * c))) * w) + ((r6 * ((((b * r4) - (c * r3)) ") * b)) * w)) is Element of the carrier of V
(b * ((((b * r4) - (c * r3)) ") * r4)) + (r6 * (- ((((b * r4) - (c * r3)) ") * r3))) is V24() V25() V41() Element of REAL
((b * ((((b * r4) - (c * r3)) ") * r4)) + (r6 * (- ((((b * r4) - (c * r3)) ") * r3)))) * v is Element of the carrier of V
(((b * ((((b * r4) - (c * r3)) ") * r4)) + (r6 * (- ((((b * r4) - (c * r3)) ") * r3)))) * v) + (((b * (- ((((b * r4) - (c * r3)) ") * c))) * w) + ((r6 * ((((b * r4) - (c * r3)) ") * b)) * w)) is Element of the carrier of V
(b * (- ((((b * r4) - (c * r3)) ") * c))) + (r6 * ((((b * r4) - (c * r3)) ") * b)) is V24() V25() V41() Element of REAL
((b * (- ((((b * r4) - (c * r3)) ") * c))) + (r6 * ((((b * r4) - (c * r3)) ") * b))) * w is Element of the carrier of V
(((b * ((((b * r4) - (c * r3)) ") * r4)) + (r6 * (- ((((b * r4) - (c * r3)) ") * r3)))) * v) + (((b * (- ((((b * r4) - (c * r3)) ") * c))) + (r6 * ((((b * r4) - (c * r3)) ") * b))) * w) is Element of the carrier of V
b is V24() V25() V41() Element of REAL
b * v is Element of the carrier of V
r6 is V24() V25() V41() Element of REAL
r6 * w is Element of the carrier of V
(b * v) + (r6 * w) is Element of the carrier of V
b * ((b * u) + (c * a)) is Element of the carrier of V
r6 * (r3 * u) is Element of the carrier of V
r6 * (r4 * a) is Element of the carrier of V
(r6 * (r3 * u)) + (r6 * (r4 * a)) is Element of the carrier of V
(b * ((b * u) + (c * a))) + ((r6 * (r3 * u)) + (r6 * (r4 * a))) is Element of the carrier of V
b * (b * u) is Element of the carrier of V
b * (c * a) is Element of the carrier of V
(b * (b * u)) + (b * (c * a)) is Element of the carrier of V
((b * (b * u)) + (b * (c * a))) + ((r6 * (r3 * u)) + (r6 * (r4 * a))) is Element of the carrier of V
((b * (b * u)) + (b * (c * a))) + (r6 * (r3 * u)) is Element of the carrier of V
(((b * (b * u)) + (b * (c * a))) + (r6 * (r3 * u))) + (r6 * (r4 * a)) is Element of the carrier of V
(b * (b * u)) + (r6 * (r3 * u)) is Element of the carrier of V
((b * (b * u)) + (r6 * (r3 * u))) + (b * (c * a)) is Element of the carrier of V
(((b * (b * u)) + (r6 * (r3 * u))) + (b * (c * a))) + (r6 * (r4 * a)) is Element of the carrier of V
b * b is V24() V25() V41() Element of REAL
(b * b) * u is Element of the carrier of V
((b * b) * u) + (r6 * (r3 * u)) is Element of the carrier of V
(((b * b) * u) + (r6 * (r3 * u))) + (b * (c * a)) is Element of the carrier of V
((((b * b) * u) + (r6 * (r3 * u))) + (b * (c * a))) + (r6 * (r4 * a)) is Element of the carrier of V
r6 * r3 is V24() V25() V41() Element of REAL
(r6 * r3) * u is Element of the carrier of V
((b * b) * u) + ((r6 * r3) * u) is Element of the carrier of V
(((b * b) * u) + ((r6 * r3) * u)) + (b * (c * a)) is Element of the carrier of V
((((b * b) * u) + ((r6 * r3) * u)) + (b * (c * a))) + (r6 * (r4 * a)) is Element of the carrier of V
b * c is V24() V25() V41() Element of REAL
(b * c) * a is Element of the carrier of V
(((b * b) * u) + ((r6 * r3) * u)) + ((b * c) * a) is Element of the carrier of V
((((b * b) * u) + ((r6 * r3) * u)) + ((b * c) * a)) + (r6 * (r4 * a)) is Element of the carrier of V
r6 * r4 is V24() V25() V41() Element of REAL
(r6 * r4) * a is Element of the carrier of V
((((b * b) * u) + ((r6 * r3) * u)) + ((b * c) * a)) + ((r6 * r4) * a) is Element of the carrier of V
(b * b) + (r6 * r3) is V24() V25() V41() Element of REAL
((b * b) + (r6 * r3)) * u is Element of the carrier of V
(((b * b) + (r6 * r3)) * u) + ((b * c) * a) is Element of the carrier of V
((((b * b) + (r6 * r3)) * u) + ((b * c) * a)) + ((r6 * r4) * a) is Element of the carrier of V
((b * c) * a) + ((r6 * r4) * a) is Element of the carrier of V
(((b * b) + (r6 * r3)) * u) + (((b * c) * a) + ((r6 * r4) * a)) is Element of the carrier of V
(b * c) + (r6 * r4) is V24() V25() V41() Element of REAL
((b * c) + (r6 * r4)) * a is Element of the carrier of V
(((b * b) + (r6 * r3)) * u) + (((b * c) + (r6 * r4)) * a) is Element of the carrier of V
a is V24() V25() V41() Element of REAL
a * u is Element of the carrier of V
b is V24() V25() V41() Element of REAL
b * a is Element of the carrier of V
(a * u) + (b * a) is Element of the carrier of V
a * (((((b * r4) - (c * r3)) ") * r4) * v) is Element of the carrier of V
a * ((- ((((b * r4) - (c * r3)) ") * c)) * w) is Element of the carrier of V
(a * (((((b * r4) - (c * r3)) ") * r4) * v)) + (a * ((- ((((b * r4) - (c * r3)) ") * c)) * w)) is Element of the carrier of V
b * (((- ((((b * r4) - (c * r3)) ") * r3)) * v) + (((((b * r4) - (c * r3)) ") * b) * w)) is Element of the carrier of V
((a * (((((b * r4) - (c * r3)) ") * r4) * v)) + (a * ((- ((((b * r4) - (c * r3)) ") * c)) * w))) + (b * (((- ((((b * r4) - (c * r3)) ") * r3)) * v) + (((((b * r4) - (c * r3)) ") * b) * w))) is Element of the carrier of V
b * ((- ((((b * r4) - (c * r3)) ") * r3)) * v) is Element of the carrier of V
b * (((((b * r4) - (c * r3)) ") * b) * w) is Element of the carrier of V
(b * ((- ((((b * r4) - (c * r3)) ") * r3)) * v)) + (b * (((((b * r4) - (c * r3)) ") * b) * w)) is Element of the carrier of V
((a * (((((b * r4) - (c * r3)) ") * r4) * v)) + (a * ((- ((((b * r4) - (c * r3)) ") * c)) * w))) + ((b * ((- ((((b * r4) - (c * r3)) ") * r3)) * v)) + (b * (((((b * r4) - (c * r3)) ") * b) * w))) is Element of the carrier of V
a * ((((b * r4) - (c * r3)) ") * r4) is V24() V25() V41() Element of REAL
(a * ((((b * r4) - (c * r3)) ") * r4)) * v is Element of the carrier of V
((a * ((((b * r4) - (c * r3)) ") * r4)) * v) + (a * ((- ((((b * r4) - (c * r3)) ") * c)) * w)) is Element of the carrier of V
(((a * ((((b * r4) - (c * r3)) ") * r4)) * v) + (a * ((- ((((b * r4) - (c * r3)) ") * c)) * w))) + ((b * ((- ((((b * r4) - (c * r3)) ") * r3)) * v)) + (b * (((((b * r4) - (c * r3)) ") * b) * w))) is Element of the carrier of V
b * ((((b * r4) - (c * r3)) ") * b) is V24() V25() V41() Element of REAL
(b * ((((b * r4) - (c * r3)) ") * b)) * w is Element of the carrier of V
(b * ((- ((((b * r4) - (c * r3)) ") * r3)) * v)) + ((b * ((((b * r4) - (c * r3)) ") * b)) * w) is Element of the carrier of V
(((a * ((((b * r4) - (c * r3)) ") * r4)) * v) + (a * ((- ((((b * r4) - (c * r3)) ") * c)) * w))) + ((b * ((- ((((b * r4) - (c * r3)) ") * r3)) * v)) + ((b * ((((b * r4) - (c * r3)) ") * b)) * w)) is Element of the carrier of V
b * (- ((((b * r4) - (c * r3)) ") * r3)) is V24() V25() V41() Element of REAL
(b * (- ((((b * r4) - (c * r3)) ") * r3))) * v is Element of the carrier of V
((b * (- ((((b * r4) - (c * r3)) ") * r3))) * v) + ((b * ((((b * r4) - (c * r3)) ") * b)) * w) is Element of the carrier of V
(((a * ((((b * r4) - (c * r3)) ") * r4)) * v) + (a * ((- ((((b * r4) - (c * r3)) ") * c)) * w))) + (((b * (- ((((b * r4) - (c * r3)) ") * r3))) * v) + ((b * ((((b * r4) - (c * r3)) ") * b)) * w)) is Element of the carrier of V
a * (- ((((b * r4) - (c * r3)) ") * c)) is V24() V25() V41() Element of REAL
(a * (- ((((b * r4) - (c * r3)) ") * c))) * w is Element of the carrier of V
((a * ((((b * r4) - (c * r3)) ") * r4)) * v) + ((a * (- ((((b * r4) - (c * r3)) ") * c))) * w) is Element of the carrier of V
(((a * ((((b * r4) - (c * r3)) ") * r4)) * v) + ((a * (- ((((b * r4) - (c * r3)) ") * c))) * w)) + (((b * (- ((((b * r4) - (c * r3)) ") * r3))) * v) + ((b * ((((b * r4) - (c * r3)) ") * b)) * w)) is Element of the carrier of V
((a * (- ((((b * r4) - (c * r3)) ") * c))) * w) + (((b * (- ((((b * r4) - (c * r3)) ") * r3))) * v) + ((b * ((((b * r4) - (c * r3)) ") * b)) * w)) is Element of the carrier of V
((a * ((((b * r4) - (c * r3)) ") * r4)) * v) + (((a * (- ((((b * r4) - (c * r3)) ") * c))) * w) + (((b * (- ((((b * r4) - (c * r3)) ") * r3))) * v) + ((b * ((((b * r4) - (c * r3)) ") * b)) * w))) is Element of the carrier of V
((a * (- ((((b * r4) - (c * r3)) ") * c))) * w) + ((b * ((((b * r4) - (c * r3)) ") * b)) * w) is Element of the carrier of V
((b * (- ((((b * r4) - (c * r3)) ") * r3))) * v) + (((a * (- ((((b * r4) - (c * r3)) ") * c))) * w) + ((b * ((((b * r4) - (c * r3)) ") * b)) * w)) is Element of the carrier of V
((a * ((((b * r4) - (c * r3)) ") * r4)) * v) + (((b * (- ((((b * r4) - (c * r3)) ") * r3))) * v) + (((a * (- ((((b * r4) - (c * r3)) ") * c))) * w) + ((b * ((((b * r4) - (c * r3)) ") * b)) * w))) is Element of the carrier of V
((a * ((((b * r4) - (c * r3)) ") * r4)) * v) + ((b * (- ((((b * r4) - (c * r3)) ") * r3))) * v) is Element of the carrier of V
(((a * ((((b * r4) - (c * r3)) ") * r4)) * v) + ((b * (- ((((b * r4) - (c * r3)) ") * r3))) * v)) + (((a * (- ((((b * r4) - (c * r3)) ") * c))) * w) + ((b * ((((b * r4) - (c * r3)) ") * b)) * w)) is Element of the carrier of V
(a * ((((b * r4) - (c * r3)) ") * r4)) + (b * (- ((((b * r4) - (c * r3)) ") * r3))) is V24() V25() V41() Element of REAL
((a * ((((b * r4) - (c * r3)) ") * r4)) + (b * (- ((((b * r4) - (c * r3)) ") * r3)))) * v is Element of the carrier of V
(((a * ((((b * r4) - (c * r3)) ") * r4)) + (b * (- ((((b * r4) - (c * r3)) ") * r3)))) * v) + (((a * (- ((((b * r4) - (c * r3)) ") * c))) * w) + ((b * ((((b * r4) - (c * r3)) ") * b)) * w)) is Element of the carrier of V
(a * (- ((((b * r4) - (c * r3)) ") * c))) + (b * ((((b * r4) - (c * r3)) ") * b)) is V24() V25() V41() Element of REAL
((a * (- ((((b * r4) - (c * r3)) ") * c))) + (b * ((((b * r4) - (c * r3)) ") * b))) * w is Element of the carrier of V
(((a * ((((b * r4) - (c * r3)) ") * r4)) + (b * (- ((((b * r4) - (c * r3)) ") * r3)))) * v) + (((a * (- ((((b * r4) - (c * r3)) ") * c))) + (b * ((((b * r4) - (c * r3)) ") * b))) * w) is Element of the carrier of V
r4 * a is V24() V25() V41() Element of REAL
(- r3) * b is V24() V25() V41() Element of REAL
(r4 * a) + ((- r3) * b) is V24() V25() V41() Element of REAL
(((b * r4) - (c * r3)) ") * ((r4 * a) + ((- r3) * b)) is V24() V25() V41() Element of REAL
r3 * b is V24() V25() V41() Element of REAL
(r4 * a) - (r3 * b) is V24() V25() V41() Element of REAL
(- c) * a is V24() V25() V41() Element of REAL
b * b is V24() V25() V41() Element of REAL
((- c) * a) + (b * b) is V24() V25() V41() Element of REAL
(((b * r4) - (c * r3)) ") * (((- c) * a) + (b * b)) is V24() V25() V41() Element of REAL
c * a is V24() V25() V41() Element of REAL
- (c * a) is V24() V25() V41() Element of REAL
(b * b) + (- (c * a)) is V24() V25() V41() Element of REAL
a " is V24() V25() V41() Element of REAL
(a ") * (b * b) is V24() V25() V41() Element of REAL
(a ") * a is V24() V25() V41() Element of REAL
((a ") * a) * c is V24() V25() V41() Element of REAL
1 * c is V24() V25() V41() Element of REAL
(a ") * b is V24() V25() V41() Element of REAL
b * ((a ") * b) is V24() V25() V41() Element of REAL
((a ") * b) * a is Element of the carrier of V
b * (((a ") * b) * a) is Element of the carrier of V
(b * u) + (b * (((a ") * b) * a)) is Element of the carrier of V
u + (((a ") * b) * a) is Element of the carrier of V
b * (u + (((a ") * b) * a)) is Element of the carrier of V
((a ") * a) * r4 is V24() V25() V41() Element of REAL
(a ") * (r3 * b) is V24() V25() V41() Element of REAL
r3 * ((a ") * b) is V24() V25() V41() Element of REAL
r3 * (((a ") * b) * a) is Element of the carrier of V
(r3 * u) + (r3 * (((a ") * b) * a)) is Element of the carrier of V
r3 * (u + (((a ") * b) * a)) is Element of the carrier of V
b " is V24() V25() V41() Element of REAL
(b ") * b is V24() V25() V41() Element of REAL
((b ") * b) * b is V24() V25() V41() Element of REAL
(b ") * (c * a) is V24() V25() V41() Element of REAL
1 * b is V24() V25() V41() Element of REAL
(b ") * a is V24() V25() V41() Element of REAL
c * ((b ") * a) is V24() V25() V41() Element of REAL
((b ") * a) * u is Element of the carrier of V
c * (((b ") * a) * u) is Element of the carrier of V
(c * (((b ") * a) * u)) + (c * a) is Element of the carrier of V
(((b ") * a) * u) + a is Element of the carrier of V
c * ((((b ") * a) * u) + a) is Element of the carrier of V
((b ") * b) * r3 is V24() V25() V41() Element of REAL
(b ") * (r4 * a) is V24() V25() V41() Element of REAL
1 * r3 is V24() V25() V41() Element of REAL
r4 * ((b ") * a) is V24() V25() V41() Element of REAL
r4 * (((b ") * a) * u) is Element of the carrier of V
(r4 * (((b ") * a) * u)) + (r4 * a) is Element of the carrier of V
r4 * ((((b ") * a) * u) + a) is Element of the carrier of V
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
0. V is V52(V) Element of the carrier of V
v is Element of the carrier of V
w is Element of the carrier of V
{w,v} is V26() Element of K32( the carrier of V)
K32( the carrier of V) is set
u is V24() V25() V41() Element of REAL
u * w is Element of the carrier of V
a is V24() V25() V41() Element of REAL
a * v is Element of the carrier of V
(u * w) + (a * v) is Element of the carrier of V
- (a * v) is Element of the carrier of V
u " is V24() V25() V41() Element of REAL
(u ") * u is V24() V25() V41() Element of REAL
((u ") * u) * w is Element of the carrier of V
(u ") * (- (a * v)) is Element of the carrier of V
1 * w is Element of the carrier of V
- a is V24() V25() V41() Element of REAL
(- a) * v is Element of the carrier of V
(u ") * ((- a) * v) is Element of the carrier of V
(u ") * (- a) is V24() V25() V41() Element of REAL
((u ") * (- a)) * v is Element of the carrier of V
- a is V24() V25() V41() Element of REAL
(- a) * v is Element of the carrier of V
b is V24() V25() V41() Element of REAL
b * v is Element of the carrier of V
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
v is Element of the carrier of V
w is Element of the carrier of V
{v,w} is V26() Element of K32( the carrier of V)
K32( the carrier of V) is set
u is Element of the carrier of V
{u,v,w} is V26() Element of K32( the carrier of V)
0. V is V52(V) Element of the carrier of V
a is V24() V25() V41() Element of REAL
a * u is Element of the carrier of V
b is V24() V25() V41() Element of REAL
b * v is Element of the carrier of V
(a * u) + (b * v) is Element of the carrier of V
c is V24() V25() V41() Element of REAL
c * w is Element of the carrier of V
((a * u) + (b * v)) + (c * w) is Element of the carrier of V
(b * v) + (c * w) is Element of the carrier of V
(a * u) + ((b * v) + (c * w)) is Element of the carrier of V
- ((b * v) + (c * w)) is Element of the carrier of V
a " is V24() V25() V41() Element of REAL
(a ") * a is V24() V25() V41() Element of REAL
((a ") * a) * u is Element of the carrier of V
(a ") * (- ((b * v) + (c * w))) is Element of the carrier of V
1 * u is Element of the carrier of V
(- 1) * ((b * v) + (c * w)) is Element of the carrier of V
(a ") * ((- 1) * ((b * v) + (c * w))) is Element of the carrier of V
(a ") * (- 1) is V24() V25() V41() Element of REAL
((a ") * (- 1)) * ((b * v) + (c * w)) is Element of the carrier of V
((a ") * (- 1)) * (b * v) is Element of the carrier of V
((a ") * (- 1)) * (c * w) is Element of the carrier of V
(((a ") * (- 1)) * (b * v)) + (((a ") * (- 1)) * (c * w)) is Element of the carrier of V
((a ") * (- 1)) * b is V24() V25() V41() Element of REAL
(((a ") * (- 1)) * b) * v is Element of the carrier of V
((((a ") * (- 1)) * b) * v) + (((a ") * (- 1)) * (c * w)) is Element of the carrier of V
((a ") * (- 1)) * c is V24() V25() V41() Element of REAL
(((a ") * (- 1)) * c) * w is Element of the carrier of V
((((a ") * (- 1)) * b) * v) + ((((a ") * (- 1)) * c) * w) is Element of the carrier of V
(0. V) + (b * v) is Element of the carrier of V
((0. V) + (b * v)) + (c * w) is Element of the carrier of V
(b * v) + (c * w) is Element of the carrier of V
r3 is V24() V25() V41() Element of REAL
r3 * v is Element of the carrier of V
r4 is V24() V25() V41() Element of REAL
r4 * w is Element of the carrier of V
(r3 * v) + (r4 * w) is Element of the carrier of V
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
v is Element of the carrier of V
{v} is V26() Element of K32( the carrier of V)
K32( the carrier of V) is set
w is V24() V25() V41() Element of REAL
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
v is Element of the carrier of V
w is Element of the carrier of V
{v,w} is V26() Element of K32( the carrier of V)
K32( the carrier of V) is set
u is V24() V25() V41() Element of REAL
a is V24() V25() V41() Element of REAL
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
v is Element of the carrier of V
w is Element of the carrier of V
u is Element of the carrier of V
{v,w,u} is V26() Element of K32( the carrier of V)
K32( the carrier of V) is set
a is V24() V25() V41() Element of REAL
b is V24() V25() V41() Element of REAL
c is V24() V25() V41() Element of REAL