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