:: ANPROJ_1 semantic presentation

K28() is set
K32() is non empty V4() V5() V6() Element of bool K28()
bool K28() is set
K27() is non empty V4() V5() V6() set
bool K27() is set
bool K32() is set
{} is set
1 is non empty V4() V5() V6() V10() V11() V12() Element of K32()
0 is V4() V5() V6() V10() V11() V12() Element of K32()
- 1 is V11() V12() Element of K28()
K39(0) is V11() V12() set
x is non empty V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
the carrier of x is non empty set
y is Element of the carrier of x
1 * y is Element of the carrier of x
y is Element of the carrier of x
y is V11() V12() Element of K28()
y * y is Element of the carrier of x
y is Element of the carrier of x
dw is V11() V12() Element of K28()
dw * y is Element of the carrier of x
x is non empty V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
the carrier of x is non empty set
V is Element of the carrier of x
x9 is Element of the carrier of x
y is V11() V12() Element of K28()
y * V is Element of the carrier of x
y is V11() V12() Element of K28()
y * x9 is Element of the carrier of x
y " is V11() V12() Element of K28()
1 * V is Element of the carrier of x
(y ") * y is V11() V12() Element of K28()
((y ") * y) * V is Element of the carrier of x
(y ") * (y * x9) is Element of the carrier of x
(y ") * y is V11() V12() Element of K28()
((y ") * y) * x9 is Element of the carrier of x
y is V11() V12() Element of K28()
y * x9 is Element of the carrier of x
y is V11() V12() Element of K28()
y * x9 is Element of the carrier of x
y is V11() V12() Element of K28()
y * x9 is Element of the carrier of x
x is non empty V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
the carrier of x is non empty set
V is Element of the carrier of x
x9 is Element of the carrier of x
y is Element of the carrier of x
y is V11() V12() Element of K28()
y * V is Element of the carrier of x
y is V11() V12() Element of K28()
y * x9 is Element of the carrier of x
dw is V11() V12() Element of K28()
dw * x9 is Element of the carrier of x
p is V11() V12() Element of K28()
p * y is Element of the carrier of x
y " is V11() V12() Element of K28()
(y ") * y is V11() V12() Element of K28()
dw * ((y ") * y) is V11() V12() Element of K28()
((y ") * y) * V is Element of the carrier of x
(y ") * (y * x9) is Element of the carrier of x
(y ") * y is V11() V12() Element of K28()
((y ") * y) * x9 is Element of the carrier of x
1 * x9 is Element of the carrier of x
(dw * ((y ") * y)) * V is Element of the carrier of x
x is non empty V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
the carrier of x is non empty set
0. x is zero Element of the carrier of x
the ZeroF of x is Element of the carrier of x
V is Element of the carrier of x
x9 is V11() V12() Element of K28()
x9 * V is Element of the carrier of x
y is V11() V12() Element of K28()
y * (0. x) is Element of the carrier of x
x is non empty V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
the carrier of x is non empty set
x is non empty V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
the carrier of x is non empty set
V is Element of the carrier of x
x9 is Element of the carrier of x
y is Element of the carrier of x
y is Element of the carrier of x
y is Element of the carrier of x
dw is Element of the carrier of x
p is V11() V12() Element of K28()
p * y is Element of the carrier of x
q is V11() V12() Element of K28()
q * x9 is Element of the carrier of x
0. x is zero Element of the carrier of x
the ZeroF of x is Element of the carrier of x
r is V11() V12() Element of K28()
r * V is Element of the carrier of x
r is V11() V12() Element of K28()
r * y is Element of the carrier of x
(r * V) + (r * y) is Element of the carrier of x
r is V11() V12() Element of K28()
r * y is Element of the carrier of x
((r * V) + (r * y)) + (r * y) is Element of the carrier of x
a39 is V11() V12() Element of K28()
a39 * dw is Element of the carrier of x
r * q is V11() V12() Element of K28()
r * p is V11() V12() Element of K28()
r * a39 is V11() V12() Element of K28()
(r * q) * x9 is Element of the carrier of x
r * (p * y) is Element of the carrier of x
((r * q) * x9) + (r * (p * y)) is Element of the carrier of x
r * (a39 * dw) is Element of the carrier of x
(((r * q) * x9) + (r * (p * y))) + (r * (a39 * dw)) is Element of the carrier of x
(r * p) * y is Element of the carrier of x
((r * q) * x9) + ((r * p) * y) is Element of the carrier of x
(((r * q) * x9) + ((r * p) * y)) + (r * (a39 * dw)) is Element of the carrier of x
(r * a39) * dw is Element of the carrier of x
(((r * q) * x9) + ((r * p) * y)) + ((r * a39) * dw) is Element of the carrier of x
x is non empty V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
the carrier of x is non empty set
V is Element of the carrier of x
x9 is Element of the carrier of x
y is Element of the carrier of x
0. x is zero Element of the carrier of x
the ZeroF of x is Element of the carrier of x
y is V11() V12() Element of K28()
y * V is Element of the carrier of x
y is V11() V12() Element of K28()
y * x9 is Element of the carrier of x
(y * V) + (y * x9) is Element of the carrier of x
dw is V11() V12() Element of K28()
dw * y is Element of the carrier of x
((y * V) + (y * x9)) + (dw * y) is Element of the carrier of x
(y * V) + (dw * y) is Element of the carrier of x
((y * V) + (dw * y)) + (y * x9) is Element of the carrier of x
(y * x9) + (dw * y) is Element of the carrier of x
((y * x9) + (dw * y)) + (y * V) is Element of the carrier of x
x is non empty V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
the carrier of x is non empty set
0. x is zero Element of the carrier of x
the ZeroF of x is Element of the carrier of x
V is Element of the carrier of x
x9 is Element of the carrier of x
y is V11() V12() Element of K28()
y * V is Element of the carrier of x
y is V11() V12() Element of K28()
y * x9 is Element of the carrier of x
(y * V) + (y * x9) is Element of the carrier of x
- y is V11() V12() Element of K28()
(- y) * x9 is Element of the carrier of x
- (y * x9) is Element of the carrier of x
- x9 is Element of the carrier of x
y * (- x9) is Element of the carrier of x
x is non empty V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
the carrier of x is non empty set
0. x is zero Element of the carrier of x
the ZeroF of x is Element of the carrier of x
V is Element of the carrier of x
x9 is Element of the carrier of x
y is Element of the carrier of x
y is V11() V12() Element of K28()
y * V is Element of the carrier of x
y " is V11() V12() Element of K28()
y is V11() V12() Element of K28()
y * x9 is Element of the carrier of x
(y * V) + (y * x9) is Element of the carrier of x
(y ") * y is V11() V12() Element of K28()
- ((y ") * y) is V11() V12() Element of K28()
(- ((y ") * y)) * x9 is Element of the carrier of x
dw is V11() V12() Element of K28()
dw * y is Element of the carrier of x
((y * V) + (y * x9)) + (dw * y) is Element of the carrier of x
(y ") * dw is V11() V12() Element of K28()
- ((y ") * dw) is V11() V12() Element of K28()
(- ((y ") * dw)) * y is Element of the carrier of x
((- ((y ") * y)) * x9) + ((- ((y ") * dw)) * y) is Element of the carrier of x
(y * x9) + (dw * y) is Element of the carrier of x
(y * V) + ((y * x9) + (dw * y)) is Element of the carrier of x
- ((y * x9) + (dw * y)) is Element of the carrier of x
- (y * x9) is Element of the carrier of x
- (dw * y) is Element of the carrier of x
(- (y * x9)) + (- (dw * y)) is Element of the carrier of x
- x9 is Element of the carrier of x
y * (- x9) is Element of the carrier of x
(y * (- x9)) + (- (dw * y)) is Element of the carrier of x
- y is Element of the carrier of x
dw * (- y) is Element of the carrier of x
(y * (- x9)) + (dw * (- y)) is Element of the carrier of x
- y is V11() V12() Element of K28()
(- y) * x9 is Element of the carrier of x
((- y) * x9) + (dw * (- y)) is Element of the carrier of x
- dw is V11() V12() Element of K28()
(- dw) * y is Element of the carrier of x
((- y) * x9) + ((- dw) * y) is Element of the carrier of x
(y ") * (((- y) * x9) + ((- dw) * y)) is Element of the carrier of x
(y ") * ((- y) * x9) is Element of the carrier of x
(y ") * ((- dw) * y) is Element of the carrier of x
((y ") * ((- y) * x9)) + ((y ") * ((- dw) * y)) is Element of the carrier of x
(y ") * (- y) is V11() V12() Element of K28()
((y ") * (- y)) * x9 is Element of the carrier of x
(((y ") * (- y)) * x9) + ((y ") * ((- dw) * y)) is Element of the carrier of x
(y ") * (- dw) is V11() V12() Element of K28()
((y ") * (- dw)) * y is Element of the carrier of x
((- ((y ") * y)) * x9) + (((y ") * (- dw)) * y) is Element of the carrier of x
x is non empty V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
the carrier of x is non empty set
V is Element of the carrier of x
x9 is Element of the carrier of x
y is Element of the carrier of x
0. x is zero Element of the carrier of x
the ZeroF of x is Element of the carrier of x
y is V11() V12() Element of K28()
y * y is Element of the carrier of x
y is V11() V12() Element of K28()
y * V is Element of the carrier of x
(y * y) + (y * V) is Element of the carrier of x
dw is V11() V12() Element of K28()
dw * x9 is Element of the carrier of x
((y * y) + (y * V)) + (dw * x9) is Element of the carrier of x
(0. x) + (y * V) is Element of the carrier of x
((0. x) + (y * V)) + (dw * x9) is Element of the carrier of x
(y * V) + (dw * x9) is Element of the carrier of x
(0. x) + (dw * x9) is Element of the carrier of x
(y * V) + (0. x) is Element of the carrier of x
- dw is V11() V12() Element of K28()
(- dw) * x9 is Element of the carrier of x
y " is V11() V12() Element of K28()
(y ") * y is V11() V12() Element of K28()
- ((y ") * y) is V11() V12() Element of K28()
(- ((y ") * y)) * V is Element of the carrier of x
(y ") * dw is V11() V12() Element of K28()
- ((y ") * dw) is V11() V12() Element of K28()
(- ((y ") * dw)) * x9 is Element of the carrier of x
((- ((y ") * y)) * V) + ((- ((y ") * dw)) * x9) is Element of the carrier of x
y is V11() V12() Element of K28()
y * V is Element of the carrier of x
y is V11() V12() Element of K28()
y * x9 is Element of the carrier of x
(y * V) + (y * x9) is Element of the carrier of x
- y is Element of the carrier of x
((y * V) + (y * x9)) + (- y) is Element of the carrier of x
(- 1) * y is Element of the carrier of x
((y * V) + (y * x9)) + ((- 1) * y) is Element of the carrier of x
y is V11() V12() Element of K28()
y * V is Element of the carrier of x
y is V11() V12() Element of K28()
y * x9 is Element of the carrier of x
(y * V) + (y * x9) is Element of the carrier of x
dw is V11() V12() Element of K28()
dw * V is Element of the carrier of x
p is V11() V12() Element of K28()
p * x9 is Element of the carrier of x
(dw * V) + (p * x9) is Element of the carrier of x
x is non empty V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
the carrier of x is non empty set
V is Element of the carrier of x
x9 is V11() V12() Element of K28()
x9 * V is Element of the carrier of x
y is V11() V12() Element of K28()
x9 + y is V11() V12() Element of K28()
y * V is Element of the carrier of x
(x9 * V) + (y * V) is Element of the carrier of x
y is V11() V12() Element of K28()
(x9 + y) + y is V11() V12() Element of K28()
((x9 + y) + y) * V is Element of the carrier of x
y * V is Element of the carrier of x
((x9 * V) + (y * V)) + (y * V) is Element of the carrier of x
(x9 + y) * V is Element of the carrier of x
((x9 + y) * V) + (y * V) is Element of the carrier of x
x is non empty V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
the carrier of x is non empty set
V is Element of the carrier of x
x9 is Element of the carrier of x
V + x9 is Element of the carrier of x
y is Element of the carrier of x
(V + x9) + y is Element of the carrier of x
y is Element of the carrier of x
V + y is Element of the carrier of x
y is Element of the carrier of x
y + y is Element of the carrier of x
x9 + y is Element of the carrier of x
(V + y) + (x9 + y) is Element of the carrier of x
dw is Element of the carrier of x
(y + y) + dw is Element of the carrier of x
((V + x9) + y) + ((y + y) + dw) is Element of the carrier of x
y + dw is Element of the carrier of x
((V + y) + (x9 + y)) + (y + dw) is Element of the carrier of x
V + (x9 + y) is Element of the carrier of x
y + (V + (x9 + y)) is Element of the carrier of x
(y + (V + (x9 + y))) + (y + dw) is Element of the carrier of x
y + (V + x9) is Element of the carrier of x
y + (y + (V + x9)) is Element of the carrier of x
(y + (y + (V + x9))) + (y + dw) is Element of the carrier of x
(y + y) + (V + x9) is Element of the carrier of x
((y + y) + (V + x9)) + (y + dw) is Element of the carrier of x
(V + x9) + (y + dw) is Element of the carrier of x
(y + y) + ((V + x9) + (y + dw)) is Element of the carrier of x
dw + ((V + x9) + y) is Element of the carrier of x
(y + y) + (dw + ((V + x9) + y)) is Element of the carrier of x
x is non empty V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
the carrier of x is non empty set
V is Element of the carrier of x
x9 is Element of the carrier of x
y is V11() V12() Element of K28()
y is V11() V12() Element of K28()
y * y is V11() V12() Element of K28()
(y * y) * V is Element of the carrier of x
y * V is Element of the carrier of x
y is V11() V12() Element of K28()
y * y is V11() V12() Element of K28()
(y * y) * x9 is Element of the carrier of x
((y * y) * V) + ((y * y) * x9) is Element of the carrier of x
y * x9 is Element of the carrier of x
(y * V) + (y * x9) is Element of the carrier of x
y * ((y * V) + (y * x9)) is Element of the carrier of x
y * (y * V) is Element of the carrier of x
(y * (y * V)) + ((y * y) * x9) is Element of the carrier of x
y * (y * x9) is Element of the carrier of x
(y * (y * V)) + (y * (y * x9)) is Element of the carrier of x
x is non empty V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
the carrier of x is non empty set
V is Element of the carrier of x
x9 is Element of the carrier of x
y is V11() V12() Element of K28()
y * V is Element of the carrier of x
y is V11() V12() Element of K28()
y * x9 is Element of the carrier of x
(y * V) + (y * x9) is Element of the carrier of x
y is V11() V12() Element of K28()
y * V is Element of the carrier of x
dw is V11() V12() Element of K28()
dw * x9 is Element of the carrier of x
(y * V) + (dw * x9) is Element of the carrier of x
- (y * x9) is Element of the carrier of x
((y * V) + (dw * x9)) + (- (y * x9)) is Element of the carrier of x
(y * x9) + (- (y * x9)) is Element of the carrier of x
(y * V) + ((y * x9) + (- (y * x9))) is Element of the carrier of x
0. x is zero Element of the carrier of x
the ZeroF of x is Element of the carrier of x
(y * V) + (0. x) is Element of the carrier of x
(dw * x9) + (- (y * x9)) is Element of the carrier of x
((dw * x9) + (- (y * x9))) + (y * V) is Element of the carrier of x
(dw * x9) - (y * x9) is Element of the carrier of x
((dw * x9) - (y * x9)) + (y * V) is Element of the carrier of x
dw - y is V11() V12() Element of K28()
(dw - y) * x9 is Element of the carrier of x
((dw - y) * x9) + (y * V) is Element of the carrier of x
- (y * V) is Element of the carrier of x
(y * V) + (- (y * V)) is Element of the carrier of x
(y * V) + (- (y * V)) is Element of the carrier of x
((dw - y) * x9) + ((y * V) + (- (y * V))) is Element of the carrier of x
((dw - y) * x9) + (0. x) is Element of the carrier of x
(y * V) - (y * V) is Element of the carrier of x
y - y is V11() V12() Element of K28()
(y - y) * V is Element of the carrier of x
x is non empty V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
the carrier of x is non empty set
V is Element of the carrier of x
x9 is Element of the carrier of x
y is Element of the carrier of x
y is V11() V12() Element of K28()
y * x9 is Element of the carrier of x
V + (y * x9) is Element of the carrier of x
y is V11() V12() Element of K28()
y * x9 is Element of the carrier of x
y + (y * x9) is Element of the carrier of x
y - y is V11() V12() Element of K28()
(y - y) * x9 is Element of the carrier of x
((y - y) * x9) + V is Element of the carrier of x
- (y * x9) is Element of the carrier of x
(V + (y * x9)) + (- (y * x9)) is Element of the carrier of x
(y * x9) + (- (y * x9)) is Element of the carrier of x
y + ((y * x9) + (- (y * x9))) is Element of the carrier of x
0. x is zero Element of the carrier of x
the ZeroF of x is Element of the carrier of x
y + (0. x) is Element of the carrier of x
(y * x9) + (- (y * x9)) is Element of the carrier of x
V + ((y * x9) + (- (y * x9))) is Element of the carrier of x
(y * x9) - (y * x9) is Element of the carrier of x
V + ((y * x9) - (y * x9)) is Element of the carrier of x
V + ((y - y) * x9) is Element of the carrier of x
x is non empty V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
the carrier of x is non empty set
V is Element of the carrier of x
x9 is Element of the carrier of x
y is Element of the carrier of x
y is V11() V12() Element of K28()
y * V is Element of the carrier of x
y is V11() V12() Element of K28()
y * x9 is Element of the carrier of x
(y * V) + (y * x9) is Element of the carrier of x
dw is V11() V12() Element of K28()
dw * y is Element of the carrier of x
((y * V) + (y * x9)) + (dw * y) is Element of the carrier of x
p is V11() V12() Element of K28()
p * V is Element of the carrier of x
q is V11() V12() Element of K28()
q * x9 is Element of the carrier of x
(p * V) + (q * x9) is Element of the carrier of x
r is V11() V12() Element of K28()
r * y is Element of the carrier of x
((p * V) + (q * x9)) + (r * y) is Element of the carrier of x
y - p is V11() V12() Element of K28()
(y - p) * V is Element of the carrier of x
y - q is V11() V12() Element of K28()
(y - q) * x9 is Element of the carrier of x
((y - p) * V) + ((y - q) * x9) is Element of the carrier of x
dw - r is V11() V12() Element of K28()
(dw - r) * y is Element of the carrier of x
(((y - p) * V) + ((y - q) * x9)) + ((dw - r) * y) is Element of the carrier of x
0. x is zero Element of the carrier of x
the ZeroF of x is Element of the carrier of x
((dw - r) * y) + ((y * V) + (y * x9)) is Element of the carrier of x
((dw - r) * y) + (y * V) is Element of the carrier of x
(((dw - r) * y) + (y * V)) + (y * x9) is Element of the carrier of x
((y - q) * x9) + (((dw - r) * y) + (y * V)) is Element of the carrier of x
((y - q) * x9) + ((dw - r) * y) is Element of the carrier of x
(((y - q) * x9) + ((dw - r) * y)) + (y * V) is Element of the carrier of x
(0. x) + (p * V) is Element of the carrier of x
((y - p) * V) + (((y - q) * x9) + ((dw - r) * y)) is Element of the carrier of x
x is non empty V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
the carrier of x is non empty set
0. x is zero Element of the carrier of x
the ZeroF of x is Element of the carrier of x
V is Element of the carrier of x
x9 is Element of the carrier of x
y is Element of the carrier of x
y is Element of the carrier of x
y is V11() V12() Element of K28()
y * V is Element of the carrier of x
dw is V11() V12() Element of K28()
dw * x9 is Element of the carrier of x
(y * V) + (dw * x9) is Element of the carrier of x
p is V11() V12() Element of K28()
p * V is Element of the carrier of x
p * dw is V11() V12() Element of K28()
q is V11() V12() Element of K28()
q * x9 is Element of the carrier of x
(p * V) + (q * x9) is Element of the carrier of x
y * q is V11() V12() Element of K28()
(y * q) - (p * dw) is V11() V12() Element of K28()
r is Element of the carrier of x
r is Element of the carrier of x
r is Element of the carrier of x
a39 is Element of the carrier of x
b39 is V11() V12() Element of K28()
b39 * r is Element of the carrier of x
a1 is V11() V12() Element of K28()
a1 * r is Element of the carrier of x
b1 is V11() V12() Element of K28()
b1 * r is Element of the carrier of x
(b39 * r) + (b1 * r) is Element of the carrier of x
a1 * b1 is V11() V12() Element of K28()
a29 is V11() V12() Element of K28()
a29 * r is Element of the carrier of x
(a1 * r) + (a29 * r) is Element of the carrier of x
b39 * a29 is V11() V12() Element of K28()
(b39 * a29) - (a1 * b1) is V11() V12() Element of K28()
- a1 is V11() V12() Element of K28()
(- a1) * b1 is V11() V12() Element of K28()
0 * r is Element of the carrier of x
(0. x) + (0 * r) is Element of the carrier of x
(0. x) + (0. x) is Element of the carrier of x
b1 " is V11() V12() Element of K28()
a29 * (b1 ") is V11() V12() Element of K28()
(0. x) + (b1 * r) is Element of the carrier of x
(0. x) + (a29 * r) is Element of the carrier of x
(b1 ") * r is Element of the carrier of x
a29 * ((b1 ") * r) is Element of the carrier of x
(a29 * (b1 ")) * r is Element of the carrier of x
1 * a39 is Element of the carrier of x
y " is V11() V12() Element of K28()
p * (y ") is V11() V12() Element of K28()
(p * V) + (0. x) is Element of the carrier of x
(y * V) + (0. x) is Element of the carrier of x
(y ") * y is Element of the carrier of x
p * ((y ") * y) is Element of the carrier of x
(p * (y ")) * y is Element of the carrier of x
1 * y is Element of the carrier of x
q * y is Element of the carrier of x
(y * q) * V is Element of the carrier of x
q * dw is V11() V12() Element of K28()
(q * dw) * x9 is Element of the carrier of x
((y * q) * V) + ((q * dw) * x9) is Element of the carrier of x
dw * y is Element of the carrier of x
(p * dw) * V is Element of the carrier of x
dw * q is V11() V12() Element of K28()
(dw * q) * x9 is Element of the carrier of x
((p * dw) * V) + ((dw * q) * x9) is Element of the carrier of x
x is non empty V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
the carrier of x is non empty set
0. x is zero Element of the carrier of x
the ZeroF of x is Element of the carrier of x
V is Element of the carrier of x
x9 is Element of the carrier of x
y is Element of the carrier of x
y is Element of the carrier of x
y is Element of the carrier of x
dw is Element of the carrier of x
(0. x) + (0. x) is Element of the carrier of x
1 * y is Element of the carrier of x
(1 * y) + (0. x) is Element of the carrier of x
0 * y is Element of the carrier of x
(1 * y) + (0 * y) is Element of the carrier of x
((1 * y) + (0 * y)) + (0. x) is Element of the carrier of x
0 * dw is Element of the carrier of x
((1 * y) + (0 * y)) + (0 * dw) is Element of the carrier of x
x is non empty V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
the carrier of x is non empty set
V is Element of the carrier of x
x9 is Element of the carrier of x
y is Element of the carrier of x
y is Element of the carrier of x
y is Element of the carrier of x
dw is Element of the carrier of x
0 * dw is Element of the carrier of x
0. x is zero Element of the carrier of x
the ZeroF of x is Element of the carrier of x
p is V11() V12() Element of K28()
p * y is Element of the carrier of x
q is V11() V12() Element of K28()
q * y is Element of the carrier of x
- (q * y) is Element of the carrier of x
(p * y) + (- (q * y)) is Element of the carrier of x
(- 1) * (q * y) is Element of the carrier of x
(p * y) + ((- 1) * (q * y)) is Element of the carrier of x
(- 1) * q is V11() V12() Element of K28()
((- 1) * q) * y is Element of the carrier of x
(p * y) + (((- 1) * q) * y) is Element of the carrier of x
(0 * dw) + (p * y) is Element of the carrier of x
((0 * dw) + (p * y)) + (((- 1) * q) * y) is Element of the carrier of x
x is non empty V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
the carrier of x is non empty set
V is Element of the carrier of x
x9 is Element of the carrier of x
y is Element of the carrier of x
0. x is zero Element of the carrier of x
the ZeroF of x is Element of the carrier of x
x is non empty V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
the carrier of x is non empty set
0. x is zero Element of the carrier of x
the ZeroF of x is Element of the carrier of x
V is Element of the carrier of x
x9 is Element of the carrier of x
V + x9 is Element of the carrier of x
- V is Element of the carrier of x
(- 1) * V is Element of the carrier of x
x is non empty V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
the carrier of x is non empty set
V is Element of the carrier of x
x9 is Element of the carrier of x
y is Element of the carrier of x
y is Element of the carrier of x
y is Element of the carrier of x
dw is V11() V12() Element of K28()
dw * V is Element of the carrier of x
p is V11() V12() Element of K28()
p * x9 is Element of the carrier of x
(dw * V) + (p * x9) is Element of the carrier of x
q is V11() V12() Element of K28()
q * V is Element of the carrier of x
r is V11() V12() Element of K28()
r * x9 is Element of the carrier of x
(q * V) + (r * x9) is Element of the carrier of x
r is V11() V12() Element of K28()
r * V is Element of the carrier of x
r is V11() V12() Element of K28()
r * x9 is Element of the carrier of x
(r * V) + (r * x9) is Element of the carrier of x
r * r is V11() V12() Element of K28()
q * r is V11() V12() Element of K28()
(r * r) - (q * r) is V11() V12() Element of K28()
dw * r is V11() V12() Element of K28()
- (dw * r) is V11() V12() Element of K28()
q * p is V11() V12() Element of K28()
(- (dw * r)) + (q * p) is V11() V12() Element of K28()
dw * r is V11() V12() Element of K28()
r * p is V11() V12() Element of K28()
(dw * r) - (r * p) is V11() V12() Element of K28()
0. x is zero Element of the carrier of x
the ZeroF of x is Element of the carrier of x
(q * p) - (dw * r) is V11() V12() Element of K28()
((r * r) - (q * r)) * dw is V11() V12() Element of K28()
((- (dw * r)) + (q * p)) * r is V11() V12() Element of K28()
(((r * r) - (q * r)) * dw) + (((- (dw * r)) + (q * p)) * r) is V11() V12() Element of K28()
((dw * r) - (r * p)) * q is V11() V12() Element of K28()
((((r * r) - (q * r)) * dw) + (((- (dw * r)) + (q * p)) * r)) + (((dw * r) - (r * p)) * q) is V11() V12() Element of K28()
(((((r * r) - (q * r)) * dw) + (((- (dw * r)) + (q * p)) * r)) + (((dw * r) - (r * p)) * q)) * V is Element of the carrier of x
((r * r) - (q * r)) * p is V11() V12() Element of K28()
((- (dw * r)) + (q * p)) * r is V11() V12() Element of K28()
(((r * r) - (q * r)) * p) + (((- (dw * r)) + (q * p)) * r) is V11() V12() Element of K28()
((dw * r) - (r * p)) * r is V11() V12() Element of K28()
((((r * r) - (q * r)) * p) + (((- (dw * r)) + (q * p)) * r)) + (((dw * r) - (r * p)) * r) is V11() V12() Element of K28()
(((((r * r) - (q * r)) * p) + (((- (dw * r)) + (q * p)) * r)) + (((dw * r) - (r * p)) * r)) * x9 is Element of the carrier of x
((((((r * r) - (q * r)) * dw) + (((- (dw * r)) + (q * p)) * r)) + (((dw * r) - (r * p)) * q)) * V) + ((((((r * r) - (q * r)) * p) + (((- (dw * r)) + (q * p)) * r)) + (((dw * r) - (r * p)) * r)) * x9) is Element of the carrier of x
(((r * r) - (q * r)) * dw) * V is Element of the carrier of x
(((- (dw * r)) + (q * p)) * r) * V is Element of the carrier of x
((((r * r) - (q * r)) * dw) * V) + ((((- (dw * r)) + (q * p)) * r) * V) is Element of the carrier of x
(((dw * r) - (r * p)) * q) * V is Element of the carrier of x
(((((r * r) - (q * r)) * dw) * V) + ((((- (dw * r)) + (q * p)) * r) * V)) + ((((dw * r) - (r * p)) * q) * V) is Element of the carrier of x
(((r * r) - (q * r)) * p) * x9 is Element of the carrier of x
(((- (dw * r)) + (q * p)) * r) * x9 is Element of the carrier of x
((((r * r) - (q * r)) * p) * x9) + ((((- (dw * r)) + (q * p)) * r) * x9) is Element of the carrier of x
(((dw * r) - (r * p)) * r) * x9 is Element of the carrier of x
(((((r * r) - (q * r)) * p) * x9) + ((((- (dw * r)) + (q * p)) * r) * x9)) + ((((dw * r) - (r * p)) * r) * x9) is Element of the carrier of x
((((((r * r) - (q * r)) * dw) * V) + ((((- (dw * r)) + (q * p)) * r) * V)) + ((((dw * r) - (r * p)) * q) * V)) + ((((((r * r) - (q * r)) * p) * x9) + ((((- (dw * r)) + (q * p)) * r) * x9)) + ((((dw * r) - (r * p)) * r) * x9)) is Element of the carrier of x
((((r * r) - (q * r)) * dw) * V) + ((((r * r) - (q * r)) * p) * x9) is Element of the carrier of x
((((- (dw * r)) + (q * p)) * r) * V) + ((((- (dw * r)) + (q * p)) * r) * x9) is Element of the carrier of x
(((((r * r) - (q * r)) * dw) * V) + ((((r * r) - (q * r)) * p) * x9)) + (((((- (dw * r)) + (q * p)) * r) * V) + ((((- (dw * r)) + (q * p)) * r) * x9)) is Element of the carrier of x
((((dw * r) - (r * p)) * q) * V) + ((((dw * r) - (r * p)) * r) * x9) is Element of the carrier of x
((((((r * r) - (q * r)) * dw) * V) + ((((r * r) - (q * r)) * p) * x9)) + (((((- (dw * r)) + (q * p)) * r) * V) + ((((- (dw * r)) + (q * p)) * r) * x9))) + (((((dw * r) - (r * p)) * q) * V) + ((((dw * r) - (r * p)) * r) * x9)) is Element of the carrier of x
((dw * r) - (r * p)) * ((q * V) + (r * x9)) is Element of the carrier of x
((r * r) - (q * r)) * ((dw * V) + (p * x9)) is Element of the carrier of x
((- (dw * r)) + (q * p)) * ((r * V) + (r * x9)) is Element of the carrier of x
x is non empty V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
the carrier of x is non empty set
V is Element of the carrier of x
x9 is Element of the carrier of x
y is V11() V12() Element of K28()
y is V11() V12() Element of K28()
y * V is Element of the carrier of x
y * y is V11() V12() Element of K28()
(y * y) * V is Element of the carrier of x
y is V11() V12() Element of K28()
y * x9 is Element of the carrier of x
(y * V) + (y * x9) is Element of the carrier of x
y * ((y * V) + (y * x9)) is Element of the carrier of x
y * y is V11() V12() Element of K28()
(y * y) * x9 is Element of the carrier of x
((y * y) * V) + ((y * y) * x9) is Element of the carrier of x
y * (y * V) is Element of the carrier of x
(y * (y * V)) + ((y * y) * x9) is Element of the carrier of x
y * (y * x9) is Element of the carrier of x
(y * (y * V)) + (y * (y * x9)) is Element of the carrier of x
x is non empty V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
the carrier of x is non empty set
V is Element of the carrier of x
x9 is Element of the carrier of x
y is Element of the carrier of x
y is Element of the carrier of x
y is Element of the carrier of x
0. x is zero Element of the carrier of x
the ZeroF of x is Element of the carrier of x
dw is Element of the carrier of x
p is Element of the carrier of x
q is Element of the carrier of x
dw is V11() V12() Element of K28()
dw * V is Element of the carrier of x
p is V11() V12() Element of K28()
p * x9 is Element of the carrier of x
(dw * V) + (p * x9) is Element of the carrier of x
q is V11() V12() Element of K28()
q * x9 is Element of the carrier of x
r is V11() V12() Element of K28()
r * y is Element of the carrier of x
(q * x9) + (r * y) is Element of the carrier of x
r is V11() V12() Element of K28()
r * y is Element of the carrier of x
r * dw is V11() V12() Element of K28()
(r * dw) * V is Element of the carrier of x
r * p is V11() V12() Element of K28()
r is V11() V12() Element of K28()
r * y is Element of the carrier of x
(r * y) + (r * y) is Element of the carrier of x
r * q is V11() V12() Element of K28()
(r * p) + (r * q) is V11() V12() Element of K28()
((r * p) + (r * q)) * x9 is Element of the carrier of x
((r * dw) * V) + (((r * p) + (r * q)) * x9) is Element of the carrier of x
r * r is V11() V12() Element of K28()
(r * r) * y is Element of the carrier of x
(((r * dw) * V) + (((r * p) + (r * q)) * x9)) + ((r * r) * y) is Element of the carrier of x
(r * p) * x9 is Element of the carrier of x
((r * dw) * V) + ((r * p) * x9) is Element of the carrier of x
r * ((q * x9) + (r * y)) is Element of the carrier of x
(((r * dw) * V) + ((r * p) * x9)) + (r * ((q * x9) + (r * y))) is Element of the carrier of x
(r * q) * x9 is Element of the carrier of x
((r * q) * x9) + ((r * r) * y) is Element of the carrier of x
(((r * dw) * V) + ((r * p) * x9)) + (((r * q) * x9) + ((r * r) * y)) is Element of the carrier of x
(((r * dw) * V) + ((r * p) * x9)) + ((r * q) * x9) is Element of the carrier of x
((((r * dw) * V) + ((r * p) * x9)) + ((r * q) * x9)) + ((r * r) * y) is Element of the carrier of x
((r * p) * x9) + ((r * q) * x9) is Element of the carrier of x
((r * dw) * V) + (((r * p) * x9) + ((r * q) * x9)) is Element of the carrier of x
(((r * dw) * V) + (((r * p) * x9) + ((r * q) * x9))) + ((r * r) * y) is Element of the carrier of x
q " is V11() V12() Element of K28()
p * (q ") is V11() V12() Element of K28()
- (p * (q ")) is V11() V12() Element of K28()
1 * y is Element of the carrier of x
(- (p * (q "))) * y is Element of the carrier of x
(1 * y) + ((- (p * (q "))) * y) is Element of the carrier of x
- y is Element of the carrier of x
(p * (q ")) * (- y) is Element of the carrier of x
(1 * y) + ((p * (q ")) * (- y)) is Element of the carrier of x
(p * (q ")) * y is Element of the carrier of x
- ((p * (q ")) * y) is Element of the carrier of x
(1 * y) + (- ((p * (q ")) * y)) is Element of the carrier of x
- (1 * y) is Element of the carrier of x
1 * p is V11() V12() Element of K28()
(- (p * (q "))) * q is V11() V12() Element of K28()
(1 * p) + ((- (p * (q "))) * q) is V11() V12() Element of K28()
- p is V11() V12() Element of K28()
(q ") * q is V11() V12() Element of K28()
(- p) * ((q ") * q) is V11() V12() Element of K28()
p + ((- p) * ((q ") * q)) is V11() V12() Element of K28()
(- p) * 1 is V11() V12() Element of K28()
p + ((- p) * 1) is V11() V12() Element of K28()
1 * dw is V11() V12() Element of K28()
(1 * dw) * V is Element of the carrier of x
0 * x9 is Element of the carrier of x
((1 * dw) * V) + (0 * x9) is Element of the carrier of x
(- (p * (q "))) * r is V11() V12() Element of K28()
((- (p * (q "))) * r) * y is Element of the carrier of x
(((1 * dw) * V) + (0 * x9)) + (((- (p * (q "))) * r) * y) is Element of the carrier of x
((1 * dw) * V) + (0. x) is Element of the carrier of x
(((1 * dw) * V) + (0. x)) + (((- (p * (q "))) * r) * y) is Element of the carrier of x
((1 * dw) * V) + (((- (p * (q "))) * r) * y) is Element of the carrier of x
0 * y is Element of the carrier of x
1 * y is Element of the carrier of x
(0 * y) + (1 * y) is Element of the carrier of x
(0. x) + (1 * y) is Element of the carrier of x
(0. x) + y is Element of the carrier of x
0 * p is V11() V12() Element of K28()
1 * q is V11() V12() Element of K28()
(0 * p) + (1 * q) is V11() V12() Element of K28()
0 * dw is V11() V12() Element of K28()
(0 * dw) * V is Element of the carrier of x
((0 * dw) * V) + (0 * x9) is Element of the carrier of x
1 * r is V11() V12() Element of K28()
(1 * r) * y is Element of the carrier of x
(((0 * dw) * V) + (0 * x9)) + ((1 * r) * y) is Element of the carrier of x
((0 * dw) * V) + (0. x) is Element of the carrier of x
(((0 * dw) * V) + (0. x)) + ((1 * r) * y) is Element of the carrier of x
((0 * dw) * V) + ((1 * r) * y) is Element of the carrier of x
r is Element of the carrier of x
r is Element of the carrier of x
0 * y is Element of the carrier of x
(1 * y) + (0 * y) is Element of the carrier of x
y + (0 * y) is Element of the carrier of x
y + (0. x) is Element of the carrier of x
0 * q is V11() V12() Element of K28()
(1 * p) + (0 * q) is V11() V12() Element of K28()
0 * r is V11() V12() Element of K28()
(0 * r) * y is Element of the carrier of x
(((1 * dw) * V) + (0 * x9)) + ((0 * r) * y) is Element of the carrier of x
(((1 * dw) * V) + (0. x)) + ((0 * r) * y) is Element of the carrier of x
((1 * dw) * V) + ((0 * r) * y) is Element of the carrier of x
r is Element of the carrier of x
r is Element of the carrier of x
r is Element of the carrier of x
a39 is Element of the carrier of x
x is non empty V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
the carrier of x is non empty set
V is Element of the carrier of x
x9 is Element of the carrier of x
y is Element of the carrier of x
y is Element of the carrier of x
0. x is zero Element of the carrier of x
the ZeroF of x is Element of the carrier of x
y + y is Element of the carrier of x
1 * y is Element of the carrier of x
1 * y is Element of the carrier of x
(1 * y) + (1 * y) is Element of the carrier of x
(- 1) * (y + y) is Element of the carrier of x
((1 * y) + (1 * y)) + ((- 1) * (y + y)) is Element of the carrier of x
y + (1 * y) is Element of the carrier of x
(y + (1 * y)) + ((- 1) * (y + y)) is Element of the carrier of x
(y + y) + ((- 1) * (y + y)) is Element of the carrier of x
- (y + y) is Element of the carrier of x
(y + y) + (- (y + y)) is Element of the carrier of x
y + y is Element of the carrier of x
- y is Element of the carrier of x
- y is Element of the carrier of x
(- y) + (- y) is Element of the carrier of x
(y + y) + ((- y) + (- y)) is Element of the carrier of x
y + ((- y) + (- y)) is Element of the carrier of x
y + (y + ((- y) + (- y))) is Element of the carrier of x
y + (- y) is Element of the carrier of x
(y + (- y)) + (- y) is Element of the carrier of x
y + ((y + (- y)) + (- y)) is Element of the carrier of x
(0. x) + (- y) is Element of the carrier of x
y + ((0. x) + (- y)) is Element of the carrier of x
y + (- y) is Element of the carrier of x
dw is V11() V12() Element of K28()
dw * y is Element of the carrier of x
p is V11() V12() Element of K28()
p * (y + y) is Element of the carrier of x
p * y is Element of the carrier of x
- (p * y) is Element of the carrier of x
(- (p * y)) + (dw * y) is Element of the carrier of x
p * y is Element of the carrier of x
(p * y) + (p * y) is Element of the carrier of x
(- (p * y)) + ((p * y) + (p * y)) is Element of the carrier of x
(p * y) + (- (p * y)) is Element of the carrier of x
((p * y) + (- (p * y))) + (p * y) is Element of the carrier of x
(0. x) + (p * y) is Element of the carrier of x
p * (- y) is Element of the carrier of x
(dw * y) + (p * (- y)) is Element of the carrier of x
- p is V11() V12() Element of K28()
(- p) * y is Element of the carrier of x
(dw * y) + ((- p) * y) is Element of the carrier of x
dw + (- p) is V11() V12() Element of K28()
(dw + (- p)) * y is Element of the carrier of x
dw is V11() V12() Element of K28()
dw * y is Element of the carrier of x
p is V11() V12() Element of K28()
p * (y + y) is Element of the carrier of x
p * y is Element of the carrier of x
- (p * y) is Element of the carrier of x
(dw * y) + (- (p * y)) is Element of the carrier of x
p * y is Element of the carrier of x
(p * y) + (p * y) is Element of the carrier of x
((p * y) + (p * y)) + (- (p * y)) is Element of the carrier of x
(p * y) + (- (p * y)) is Element of the carrier of x
(p * y) + ((p * y) + (- (p * y))) is Element of the carrier of x
(p * y) + (0. x) is Element of the carrier of x
p * (- y) is Element of the carrier of x
(dw * y) + (p * (- y)) is Element of the carrier of x
- p is V11() V12() Element of K28()
(- p) * y is Element of the carrier of x
(dw * y) + ((- p) * y) is Element of the carrier of x
dw + (- p) is V11() V12() Element of K28()
(dw + (- p)) * y is Element of the carrier of x
y is Element of the carrier of x
dw is Element of the carrier of x
p is Element of the carrier of x
x is non empty V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
the carrier of x is non empty set
V is Element of the carrier of x
x9 is Element of the carrier of x
y is Element of the carrier of x
y is Element of the carrier of x
y is Element of the carrier of x
x is non empty V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
the carrier of x is non empty set
V is Element of the carrier of x
x9 is Element of the carrier of x
y is Element of the carrier of x
y is Element of the carrier of x
y is Element of the carrier of x
dw is Element of the carrier of x
x is non empty V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
the carrier of x is non empty set
V is Element of the carrier of x
x9 is Element of the carrier of x
y is Element of the carrier of x
y is V11() V12() Element of K28()
y * V is Element of the carrier of x
y is V11() V12() Element of K28()
y * x9 is Element of the carrier of x
(y * V) + (y * x9) is Element of the carrier of x
dw is V11() V12() Element of K28()
dw * x9 is Element of the carrier of x
p is V11() V12() Element of K28()
p * y is Element of the carrier of x
(dw * x9) + (p * y) is Element of the carrier of x
q is V11() V12() Element of K28()
q * V is Element of the carrier of x
r is V11() V12() Element of K28()
r * y is Element of the carrier of x
(q * V) + (r * y) is Element of the carrier of x
r is V11() V12() Element of K28()
r * ((y * V) + (y * x9)) is Element of the carrier of x
r is V11() V12() Element of K28()
r * ((dw * x9) + (p * y)) is Element of the carrier of x
(r * ((y * V) + (y * x9))) + (r * ((dw * x9) + (p * y))) is Element of the carrier of x
a39 is V11() V12() Element of K28()
a39 * ((q * V) + (r * y)) is Element of the carrier of x
((r * ((y * V) + (y * x9))) + (r * ((dw * x9) + (p * y)))) + (a39 * ((q * V) + (r * y))) is Element of the carrier of x
r * y is V11() V12() Element of K28()
a39 * q is V11() V12() Element of K28()
(r * y) + (a39 * q) is V11() V12() Element of K28()
((r * y) + (a39 * q)) * V is Element of the carrier of x
r * y is V11() V12() Element of K28()
r * dw is V11() V12() Element of K28()
(r * y) + (r * dw) is V11() V12() Element of K28()
((r * y) + (r * dw)) * x9 is Element of the carrier of x
(((r * y) + (a39 * q)) * V) + (((r * y) + (r * dw)) * x9) is Element of the carrier of x
r * p is V11() V12() Element of K28()
a39 * r is V11() V12() Element of K28()
(r * p) + (a39 * r) is V11() V12() Element of K28()
((r * p) + (a39 * r)) * y is Element of the carrier of x
((((r * y) + (a39 * q)) * V) + (((r * y) + (r * dw)) * x9)) + (((r * p) + (a39 * r)) * y) is Element of the carrier of x
(a39 * q) * V is Element of the carrier of x
(a39 * r) * y is Element of the carrier of x
((a39 * q) * V) + ((a39 * r) * y) is Element of the carrier of x
(r * y) * V is Element of the carrier of x
(r * y) * x9 is Element of the carrier of x
((r * y) * V) + ((r * y) * x9) is Element of the carrier of x
(r * dw) * x9 is Element of the carrier of x
(r * p) * y is Element of the carrier of x
((r * dw) * x9) + ((r * p) * y) is Element of the carrier of x
(((r * y) * V) + ((r * y) * x9)) + ((r * dw) * x9) is Element of the carrier of x
((((r * y) * V) + ((r * y) * x9)) + ((r * dw) * x9)) + ((r * p) * y) is Element of the carrier of x
(((((r * y) * V) + ((r * y) * x9)) + ((r * dw) * x9)) + ((r * p) * y)) + (((a39 * q) * V) + ((a39 * r) * y)) is Element of the carrier of x
((r * y) * x9) + ((r * dw) * x9) is Element of the carrier of x
((r * y) * V) + (((r * y) * x9) + ((r * dw) * x9)) is Element of the carrier of x
(((r * y) * V) + (((r * y) * x9) + ((r * dw) * x9))) + ((r * p) * y) is Element of the carrier of x
((((r * y) * V) + (((r * y) * x9) + ((r * dw) * x9))) + ((r * p) * y)) + (((a39 * q) * V) + ((a39 * r) * y)) is Element of the carrier of x
((r * y) * V) + (((r * y) + (r * dw)) * x9) is Element of the carrier of x
(((r * y) * V) + (((r * y) + (r * dw)) * x9)) + ((r * p) * y) is Element of the carrier of x
((((r * y) * V) + (((r * y) + (r * dw)) * x9)) + ((r * p) * y)) + (((a39 * q) * V) + ((a39 * r) * y)) is Element of the carrier of x
((a39 * r) * y) + ((a39 * q) * V) is Element of the carrier of x
((r * p) * y) + (((a39 * r) * y) + ((a39 * q) * V)) is Element of the carrier of x
(((r * y) * V) + (((r * y) + (r * dw)) * x9)) + (((r * p) * y) + (((a39 * r) * y) + ((a39 * q) * V))) is Element of the carrier of x
((r * p) * y) + ((a39 * r) * y) is Element of the carrier of x
(((r * p) * y) + ((a39 * r) * y)) + ((a39 * q) * V) is Element of the carrier of x
(((r * y) * V) + (((r * y) + (r * dw)) * x9)) + ((((r * p) * y) + ((a39 * r) * y)) + ((a39 * q) * V)) is Element of the carrier of x
(((r * p) + (a39 * r)) * y) + ((a39 * q) * V) is Element of the carrier of x
(((r * y) * V) + (((r * y) + (r * dw)) * x9)) + ((((r * p) + (a39 * r)) * y) + ((a39 * q) * V)) is Element of the carrier of x
(((r * y) + (r * dw)) * x9) + ((((r * p) + (a39 * r)) * y) + ((a39 * q) * V)) is Element of the carrier of x
((r * y) * V) + ((((r * y) + (r * dw)) * x9) + ((((r * p) + (a39 * r)) * y) + ((a39 * q) * V))) is Element of the carrier of x
(((r * y) + (r * dw)) * x9) + (((r * p) + (a39 * r)) * y) is Element of the carrier of x
((a39 * q) * V) + ((((r * y) + (r * dw)) * x9) + (((r * p) + (a39 * r)) * y)) is Element of the carrier of x
((r * y) * V) + (((a39 * q) * V) + ((((r * y) + (r * dw)) * x9) + (((r * p) + (a39 * r)) * y))) is Element of the carrier of x
((r * y) * V) + ((a39 * q) * V) is Element of the carrier of x
(((r * y) * V) + ((a39 * q) * V)) + ((((r * y) + (r * dw)) * x9) + (((r * p) + (a39 * r)) * y)) is Element of the carrier of x
(((r * y) + (a39 * q)) * V) + ((((r * y) + (r * dw)) * x9) + (((r * p) + (a39 * r)) * y)) is Element of the carrier of x
x is non empty V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
the carrier of x is non empty set
V is Element of the carrier of x
x9 is Element of the carrier of x
y is Element of the carrier of x
y is Element of the carrier of x
y is Element of the carrier of x
dw is Element of the carrier of x
p is Element of the carrier of x
q is V11() V12() Element of K28()
q * x9 is Element of the carrier of x
r is V11() V12() Element of K28()
r * y is Element of the carrier of x
(q * x9) + (r * y) is Element of the carrier of x
r is V11() V12() Element of K28()
r * V is Element of the carrier of x
r is V11() V12() Element of K28()
r * x9 is Element of the carrier of x
(r * V) + (r * x9) is Element of the carrier of x
a39 is V11() V12() Element of K28()
a39 * x9 is Element of the carrier of x
b39 is V11() V12() Element of K28()
b39 * y is Element of the carrier of x
(a39 * x9) + (b39 * y) is Element of the carrier of x
a1 is V11() V12() Element of K28()
a1 * V is Element of the carrier of x
b1 is V11() V12() Element of K28()
b1 * y is Element of the carrier of x
(a1 * V) + (b1 * y) is Element of the carrier of x
a29 is V11() V12() Element of K28()
a29 * y is Element of the carrier of x
b29 is V11() V12() Element of K28()
b29 * y is Element of the carrier of x
(a29 * y) + (b29 * y) is Element of the carrier of x
a3 is V11() V12() Element of K28()
a3 * V is Element of the carrier of x
b3 is V11() V12() Element of K28()
b3 * y is Element of the carrier of x
(a3 * V) + (b3 * y) is Element of the carrier of x
0. x is zero Element of the carrier of x
the ZeroF of x is Element of the carrier of x
A is V11() V12() Element of K28()
A * dw is Element of the carrier of x
B is V11() V12() Element of K28()
B * y is Element of the carrier of x
(A * dw) + (B * y) is Element of the carrier of x
C is V11() V12() Element of K28()
C * p is Element of the carrier of x
((A * dw) + (B * y)) + (C * p) is Element of the carrier of x
A * a1 is V11() V12() Element of K28()
C * a3 is V11() V12() Element of K28()
(A * a1) + (C * a3) is V11() V12() Element of K28()
((A * a1) + (C * a3)) * V is Element of the carrier of x
A * b1 is V11() V12() Element of K28()
B * a29 is V11() V12() Element of K28()
(A * b1) + (B * a29) is V11() V12() Element of K28()
((A * b1) + (B * a29)) * y is Element of the carrier of x
(((A * a1) + (C * a3)) * V) + (((A * b1) + (B * a29)) * y) is Element of the carrier of x
B * b29 is V11() V12() Element of K28()
C * b3 is V11() V12() Element of K28()
(B * b29) + (C * b3) is V11() V12() Element of K28()
((B * b29) + (C * b3)) * y is Element of the carrier of x
((((A * a1) + (C * a3)) * V) + (((A * b1) + (B * a29)) * y)) + (((B * b29) + (C * b3)) * y) is Element of the carrier of x
C * ((a39 * x9) + (b39 * y)) is Element of the carrier of x
B * ((a29 * y) + (b29 * y)) is Element of the carrier of x
(C * ((a39 * x9) + (b39 * y))) + (B * ((a29 * y) + (b29 * y))) is Element of the carrier of x
A * ((q * x9) + (r * y)) is Element of the carrier of x
((C * ((a39 * x9) + (b39 * y))) + (B * ((a29 * y) + (b29 * y)))) + (A * ((q * x9) + (r * y))) is Element of the carrier of x
C * a39 is V11() V12() Element of K28()
A * q is V11() V12() Element of K28()
(C * a39) + (A * q) is V11() V12() Element of K28()
((C * a39) + (A * q)) * x9 is Element of the carrier of x
C * b39 is V11() V12() Element of K28()
(C * b39) + (B * a29) is V11() V12() Element of K28()
((C * b39) + (B * a29)) * y is Element of the carrier of x
(((C * a39) + (A * q)) * x9) + (((C * b39) + (B * a29)) * y) is Element of the carrier of x
A * r is V11() V12() Element of K28()
(B * b29) + (A * r) is V11() V12() Element of K28()
((B * b29) + (A * r)) * y is Element of the carrier of x
((((C * a39) + (A * q)) * x9) + (((C * b39) + (B * a29)) * y)) + (((B * b29) + (A * r)) * y) is Element of the carrier of x
B * r is V11() V12() Element of K28()
(B * r) + (C * a3) is V11() V12() Element of K28()
((B * r) + (C * a3)) * V is Element of the carrier of x
B * r is V11() V12() Element of K28()
(B * r) + (A * q) is V11() V12() Element of K28()
((B * r) + (A * q)) * x9 is Element of the carrier of x
(((B * r) + (C * a3)) * V) + (((B * r) + (A * q)) * x9) is Element of the carrier of x
(A * r) + (C * b3) is V11() V12() Element of K28()
((A * r) + (C * b3)) * y is Element of the carrier of x
((((B * r) + (C * a3)) * V) + (((B * r) + (A * q)) * x9)) + (((A * r) + (C * b3)) * y) is Element of the carrier of x
(B * r) + (A * a1) is V11() V12() Element of K28()
((B * r) + (A * a1)) * V is Element of the carrier of x
(B * r) + (C * a39) is V11() V12() Element of K28()
((B * r) + (C * a39)) * x9 is Element of the carrier of x
(((B * r) + (A * a1)) * V) + (((B * r) + (C * a39)) * x9) is Element of the carrier of x
(C * b39) + (A * b1) is V11() V12() Element of K28()
((C * b39) + (A * b1)) * y is Element of the carrier of x
((((B * r) + (A * a1)) * V) + (((B * r) + (C * a39)) * x9)) + (((C * b39) + (A * b1)) * y) is Element of the carrier of x
0 * V is Element of the carrier of x
0 * y is Element of the carrier of x
(0 * V) + (0 * y) is Element of the carrier of x
(0. x) + (0 * y) is Element of the carrier of x
(0. x) + (0. x) is Element of the carrier of x
0 * x9 is Element of the carrier of x
(0 * V) + (0 * x9) is Element of the carrier of x
(0. x) + (0 * x9) is Element of the carrier of x
0 * y is Element of the carrier of x
(0 * V) + (0 * y) is Element of the carrier of x
(0. x) + (0 * y) is Element of the carrier of x
x is non empty V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
NonZero x is Element of bool the carrier of x
the carrier of x is non empty set
bool the carrier of x is set
[#] x is non empty non proper Element of bool the carrier of x
0. x is zero Element of the carrier of x
the ZeroF of x is Element of the carrier of x
{(0. x)} is set
([#] x) \ {(0. x)} is Element of bool the carrier of x
[:(NonZero x),(NonZero x):] is set
bool [:(NonZero x),(NonZero x):] is set
V is set
V is set
y is Element of the carrier of x
x9 is set
y is Element of the carrier of x
V is set
y is Element of the carrier of x
x9 is set
y is Element of the carrier of x
dw is Element of the carrier of x
y is set
p is Element of the carrier of x
V is V16() V19( NonZero x) V20( NonZero x) V23() V28() V34( NonZero x) Element of bool [:(NonZero x),(NonZero x):]
x9 is set
y is set
[x9,y] is V35() set
y is set
y is set
dw is Element of the carrier of x
p is Element of the carrier of x
[y,y] is V35() set
V is V16() V19( NonZero x) V20( NonZero x) V23() V28() V34( NonZero x) Element of bool [:(NonZero x),(NonZero x):]
x9 is V16() V19( NonZero x) V20( NonZero x) V23() V28() V34( NonZero x) Element of bool [:(NonZero x),(NonZero x):]
y is set
y is set
[y,y] is V35() set
y is Element of the carrier of x
dw is Element of the carrier of x
y is Element of the carrier of x
dw is Element of the carrier of x
x is non empty V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
(x) is V16() V19( NonZero x) V20( NonZero x) V23() V28() V34( NonZero x) Element of bool [:(NonZero x),(NonZero x):]
NonZero x is Element of bool the carrier of x
the carrier of x is non empty set
bool the carrier of x is set
[#] x is non empty non proper Element of bool the carrier of x
0. x is zero Element of the carrier of x
the ZeroF of x is Element of the carrier of x
{(0. x)} is set
([#] x) \ {(0. x)} is Element of bool the carrier of x
[:(NonZero x),(NonZero x):] is set
bool [:(NonZero x),(NonZero x):] is set
V is set
x9 is set
[V,x9] is V35() set
y is Element of the carrier of x
dw is Element of the carrier of x
y is Element of the carrier of x
y is Element of the carrier of x
x is non empty V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
the carrier of x is non empty set
(x) is V16() V19( NonZero x) V20( NonZero x) V23() V28() V34( NonZero x) Element of bool [:(NonZero x),(NonZero x):]
NonZero x is Element of bool the carrier of x
bool the carrier of x is set
[#] x is non empty non proper Element of bool the carrier of x
0. x is zero Element of the carrier of x
the ZeroF of x is Element of the carrier of x
{(0. x)} is set
([#] x) \ {(0. x)} is Element of bool the carrier of x
[:(NonZero x),(NonZero x):] is set
bool [:(NonZero x),(NonZero x):] is set
V is Element of the carrier of x
x9 is Element of the carrier of x
[V,x9] is V35() set
y is Element of the carrier of x
y is Element of the carrier of x
x is non empty V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
the carrier of x is non empty set
NonZero x is Element of bool the carrier of x
bool the carrier of x is set
[#] x is non empty non proper Element of bool the carrier of x
0. x is zero Element of the carrier of x
the ZeroF of x is Element of the carrier of x
{(0. x)} is set
([#] x) \ {(0. x)} is Element of bool the carrier of x
(x) is V16() V19( NonZero x) V20( NonZero x) V23() V28() V34( NonZero x) Element of bool [:(NonZero x),(NonZero x):]
[:(NonZero x),(NonZero x):] is set
bool [:(NonZero x),(NonZero x):] is set
V is Element of the carrier of x
Class ((x),V) is Element of bool (NonZero x)
bool (NonZero x) is set
x is non empty V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
NonZero x is Element of bool the carrier of x
the carrier of x is non empty set
bool the carrier of x is set
[#] x is non empty non proper Element of bool the carrier of x
0. x is zero Element of the carrier of x
the ZeroF of x is Element of the carrier of x
{(0. x)} is set
([#] x) \ {(0. x)} is Element of bool the carrier of x
bool (NonZero x) is set
bool (bool (NonZero x)) is set
(x) is V16() V19( NonZero x) V20( NonZero x) V23() V28() V34( NonZero x) Element of bool [:(NonZero x),(NonZero x):]
[:(NonZero x),(NonZero x):] is set
bool [:(NonZero x),(NonZero x):] is set
Class (x) is a_partition of NonZero x
y is Element of bool (bool (NonZero x))
V is set
y is Element of bool (bool (NonZero x))
x9 is set
x is non empty V79() V80() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
the carrier of x is non empty set
V is Element of the carrier of x
x9 is Element of the carrier of x
0. x is zero Element of the carrier of x
the ZeroF of x is Element of the carrier of x
x is non empty V79() V80() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
the carrier of x is non empty set
0. x is zero Element of the carrier of x
the ZeroF of x is Element of the carrier of x
V is Element of the carrier of x
x9 is Element of the carrier of x
V is Element of the carrier of x
x9 is Element of the carrier of x
(0. x) + (0. x) is Element of the carrier of x
1 * V is Element of the carrier of x
(1 * V) + (0. x) is Element of the carrier of x
0 * x9 is Element of the carrier of x
(1 * V) + (0 * x9) is Element of the carrier of x
x is non empty non trivial V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
(x) is set
the carrier of x is non empty non trivial set
0. x is zero Element of the carrier of x
the ZeroF of x is Element of the carrier of x
V is Element of the carrier of x
(x,V) is Element of bool (NonZero x)
NonZero x is non empty Element of bool the carrier of x
bool the carrier of x is set
[#] x is non empty non proper Element of bool the carrier of x
{(0. x)} is set
([#] x) \ {(0. x)} is Element of bool the carrier of x
bool (NonZero x) is set
(x) is V16() V19( NonZero x) V20( NonZero x) V23() V28() V34( NonZero x) Element of bool [:(NonZero x),(NonZero x):]
[:(NonZero x),(NonZero x):] is set
bool [:(NonZero x),(NonZero x):] is set
Class ((x),V) is Element of bool (NonZero x)
bool (bool (NonZero x)) is set
Class (x) is a_partition of NonZero x
y is Element of bool (bool (NonZero x))
x is non empty non trivial V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
the carrier of x is non empty non trivial set
(x) is non empty set
V is Element of the carrier of x
(x,V) is Element of bool (NonZero x)
NonZero x is non empty Element of bool the carrier of x
bool the carrier of x is set
[#] x is non empty non proper Element of bool the carrier of x
0. x is zero Element of the carrier of x
the ZeroF of x is Element of the carrier of x
{(0. x)} is set
([#] x) \ {(0. x)} is Element of bool the carrier of x
bool (NonZero x) is set
(x) is V16() V19( NonZero x) V20( NonZero x) V23() V28() V34( NonZero x) Element of bool [:(NonZero x),(NonZero x):]
[:(NonZero x),(NonZero x):] is set
bool [:(NonZero x),(NonZero x):] is set
Class ((x),V) is Element of bool (NonZero x)
Class (x) is a_partition of NonZero x
x is non empty non trivial V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
the carrier of x is non empty non trivial set
V is Element of the carrier of x
(x,V) is Element of bool (NonZero x)
NonZero x is non empty Element of bool the carrier of x
bool the carrier of x is set
[#] x is non empty non proper Element of bool the carrier of x
0. x is zero Element of the carrier of x
the ZeroF of x is Element of the carrier of x
{(0. x)} is set
([#] x) \ {(0. x)} is Element of bool the carrier of x
bool (NonZero x) is set
(x) is V16() V19( NonZero x) V20( NonZero x) V23() V28() V34( NonZero x) Element of bool [:(NonZero x),(NonZero x):]
[:(NonZero x),(NonZero x):] is set
bool [:(NonZero x),(NonZero x):] is set
Class ((x),V) is Element of bool (NonZero x)
x9 is Element of the carrier of x
(x,x9) is Element of bool (NonZero x)
Class ((x),x9) is Element of bool (NonZero x)
[V,x9] is V35() set
x is non empty non trivial V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
(x) is non empty set
the carrier of x is non empty non trivial set
[:(x),(x),(x):] is set
y is set
y is set
y is Relation3 of (x)
y is set
dw is set
p is set
[y,dw,p] is V35() V36() set
[y,dw] is V35() set
[[y,dw],p] is V35() set
r is Element of the carrier of x
(x,r) is Element of bool (NonZero x)
NonZero x is non empty Element of bool the carrier of x
bool the carrier of x is set
[#] x is non empty non proper Element of bool the carrier of x
0. x is zero Element of the carrier of x
the ZeroF of x is Element of the carrier of x
{(0. x)} is set
([#] x) \ {(0. x)} is Element of bool the carrier of x
bool (NonZero x) is set
(x) is V16() V19( NonZero x) V20( NonZero x) V23() V28() V34( NonZero x) Element of bool [:(NonZero x),(NonZero x):]
[:(NonZero x),(NonZero x):] is set
bool [:(NonZero x),(NonZero x):] is set
Class ((x),r) is Element of bool (NonZero x)
r is Element of the carrier of x
(x,r) is Element of bool (NonZero x)
Class ((x),r) is Element of bool (NonZero x)
r is Element of the carrier of x
(x,r) is Element of bool (NonZero x)
Class ((x),r) is Element of bool (NonZero x)
q is Element of the carrier of x
(x,q) is Element of bool (NonZero x)
Class ((x),q) is Element of bool (NonZero x)
r is Element of the carrier of x
(x,r) is Element of bool (NonZero x)
Class ((x),r) is Element of bool (NonZero x)
r is Element of the carrier of x
(x,r) is Element of bool (NonZero x)
Class ((x),r) is Element of bool (NonZero x)
[(x,q),(x,r),(x,r)] is V35() V36() set
[(x,q),(x,r)] is V35() set
[[(x,q),(x,r)],(x,r)] is V35() set
q is Element of the carrier of x
(x,q) is Element of bool (NonZero x)
Class ((x),q) is Element of bool (NonZero x)
r is Element of the carrier of x
(x,r) is Element of bool (NonZero x)
Class ((x),r) is Element of bool (NonZero x)
r is Element of the carrier of x
(x,r) is Element of bool (NonZero x)
Class ((x),r) is Element of bool (NonZero x)
r is Element of the carrier of x
(x,r) is Element of bool (NonZero x)
Class ((x),r) is Element of bool (NonZero x)
a39 is Element of the carrier of x
(x,a39) is Element of bool (NonZero x)
Class ((x),a39) is Element of bool (NonZero x)
b39 is Element of the carrier of x
(x,b39) is Element of bool (NonZero x)
Class ((x),b39) is Element of bool (NonZero x)
[:(x),(x),(x):] is set
y is Relation3 of (x)
y is Relation3 of (x)
y is set
dw is Element of (x)
p is Element of (x)
q is Element of (x)
[dw,p,q] is V35() V36() set
[dw,p] is V35() set
[[dw,p],q] is V35() set
r is Element of the carrier of x
(x,r) is Element of bool (NonZero x)
NonZero x is non empty Element of bool the carrier of x
bool the carrier of x is set
[#] x is non empty non proper Element of bool the carrier of x
0. x is zero Element of the carrier of x
the ZeroF of x is Element of the carrier of x
{(0. x)} is set
([#] x) \ {(0. x)} is Element of bool the carrier of x
bool (NonZero x) is set
(x) is V16() V19( NonZero x) V20( NonZero x) V23() V28() V34( NonZero x) Element of bool [:(NonZero x),(NonZero x):]
[:(NonZero x),(NonZero x):] is set
bool [:(NonZero x),(NonZero x):] is set
Class ((x),r) is Element of bool (NonZero x)
r is Element of the carrier of x
(x,r) is Element of bool (NonZero x)
Class ((x),r) is Element of bool (NonZero x)
r is Element of the carrier of x
(x,r) is Element of bool (NonZero x)
Class ((x),r) is Element of bool (NonZero x)
dw is Element of (x)
p is Element of (x)
q is Element of (x)
[dw,p,q] is V35() V36() set
[dw,p] is V35() set
[[dw,p],q] is V35() set
r is Element of the carrier of x
(x,r) is Element of bool (NonZero x)
NonZero x is non empty Element of bool the carrier of x
bool the carrier of x is set
[#] x is non empty non proper Element of bool the carrier of x
0. x is zero Element of the carrier of x
the ZeroF of x is Element of the carrier of x
{(0. x)} is set
([#] x) \ {(0. x)} is Element of bool the carrier of x
bool (NonZero x) is set
(x) is V16() V19( NonZero x) V20( NonZero x) V23() V28() V34( NonZero x) Element of bool [:(NonZero x),(NonZero x):]
[:(NonZero x),(NonZero x):] is set
bool [:(NonZero x),(NonZero x):] is set
Class ((x),r) is Element of bool (NonZero x)
r is Element of the carrier of x
(x,r) is Element of bool (NonZero x)
Class ((x),r) is Element of bool (NonZero x)
r is Element of the carrier of x
(x,r) is Element of bool (NonZero x)
Class ((x),r) is Element of bool (NonZero x)
x is non empty non trivial V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
(x) is non empty set
(x) is Relation3 of (x)
CollStr(# (x),(x) #) is strict CollStr
x is non empty non trivial V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
(x) is strict CollStr
(x) is non empty set
(x) is Relation3 of (x)
CollStr(# (x),(x) #) is strict CollStr
x is non empty non trivial V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
(x) is non empty strict CollStr
(x) is non empty set
(x) is Relation3 of (x)
CollStr(# (x),(x) #) is strict CollStr
the carrier of (x) is non empty set
V is non empty non trivial V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
(V) is non empty strict CollStr
(V) is non empty set
(V) is Relation3 of (V)
CollStr(# (V),(V) #) is strict CollStr
the Collinearity of (V) is Relation3 of the carrier of (V)
the carrier of (V) is non empty set
x is set
V is set
x9 is set
[x,V,x9] is V35() V36() set
[x,V] is V35() set
[[x,V],x9] is V35() set
y is non empty non trivial V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
(y) is non empty strict CollStr
(y) is non empty set
(y) is Relation3 of (y)
CollStr(# (y),(y) #) is strict CollStr
the Collinearity of (y) is Relation3 of the carrier of (y)
the carrier of (y) is non empty set
the carrier of y is non empty non trivial set
x is non empty non trivial V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
the carrier of x is non empty non trivial set
(x) is non empty strict CollStr
(x) is non empty set
(x) is Relation3 of (x)
CollStr(# (x),(x) #) is strict CollStr
the Collinearity of (x) is Relation3 of the carrier of (x)
the carrier of (x) is non empty set
V is Element of the carrier of x
(x,V) is Element of bool (NonZero x)
NonZero x is non empty Element of bool the carrier of x
bool the carrier of x is set
[#] x is non empty non proper Element of bool the carrier of x
0. x is zero Element of the carrier of x
the ZeroF of x is Element of the carrier of x
{(0. x)} is set
([#] x) \ {(0. x)} is Element of bool the carrier of x
bool (NonZero x) is set
(x) is V16() V19( NonZero x) V20( NonZero x) V23() V28() V34( NonZero x) Element of bool [:(NonZero x),(NonZero x):]
[:(NonZero x),(NonZero x):] is set
bool [:(NonZero x),(NonZero x):] is set
Class ((x),V) is Element of bool (NonZero x)
x9 is Element of the carrier of x
(x,x9) is Element of bool (NonZero x)
Class ((x),x9) is Element of bool (NonZero x)
y is Element of the carrier of x
(x,y) is Element of bool (NonZero x)
Class ((x),y) is Element of bool (NonZero x)
[(x,V),(x,x9),(x,y)] is V35() V36() set
[(x,V),(x,x9)] is V35() set
[[(x,V),(x,x9)],(x,y)] is V35() set
y is set
y is set
dw is set
p is Element of the carrier of x
(x,p) is Element of bool (NonZero x)
Class ((x),p) is Element of bool (NonZero x)
q is Element of the carrier of x
(x,q) is Element of bool (NonZero x)
Class ((x),q) is Element of bool (NonZero x)
r is Element of the carrier of x
(x,r) is Element of bool (NonZero x)
Class ((x),r) is Element of bool (NonZero x)
x is set
V is non empty non trivial V79() V80() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() RLSStruct
(V) is non empty strict CollStr
(V) is non empty set
(V) is Relation3 of (V)
CollStr(# (V),(V) #) is strict CollStr
the carrier of (V) is non empty set
the carrier of V is non empty non trivial set
NonZero V is non empty Element of bool the carrier of V
bool the carrier of V is set
[#] V is non empty non proper Element of bool the carrier of V
0. V is zero Element of the carrier of V
the ZeroF of V is Element of the carrier of V
{(0. V)} is set
([#] V) \ {(0. V)} is Element of bool the carrier of V
bool (NonZero V) is set
bool (bool (NonZero V)) is set
(V) is V16() V19( NonZero V) V20( NonZero V) V23() V28() V34( NonZero V) Element of bool [:(NonZero V),(NonZero V):]
[:(NonZero V),(NonZero V):] is set
bool [:(NonZero V),(NonZero V):] is set
Class (V) is a_partition of NonZero V
y is Element of bool (bool (NonZero V))
x9 is Element of bool (NonZero V)
y is Element of bool (bool (NonZero V))
y is set
Class ((V),y) is Element of bool (NonZero V)
y is Element of the carrier of V
y is Element of the carrier of V
(V,y) is Element of bool (NonZero V)
Class ((V),y) is Element of bool (NonZero V)
x9 is Element of the carrier of V
(V,x9) is Element of bool (NonZero V)
Class ((V),x9) is Element of bool (NonZero V)
y is Element of the carrier of V
(V,y) is Element of bool (NonZero V)
Class ((V),y) is Element of bool (NonZero V)