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