:: 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

c

(x * V0) + (c

p * x is V17() V27() V28() Element of REAL

q * c

(p * x) + (q * c

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

c

c9 is V17() V27() V28() Element of REAL

c9 * y0 is Element of the carrier of V0

(c

q * c

x * c9 is V17() V27() V28() Element of REAL

(q * c

(c

(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

c

a * c

(a * c

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

(POS * (POS ")) * c

POS * c

(POS * c

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

c

c9 is V17() V27() V28() Element of REAL

c9 * y0 is Element of the carrier of V0

(c

q * c

x * c9 is V17() V27() V28() Element of REAL

(q * c

a + c

POS * (a + c

p + c9 is V17() V27() V28() Element of REAL

K * (p + c9) is V17() V27() V28() Element of REAL

(POS * (a + c

a - c

POS * (a - c

p - c9 is V17() V27() V28() Element of REAL

K * (p - c9) is V17() V27() V28() Element of REAL

(POS * (a - c

(a + c

(p + c9) * y0 is Element of the carrier of V0

((a + c

(a - c

(p - c9) * y0 is Element of the carrier of V0

((a - c

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

c

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