:: ANALMETR semantic presentation

REAL is V29() V30() V31() V35() set
NAT is V29() V30() V31() V32() V33() V34() V35() Element of bool REAL
bool REAL is non empty set
NAT is V29() V30() V31() V32() V33() V34() V35() set
bool NAT is non empty set
bool NAT is non empty set
{} is empty V29() V30() V31() V32() V33() V34() V35() set
1 is non empty V17() V18() V19() V26() V27() V28() V29() V30() V31() V32() V33() V34() Element of NAT
0 is empty V17() V18() V19() V26() V27() V28() V29() V30() V31() V32() V33() V34() V35() Element of NAT
- 1 is V17() V27() V28() Element of REAL
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
w0 + w0 is Element of the carrier of V0
w0 - w0 is Element of the carrier of V0
- w0 is Element of the carrier of V0
K176(V0,w0,(- w0)) is Element of the carrier of V0
y0 is V17() V27() V28() Element of REAL
y0 * y0 is Element of the carrier of V0
POS is V17() V27() V28() Element of REAL
POS * V0 is Element of the carrier of V0
(y0 * y0) + (POS * V0) is Element of the carrier of V0
K is V17() V27() V28() Element of REAL
K * y0 is Element of the carrier of V0
y0 + K is V17() V27() V28() Element of REAL
(y0 + K) * y0 is Element of the carrier of V0
y0 - K is V17() V27() V28() Element of REAL
(y0 - K) * y0 is Element of the carrier of V0
a is V17() V27() V28() Element of REAL
a * V0 is Element of the carrier of V0
(K * y0) + (a * V0) is Element of the carrier of V0
POS + a is V17() V27() V28() Element of REAL
(POS + a) * V0 is Element of the carrier of V0
((y0 + K) * y0) + ((POS + a) * V0) is Element of the carrier of V0
POS - a is V17() V27() V28() Element of REAL
(POS - a) * V0 is Element of the carrier of V0
((y0 - K) * y0) + ((POS - a) * V0) is Element of the carrier of V0
((y0 * y0) + (POS * V0)) + (K * y0) is Element of the carrier of V0
(((y0 * y0) + (POS * V0)) + (K * y0)) + (a * V0) is Element of the carrier of V0
(y0 * y0) + (K * y0) is Element of the carrier of V0
((y0 * y0) + (K * y0)) + (POS * V0) is Element of the carrier of V0
(((y0 * y0) + (K * y0)) + (POS * V0)) + (a * V0) is Element of the carrier of V0
((y0 + K) * y0) + (POS * V0) is Element of the carrier of V0
(((y0 + K) * y0) + (POS * V0)) + (a * V0) is Element of the carrier of V0
(POS * V0) + (a * V0) is Element of the carrier of V0
((y0 + K) * y0) + ((POS * V0) + (a * V0)) is Element of the carrier of V0
- (K * y0) is Element of the carrier of V0
- (a * V0) is Element of the carrier of V0
(- (K * y0)) + (- (a * V0)) is Element of the carrier of V0
((y0 * y0) + (POS * V0)) + ((- (K * y0)) + (- (a * V0))) is Element of the carrier of V0
- y0 is Element of the carrier of V0
K * (- y0) is Element of the carrier of V0
(K * (- y0)) + (- (a * V0)) is Element of the carrier of V0
((y0 * y0) + (POS * V0)) + ((K * (- y0)) + (- (a * V0))) is Element of the carrier of V0
- V0 is Element of the carrier of V0
a * (- V0) is Element of the carrier of V0
(K * (- y0)) + (a * (- V0)) is Element of the carrier of V0
((y0 * y0) + (POS * V0)) + ((K * (- y0)) + (a * (- V0))) is Element of the carrier of V0
- K is V17() V27() V28() Element of REAL
(- K) * y0 is Element of the carrier of V0
((- K) * y0) + (a * (- V0)) is Element of the carrier of V0
((y0 * y0) + (POS * V0)) + (((- K) * y0) + (a * (- V0))) is Element of the carrier of V0
- a is V17() V27() V28() Element of REAL
(- a) * V0 is Element of the carrier of V0
((- K) * y0) + ((- a) * V0) is Element of the carrier of V0
((y0 * y0) + (POS * V0)) + (((- K) * y0) + ((- a) * V0)) is Element of the carrier of V0
((y0 * y0) + (POS * V0)) + ((- K) * y0) is Element of the carrier of V0
(((y0 * y0) + (POS * V0)) + ((- K) * y0)) + ((- a) * V0) is Element of the carrier of V0
(y0 * y0) + ((- K) * y0) is Element of the carrier of V0
((y0 * y0) + ((- K) * y0)) + (POS * V0) is Element of the carrier of V0
(((y0 * y0) + ((- K) * y0)) + (POS * V0)) + ((- a) * V0) is Element of the carrier of V0
y0 + (- K) is V17() V27() V28() Element of REAL
(y0 + (- K)) * y0 is Element of the carrier of V0
((y0 + (- K)) * y0) + (POS * V0) is Element of the carrier of V0
(((y0 + (- K)) * y0) + (POS * V0)) + ((- a) * V0) is Element of the carrier of V0
(POS * V0) + ((- a) * V0) is Element of the carrier of V0
((y0 + (- K)) * y0) + ((POS * V0) + ((- a) * V0)) is Element of the carrier of V0
POS + (- a) is V17() V27() V28() Element of REAL
(POS + (- a)) * V0 is Element of the carrier of V0
((y0 - K) * y0) + ((POS + (- a)) * V0) is Element of the carrier of V0
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
0. V0 is V59(V0) Element of the carrier of V0
the ZeroF of V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
0 * w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
0 * y0 is Element of the carrier of V0
(0 * w0) + (0 * y0) is Element of the carrier of V0
(0. V0) + (0 * y0) is Element of the carrier of V0
(0. V0) + (0. V0) is Element of the carrier of V0
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
V0 is Element of the carrier of V0
w0 is V17() V27() V28() Element of REAL
w0 * y0 is Element of the carrier of V0
y0 is V17() V27() V28() Element of REAL
y0 * V0 is Element of the carrier of V0
(w0 * y0) + (y0 * V0) is Element of the carrier of V0
POS is V17() V27() V28() Element of REAL
POS * w0 is Element of the carrier of V0
POS * w0 is V17() V27() V28() Element of REAL
(POS * w0) * y0 is Element of the carrier of V0
POS * y0 is V17() V27() V28() Element of REAL
(POS * y0) * V0 is Element of the carrier of V0
((POS * w0) * y0) + ((POS * y0) * V0) is Element of the carrier of V0
POS * (w0 * y0) is Element of the carrier of V0
POS * (y0 * V0) is Element of the carrier of V0
(POS * (w0 * y0)) + (POS * (y0 * V0)) is Element of the carrier of V0
((POS * w0) * y0) + (POS * (y0 * V0)) is Element of the carrier of V0
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
V0 is V17() V27() V28() Element of REAL
V0 * w0 is Element of the carrier of V0
w0 is V17() V27() V28() Element of REAL
w0 * y0 is Element of the carrier of V0
(V0 * w0) + (w0 * y0) is Element of the carrier of V0
y0 is V17() V27() V28() Element of REAL
y0 * w0 is Element of the carrier of V0
POS is V17() V27() V28() Element of REAL
POS * y0 is Element of the carrier of V0
(y0 * w0) + (POS * y0) is Element of the carrier of V0
0. V0 is V59(V0) Element of the carrier of V0
the ZeroF of V0 is Element of the carrier of V0
((V0 * w0) + (w0 * y0)) - ((y0 * w0) + (POS * y0)) is Element of the carrier of V0
- ((y0 * w0) + (POS * y0)) is Element of the carrier of V0
K176(V0,((V0 * w0) + (w0 * y0)),(- ((y0 * w0) + (POS * y0)))) is Element of the carrier of V0
V0 - y0 is V17() V27() V28() Element of REAL
(V0 - y0) * w0 is Element of the carrier of V0
w0 - POS is V17() V27() V28() Element of REAL
(w0 - POS) * y0 is Element of the carrier of V0
((V0 - y0) * w0) + ((w0 - POS) * y0) is Element of the carrier of V0
- y0 is V17() V27() V28() Element of REAL
(- y0) + V0 is V17() V27() V28() Element of REAL
- POS is V17() V27() V28() Element of REAL
(- POS) + w0 is V17() V27() V28() Element of REAL
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
y0 is V17() V27() V28() Element of REAL
y0 * V0 is Element of the carrier of V0
POS is V17() V27() V28() Element of REAL
POS * w0 is Element of the carrier of V0
(y0 * V0) + (POS * w0) is Element of the carrier of V0
K is V17() V27() V28() Element of REAL
K * V0 is Element of the carrier of V0
a is V17() V27() V28() Element of REAL
a * w0 is Element of the carrier of V0
(K * V0) + (a * w0) is Element of the carrier of V0
y0 * K is V17() V27() V28() Element of REAL
POS * a is V17() V27() V28() Element of REAL
(y0 * K) + (POS * a) is V17() V27() V28() Element of REAL
p is V17() V27() V28() Element of REAL
p * V0 is Element of the carrier of V0
q is V17() V27() V28() Element of REAL
q * w0 is Element of the carrier of V0
(p * V0) + (q * w0) is Element of the carrier of V0
x is V17() V27() V28() Element of REAL
x * V0 is Element of the carrier of V0
c₁₃ is V17() V27() V28() Element of REAL
c₁₃ * w0 is Element of the carrier of V0
(x * V0) + (c₁₃ * w0) is Element of the carrier of V0
p * x is V17() V27() V28() Element of REAL
q * c₁₃ is V17() V27() V28() Element of REAL
(p * x) + (q * c₁₃) is V17() V27() V28() Element of REAL
y0 is V17() V27() V28() Element of REAL
y0 * V0 is Element of the carrier of V0
POS is V17() V27() V28() Element of REAL
POS * w0 is Element of the carrier of V0
(y0 * V0) + (POS * w0) is Element of the carrier of V0
K is V17() V27() V28() Element of REAL
K * V0 is Element of the carrier of V0
a is V17() V27() V28() Element of REAL
a * w0 is Element of the carrier of V0
(K * V0) + (a * w0) is Element of the carrier of V0
y0 * K is V17() V27() V28() Element of REAL
POS * a is V17() V27() V28() Element of REAL
(y0 * K) + (POS * a) is V17() V27() V28() Element of REAL
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
0. V0 is V59(V0) Element of the carrier of V0
the ZeroF of V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
1 * w0 is Element of the carrier of V0
(1 * w0) + (0. V0) is Element of the carrier of V0
0 * y0 is Element of the carrier of V0
(1 * w0) + (0 * y0) is Element of the carrier of V0
1 * y0 is Element of the carrier of V0
(0. V0) + (1 * y0) is Element of the carrier of V0
0 * w0 is Element of the carrier of V0
(0 * w0) + (1 * y0) is Element of the carrier of V0
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
0. V0 is V59(V0) Element of the carrier of V0
the ZeroF of V0 is Element of the carrier of V0
(0. V0) + y0 is Element of the carrier of V0
1 * y0 is Element of the carrier of V0
(0. V0) + (1 * y0) is Element of the carrier of V0
0 * w0 is Element of the carrier of V0
(0 * w0) + (1 * y0) is Element of the carrier of V0
1 * 0 is V17() V27() V28() Element of REAL
0 * 1 is V17() V27() V28() Element of REAL
(1 * 0) + (0 * 1) is V17() V27() V28() Element of REAL
w0 + (0. V0) is Element of the carrier of V0
1 * w0 is Element of the carrier of V0
(1 * w0) + (0. V0) is Element of the carrier of V0
0 * y0 is Element of the carrier of V0
(1 * w0) + (0 * y0) is Element of the carrier of V0
V0 is non empty V78() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
0. V0 is V59(V0) Element of the carrier of V0
the ZeroF of V0 is Element of the carrier of V0
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
0. V0 is V59(V0) Element of the carrier of V0
the ZeroF of V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
y0 is V17() V27() V28() Element of REAL
y0 * V0 is Element of the carrier of V0
POS is V17() V27() V28() Element of REAL
POS * w0 is Element of the carrier of V0
(y0 * V0) + (POS * w0) is Element of the carrier of V0
K is V17() V27() V28() Element of REAL
K * V0 is Element of the carrier of V0
a is V17() V27() V28() Element of REAL
a * w0 is Element of the carrier of V0
(K * V0) + (a * w0) is Element of the carrier of V0
y0 * K is V17() V27() V28() Element of REAL
POS * a is V17() V27() V28() Element of REAL
(y0 * K) + (POS * a) is V17() V27() V28() Element of REAL
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
0. V0 is V59(V0) Element of the carrier of V0
the ZeroF of V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
y0 is V17() V27() V28() Element of REAL
y0 * w0 is Element of the carrier of V0
POS is V17() V27() V28() Element of REAL
POS * y0 is Element of the carrier of V0
(y0 * w0) + (POS * y0) is Element of the carrier of V0
K is V17() V27() V28() Element of REAL
K * w0 is Element of the carrier of V0
a is V17() V27() V28() Element of REAL
a * y0 is Element of the carrier of V0
(K * w0) + (a * y0) is Element of the carrier of V0
(0. V0) + (0. V0) is Element of the carrier of V0
0 * w0 is Element of the carrier of V0
(0 * w0) + (0. V0) is Element of the carrier of V0
0 * y0 is Element of the carrier of V0
(0 * w0) + (0 * y0) is Element of the carrier of V0
y0 * 0 is V17() V27() V28() Element of REAL
POS * 0 is V17() V27() V28() Element of REAL
(y0 * 0) + (POS * 0) is V17() V27() V28() Element of REAL
0 * K is V17() V27() V28() Element of REAL
0 * a is V17() V27() V28() Element of REAL
(0 * K) + (0 * a) is V17() V27() V28() Element of REAL
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
y0 is V17() V27() V28() Element of REAL
y0 * w0 is Element of the carrier of V0
POS is V17() V27() V28() Element of REAL
POS * y0 is Element of the carrier of V0
K is V17() V27() V28() Element of REAL
K * V0 is Element of the carrier of V0
a is V17() V27() V28() Element of REAL
a * w0 is Element of the carrier of V0
(K * V0) + (a * w0) is Element of the carrier of V0
p is V17() V27() V28() Element of REAL
p * V0 is Element of the carrier of V0
q is V17() V27() V28() Element of REAL
q * w0 is Element of the carrier of V0
(p * V0) + (q * w0) is Element of the carrier of V0
K * p is V17() V27() V28() Element of REAL
a * q is V17() V27() V28() Element of REAL
(K * p) + (a * q) is V17() V27() V28() Element of REAL
POS * (p * V0) is Element of the carrier of V0
POS * (q * w0) is Element of the carrier of V0
(POS * (p * V0)) + (POS * (q * w0)) is Element of the carrier of V0
POS * p is V17() V27() V28() Element of REAL
(POS * p) * V0 is Element of the carrier of V0
((POS * p) * V0) + (POS * (q * w0)) is Element of the carrier of V0
POS * q is V17() V27() V28() Element of REAL
(POS * q) * w0 is Element of the carrier of V0
((POS * p) * V0) + ((POS * q) * w0) is Element of the carrier of V0
y0 * K is V17() V27() V28() Element of REAL
(y0 * K) * (POS * p) is V17() V27() V28() Element of REAL
y0 * a is V17() V27() V28() Element of REAL
(y0 * a) * (POS * q) is V17() V27() V28() Element of REAL
((y0 * K) * (POS * p)) + ((y0 * a) * (POS * q)) is V17() V27() V28() Element of REAL
POS * y0 is V17() V27() V28() Element of REAL
(POS * y0) * ((K * p) + (a * q)) is V17() V27() V28() Element of REAL
y0 * (K * V0) is Element of the carrier of V0
y0 * (a * w0) is Element of the carrier of V0
(y0 * (K * V0)) + (y0 * (a * w0)) is Element of the carrier of V0
(y0 * K) * V0 is Element of the carrier of V0
((y0 * K) * V0) + (y0 * (a * w0)) is Element of the carrier of V0
(y0 * a) * w0 is Element of the carrier of V0
((y0 * K) * V0) + ((y0 * a) * w0) is Element of the carrier of V0
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
y0 is V17() V27() V28() Element of REAL
y0 * w0 is Element of the carrier of V0
POS is V17() V27() V28() Element of REAL
POS * y0 is Element of the carrier of V0
1 * y0 is Element of the carrier of V0
1 * w0 is Element of the carrier of V0
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
0. V0 is V59(V0) Element of the carrier of V0
the ZeroF of V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
V0 is Element of the carrier of V0
w0 is V17() V27() V28() Element of REAL
w0 * w0 is Element of the carrier of V0
y0 is V17() V27() V28() Element of REAL
y0 * y0 is Element of the carrier of V0
(w0 * w0) + (y0 * y0) is Element of the carrier of V0
y0 * w0 is Element of the carrier of V0
- w0 is V17() V27() V28() Element of REAL
(- w0) * y0 is Element of the carrier of V0
(y0 * w0) + ((- w0) * y0) is Element of the carrier of V0
w0 * y0 is V17() V27() V28() Element of REAL
y0 * (- w0) is V17() V27() V28() Element of REAL
(w0 * y0) + (y0 * (- w0)) is V17() V27() V28() Element of REAL
K is Element of the carrier of V0
0 * w0 is Element of the carrier of V0
(0 * w0) + (0. V0) is Element of the carrier of V0
POS is Element of the carrier of V0
POS is Element of the carrier of V0
K is Element of the carrier of V0
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
0. V0 is V59(V0) Element of the carrier of V0
the ZeroF of V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
POS is V17() V27() V28() Element of REAL
POS * w0 is Element of the carrier of V0
K is V17() V27() V28() Element of REAL
K * y0 is Element of the carrier of V0
(POS * w0) + (K * y0) is Element of the carrier of V0
a is V17() V27() V28() Element of REAL
a * w0 is Element of the carrier of V0
p is V17() V27() V28() Element of REAL
p * y0 is Element of the carrier of V0
(a * w0) + (p * y0) is Element of the carrier of V0
POS * a is V17() V27() V28() Element of REAL
K * p is V17() V27() V28() Element of REAL
(POS * a) + (K * p) is V17() V27() V28() Element of REAL
q is V17() V27() V28() Element of REAL
q * w0 is Element of the carrier of V0
x is V17() V27() V28() Element of REAL
x * y0 is Element of the carrier of V0
(q * w0) + (x * y0) is Element of the carrier of V0
c₁₃ is V17() V27() V28() Element of REAL
c₁₃ * w0 is Element of the carrier of V0
c9 is V17() V27() V28() Element of REAL
c9 * y0 is Element of the carrier of V0
(c₁₃ * w0) + (c9 * y0) is Element of the carrier of V0
q * c₁₃ is V17() V27() V28() Element of REAL
x * c9 is V17() V27() V28() Element of REAL
(q * c₁₃) + (x * c9) is V17() V27() V28() Element of REAL
(c₁₃ * w0) + (0. V0) is Element of the carrier of V0
(a * w0) + (0. V0) is Element of the carrier of V0
1 * w0 is Element of the carrier of V0
0 * w0 is Element of the carrier of V0
0 * y0 is Element of the carrier of V0
c₁₃ * w0 is Element of the carrier of V0
c₁₃ * (a * w0) is Element of the carrier of V0
a * c₁₃ is V17() V27() V28() Element of REAL
(a * c₁₃) * w0 is Element of the carrier of V0
a * y0 is Element of the carrier of V0
d9 is V17() V27() V28() Element of REAL
d9 * w0 is Element of the carrier of V0
M is V17() V27() V28() Element of REAL
M * y0 is Element of the carrier of V0
- K is V17() V27() V28() Element of REAL
(- K) * p is V17() V27() V28() Element of REAL
POS " is V17() V27() V28() Element of REAL
((- K) * p) * (POS ") is V17() V27() V28() Element of REAL
c9 * (((- K) * p) * (POS ")) is V17() V27() V28() Element of REAL
(- K) * c9 is V17() V27() V28() Element of REAL
((- K) * c9) * (POS ") is V17() V27() V28() Element of REAL
p * (((- K) * c9) * (POS ")) is V17() V27() V28() Element of REAL
1 * a is V17() V27() V28() Element of REAL
POS * (POS ") is V17() V27() V28() Element of REAL
(POS * (POS ")) * a is V17() V27() V28() Element of REAL
(POS * a) * (POS ") is V17() V27() V28() Element of REAL
1 * c₁₃ is V17() V27() V28() Element of REAL
(POS * (POS ")) * c₁₃ is V17() V27() V28() Element of REAL
POS * c₁₃ is V17() V27() V28() Element of REAL
(POS * c₁₃) * (POS ") is V17() V27() V28() Element of REAL
p * y0 is Element of the carrier of V0
(p * (((- K) * c9) * (POS "))) * w0 is Element of the carrier of V0
p * c9 is V17() V27() V28() Element of REAL
(p * c9) * y0 is Element of the carrier of V0
((p * (((- K) * c9) * (POS "))) * w0) + ((p * c9) * y0) is Element of the carrier of V0
d9 is V17() V27() V28() Element of REAL
d9 * w0 is Element of the carrier of V0
M is V17() V27() V28() Element of REAL
M * y0 is Element of the carrier of V0
1 * y0 is Element of the carrier of V0
d9 is V17() V27() V28() Element of REAL
d9 * w0 is Element of the carrier of V0
M is V17() V27() V28() Element of REAL
M * y0 is Element of the carrier of V0
N is V17() V27() V28() Element of REAL
N * w0 is Element of the carrier of V0
p is V17() V27() V28() Element of REAL
p * y0 is Element of the carrier of V0
d9 is V17() V27() V28() Element of REAL
d9 * w0 is Element of the carrier of V0
M is V17() V27() V28() Element of REAL
M * y0 is Element of the carrier of V0
N is V17() V27() V28() Element of REAL
N * w0 is Element of the carrier of V0
p is V17() V27() V28() Element of REAL
p * y0 is Element of the carrier of V0
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
w0 + y0 is Element of the carrier of V0
w0 - y0 is Element of the carrier of V0
- y0 is Element of the carrier of V0
K176(V0,w0,(- y0)) is Element of the carrier of V0
POS is V17() V27() V28() Element of REAL
POS * w0 is Element of the carrier of V0
K is V17() V27() V28() Element of REAL
K * y0 is Element of the carrier of V0
(POS * w0) + (K * y0) is Element of the carrier of V0
a is V17() V27() V28() Element of REAL
a * w0 is Element of the carrier of V0
p is V17() V27() V28() Element of REAL
p * y0 is Element of the carrier of V0
(a * w0) + (p * y0) is Element of the carrier of V0
POS * a is V17() V27() V28() Element of REAL
K * p is V17() V27() V28() Element of REAL
(POS * a) + (K * p) is V17() V27() V28() Element of REAL
q is V17() V27() V28() Element of REAL
q * w0 is Element of the carrier of V0
x is V17() V27() V28() Element of REAL
x * y0 is Element of the carrier of V0
(q * w0) + (x * y0) is Element of the carrier of V0
c₁₃ is V17() V27() V28() Element of REAL
c₁₃ * w0 is Element of the carrier of V0
c9 is V17() V27() V28() Element of REAL
c9 * y0 is Element of the carrier of V0
(c₁₃ * w0) + (c9 * y0) is Element of the carrier of V0
q * c₁₃ is V17() V27() V28() Element of REAL
x * c9 is V17() V27() V28() Element of REAL
(q * c₁₃) + (x * c9) is V17() V27() V28() Element of REAL
a + c₁₃ is V17() V27() V28() Element of REAL
POS * (a + c₁₃) is V17() V27() V28() Element of REAL
p + c9 is V17() V27() V28() Element of REAL
K * (p + c9) is V17() V27() V28() Element of REAL
(POS * (a + c₁₃)) + (K * (p + c9)) is V17() V27() V28() Element of REAL
a - c₁₃ is V17() V27() V28() Element of REAL
POS * (a - c₁₃) is V17() V27() V28() Element of REAL
p - c9 is V17() V27() V28() Element of REAL
K * (p - c9) is V17() V27() V28() Element of REAL
(POS * (a - c₁₃)) + (K * (p - c9)) is V17() V27() V28() Element of REAL
(a + c₁₃) * w0 is Element of the carrier of V0
(p + c9) * y0 is Element of the carrier of V0
((a + c₁₃) * w0) + ((p + c9) * y0) is Element of the carrier of V0
(a - c₁₃) * w0 is Element of the carrier of V0
(p - c9) * y0 is Element of the carrier of V0
((a - c₁₃) * w0) + ((p - c9) * y0) is Element of the carrier of V0
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
0. V0 is V59(V0) Element of the carrier of V0
the ZeroF of V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
V0 is Element of the carrier of V0
w0 is V17() V27() V28() Element of REAL
w0 * w0 is V17() V27() V28() Element of REAL
w0 is V17() V27() V28() Element of REAL
w0 * w0 is Element of the carrier of V0
y0 is V17() V27() V28() Element of REAL
y0 * y0 is Element of the carrier of V0
(w0 * w0) + (y0 * y0) is Element of the carrier of V0
POS is V17() V27() V28() Element of REAL
POS * w0 is Element of the carrier of V0
K is V17() V27() V28() Element of REAL
K * y0 is Element of the carrier of V0
(POS * w0) + (K * y0) is Element of the carrier of V0
w0 * POS is V17() V27() V28() Element of REAL
y0 * K is V17() V27() V28() Element of REAL
(w0 * POS) + (y0 * K) is V17() V27() V28() Element of REAL
y0 * y0 is V17() V27() V28() Element of REAL
w0 * w0 is V17() V27() V28() Element of REAL
0 * w0 is Element of the carrier of V0
(0 * w0) + (0. V0) is Element of the carrier of V0
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
V0 - w0 is Element of the carrier of V0
- w0 is Element of the carrier of V0
K176(V0,V0,(- w0)) is Element of the carrier of V0
y0 is Element of the carrier of V0
w0 - y0 is Element of the carrier of V0
- y0 is Element of the carrier of V0
K176(V0,w0,(- y0)) is Element of the carrier of V0
y0 - V0 is Element of the carrier of V0
- V0 is Element of the carrier of V0
K176(V0,y0,(- V0)) is Element of the carrier of V0
POS is V17() V27() V28() Element of REAL
POS * w0 is Element of the carrier of V0
K is V17() V27() V28() Element of REAL
K * y0 is Element of the carrier of V0
(POS * w0) + (K * y0) is Element of the carrier of V0
a is V17() V27() V28() Element of REAL
a * w0 is Element of the carrier of V0
p is V17() V27() V28() Element of REAL
p * y0 is Element of the carrier of V0
(a * w0) + (p * y0) is Element of the carrier of V0
q is V17() V27() V28() Element of REAL
q * w0 is Element of the carrier of V0
x is V17() V27() V28() Element of REAL
x * y0 is Element of the carrier of V0
(q * w0) + (x * y0) is Element of the carrier of V0
POS - q is V17() V27() V28() Element of REAL
(POS - q) * w0 is Element of the carrier of V0
K - x is V17() V27() V28() Element of REAL
(K - x) * y0 is Element of the carrier of V0
((POS - q) * w0) + ((K - x) * y0) is Element of the carrier of V0
a - POS is V17() V27() V28() Element of REAL
(a - POS) * w0 is Element of the carrier of V0
p - K is V17() V27() V28() Element of REAL
(p - K) * y0 is Element of the carrier of V0
((a - POS) * w0) + ((p - K) * y0) is Element of the carrier of V0
q * (a - POS) is V17() V27() V28() Element of REAL
x * (p - K) is V17() V27() V28() Element of REAL
(q * (a - POS)) + (x * (p - K)) is V17() V27() V28() Element of REAL
q - a is V17() V27() V28() Element of REAL
(q - a) * w0 is Element of the carrier of V0
x - p is V17() V27() V28() Element of REAL
(x - p) * y0 is Element of the carrier of V0
((q - a) * w0) + ((x - p) * y0) is Element of the carrier of V0
POS * (q - a) is V17() V27() V28() Element of REAL
K * (x - p) is V17() V27() V28() Element of REAL
(POS * (q - a)) + (K * (x - p)) is V17() V27() V28() Element of REAL
a * (POS - q) is V17() V27() V28() Element of REAL
p * (K - x) is V17() V27() V28() Element of REAL
(a * (POS - q)) + (p * (K - x)) is V17() V27() V28() Element of REAL
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
0. V0 is V59(V0) Element of the carrier of V0
the ZeroF of V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
y0 is V17() V27() V28() Element of REAL
y0 * w0 is Element of the carrier of V0
POS is V17() V27() V28() Element of REAL
POS * y0 is Element of the carrier of V0
(y0 * w0) + (POS * y0) is Element of the carrier of V0
K is V17() V27() V28() Element of REAL
K * w0 is Element of the carrier of V0
a is V17() V27() V28() Element of REAL
a * y0 is Element of the carrier of V0
(K * w0) + (a * y0) is Element of the carrier of V0
K * y0 is V17() V27() V28() Element of REAL
a * POS is V17() V27() V28() Element of REAL
(K * y0) + (a * POS) is V17() V27() V28() Element of REAL
y0 * y0 is V17() V27() V28() Element of REAL
POS * POS is V17() V27() V28() Element of REAL
(y0 * y0) + (POS * POS) is V17() V27() V28() Element of REAL
((y0 * y0) + (POS * POS)) " is V17() V27() V28() Element of REAL
((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ") is V17() V27() V28() Element of REAL
(((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * V0 is Element of the carrier of V0
(((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * y0 is V17() V27() V28() Element of REAL
((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * y0) * w0 is Element of the carrier of V0
(((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * POS is V17() V27() V28() Element of REAL
((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * POS) * y0 is Element of the carrier of V0
(((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * y0) * w0) + (((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * POS) * y0) is Element of the carrier of V0
w0 - ((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * V0) is Element of the carrier of V0
- ((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * V0) is Element of the carrier of V0
K176(V0,w0,(- ((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * V0))) is Element of the carrier of V0
K - ((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * y0) is V17() V27() V28() Element of REAL
(K - ((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * y0)) * w0 is Element of the carrier of V0
a - ((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * POS) is V17() V27() V28() Element of REAL
(a - ((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * POS)) * y0 is Element of the carrier of V0
((K - ((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * y0)) * w0) + ((a - ((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * POS)) * y0) is Element of the carrier of V0
(K - ((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * y0)) * y0 is V17() V27() V28() Element of REAL
(a - ((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * POS)) * POS is V17() V27() V28() Element of REAL
((K - ((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * y0)) * y0) + ((a - ((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * POS)) * POS) is V17() V27() V28() Element of REAL
y0 * K is V17() V27() V28() Element of REAL
POS * a is V17() V27() V28() Element of REAL
(y0 * K) + (POS * a) is V17() V27() V28() Element of REAL
y0 * ((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * y0) is V17() V27() V28() Element of REAL
POS * ((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * POS) is V17() V27() V28() Element of REAL
(y0 * ((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * y0)) + (POS * ((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * POS)) is V17() V27() V28() Element of REAL
(- 1) * ((y0 * ((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * y0)) + (POS * ((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * POS))) is V17() V27() V28() Element of REAL
((y0 * K) + (POS * a)) + ((- 1) * ((y0 * ((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * y0)) + (POS * ((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * POS)))) is V17() V27() V28() Element of REAL
(((y0 * y0) + (POS * POS)) ") * ((y0 * y0) + (POS * POS)) is V17() V27() V28() Element of REAL
((K * y0) + (a * POS)) * ((((y0 * y0) + (POS * POS)) ") * ((y0 * y0) + (POS * POS))) is V17() V27() V28() Element of REAL
(- 1) * (((K * y0) + (a * POS)) * ((((y0 * y0) + (POS * POS)) ") * ((y0 * y0) + (POS * POS)))) is V17() V27() V28() Element of REAL
((K * y0) + (a * POS)) * 1 is V17() V27() V28() Element of REAL
(- 1) * (((K * y0) + (a * POS)) * 1) is V17() V27() V28() Element of REAL
- ((y0 * K) + (POS * a)) is V17() V27() V28() Element of REAL
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
y0 - w0 is Element of the carrier of V0
- w0 is Element of the carrier of V0
K176(V0,y0,(- w0)) is Element of the carrier of V0
V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
w0 - V0 is Element of the carrier of V0
- V0 is Element of the carrier of V0
K176(V0,w0,(- V0)) is Element of the carrier of V0
POS is Element of the carrier of V0
y0 is Element of the carrier of V0
POS - y0 is Element of the carrier of V0
- y0 is Element of the carrier of V0
K176(V0,POS,(- y0)) is Element of the carrier of V0
a is Element of the carrier of V0
K is Element of the carrier of V0
a - K is Element of the carrier of V0
- K is Element of the carrier of V0
K176(V0,a,(- K)) is Element of the carrier of V0
p is V17() V27() V28() Element of REAL
p * (POS - y0) is Element of the carrier of V0
q is V17() V27() V28() Element of REAL
q * (a - K) is Element of the carrier of V0
0. V0 is V59(V0) Element of the carrier of V0
the ZeroF of V0 is Element of the carrier of V0
POS is Element of the carrier of V0
y0 is Element of the carrier of V0
POS - y0 is Element of the carrier of V0
- y0 is Element of the carrier of V0
K176(V0,POS,(- y0)) is Element of the carrier of V0
a is Element of the carrier of V0
K is Element of the carrier of V0
a - K is Element of the carrier of V0
- K is Element of the carrier of V0
K176(V0,a,(- K)) is Element of the carrier of V0
p is V17() V27() V28() Element of REAL
p * (POS - y0) is Element of the carrier of V0
q is V17() V27() V28() Element of REAL
q * (a - K) is Element of the carrier of V0
K - a is Element of the carrier of V0
- a is Element of the carrier of V0
K176(V0,K,(- a)) is Element of the carrier of V0
- (K - a) is Element of the carrier of V0
q * (- (K - a)) is Element of the carrier of V0
- q is V17() V27() V28() Element of REAL
(- q) * (K - a) is Element of the carrier of V0
y0 is V17() V27() V28() Element of REAL
y0 * (y0 - w0) is Element of the carrier of V0
POS is V17() V27() V28() Element of REAL
POS * (w0 - V0) is Element of the carrier of V0
- y0 is V17() V27() V28() Element of REAL
- POS is V17() V27() V28() Element of REAL
w0 - y0 is Element of the carrier of V0
- y0 is Element of the carrier of V0
K176(V0,w0,(- y0)) is Element of the carrier of V0
(- y0) * (w0 - y0) is Element of the carrier of V0
- (w0 - y0) is Element of the carrier of V0
y0 * (- (w0 - y0)) is Element of the carrier of V0
V0 - w0 is Element of the carrier of V0
- w0 is Element of the carrier of V0
K176(V0,V0,(- w0)) is Element of the carrier of V0
- (V0 - w0) is Element of the carrier of V0
POS * (- (V0 - w0)) is Element of the carrier of V0
(- POS) * (V0 - w0) is Element of the carrier of V0
y0 is Element of the carrier of V0
POS is Element of the carrier of V0
K is Element of the carrier of V0
a is Element of the carrier of V0
POS - y0 is Element of the carrier of V0
- y0 is Element of the carrier of V0
K176(V0,POS,(- y0)) is Element of the carrier of V0
1 * (POS - y0) is Element of the carrier of V0
a - K is Element of the carrier of V0
- K is Element of the carrier of V0
K176(V0,a,(- K)) is Element of the carrier of V0
0 * (a - K) is Element of the carrier of V0
1 * (a - K) is Element of the carrier of V0
0 * (POS - y0) is Element of the carrier of V0
p is V17() V27() V28() Element of REAL
q is V17() V27() V28() Element of REAL
p * (POS - y0) is Element of the carrier of V0
q * (a - K) is Element of the carrier of V0
p is V17() V27() V28() Element of REAL
p * (POS - y0) is Element of the carrier of V0
q is V17() V27() V28() Element of REAL
q * (a - K) is Element of the carrier of V0
x is V17() V27() V28() Element of REAL
x * (POS - y0) is Element of the carrier of V0
c₁₃ is V17() V27() V28() Element of REAL
c₁₃ * (a - K) is Element of the carrier of V0
c9 is V17() V27() V28() Element of REAL
c9 * (POS - y0) is Element of the carrier of V0
d9 is V17() V27() V28() Element of REAL
d9 * (a - K) is Element of the carrier of V0
y0 is V17() V27() V28() Element of REAL
y0 * (y0 - w0) is Element of the carrier of V0
POS is V17() V27() V28() Element of REAL
POS * (V0 - w0) is Element of the carrier of V0
- POS is V17() V27() V28() Element of REAL
(- POS) * (w0 - V0) is Element of the carrier of V0
- (w0 - V0) is Element of the carrier of V0
POS * (- (w0 - V0)) is Element of the carrier of V0
y0 is V17() V27() V28() Element of REAL
y0 * (y0 - w0) is Element of the carrier of V0
POS is V17() V27() V28() Element of REAL
POS * (w0 - V0) is Element of the carrier of V0
K is V17() V27() V28() Element of REAL
K * (y0 - w0) is Element of the carrier of V0
a is V17() V27() V28() Element of REAL
a * (w0 - V0) is Element of the carrier of V0
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
[: the carrier of V0, the carrier of V0:] is non empty set
DirPar V0 is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
[:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
lambda (DirPar V0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
[w0,y0] is Element of [: the carrier of V0, the carrier of V0:]
y0 - w0 is Element of the carrier of V0
- w0 is Element of the carrier of V0
K176(V0,y0,(- w0)) is Element of the carrier of V0
V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
[V0,w0] is Element of [: the carrier of V0, the carrier of V0:]
[[w0,y0],[V0,w0]] is Element of [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
w0 - V0 is Element of the carrier of V0
- V0 is Element of the carrier of V0
K176(V0,w0,(- V0)) is Element of the carrier of V0
[w0,V0] is Element of [: the carrier of V0, the carrier of V0:]
[[w0,y0],[w0,V0]] is Element of [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
y0 is V17() V27() V28() Element of REAL
y0 * (y0 - w0) is Element of the carrier of V0
POS is V17() V27() V28() Element of REAL
POS * (w0 - V0) is Element of the carrier of V0
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
[: the carrier of V0, the carrier of V0:] is non empty set
[:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
w0 is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
y0 is set
POS is set
[y0,POS] is set
K is Element of the carrier of V0
a is Element of the carrier of V0
[K,a] is Element of [: the carrier of V0, the carrier of V0:]
p is Element of the carrier of V0
q is Element of the carrier of V0
[p,q] is Element of [: the carrier of V0, the carrier of V0:]
V0 is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
w0 is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
y0 is set
POS is set
[y0,POS] is set
K is Element of the carrier of V0
a is Element of the carrier of V0
[K,a] is Element of [: the carrier of V0, the carrier of V0:]
p is Element of the carrier of V0
q is Element of the carrier of V0
[p,q] is Element of [: the carrier of V0, the carrier of V0:]
K is Element of the carrier of V0
a is Element of the carrier of V0
[K,a] is Element of [: the carrier of V0, the carrier of V0:]
p is Element of the carrier of V0
q is Element of the carrier of V0
[p,q] is Element of [: the carrier of V0, the carrier of V0:]
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
OASpace V0 is non empty strict AffinStruct
Lambda (OASpace V0) is non empty strict AffinStruct
the carrier of (Lambda (OASpace V0)) is non empty set
the carrier of V0 is non empty set
the carrier of (OASpace V0) is non empty set
the CONGR of (OASpace V0) is V7() V10([: the carrier of (OASpace V0), the carrier of (OASpace V0):]) V11([: the carrier of (OASpace V0), the carrier of (OASpace V0):]) Element of bool [:[: the carrier of (OASpace V0), the carrier of (OASpace V0):],[: the carrier of (OASpace V0), the carrier of (OASpace V0):]:]
[: the carrier of (OASpace V0), the carrier of (OASpace V0):] is non empty set
[:[: the carrier of (OASpace V0), the carrier of (OASpace V0):],[: the carrier of (OASpace V0), the carrier of (OASpace V0):]:] is non empty set
bool [:[: the carrier of (OASpace V0), the carrier of (OASpace V0):],[: the carrier of (OASpace V0), the carrier of (OASpace V0):]:] is non empty set
lambda the CONGR of (OASpace V0) is V7() V10([: the carrier of (OASpace V0), the carrier of (OASpace V0):]) V11([: the carrier of (OASpace V0), the carrier of (OASpace V0):]) Element of bool [:[: the carrier of (OASpace V0), the carrier of (OASpace V0):],[: the carrier of (OASpace V0), the carrier of (OASpace V0):]:]
AffinStruct(# the carrier of (OASpace V0),(lambda the CONGR of (OASpace V0)) #) is strict AffinStruct
DirPar V0 is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
[: the carrier of V0, the carrier of V0:] is non empty set
[:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
AffinStruct(# the carrier of V0,(DirPar V0) #) is strict AffinStruct
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
OASpace V0 is non empty strict AffinStruct
Lambda (OASpace V0) is non empty strict AffinStruct
the CONGR of (Lambda (OASpace V0)) is V7() V10([: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):]) V11([: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):]) Element of bool [:[: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):],[: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):]:]
the carrier of (Lambda (OASpace V0)) is non empty set
[: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):] is non empty set
[:[: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):],[: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):]:] is non empty set
bool [:[: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):],[: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):]:] is non empty set
the carrier of V0 is non empty set
DirPar V0 is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
[: the carrier of V0, the carrier of V0:] is non empty set
[:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
lambda (DirPar V0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
the carrier of (OASpace V0) is non empty set
the CONGR of (OASpace V0) is V7() V10([: the carrier of (OASpace V0), the carrier of (OASpace V0):]) V11([: the carrier of (OASpace V0), the carrier of (OASpace V0):]) Element of bool [:[: the carrier of (OASpace V0), the carrier of (OASpace V0):],[: the carrier of (OASpace V0), the carrier of (OASpace V0):]:]
[: the carrier of (OASpace V0), the carrier of (OASpace V0):] is non empty set
[:[: the carrier of (OASpace V0), the carrier of (OASpace V0):],[: the carrier of (OASpace V0), the carrier of (OASpace V0):]:] is non empty set
bool [:[: the carrier of (OASpace V0), the carrier of (OASpace V0):],[: the carrier of (OASpace V0), the carrier of (OASpace V0):]:] is non empty set
lambda the CONGR of (OASpace V0) is V7() V10([: the carrier of (OASpace V0), the carrier of (OASpace V0):]) V11([: the carrier of (OASpace V0), the carrier of (OASpace V0):]) Element of bool [:[: the carrier of (OASpace V0), the carrier of (OASpace V0):],[: the carrier of (OASpace V0), the carrier of (OASpace V0):]:]
AffinStruct(# the carrier of (OASpace V0),(lambda the CONGR of (OASpace V0)) #) is strict AffinStruct
AffinStruct(# the carrier of V0,(DirPar V0) #) is strict AffinStruct
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
OASpace V0 is non empty strict AffinStruct
Lambda (OASpace V0) is non empty strict AffinStruct
the carrier of (Lambda (OASpace V0)) is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
y0 - w0 is Element of the carrier of V0
- w0 is Element of the carrier of V0
K176(V0,y0,(- w0)) is Element of the carrier of V0
V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
w0 - V0 is Element of the carrier of V0
- V0 is Element of the carrier of V0
K176(V0,w0,(- V0)) is Element of the carrier of V0
y0 is Element of the carrier of (Lambda (OASpace V0))
POS is Element of the carrier of (Lambda (OASpace V0))
K is Element of the carrier of (Lambda (OASpace V0))
a is Element of the carrier of (Lambda (OASpace V0))
[: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):] is non empty set
[y0,POS] is Element of [: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):]
[K,a] is Element of [: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):]
[[y0,POS],[K,a]] is Element of [:[: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):],[: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):]:]
[:[: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):],[: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):]:] is non empty set
the CONGR of (Lambda (OASpace V0)) is V7() V10([: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):]) V11([: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):]) Element of bool [:[: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):],[: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):]:]
bool [:[: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):],[: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):]:] is non empty set
[: the carrier of V0, the carrier of V0:] is non empty set
[w0,y0] is Element of [: the carrier of V0, the carrier of V0:]
[V0,w0] is Element of [: the carrier of V0, the carrier of V0:]
[[w0,y0],[V0,w0]] is Element of [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
[:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
DirPar V0 is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
lambda (DirPar V0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
p is V17() V27() V28() Element of REAL
p * (y0 - w0) is Element of the carrier of V0
q is V17() V27() V28() Element of REAL
q * (w0 - V0) is Element of the carrier of V0
the non empty set is non empty set
[: the non empty set , the non empty set :] is non empty set
[:[: the non empty set , the non empty set :],[: the non empty set , the non empty set :]:] is non empty set
bool [:[: the non empty set , the non empty set :],[: the non empty set , the non empty set :]:] is non empty set
the V7() V10([: the non empty set , the non empty set :]) V11([: the non empty set , the non empty set :]) Element of bool [:[: the non empty set , the non empty set :],[: the non empty set , the non empty set :]:] is V7() V10([: the non empty set , the non empty set :]) V11([: the non empty set , the non empty set :]) Element of bool [:[: the non empty set , the non empty set :],[: the non empty set , the non empty set :]:]
( the non empty set , the V7() V10([: the non empty set , the non empty set :]) V11([: the non empty set , the non empty set :]) Element of bool [:[: the non empty set , the non empty set :],[: the non empty set , the non empty set :]:], the V7() V10([: the non empty set , the non empty set :]) V11([: the non empty set , the non empty set :]) Element of bool [:[: the non empty set , the non empty set :],[: the non empty set , the non empty set :]:]) is () ()
the carrier of ( the non empty set , the V7() V10([: the non empty set , the non empty set :]) V11([: the non empty set , the non empty set :]) Element of bool [:[: the non empty set , the non empty set :],[: the non empty set , the non empty set :]:], the V7() V10([: the non empty set , the non empty set :]) V11([: the non empty set , the non empty set :]) Element of bool [:[: the non empty set , the non empty set :],[: the non empty set , the non empty set :]:]) is set
V0 is non empty ()
the carrier of V0 is non empty set
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
DirPar V0 is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
[: the carrier of V0, the carrier of V0:] is non empty set
[:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
lambda (DirPar V0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
(V0,w0,y0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
( the carrier of V0,(lambda (DirPar V0)),(V0,w0,y0)) is () ()
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
(V0,w0,y0) is () ()
DirPar V0 is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
[: the carrier of V0, the carrier of V0:] is non empty set
[:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
lambda (DirPar V0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
(V0,w0,y0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
( the carrier of V0,(lambda (DirPar V0)),(V0,w0,y0)) is () ()
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
POS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of POS is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
(V0,w0,y0) is non empty () ()
DirPar V0 is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
[: the carrier of V0, the carrier of V0:] is non empty set
[:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
lambda (DirPar V0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
(V0,w0,y0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
( the carrier of V0,(lambda (DirPar V0)),(V0,w0,y0)) is () ()
the carrier of (V0,w0,y0) is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
(V0,w0,y0) is non empty () ()
DirPar V0 is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
[: the carrier of V0, the carrier of V0:] is non empty set
[:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
lambda (DirPar V0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
(V0,w0,y0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
( the carrier of V0,(lambda (DirPar V0)),(V0,w0,y0)) is () ()
the CONGR of (V0,w0,y0) is V7() V10([: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):]) V11([: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):]) Element of bool [:[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):],[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):]:]
the carrier of (V0,w0,y0) is non empty set
[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):] is non empty set
[:[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):],[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):]:] is non empty set
bool [:[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):],[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):]:] is non empty set
K is Element of the carrier of POS
a is Element of the carrier of POS
(POS,K,a) is non empty () ()
DirPar POS is V7() V10([: the carrier of POS, the carrier of POS:]) V11([: the carrier of POS, the carrier of POS:]) Element of bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:]
[: the carrier of POS, the carrier of POS:] is non empty set
[:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
lambda (DirPar POS) is V7() V10([: the carrier of POS, the carrier of POS:]) V11([: the carrier of POS, the carrier of POS:]) Element of bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:]
(POS,K,a) is V7() V10([: the carrier of POS, the carrier of POS:]) V11([: the carrier of POS, the carrier of POS:]) Element of bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:]
( the carrier of POS,(lambda (DirPar POS)),(POS,K,a)) is () ()
the of (POS,K,a) is V7() V10([: the carrier of (POS,K,a), the carrier of (POS,K,a):]) V11([: the carrier of (POS,K,a), the carrier of (POS,K,a):]) Element of bool [:[: the carrier of (POS,K,a), the carrier of (POS,K,a):],[: the carrier of (POS,K,a), the carrier of (POS,K,a):]:]
the carrier of (POS,K,a) is non empty set
[: the carrier of (POS,K,a), the carrier of (POS,K,a):] is non empty set
[:[: the carrier of (POS,K,a), the carrier of (POS,K,a):],[: the carrier of (POS,K,a), the carrier of (POS,K,a):]:] is non empty set
bool [:[: the carrier of (POS,K,a), the carrier of (POS,K,a):],[: the carrier of (POS,K,a), the carrier of (POS,K,a):]:] is non empty set
V0 is non empty ()
the carrier of V0 is non empty set
the CONGR of V0 is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
[: the carrier of V0, the carrier of V0:] is non empty set
[:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
AffinStruct(# the carrier of V0, the CONGR of V0 #) is strict AffinStruct
V0 is non empty ()
(V0) is strict AffinStruct
the carrier of V0 is non empty set
the CONGR of V0 is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
[: the carrier of V0, the carrier of V0:] is non empty set
[:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
AffinStruct(# the carrier of V0, the CONGR of V0 #) is strict