REAL is V29() V30() V31() V35() set
NAT is V29() V30() V31() V32() V33() V34() V35() M2( bool REAL)
bool REAL is set
NAT is V29() V30() V31() V32() V33() V34() V35() set
bool NAT is set
bool NAT is set
0 is set
1 is V4() V17() V18() V26() V27() V28() V29() V30() V31() V32() V33() V34() V40() M3( REAL , NAT )
0 is V17() V26() V27() V28() V29() V30() V31() V32() V33() V34() V40() M3( REAL , NAT )
V is non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is V4() set
u is M2( the carrier of V)
v is M2( the carrier of V)
u1 is M2( the carrier of V)
v1 is M2( the carrier of V)
u + v1 is M2( the carrier of V)
u - v1 is M2( the carrier of V)
- v1 is M2( the carrier of V)
u + (- v1) is M2( the carrier of V)
x is V17() V27() V28() M2( REAL )
x * v is M2( the carrier of V)
y is V17() V27() V28() M2( REAL )
y * u1 is M2( the carrier of V)
(x * v) + (y * u1) is M2( the carrier of V)
p is V17() V27() V28() M2( REAL )
p * v is M2( the carrier of V)
x + p is V17() V27() V28() M2( REAL )
(x + p) * v is M2( the carrier of V)
x - p is V17() V27() V28() M2( REAL )
(x - p) * v is M2( the carrier of V)
q is V17() V27() V28() M2( REAL )
q * u1 is M2( the carrier of V)
(p * v) + (q * u1) is M2( the carrier of V)
y + q is V17() V27() V28() M2( REAL )
(y + q) * u1 is M2( the carrier of V)
((x + p) * v) + ((y + q) * u1) is M2( the carrier of V)
y - q is V17() V27() V28() M2( REAL )
(y - q) * u1 is M2( the carrier of V)
((x - p) * v) + ((y - q) * u1) is M2( the carrier of V)
((x * v) + (y * u1)) + (p * v) is M2( the carrier of V)
(((x * v) + (y * u1)) + (p * v)) + (q * u1) is M2( the carrier of V)
(x * v) + (p * v) is M2( the carrier of V)
((x * v) + (p * v)) + (y * u1) is M2( the carrier of V)
(((x * v) + (p * v)) + (y * u1)) + (q * u1) is M2( the carrier of V)
((x + p) * v) + (y * u1) is M2( the carrier of V)
(((x + p) * v) + (y * u1)) + (q * u1) is M2( the carrier of V)
(y * u1) + (q * u1) is M2( the carrier of V)
((x + p) * v) + ((y * u1) + (q * u1)) is M2( the carrier of V)
- (p * v) is M2( the carrier of V)
- (q * u1) is M2( the carrier of V)
(- (p * v)) + (- (q * u1)) is M2( the carrier of V)
((x * v) + (y * u1)) + ((- (p * v)) + (- (q * u1))) is M2( the carrier of V)
- v is M2( the carrier of V)
p * (- v) is M2( the carrier of V)
(p * (- v)) + (- (q * u1)) is M2( the carrier of V)
((x * v) + (y * u1)) + ((p * (- v)) + (- (q * u1))) is M2( the carrier of V)
- u1 is M2( the carrier of V)
q * (- u1) is M2( the carrier of V)
(p * (- v)) + (q * (- u1)) is M2( the carrier of V)
((x * v) + (y * u1)) + ((p * (- v)) + (q * (- u1))) is M2( the carrier of V)
- p is V17() V27() V28() M2( REAL )
(- p) * v is M2( the carrier of V)
((- p) * v) + (q * (- u1)) is M2( the carrier of V)
((x * v) + (y * u1)) + (((- p) * v) + (q * (- u1))) is M2( the carrier of V)
- q is V17() V27() V28() M2( REAL )
(- q) * u1 is M2( the carrier of V)
((- p) * v) + ((- q) * u1) is M2( the carrier of V)
((x * v) + (y * u1)) + (((- p) * v) + ((- q) * u1)) is M2( the carrier of V)
((x * v) + (y * u1)) + ((- p) * v) is M2( the carrier of V)
(((x * v) + (y * u1)) + ((- p) * v)) + ((- q) * u1) is M2( the carrier of V)
(x * v) + ((- p) * v) is M2( the carrier of V)
((x * v) + ((- p) * v)) + (y * u1) is M2( the carrier of V)
(((x * v) + ((- p) * v)) + (y * u1)) + ((- q) * u1) is M2( the carrier of V)
x + (- p) is V17() V27() V28() M2( REAL )
(x + (- p)) * v is M2( the carrier of V)
((x + (- p)) * v) + (y * u1) is M2( the carrier of V)
(((x + (- p)) * v) + (y * u1)) + ((- q) * u1) is M2( the carrier of V)
(y * u1) + ((- q) * u1) is M2( the carrier of V)
((x + (- p)) * v) + ((y * u1) + ((- q) * u1)) is M2( the carrier of V)
y + (- q) is V17() V27() V28() M2( REAL )
(y + (- q)) * u1 is M2( the carrier of V)
((x - p) * v) + ((y + (- q)) * u1) is M2( the carrier of V)
V is non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is V4() set
u is M2( the carrier of V)
v is M2( the carrier of V)
u1 is M2( the carrier of V)
v1 is V17() V27() V28() M2( REAL )
v1 * v is M2( the carrier of V)
x is V17() V27() V28() M2( REAL )
x * u1 is M2( the carrier of V)
(v1 * v) + (x * u1) is M2( the carrier of V)
y is V17() V27() V28() M2( REAL )
y * u is M2( the carrier of V)
y * v1 is V17() V27() V28() M2( REAL )
(y * v1) * v is M2( the carrier of V)
y * x is V17() V27() V28() M2( REAL )
(y * x) * u1 is M2( the carrier of V)
((y * v1) * v) + ((y * x) * u1) is M2( the carrier of V)
y * (v1 * v) is M2( the carrier of V)
y * (x * u1) is M2( the carrier of V)
(y * (v1 * v)) + (y * (x * u1)) is M2( the carrier of V)
((y * v1) * v) + (y * (x * u1)) is M2( the carrier of V)
V is non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is V4() set
u is M2( the carrier of V)
v is M2( the carrier of V)
u1 is V17() V27() V28() M2( REAL )
u1 * u is M2( the carrier of V)
v1 is V17() V27() V28() M2( REAL )
v1 * v is M2( the carrier of V)
(u1 * u) + (v1 * v) is M2( the carrier of V)
x is V17() V27() V28() M2( REAL )
x * u is M2( the carrier of V)
y is V17() V27() V28() M2( REAL )
y * v is M2( the carrier of V)
(x * u) + (y * v) is M2( the carrier of V)
0. V is V60(V) M2( the carrier of V)
the ZeroF of V is M2( the carrier of V)
((u1 * u) + (v1 * v)) - ((x * u) + (y * v)) is M2( the carrier of V)
- ((x * u) + (y * v)) is M2( the carrier of V)
((u1 * u) + (v1 * v)) + (- ((x * u) + (y * v))) is M2( the carrier of V)
u1 - x is V17() V27() V28() M2( REAL )
(u1 - x) * u is M2( the carrier of V)
v1 - y is V17() V27() V28() M2( REAL )
(v1 - y) * v is M2( the carrier of V)
((u1 - x) * u) + ((v1 - y) * v) is M2( the carrier of V)
- x is V17() V27() V28() M2( REAL )
(- x) + u1 is V17() V27() V28() M2( REAL )
- y is V17() V27() V28() M2( REAL )
(- y) + v1 is V17() V27() V28() M2( REAL )
V is non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is V4() set
0. V is V60(V) M2( the carrier of V)
the ZeroF of V is M2( the carrier of V)
u is M2( the carrier of V)
v is M2( the carrier of V)
u1 is V17() V27() V28() M2( REAL )
v1 is V17() V27() V28() M2( REAL )
u1 * u is M2( the carrier of V)
v1 * v is M2( the carrier of V)
(u1 * u) + (v1 * v) is M2( the carrier of V)
0 * v is M2( the carrier of V)
(0. V) + (0 * v) is M2( the carrier of V)
(0. V) + (0. V) is M2( the carrier of V)
u1 is V17() V27() V28() M2( REAL )
v1 is V17() V27() V28() M2( REAL )
u1 * u is M2( the carrier of V)
v1 * v is M2( the carrier of V)
(u1 * u) + (v1 * v) is M2( the carrier of V)
1 * (0. V) is M2( the carrier of V)
(0. V) + (1 * (0. V)) is M2( the carrier of V)
(0. V) + (0. V) is M2( the carrier of V)
V is non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is V4() set
u is M2( the carrier of V)
v is M2( the carrier of V)
u1 is M2( the carrier of V)
pr1 (u,v,u1) is V17() V27() V28() M2( REAL )
(pr1 (u,v,u1)) * u is M2( the carrier of V)
pr2 (u,v,u1) is V17() V27() V28() M2( REAL )
(pr2 (u,v,u1)) * v is M2( the carrier of V)
((pr1 (u,v,u1)) * u) + ((pr2 (u,v,u1)) * v) is M2( the carrier of V)
v1 is V17() V27() V28() M2( REAL )
v1 * v is M2( the carrier of V)
((pr1 (u,v,u1)) * u) + (v1 * v) is M2( the carrier of V)
V is non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is V4() set
u is M2( the carrier of V)
v is M2( the carrier of V)
u1 is M2( the carrier of V)
pr1 (u,v,u1) is V17() V27() V28() M2( REAL )
pr2 (u,v,u1) is V17() V27() V28() M2( REAL )
v1 is V17() V27() V28() M2( REAL )
v1 * u is M2( the carrier of V)
x is V17() V27() V28() M2( REAL )
x * v is M2( the carrier of V)
(v1 * u) + (x * v) is M2( the carrier of V)
(pr1 (u,v,u1)) * u is M2( the carrier of V)
(pr2 (u,v,u1)) * v is M2( the carrier of V)
((pr1 (u,v,u1)) * u) + ((pr2 (u,v,u1)) * v) is M2( the carrier of V)
V is non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is V4() set
u is M2( the carrier of V)
v is M2( the carrier of V)
u1 is M2( the carrier of V)
pr1 (u,v,u1) is V17() V27() V28() M2( REAL )
pr2 (u,v,u1) is V17() V27() V28() M2( REAL )
v1 is M2( the carrier of V)
u1 + v1 is M2( the carrier of V)
pr1 (u,v,(u1 + v1)) is V17() V27() V28() M2( REAL )
pr1 (u,v,v1) is V17() V27() V28() M2( REAL )
(pr1 (u,v,u1)) + (pr1 (u,v,v1)) is V17() V27() V28() M2( REAL )
pr2 (u,v,(u1 + v1)) is V17() V27() V28() M2( REAL )
pr2 (u,v,v1) is V17() V27() V28() M2( REAL )
(pr2 (u,v,u1)) + (pr2 (u,v,v1)) is V17() V27() V28() M2( REAL )
u1 - v1 is M2( the carrier of V)
- v1 is M2( the carrier of V)
u1 + (- v1) is M2( the carrier of V)
pr1 (u,v,(u1 - v1)) is V17() V27() V28() M2( REAL )
(pr1 (u,v,u1)) - (pr1 (u,v,v1)) is V17() V27() V28() M2( REAL )
pr2 (u,v,(u1 - v1)) is V17() V27() V28() M2( REAL )
(pr2 (u,v,u1)) - (pr2 (u,v,v1)) is V17() V27() V28() M2( REAL )
x is V17() V27() V28() M2( REAL )
x * u1 is M2( the carrier of V)
pr1 (u,v,(x * u1)) is V17() V27() V28() M2( REAL )
x * (pr1 (u,v,u1)) is V17() V27() V28() M2( REAL )
pr2 (u,v,(x * u1)) is V17() V27() V28() M2( REAL )
x * (pr2 (u,v,u1)) is V17() V27() V28() M2( REAL )
(pr1 (u,v,u1)) * u is M2( the carrier of V)
(pr2 (u,v,u1)) * v is M2( the carrier of V)
((pr1 (u,v,u1)) * u) + ((pr2 (u,v,u1)) * v) is M2( the carrier of V)
(pr1 (u,v,v1)) * u is M2( the carrier of V)
(pr2 (u,v,v1)) * v is M2( the carrier of V)
((pr1 (u,v,v1)) * u) + ((pr2 (u,v,v1)) * v) is M2( the carrier of V)
(((pr1 (u,v,u1)) * u) + ((pr2 (u,v,u1)) * v)) + ((pr1 (u,v,v1)) * u) is M2( the carrier of V)
((((pr1 (u,v,u1)) * u) + ((pr2 (u,v,u1)) * v)) + ((pr1 (u,v,v1)) * u)) + ((pr2 (u,v,v1)) * v) is M2( the carrier of V)
((pr1 (u,v,u1)) * u) + ((pr1 (u,v,v1)) * u) is M2( the carrier of V)
(((pr1 (u,v,u1)) * u) + ((pr1 (u,v,v1)) * u)) + ((pr2 (u,v,u1)) * v) is M2( the carrier of V)
((((pr1 (u,v,u1)) * u) + ((pr1 (u,v,v1)) * u)) + ((pr2 (u,v,u1)) * v)) + ((pr2 (u,v,v1)) * v) is M2( the carrier of V)
((pr2 (u,v,u1)) * v) + ((pr2 (u,v,v1)) * v) is M2( the carrier of V)
(((pr1 (u,v,u1)) * u) + ((pr1 (u,v,v1)) * u)) + (((pr2 (u,v,u1)) * v) + ((pr2 (u,v,v1)) * v)) is M2( the carrier of V)
((pr1 (u,v,u1)) + (pr1 (u,v,v1))) * u is M2( the carrier of V)
(((pr1 (u,v,u1)) + (pr1 (u,v,v1))) * u) + (((pr2 (u,v,u1)) * v) + ((pr2 (u,v,v1)) * v)) is M2( the carrier of V)
((pr2 (u,v,u1)) + (pr2 (u,v,v1))) * v is M2( the carrier of V)
(((pr1 (u,v,u1)) + (pr1 (u,v,v1))) * u) + (((pr2 (u,v,u1)) + (pr2 (u,v,v1))) * v) is M2( the carrier of V)
((pr1 (u,v,u1)) - (pr1 (u,v,v1))) * u is M2( the carrier of V)
((pr2 (u,v,u1)) - (pr2 (u,v,v1))) * v is M2( the carrier of V)
(((pr1 (u,v,u1)) - (pr1 (u,v,v1))) * u) + (((pr2 (u,v,u1)) - (pr2 (u,v,v1))) * v) is M2( the carrier of V)
(x * (pr1 (u,v,u1))) * u is M2( the carrier of V)
(x * (pr2 (u,v,u1))) * v is M2( the carrier of V)
((x * (pr1 (u,v,u1))) * u) + ((x * (pr2 (u,v,u1))) * v) is M2( the carrier of V)
V is non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is V4() set
u is M2( the carrier of V)
v is M2( the carrier of V)
u1 is M2( the carrier of V)
pr1 (u,v,u1) is V17() V27() V28() M2( REAL )
(pr1 (u,v,u1)) * u is M2( the carrier of V)
pr2 (u,v,u1) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,u1)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,u1))) * v is M2( the carrier of V)
((pr1 (u,v,u1)) * u) + ((- (pr2 (u,v,u1))) * v) is M2( the carrier of V)
V is non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is V4() set
u is M2( the carrier of V)
v is M2( the carrier of V)
u1 is M2( the carrier of V)
(V,u,v,u1) is M2( the carrier of V)
pr1 (u,v,u1) is V17() V27() V28() M2( REAL )
(pr1 (u,v,u1)) * u is M2( the carrier of V)
pr2 (u,v,u1) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,u1)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,u1))) * v is M2( the carrier of V)
((pr1 (u,v,u1)) * u) + ((- (pr2 (u,v,u1))) * v) is M2( the carrier of V)
v1 is M2( the carrier of V)
u1 + v1 is M2( the carrier of V)
(V,u,v,(u1 + v1)) is M2( the carrier of V)
pr1 (u,v,(u1 + v1)) is V17() V27() V28() M2( REAL )
(pr1 (u,v,(u1 + v1))) * u is M2( the carrier of V)
pr2 (u,v,(u1 + v1)) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,(u1 + v1))) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,(u1 + v1)))) * v is M2( the carrier of V)
((pr1 (u,v,(u1 + v1))) * u) + ((- (pr2 (u,v,(u1 + v1)))) * v) is M2( the carrier of V)
(V,u,v,v1) is M2( the carrier of V)
pr1 (u,v,v1) is V17() V27() V28() M2( REAL )
(pr1 (u,v,v1)) * u is M2( the carrier of V)
pr2 (u,v,v1) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,v1)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,v1))) * v is M2( the carrier of V)
((pr1 (u,v,v1)) * u) + ((- (pr2 (u,v,v1))) * v) is M2( the carrier of V)
(V,u,v,u1) + (V,u,v,v1) is M2( the carrier of V)
(pr1 (u,v,u1)) + (pr1 (u,v,v1)) is V17() V27() V28() M2( REAL )
((pr1 (u,v,u1)) + (pr1 (u,v,v1))) * u is M2( the carrier of V)
(((pr1 (u,v,u1)) + (pr1 (u,v,v1))) * u) + ((- (pr2 (u,v,(u1 + v1)))) * v) is M2( the carrier of V)
(pr2 (u,v,u1)) + (pr2 (u,v,v1)) is V17() V27() V28() M2( REAL )
- ((pr2 (u,v,u1)) + (pr2 (u,v,v1))) is V17() V27() V28() M2( REAL )
(- ((pr2 (u,v,u1)) + (pr2 (u,v,v1)))) * v is M2( the carrier of V)
(((pr1 (u,v,u1)) + (pr1 (u,v,v1))) * u) + ((- ((pr2 (u,v,u1)) + (pr2 (u,v,v1)))) * v) is M2( the carrier of V)
((pr1 (u,v,u1)) * u) + ((pr1 (u,v,v1)) * u) is M2( the carrier of V)
(((pr1 (u,v,u1)) * u) + ((pr1 (u,v,v1)) * u)) + ((- ((pr2 (u,v,u1)) + (pr2 (u,v,v1)))) * v) is M2( the carrier of V)
- v is M2( the carrier of V)
((pr2 (u,v,u1)) + (pr2 (u,v,v1))) * (- v) is M2( the carrier of V)
(((pr1 (u,v,u1)) * u) + ((pr1 (u,v,v1)) * u)) + (((pr2 (u,v,u1)) + (pr2 (u,v,v1))) * (- v)) is M2( the carrier of V)
((pr2 (u,v,u1)) + (pr2 (u,v,v1))) * v is M2( the carrier of V)
- (((pr2 (u,v,u1)) + (pr2 (u,v,v1))) * v) is M2( the carrier of V)
(((pr1 (u,v,u1)) * u) + ((pr1 (u,v,v1)) * u)) + (- (((pr2 (u,v,u1)) + (pr2 (u,v,v1))) * v)) is M2( the carrier of V)
(pr2 (u,v,u1)) * v is M2( the carrier of V)
(pr2 (u,v,v1)) * v is M2( the carrier of V)
((pr2 (u,v,u1)) * v) + ((pr2 (u,v,v1)) * v) is M2( the carrier of V)
- (((pr2 (u,v,u1)) * v) + ((pr2 (u,v,v1)) * v)) is M2( the carrier of V)
(((pr1 (u,v,u1)) * u) + ((pr1 (u,v,v1)) * u)) + (- (((pr2 (u,v,u1)) * v) + ((pr2 (u,v,v1)) * v))) is M2( the carrier of V)
- ((pr2 (u,v,u1)) * v) is M2( the carrier of V)
- ((pr2 (u,v,v1)) * v) is M2( the carrier of V)
(- ((pr2 (u,v,u1)) * v)) + (- ((pr2 (u,v,v1)) * v)) is M2( the carrier of V)
(((pr1 (u,v,u1)) * u) + ((pr1 (u,v,v1)) * u)) + ((- ((pr2 (u,v,u1)) * v)) + (- ((pr2 (u,v,v1)) * v))) is M2( the carrier of V)
((pr1 (u,v,v1)) * u) + ((- ((pr2 (u,v,u1)) * v)) + (- ((pr2 (u,v,v1)) * v))) is M2( the carrier of V)
((pr1 (u,v,u1)) * u) + (((pr1 (u,v,v1)) * u) + ((- ((pr2 (u,v,u1)) * v)) + (- ((pr2 (u,v,v1)) * v)))) is M2( the carrier of V)
((pr1 (u,v,v1)) * u) + (- ((pr2 (u,v,v1)) * v)) is M2( the carrier of V)
(- ((pr2 (u,v,u1)) * v)) + (((pr1 (u,v,v1)) * u) + (- ((pr2 (u,v,v1)) * v))) is M2( the carrier of V)
((pr1 (u,v,u1)) * u) + ((- ((pr2 (u,v,u1)) * v)) + (((pr1 (u,v,v1)) * u) + (- ((pr2 (u,v,v1)) * v)))) is M2( the carrier of V)
((pr1 (u,v,u1)) * u) + (- ((pr2 (u,v,u1)) * v)) is M2( the carrier of V)
(((pr1 (u,v,u1)) * u) + (- ((pr2 (u,v,u1)) * v))) + (((pr1 (u,v,v1)) * u) + (- ((pr2 (u,v,v1)) * v))) is M2( the carrier of V)
(pr2 (u,v,u1)) * (- v) is M2( the carrier of V)
((pr1 (u,v,u1)) * u) + ((pr2 (u,v,u1)) * (- v)) is M2( the carrier of V)
(((pr1 (u,v,u1)) * u) + ((pr2 (u,v,u1)) * (- v))) + (((pr1 (u,v,v1)) * u) + (- ((pr2 (u,v,v1)) * v))) is M2( the carrier of V)
(pr2 (u,v,v1)) * (- v) is M2( the carrier of V)
((pr1 (u,v,v1)) * u) + ((pr2 (u,v,v1)) * (- v)) is M2( the carrier of V)
(((pr1 (u,v,u1)) * u) + ((pr2 (u,v,u1)) * (- v))) + (((pr1 (u,v,v1)) * u) + ((pr2 (u,v,v1)) * (- v))) is M2( the carrier of V)
(((pr1 (u,v,u1)) * u) + ((- (pr2 (u,v,u1))) * v)) + (((pr1 (u,v,v1)) * u) + ((pr2 (u,v,v1)) * (- v))) is M2( the carrier of V)
V is non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is V4() set
u is M2( the carrier of V)
v is M2( the carrier of V)
u1 is M2( the carrier of V)
(V,u,v,u1) is M2( the carrier of V)
pr1 (u,v,u1) is V17() V27() V28() M2( REAL )
(pr1 (u,v,u1)) * u is M2( the carrier of V)
pr2 (u,v,u1) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,u1)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,u1))) * v is M2( the carrier of V)
((pr1 (u,v,u1)) * u) + ((- (pr2 (u,v,u1))) * v) is M2( the carrier of V)
v1 is V17() V27() V28() M2( REAL )
v1 * u1 is M2( the carrier of V)
(V,u,v,(v1 * u1)) is M2( the carrier of V)
pr1 (u,v,(v1 * u1)) is V17() V27() V28() M2( REAL )
(pr1 (u,v,(v1 * u1))) * u is M2( the carrier of V)
pr2 (u,v,(v1 * u1)) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,(v1 * u1))) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,(v1 * u1)))) * v is M2( the carrier of V)
((pr1 (u,v,(v1 * u1))) * u) + ((- (pr2 (u,v,(v1 * u1)))) * v) is M2( the carrier of V)
v1 * (V,u,v,u1) is M2( the carrier of V)
v1 * (pr1 (u,v,u1)) is V17() V27() V28() M2( REAL )
(v1 * (pr1 (u,v,u1))) * u is M2( the carrier of V)
((v1 * (pr1 (u,v,u1))) * u) + ((- (pr2 (u,v,(v1 * u1)))) * v) is M2( the carrier of V)
v1 * (pr2 (u,v,u1)) is V17() V27() V28() M2( REAL )
- (v1 * (pr2 (u,v,u1))) is V17() V27() V28() M2( REAL )
(- (v1 * (pr2 (u,v,u1)))) * v is M2( the carrier of V)
((v1 * (pr1 (u,v,u1))) * u) + ((- (v1 * (pr2 (u,v,u1)))) * v) is M2( the carrier of V)
- v is M2( the carrier of V)
(v1 * (pr2 (u,v,u1))) * (- v) is M2( the carrier of V)
((v1 * (pr1 (u,v,u1))) * u) + ((v1 * (pr2 (u,v,u1))) * (- v)) is M2( the carrier of V)
(v1 * (pr2 (u,v,u1))) * v is M2( the carrier of V)
- ((v1 * (pr2 (u,v,u1))) * v) is M2( the carrier of V)
((v1 * (pr1 (u,v,u1))) * u) + (- ((v1 * (pr2 (u,v,u1))) * v)) is M2( the carrier of V)
(pr2 (u,v,u1)) * v is M2( the carrier of V)
v1 * ((pr2 (u,v,u1)) * v) is M2( the carrier of V)
- (v1 * ((pr2 (u,v,u1)) * v)) is M2( the carrier of V)
((v1 * (pr1 (u,v,u1))) * u) + (- (v1 * ((pr2 (u,v,u1)) * v))) is M2( the carrier of V)
- ((pr2 (u,v,u1)) * v) is M2( the carrier of V)
v1 * (- ((pr2 (u,v,u1)) * v)) is M2( the carrier of V)
((v1 * (pr1 (u,v,u1))) * u) + (v1 * (- ((pr2 (u,v,u1)) * v))) is M2( the carrier of V)
v1 * ((pr1 (u,v,u1)) * u) is M2( the carrier of V)
(v1 * ((pr1 (u,v,u1)) * u)) + (v1 * (- ((pr2 (u,v,u1)) * v))) is M2( the carrier of V)
((pr1 (u,v,u1)) * u) + (- ((pr2 (u,v,u1)) * v)) is M2( the carrier of V)
v1 * (((pr1 (u,v,u1)) * u) + (- ((pr2 (u,v,u1)) * v))) is M2( the carrier of V)
(pr2 (u,v,u1)) * (- v) is M2( the carrier of V)
((pr1 (u,v,u1)) * u) + ((pr2 (u,v,u1)) * (- v)) is M2( the carrier of V)
v1 * (((pr1 (u,v,u1)) * u) + ((pr2 (u,v,u1)) * (- v))) is M2( the carrier of V)
V is non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is V4() set
0. V is V60(V) M2( the carrier of V)
the ZeroF of V is M2( the carrier of V)
u is M2( the carrier of V)
v is M2( the carrier of V)
(V,u,v,(0. V)) is M2( the carrier of V)
pr1 (u,v,(0. V)) is V17() V27() V28() M2( REAL )
(pr1 (u,v,(0. V))) * u is M2( the carrier of V)
pr2 (u,v,(0. V)) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,(0. V))) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,(0. V)))) * v is M2( the carrier of V)
((pr1 (u,v,(0. V))) * u) + ((- (pr2 (u,v,(0. V)))) * v) is M2( the carrier of V)
the M2( the carrier of V) is M2( the carrier of V)
0 * the M2( the carrier of V) is M2( the carrier of V)
(V,u,v,(0 * the M2( the carrier of V))) is M2( the carrier of V)
pr1 (u,v,(0 * the M2( the carrier of V))) is V17() V27() V28() M2( REAL )
(pr1 (u,v,(0 * the M2( the carrier of V)))) * u is M2( the carrier of V)
pr2 (u,v,(0 * the M2( the carrier of V))) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,(0 * the M2( the carrier of V)))) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,(0 * the M2( the carrier of V))))) * v is M2( the carrier of V)
((pr1 (u,v,(0 * the M2( the carrier of V)))) * u) + ((- (pr2 (u,v,(0 * the M2( the carrier of V))))) * v) is M2( the carrier of V)
(V,u,v, the M2( the carrier of V)) is M2( the carrier of V)
pr1 (u,v, the M2( the carrier of V)) is V17() V27() V28() M2( REAL )
(pr1 (u,v, the M2( the carrier of V))) * u is M2( the carrier of V)
pr2 (u,v, the M2( the carrier of V)) is V17() V27() V28() M2( REAL )
- (pr2 (u,v, the M2( the carrier of V))) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v, the M2( the carrier of V)))) * v is M2( the carrier of V)
((pr1 (u,v, the M2( the carrier of V))) * u) + ((- (pr2 (u,v, the M2( the carrier of V)))) * v) is M2( the carrier of V)
0 * (V,u,v, the M2( the carrier of V)) is M2( the carrier of V)
V is non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is V4() set
u is M2( the carrier of V)
v is M2( the carrier of V)
u1 is M2( the carrier of V)
- u1 is M2( the carrier of V)
(V,u,v,(- u1)) is M2( the carrier of V)
pr1 (u,v,(- u1)) is V17() V27() V28() M2( REAL )
(pr1 (u,v,(- u1))) * u is M2( the carrier of V)
pr2 (u,v,(- u1)) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,(- u1))) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,(- u1)))) * v is M2( the carrier of V)
((pr1 (u,v,(- u1))) * u) + ((- (pr2 (u,v,(- u1)))) * v) is M2( the carrier of V)
(V,u,v,u1) is M2( the carrier of V)
pr1 (u,v,u1) is V17() V27() V28() M2( REAL )
(pr1 (u,v,u1)) * u is M2( the carrier of V)
pr2 (u,v,u1) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,u1)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,u1))) * v is M2( the carrier of V)
((pr1 (u,v,u1)) * u) + ((- (pr2 (u,v,u1))) * v) is M2( the carrier of V)
- (V,u,v,u1) is M2( the carrier of V)
(pr2 (u,v,u1)) * v is M2( the carrier of V)
((pr1 (u,v,u1)) * u) + ((pr2 (u,v,u1)) * v) is M2( the carrier of V)
- (((pr1 (u,v,u1)) * u) + ((pr2 (u,v,u1)) * v)) is M2( the carrier of V)
- ((pr1 (u,v,u1)) * u) is M2( the carrier of V)
- ((pr2 (u,v,u1)) * v) is M2( the carrier of V)
(- ((pr1 (u,v,u1)) * u)) + (- ((pr2 (u,v,u1)) * v)) is M2( the carrier of V)
- u is M2( the carrier of V)
(pr1 (u,v,u1)) * (- u) is M2( the carrier of V)
((pr1 (u,v,u1)) * (- u)) + (- ((pr2 (u,v,u1)) * v)) is M2( the carrier of V)
- (pr1 (u,v,u1)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,u1))) * u is M2( the carrier of V)
((- (pr1 (u,v,u1))) * u) + (- ((pr2 (u,v,u1)) * v)) is M2( the carrier of V)
- v is M2( the carrier of V)
(pr2 (u,v,u1)) * (- v) is M2( the carrier of V)
((- (pr1 (u,v,u1))) * u) + ((pr2 (u,v,u1)) * (- v)) is M2( the carrier of V)
((- (pr1 (u,v,u1))) * u) + ((- (pr2 (u,v,u1))) * v) is M2( the carrier of V)
((- (pr1 (u,v,u1))) * u) + ((- (pr2 (u,v,(- u1)))) * v) is M2( the carrier of V)
- (- (pr2 (u,v,u1))) is V17() V27() V28() M2( REAL )
(- (- (pr2 (u,v,u1)))) * v is M2( the carrier of V)
((- (pr1 (u,v,u1))) * u) + ((- (- (pr2 (u,v,u1)))) * v) is M2( the carrier of V)
((pr1 (u,v,u1)) * (- u)) + ((- (- (pr2 (u,v,u1)))) * v) is M2( the carrier of V)
(- ((pr1 (u,v,u1)) * u)) + ((- (- (pr2 (u,v,u1)))) * v) is M2( the carrier of V)
(- (pr2 (u,v,u1))) * (- v) is M2( the carrier of V)
(- ((pr1 (u,v,u1)) * u)) + ((- (pr2 (u,v,u1))) * (- v)) is M2( the carrier of V)
- ((- (pr2 (u,v,u1))) * v) is M2( the carrier of V)
(- ((pr1 (u,v,u1)) * u)) + (- ((- (pr2 (u,v,u1))) * v)) is M2( the carrier of V)
V is non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is V4() set
u is M2( the carrier of V)
v is M2( the carrier of V)
u1 is M2( the carrier of V)
(V,u,v,u1) is M2( the carrier of V)
pr1 (u,v,u1) is V17() V27() V28() M2( REAL )
(pr1 (u,v,u1)) * u is M2( the carrier of V)
pr2 (u,v,u1) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,u1)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,u1))) * v is M2( the carrier of V)
((pr1 (u,v,u1)) * u) + ((- (pr2 (u,v,u1))) * v) is M2( the carrier of V)
v1 is M2( the carrier of V)
u1 - v1 is M2( the carrier of V)
- v1 is M2( the carrier of V)
u1 + (- v1) is M2( the carrier of V)
(V,u,v,(u1 - v1)) is M2( the carrier of V)
pr1 (u,v,(u1 - v1)) is V17() V27() V28() M2( REAL )
(pr1 (u,v,(u1 - v1))) * u is M2( the carrier of V)
pr2 (u,v,(u1 - v1)) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,(u1 - v1))) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,(u1 - v1)))) * v is M2( the carrier of V)
((pr1 (u,v,(u1 - v1))) * u) + ((- (pr2 (u,v,(u1 - v1)))) * v) is M2( the carrier of V)
(V,u,v,v1) is M2( the carrier of V)
pr1 (u,v,v1) is V17() V27() V28() M2( REAL )
(pr1 (u,v,v1)) * u is M2( the carrier of V)
pr2 (u,v,v1) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,v1)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,v1))) * v is M2( the carrier of V)
((pr1 (u,v,v1)) * u) + ((- (pr2 (u,v,v1))) * v) is M2( the carrier of V)
(V,u,v,u1) - (V,u,v,v1) is M2( the carrier of V)
- (V,u,v,v1) is M2( the carrier of V)
(V,u,v,u1) + (- (V,u,v,v1)) is M2( the carrier of V)
(V,u,v,(- v1)) is M2( the carrier of V)
pr1 (u,v,(- v1)) is V17() V27() V28() M2( REAL )
(pr1 (u,v,(- v1))) * u is M2( the carrier of V)
pr2 (u,v,(- v1)) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,(- v1))) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,(- v1)))) * v is M2( the carrier of V)
((pr1 (u,v,(- v1))) * u) + ((- (pr2 (u,v,(- v1)))) * v) is M2( the carrier of V)
(V,u,v,u1) + (V,u,v,(- v1)) is M2( the carrier of V)
V is non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is V4() set
u is M2( the carrier of V)
v is M2( the carrier of V)
u1 is M2( the carrier of V)
(V,u,v,u1) is M2( the carrier of V)
pr1 (u,v,u1) is V17() V27() V28() M2( REAL )
(pr1 (u,v,u1)) * u is M2( the carrier of V)
pr2 (u,v,u1) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,u1)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,u1))) * v is M2( the carrier of V)
((pr1 (u,v,u1)) * u) + ((- (pr2 (u,v,u1))) * v) is M2( the carrier of V)
v1 is M2( the carrier of V)
(V,u,v,v1) is M2( the carrier of V)
pr1 (u,v,v1) is V17() V27() V28() M2( REAL )
(pr1 (u,v,v1)) * u is M2( the carrier of V)
pr2 (u,v,v1) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,v1)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,v1))) * v is M2( the carrier of V)
((pr1 (u,v,v1)) * u) + ((- (pr2 (u,v,v1))) * v) is M2( the carrier of V)
(((pr1 (u,v,u1)) * u) + ((- (pr2 (u,v,u1))) * v)) - (((pr1 (u,v,v1)) * u) + ((- (pr2 (u,v,v1))) * v)) is M2( the carrier of V)
- (((pr1 (u,v,v1)) * u) + ((- (pr2 (u,v,v1))) * v)) is M2( the carrier of V)
(((pr1 (u,v,u1)) * u) + ((- (pr2 (u,v,u1))) * v)) + (- (((pr1 (u,v,v1)) * u) + ((- (pr2 (u,v,v1))) * v))) is M2( the carrier of V)
0. V is V60(V) M2( the carrier of V)
the ZeroF of V is M2( the carrier of V)
(((pr1 (u,v,u1)) * u) + ((- (pr2 (u,v,u1))) * v)) - ((pr1 (u,v,v1)) * u) is M2( the carrier of V)
- ((pr1 (u,v,v1)) * u) is M2( the carrier of V)
(((pr1 (u,v,u1)) * u) + ((- (pr2 (u,v,u1))) * v)) + (- ((pr1 (u,v,v1)) * u)) is M2( the carrier of V)
((((pr1 (u,v,u1)) * u) + ((- (pr2 (u,v,u1))) * v)) - ((pr1 (u,v,v1)) * u)) - ((- (pr2 (u,v,v1))) * v) is M2( the carrier of V)
- ((- (pr2 (u,v,v1))) * v) is M2( the carrier of V)
((((pr1 (u,v,u1)) * u) + ((- (pr2 (u,v,u1))) * v)) - ((pr1 (u,v,v1)) * u)) + (- ((- (pr2 (u,v,v1))) * v)) is M2( the carrier of V)
((pr1 (u,v,u1)) * u) + (- ((pr1 (u,v,v1)) * u)) is M2( the carrier of V)
(((pr1 (u,v,u1)) * u) + (- ((pr1 (u,v,v1)) * u))) + ((- (pr2 (u,v,u1))) * v) is M2( the carrier of V)
((((pr1 (u,v,u1)) * u) + (- ((pr1 (u,v,v1)) * u))) + ((- (pr2 (u,v,u1))) * v)) - ((- (pr2 (u,v,v1))) * v) is M2( the carrier of V)
((((pr1 (u,v,u1)) * u) + (- ((pr1 (u,v,v1)) * u))) + ((- (pr2 (u,v,u1))) * v)) + (- ((- (pr2 (u,v,v1))) * v)) is M2( the carrier of V)
((pr1 (u,v,u1)) * u) - ((pr1 (u,v,v1)) * u) is M2( the carrier of V)
((pr1 (u,v,u1)) * u) + (- ((pr1 (u,v,v1)) * u)) is M2( the carrier of V)
((- (pr2 (u,v,u1))) * v) - ((- (pr2 (u,v,v1))) * v) is M2( the carrier of V)
((- (pr2 (u,v,u1))) * v) + (- ((- (pr2 (u,v,v1))) * v)) is M2( the carrier of V)
(((pr1 (u,v,u1)) * u) - ((pr1 (u,v,v1)) * u)) + (((- (pr2 (u,v,u1))) * v) - ((- (pr2 (u,v,v1))) * v)) is M2( the carrier of V)
(pr1 (u,v,u1)) - (pr1 (u,v,v1)) is V17() V27() V28() M2( REAL )
((pr1 (u,v,u1)) - (pr1 (u,v,v1))) * u is M2( the carrier of V)
(((pr1 (u,v,u1)) - (pr1 (u,v,v1))) * u) + (((- (pr2 (u,v,u1))) * v) - ((- (pr2 (u,v,v1))) * v)) is M2( the carrier of V)
(- (pr2 (u,v,u1))) - (- (pr2 (u,v,v1))) is V17() V27() V28() M2( REAL )
((- (pr2 (u,v,u1))) - (- (pr2 (u,v,v1)))) * v is M2( the carrier of V)
(((pr1 (u,v,u1)) - (pr1 (u,v,v1))) * u) + (((- (pr2 (u,v,u1))) - (- (pr2 (u,v,v1)))) * v) is M2( the carrier of V)
(pr2 (u,v,v1)) * v is M2( the carrier of V)
((pr1 (u,v,v1)) * u) + ((pr2 (u,v,v1)) * v) is M2( the carrier of V)
V is non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is V4() set
u is M2( the carrier of V)
v is M2( the carrier of V)
u1 is M2( the carrier of V)
(V,u,v,u1) is M2( the carrier of V)
pr1 (u,v,u1) is V17() V27() V28() M2( REAL )
(pr1 (u,v,u1)) * u is M2( the carrier of V)
pr2 (u,v,u1) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,u1)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,u1))) * v is M2( the carrier of V)
((pr1 (u,v,u1)) * u) + ((- (pr2 (u,v,u1))) * v) is M2( the carrier of V)
(V,u,v,(V,u,v,u1)) is M2( the carrier of V)
pr1 (u,v,(V,u,v,u1)) is V17() V27() V28() M2( REAL )
(pr1 (u,v,(V,u,v,u1))) * u is M2( the carrier of V)
pr2 (u,v,(V,u,v,u1)) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,(V,u,v,u1))) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,(V,u,v,u1)))) * v is M2( the carrier of V)
((pr1 (u,v,(V,u,v,u1))) * u) + ((- (pr2 (u,v,(V,u,v,u1)))) * v) is M2( the carrier of V)
pr2 (u,v,(((pr1 (u,v,u1)) * u) + ((- (pr2 (u,v,u1))) * v))) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,(((pr1 (u,v,u1)) * u) + ((- (pr2 (u,v,u1))) * v)))) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,(((pr1 (u,v,u1)) * u) + ((- (pr2 (u,v,u1))) * v))))) * v is M2( the carrier of V)
((pr1 (u,v,u1)) * u) + ((- (pr2 (u,v,(((pr1 (u,v,u1)) * u) + ((- (pr2 (u,v,u1))) * v))))) * v) is M2( the carrier of V)
- (- (pr2 (u,v,u1))) is V17() V27() V28() M2( REAL )
(- (- (pr2 (u,v,u1)))) * v is M2( the carrier of V)
((pr1 (u,v,u1)) * u) + ((- (- (pr2 (u,v,u1)))) * v) is M2( the carrier of V)
V is non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is V4() set
u is M2( the carrier of V)
v is M2( the carrier of V)
u1 is M2( the carrier of V)
(V,u,v,u1) is M2( the carrier of V)
pr1 (u,v,u1) is V17() V27() V28() M2( REAL )
(pr1 (u,v,u1)) * u is M2( the carrier of V)
pr2 (u,v,u1) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,u1)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,u1))) * v is M2( the carrier of V)
((pr1 (u,v,u1)) * u) + ((- (pr2 (u,v,u1))) * v) is M2( the carrier of V)
(V,u,v,(V,u,v,u1)) is M2( the carrier of V)
pr1 (u,v,(V,u,v,u1)) is V17() V27() V28() M2( REAL )
(pr1 (u,v,(V,u,v,u1))) * u is M2( the carrier of V)
pr2 (u,v,(V,u,v,u1)) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,(V,u,v,u1))) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,(V,u,v,u1)))) * v is M2( the carrier of V)
((pr1 (u,v,(V,u,v,u1))) * u) + ((- (pr2 (u,v,(V,u,v,u1)))) * v) is M2( the carrier of V)
V is non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is V4() set
u is M2( the carrier of V)
v is M2( the carrier of V)
u1 is M2( the carrier of V)
pr2 (u,v,u1) is V17() V27() V28() M2( REAL )
(pr2 (u,v,u1)) * u is M2( the carrier of V)
pr1 (u,v,u1) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,u1)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,u1))) * v is M2( the carrier of V)
((pr2 (u,v,u1)) * u) + ((- (pr1 (u,v,u1))) * v) is M2( the carrier of V)
V is non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is V4() set
u is M2( the carrier of V)
v is M2( the carrier of V)
u1 is M2( the carrier of V)
- u1 is M2( the carrier of V)
(V,u,v,(- u1)) is M2( the carrier of V)
pr2 (u,v,(- u1)) is V17() V27() V28() M2( REAL )
(pr2 (u,v,(- u1))) * u is M2( the carrier of V)
pr1 (u,v,(- u1)) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,(- u1))) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,(- u1)))) * v is M2( the carrier of V)
((pr2 (u,v,(- u1))) * u) + ((- (pr1 (u,v,(- u1)))) * v) is M2( the carrier of V)
(V,u,v,u1) is M2( the carrier of V)
pr2 (u,v,u1) is V17() V27() V28() M2( REAL )
(pr2 (u,v,u1)) * u is M2( the carrier of V)
pr1 (u,v,u1) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,u1)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,u1))) * v is M2( the carrier of V)
((pr2 (u,v,u1)) * u) + ((- (pr1 (u,v,u1))) * v) is M2( the carrier of V)
- (V,u,v,u1) is M2( the carrier of V)
(pr1 (u,v,u1)) * u is M2( the carrier of V)
(pr2 (u,v,u1)) * v is M2( the carrier of V)
((pr1 (u,v,u1)) * u) + ((pr2 (u,v,u1)) * v) is M2( the carrier of V)
- (((pr1 (u,v,u1)) * u) + ((pr2 (u,v,u1)) * v)) is M2( the carrier of V)
- ((pr1 (u,v,u1)) * u) is M2( the carrier of V)
- ((pr2 (u,v,u1)) * v) is M2( the carrier of V)
(- ((pr1 (u,v,u1)) * u)) + (- ((pr2 (u,v,u1)) * v)) is M2( the carrier of V)
- u is M2( the carrier of V)
(pr1 (u,v,u1)) * (- u) is M2( the carrier of V)
((pr1 (u,v,u1)) * (- u)) + (- ((pr2 (u,v,u1)) * v)) is M2( the carrier of V)
(- (pr1 (u,v,u1))) * u is M2( the carrier of V)
((- (pr1 (u,v,u1))) * u) + (- ((pr2 (u,v,u1)) * v)) is M2( the carrier of V)
- v is M2( the carrier of V)
(pr2 (u,v,u1)) * (- v) is M2( the carrier of V)
((- (pr1 (u,v,u1))) * u) + ((pr2 (u,v,u1)) * (- v)) is M2( the carrier of V)
- (pr2 (u,v,u1)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,u1))) * v is M2( the carrier of V)
((- (pr1 (u,v,u1))) * u) + ((- (pr2 (u,v,u1))) * v) is M2( the carrier of V)
(- (pr2 (u,v,u1))) * u is M2( the carrier of V)
((- (pr2 (u,v,u1))) * u) + ((- (pr1 (u,v,(- u1)))) * v) is M2( the carrier of V)
- (- (pr1 (u,v,u1))) is V17() V27() V28() M2( REAL )
(- (- (pr1 (u,v,u1)))) * v is M2( the carrier of V)
((- (pr2 (u,v,u1))) * u) + ((- (- (pr1 (u,v,u1)))) * v) is M2( the carrier of V)
(pr2 (u,v,u1)) * (- u) is M2( the carrier of V)
((pr2 (u,v,u1)) * (- u)) + ((- (- (pr1 (u,v,u1)))) * v) is M2( the carrier of V)
- ((pr2 (u,v,u1)) * u) is M2( the carrier of V)
(- ((pr2 (u,v,u1)) * u)) + ((- (- (pr1 (u,v,u1)))) * v) is M2( the carrier of V)
(- (pr1 (u,v,u1))) * (- v) is M2( the carrier of V)
(- ((pr2 (u,v,u1)) * u)) + ((- (pr1 (u,v,u1))) * (- v)) is M2( the carrier of V)
- ((- (pr1 (u,v,u1))) * v) is M2( the carrier of V)
(- ((pr2 (u,v,u1)) * u)) + (- ((- (pr1 (u,v,u1))) * v)) is M2( the carrier of V)
V is non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is V4() set
u is M2( the carrier of V)
v is M2( the carrier of V)
u1 is M2( the carrier of V)
(V,u,v,u1) is M2( the carrier of V)
pr2 (u,v,u1) is V17() V27() V28() M2( REAL )
(pr2 (u,v,u1)) * u is M2( the carrier of V)
pr1 (u,v,u1) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,u1)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,u1))) * v is M2( the carrier of V)
((pr2 (u,v,u1)) * u) + ((- (pr1 (u,v,u1))) * v) is M2( the carrier of V)
v1 is M2( the carrier of V)
u1 + v1 is M2( the carrier of V)
(V,u,v,(u1 + v1)) is M2( the carrier of V)
pr2 (u,v,(u1 + v1)) is V17() V27() V28() M2( REAL )
(pr2 (u,v,(u1 + v1))) * u is M2( the carrier of V)
pr1 (u,v,(u1 + v1)) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,(u1 + v1))) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,(u1 + v1)))) * v is M2( the carrier of V)
((pr2 (u,v,(u1 + v1))) * u) + ((- (pr1 (u,v,(u1 + v1)))) * v) is M2( the carrier of V)
(V,u,v,v1) is M2( the carrier of V)
pr2 (u,v,v1) is V17() V27() V28() M2( REAL )
(pr2 (u,v,v1)) * u is M2( the carrier of V)
pr1 (u,v,v1) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,v1)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,v1))) * v is M2( the carrier of V)
((pr2 (u,v,v1)) * u) + ((- (pr1 (u,v,v1))) * v) is M2( the carrier of V)
(V,u,v,u1) + (V,u,v,v1) is M2( the carrier of V)
(pr1 (u,v,u1)) + (pr1 (u,v,v1)) is V17() V27() V28() M2( REAL )
- ((pr1 (u,v,u1)) + (pr1 (u,v,v1))) is V17() V27() V28() M2( REAL )
(- ((pr1 (u,v,u1)) + (pr1 (u,v,v1)))) * v is M2( the carrier of V)
((pr2 (u,v,(u1 + v1))) * u) + ((- ((pr1 (u,v,u1)) + (pr1 (u,v,v1)))) * v) is M2( the carrier of V)
(pr2 (u,v,u1)) + (pr2 (u,v,v1)) is V17() V27() V28() M2( REAL )
((pr2 (u,v,u1)) + (pr2 (u,v,v1))) * u is M2( the carrier of V)
(((pr2 (u,v,u1)) + (pr2 (u,v,v1))) * u) + ((- ((pr1 (u,v,u1)) + (pr1 (u,v,v1)))) * v) is M2( the carrier of V)
((pr2 (u,v,u1)) * u) + ((pr2 (u,v,v1)) * u) is M2( the carrier of V)
(((pr2 (u,v,u1)) * u) + ((pr2 (u,v,v1)) * u)) + ((- ((pr1 (u,v,u1)) + (pr1 (u,v,v1)))) * v) is M2( the carrier of V)
- v is M2( the carrier of V)
((pr1 (u,v,u1)) + (pr1 (u,v,v1))) * (- v) is M2( the carrier of V)
(((pr2 (u,v,u1)) * u) + ((pr2 (u,v,v1)) * u)) + (((pr1 (u,v,u1)) + (pr1 (u,v,v1))) * (- v)) is M2( the carrier of V)
((pr1 (u,v,u1)) + (pr1 (u,v,v1))) * v is M2( the carrier of V)
- (((pr1 (u,v,u1)) + (pr1 (u,v,v1))) * v) is M2( the carrier of V)
(((pr2 (u,v,u1)) * u) + ((pr2 (u,v,v1)) * u)) + (- (((pr1 (u,v,u1)) + (pr1 (u,v,v1))) * v)) is M2( the carrier of V)
(pr1 (u,v,u1)) * v is M2( the carrier of V)
(pr1 (u,v,v1)) * v is M2( the carrier of V)
((pr1 (u,v,u1)) * v) + ((pr1 (u,v,v1)) * v) is M2( the carrier of V)
- (((pr1 (u,v,u1)) * v) + ((pr1 (u,v,v1)) * v)) is M2( the carrier of V)
(((pr2 (u,v,u1)) * u) + ((pr2 (u,v,v1)) * u)) + (- (((pr1 (u,v,u1)) * v) + ((pr1 (u,v,v1)) * v))) is M2( the carrier of V)
- ((pr1 (u,v,u1)) * v) is M2( the carrier of V)
- ((pr1 (u,v,v1)) * v) is M2( the carrier of V)
(- ((pr1 (u,v,u1)) * v)) + (- ((pr1 (u,v,v1)) * v)) is M2( the carrier of V)
(((pr2 (u,v,u1)) * u) + ((pr2 (u,v,v1)) * u)) + ((- ((pr1 (u,v,u1)) * v)) + (- ((pr1 (u,v,v1)) * v))) is M2( the carrier of V)
((pr2 (u,v,v1)) * u) + ((- ((pr1 (u,v,u1)) * v)) + (- ((pr1 (u,v,v1)) * v))) is M2( the carrier of V)
((pr2 (u,v,u1)) * u) + (((pr2 (u,v,v1)) * u) + ((- ((pr1 (u,v,u1)) * v)) + (- ((pr1 (u,v,v1)) * v)))) is M2( the carrier of V)
((pr2 (u,v,v1)) * u) + (- ((pr1 (u,v,v1)) * v)) is M2( the carrier of V)
(- ((pr1 (u,v,u1)) * v)) + (((pr2 (u,v,v1)) * u) + (- ((pr1 (u,v,v1)) * v))) is M2( the carrier of V)
((pr2 (u,v,u1)) * u) + ((- ((pr1 (u,v,u1)) * v)) + (((pr2 (u,v,v1)) * u) + (- ((pr1 (u,v,v1)) * v)))) is M2( the carrier of V)
((pr2 (u,v,u1)) * u) + (- ((pr1 (u,v,u1)) * v)) is M2( the carrier of V)
(((pr2 (u,v,u1)) * u) + (- ((pr1 (u,v,u1)) * v))) + (((pr2 (u,v,v1)) * u) + (- ((pr1 (u,v,v1)) * v))) is M2( the carrier of V)
(pr1 (u,v,u1)) * (- v) is M2( the carrier of V)
((pr2 (u,v,u1)) * u) + ((pr1 (u,v,u1)) * (- v)) is M2( the carrier of V)
(((pr2 (u,v,u1)) * u) + ((pr1 (u,v,u1)) * (- v))) + (((pr2 (u,v,v1)) * u) + (- ((pr1 (u,v,v1)) * v))) is M2( the carrier of V)
(pr1 (u,v,v1)) * (- v) is M2( the carrier of V)
((pr2 (u,v,v1)) * u) + ((pr1 (u,v,v1)) * (- v)) is M2( the carrier of V)
(((pr2 (u,v,u1)) * u) + ((pr1 (u,v,u1)) * (- v))) + (((pr2 (u,v,v1)) * u) + ((pr1 (u,v,v1)) * (- v))) is M2( the carrier of V)
(((pr2 (u,v,u1)) * u) + ((- (pr1 (u,v,u1))) * v)) + (((pr2 (u,v,v1)) * u) + ((pr1 (u,v,v1)) * (- v))) is M2( the carrier of V)
V is non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is V4() set
u is M2( the carrier of V)
v is M2( the carrier of V)
u1 is M2( the carrier of V)
(V,u,v,u1) is M2( the carrier of V)
pr2 (u,v,u1) is V17() V27() V28() M2( REAL )
(pr2 (u,v,u1)) * u is M2( the carrier of V)
pr1 (u,v,u1) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,u1)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,u1))) * v is M2( the carrier of V)
((pr2 (u,v,u1)) * u) + ((- (pr1 (u,v,u1))) * v) is M2( the carrier of V)
v1 is M2( the carrier of V)
u1 - v1 is M2( the carrier of V)
- v1 is M2( the carrier of V)
u1 + (- v1) is M2( the carrier of V)
(V,u,v,(u1 - v1)) is M2( the carrier of V)
pr2 (u,v,(u1 - v1)) is V17() V27() V28() M2( REAL )
(pr2 (u,v,(u1 - v1))) * u is M2( the carrier of V)
pr1 (u,v,(u1 - v1)) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,(u1 - v1))) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,(u1 - v1)))) * v is M2( the carrier of V)
((pr2 (u,v,(u1 - v1))) * u) + ((- (pr1 (u,v,(u1 - v1)))) * v) is M2( the carrier of V)
(V,u,v,v1) is M2( the carrier of V)
pr2 (u,v,v1) is V17() V27() V28() M2( REAL )
(pr2 (u,v,v1)) * u is M2( the carrier of V)
pr1 (u,v,v1) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,v1)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,v1))) * v is M2( the carrier of V)
((pr2 (u,v,v1)) * u) + ((- (pr1 (u,v,v1))) * v) is M2( the carrier of V)
(V,u,v,u1) - (V,u,v,v1) is M2( the carrier of V)
- (V,u,v,v1) is M2( the carrier of V)
(V,u,v,u1) + (- (V,u,v,v1)) is M2( the carrier of V)
(V,u,v,(- v1)) is M2( the carrier of V)
pr2 (u,v,(- v1)) is V17() V27() V28() M2( REAL )
(pr2 (u,v,(- v1))) * u is M2( the carrier of V)
pr1 (u,v,(- v1)) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,(- v1))) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,(- v1)))) * v is M2( the carrier of V)
((pr2 (u,v,(- v1))) * u) + ((- (pr1 (u,v,(- v1)))) * v) is M2( the carrier of V)
(V,u,v,u1) + (V,u,v,(- v1)) is M2( the carrier of V)
V is non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is V4() set
u is M2( the carrier of V)
v is M2( the carrier of V)
u1 is M2( the carrier of V)
(V,u,v,u1) is M2( the carrier of V)
pr2 (u,v,u1) is V17() V27() V28() M2( REAL )
(pr2 (u,v,u1)) * u is M2( the carrier of V)
pr1 (u,v,u1) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,u1)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,u1))) * v is M2( the carrier of V)
((pr2 (u,v,u1)) * u) + ((- (pr1 (u,v,u1))) * v) is M2( the carrier of V)
v1 is V17() V27() V28() M2( REAL )
v1 * u1 is M2( the carrier of V)
(V,u,v,(v1 * u1)) is M2( the carrier of V)
pr2 (u,v,(v1 * u1)) is V17() V27() V28() M2( REAL )
(pr2 (u,v,(v1 * u1))) * u is M2( the carrier of V)
pr1 (u,v,(v1 * u1)) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,(v1 * u1))) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,(v1 * u1)))) * v is M2( the carrier of V)
((pr2 (u,v,(v1 * u1))) * u) + ((- (pr1 (u,v,(v1 * u1)))) * v) is M2( the carrier of V)
v1 * (V,u,v,u1) is M2( the carrier of V)
v1 * (pr2 (u,v,u1)) is V17() V27() V28() M2( REAL )
(v1 * (pr2 (u,v,u1))) * u is M2( the carrier of V)
((v1 * (pr2 (u,v,u1))) * u) + ((- (pr1 (u,v,(v1 * u1)))) * v) is M2( the carrier of V)
v1 * (pr1 (u,v,u1)) is V17() V27() V28() M2( REAL )
- (v1 * (pr1 (u,v,u1))) is V17() V27() V28() M2( REAL )
(- (v1 * (pr1 (u,v,u1)))) * v is M2( the carrier of V)
((v1 * (pr2 (u,v,u1))) * u) + ((- (v1 * (pr1 (u,v,u1)))) * v) is M2( the carrier of V)
- v is M2( the carrier of V)
(v1 * (pr1 (u,v,u1))) * (- v) is M2( the carrier of V)
((v1 * (pr2 (u,v,u1))) * u) + ((v1 * (pr1 (u,v,u1))) * (- v)) is M2( the carrier of V)
(v1 * (pr1 (u,v,u1))) * v is M2( the carrier of V)
- ((v1 * (pr1 (u,v,u1))) * v) is M2( the carrier of V)
((v1 * (pr2 (u,v,u1))) * u) + (- ((v1 * (pr1 (u,v,u1))) * v)) is M2( the carrier of V)
(pr1 (u,v,u1)) * v is M2( the carrier of V)
v1 * ((pr1 (u,v,u1)) * v) is M2( the carrier of V)
- (v1 * ((pr1 (u,v,u1)) * v)) is M2( the carrier of V)
((v1 * (pr2 (u,v,u1))) * u) + (- (v1 * ((pr1 (u,v,u1)) * v))) is M2( the carrier of V)
- ((pr1 (u,v,u1)) * v) is M2( the carrier of V)
v1 * (- ((pr1 (u,v,u1)) * v)) is M2( the carrier of V)
((v1 * (pr2 (u,v,u1))) * u) + (v1 * (- ((pr1 (u,v,u1)) * v))) is M2( the carrier of V)
v1 * ((pr2 (u,v,u1)) * u) is M2( the carrier of V)
(v1 * ((pr2 (u,v,u1)) * u)) + (v1 * (- ((pr1 (u,v,u1)) * v))) is M2( the carrier of V)
((pr2 (u,v,u1)) * u) + (- ((pr1 (u,v,u1)) * v)) is M2( the carrier of V)
v1 * (((pr2 (u,v,u1)) * u) + (- ((pr1 (u,v,u1)) * v))) is M2( the carrier of V)
(pr1 (u,v,u1)) * (- v) is M2( the carrier of V)
((pr2 (u,v,u1)) * u) + ((pr1 (u,v,u1)) * (- v)) is M2( the carrier of V)
v1 * (((pr2 (u,v,u1)) * u) + ((pr1 (u,v,u1)) * (- v))) is M2( the carrier of V)
V is non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is V4() set
u is M2( the carrier of V)
v is M2( the carrier of V)
u1 is M2( the carrier of V)
(V,u,v,u1) is M2( the carrier of V)
pr2 (u,v,u1) is V17() V27() V28() M2( REAL )
(pr2 (u,v,u1)) * u is M2( the carrier of V)
pr1 (u,v,u1) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,u1)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,u1))) * v is M2( the carrier of V)
((pr2 (u,v,u1)) * u) + ((- (pr1 (u,v,u1))) * v) is M2( the carrier of V)
v1 is M2( the carrier of V)
(V,u,v,v1) is M2( the carrier of V)
pr2 (u,v,v1) is V17() V27() V28() M2( REAL )
(pr2 (u,v,v1)) * u is M2( the carrier of V)
pr1 (u,v,v1) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,v1)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,v1))) * v is M2( the carrier of V)
((pr2 (u,v,v1)) * u) + ((- (pr1 (u,v,v1))) * v) is M2( the carrier of V)
(((pr2 (u,v,u1)) * u) + ((- (pr1 (u,v,u1))) * v)) - (((pr2 (u,v,v1)) * u) + ((- (pr1 (u,v,v1))) * v)) is M2( the carrier of V)
- (((pr2 (u,v,v1)) * u) + ((- (pr1 (u,v,v1))) * v)) is M2( the carrier of V)
(((pr2 (u,v,u1)) * u) + ((- (pr1 (u,v,u1))) * v)) + (- (((pr2 (u,v,v1)) * u) + ((- (pr1 (u,v,v1))) * v))) is M2( the carrier of V)
0. V is V60(V) M2( the carrier of V)
the ZeroF of V is M2( the carrier of V)
(((pr2 (u,v,u1)) * u) + ((- (pr1 (u,v,u1))) * v)) - ((pr2 (u,v,v1)) * u) is M2( the carrier of V)
- ((pr2 (u,v,v1)) * u) is M2( the carrier of V)
(((pr2 (u,v,u1)) * u) + ((- (pr1 (u,v,u1))) * v)) + (- ((pr2 (u,v,v1)) * u)) is M2( the carrier of V)
((((pr2 (u,v,u1)) * u) + ((- (pr1 (u,v,u1))) * v)) - ((pr2 (u,v,v1)) * u)) - ((- (pr1 (u,v,v1))) * v) is M2( the carrier of V)
- ((- (pr1 (u,v,v1))) * v) is M2( the carrier of V)
((((pr2 (u,v,u1)) * u) + ((- (pr1 (u,v,u1))) * v)) - ((pr2 (u,v,v1)) * u)) + (- ((- (pr1 (u,v,v1))) * v)) is M2( the carrier of V)
((pr2 (u,v,u1)) * u) + (- ((pr2 (u,v,v1)) * u)) is M2( the carrier of V)
(((pr2 (u,v,u1)) * u) + (- ((pr2 (u,v,v1)) * u))) + ((- (pr1 (u,v,u1))) * v) is M2( the carrier of V)
((((pr2 (u,v,u1)) * u) + (- ((pr2 (u,v,v1)) * u))) + ((- (pr1 (u,v,u1))) * v)) - ((- (pr1 (u,v,v1))) * v) is M2( the carrier of V)
((((pr2 (u,v,u1)) * u) + (- ((pr2 (u,v,v1)) * u))) + ((- (pr1 (u,v,u1))) * v)) + (- ((- (pr1 (u,v,v1))) * v)) is M2( the carrier of V)
((pr2 (u,v,u1)) * u) - ((pr2 (u,v,v1)) * u) is M2( the carrier of V)
((pr2 (u,v,u1)) * u) + (- ((pr2 (u,v,v1)) * u)) is M2( the carrier of V)
((- (pr1 (u,v,u1))) * v) - ((- (pr1 (u,v,v1))) * v) is M2( the carrier of V)
((- (pr1 (u,v,u1))) * v) + (- ((- (pr1 (u,v,v1))) * v)) is M2( the carrier of V)
(((pr2 (u,v,u1)) * u) - ((pr2 (u,v,v1)) * u)) + (((- (pr1 (u,v,u1))) * v) - ((- (pr1 (u,v,v1))) * v)) is M2( the carrier of V)
(pr2 (u,v,u1)) - (pr2 (u,v,v1)) is V17() V27() V28() M2( REAL )
((pr2 (u,v,u1)) - (pr2 (u,v,v1))) * u is M2( the carrier of V)
(((pr2 (u,v,u1)) - (pr2 (u,v,v1))) * u) + (((- (pr1 (u,v,u1))) * v) - ((- (pr1 (u,v,v1))) * v)) is M2( the carrier of V)
(- (pr1 (u,v,u1))) - (- (pr1 (u,v,v1))) is V17() V27() V28() M2( REAL )
((- (pr1 (u,v,u1))) - (- (pr1 (u,v,v1)))) * v is M2( the carrier of V)
(((pr2 (u,v,u1)) - (pr2 (u,v,v1))) * u) + (((- (pr1 (u,v,u1))) - (- (pr1 (u,v,v1)))) * v) is M2( the carrier of V)
(pr1 (u,v,v1)) * u is M2( the carrier of V)
(pr2 (u,v,v1)) * v is M2( the carrier of V)
((pr1 (u,v,v1)) * u) + ((pr2 (u,v,v1)) * v) is M2( the carrier of V)
V is non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is V4() set
u is M2( the carrier of V)
v is M2( the carrier of V)
u1 is M2( the carrier of V)
(V,u,v,u1) is M2( the carrier of V)
pr2 (u,v,u1) is V17() V27() V28() M2( REAL )
(pr2 (u,v,u1)) * u is M2( the carrier of V)
pr1 (u,v,u1) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,u1)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,u1))) * v is M2( the carrier of V)
((pr2 (u,v,u1)) * u) + ((- (pr1 (u,v,u1))) * v) is M2( the carrier of V)
(V,u,v,(V,u,v,u1)) is M2( the carrier of V)
pr2 (u,v,(V,u,v,u1)) is V17() V27() V28() M2( REAL )
(pr2 (u,v,(V,u,v,u1))) * u is M2( the carrier of V)
pr1 (u,v,(V,u,v,u1)) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,(V,u,v,u1))) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,(V,u,v,u1)))) * v is M2( the carrier of V)
((pr2 (u,v,(V,u,v,u1))) * u) + ((- (pr1 (u,v,(V,u,v,u1)))) * v) is M2( the carrier of V)
- u1 is M2( the carrier of V)
(- (pr1 (u,v,u1))) * u is M2( the carrier of V)
pr1 (u,v,(((pr2 (u,v,u1)) * u) + ((- (pr1 (u,v,u1))) * v))) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,(((pr2 (u,v,u1)) * u) + ((- (pr1 (u,v,u1))) * v)))) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,(((pr2 (u,v,u1)) * u) + ((- (pr1 (u,v,u1))) * v))))) * v is M2( the carrier of V)
((- (pr1 (u,v,u1))) * u) + ((- (pr1 (u,v,(((pr2 (u,v,u1)) * u) + ((- (pr1 (u,v,u1))) * v))))) * v) is M2( the carrier of V)
- (pr2 (u,v,u1)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,u1))) * v is M2( the carrier of V)
((- (pr1 (u,v,u1))) * u) + ((- (pr2 (u,v,u1))) * v) is M2( the carrier of V)
- u is M2( the carrier of V)
(pr1 (u,v,u1)) * (- u) is M2( the carrier of V)
((pr1 (u,v,u1)) * (- u)) + ((- (pr2 (u,v,u1))) * v) is M2( the carrier of V)
(pr1 (u,v,u1)) * u is M2( the carrier of V)
- ((pr1 (u,v,u1)) * u) is M2( the carrier of V)
(- ((pr1 (u,v,u1)) * u)) + ((- (pr2 (u,v,u1))) * v) is M2( the carrier of V)
- v is M2( the carrier of V)
(pr2 (u,v,u1)) * (- v) is M2( the carrier of V)
(- ((pr1 (u,v,u1)) * u)) + ((pr2 (u,v,u1)) * (- v)) is M2( the carrier of V)
(pr2 (u,v,u1)) * v is M2( the carrier of V)
- ((pr2 (u,v,u1)) * v) is M2( the carrier of V)
(- ((pr1 (u,v,u1)) * u)) + (- ((pr2 (u,v,u1)) * v)) is M2( the carrier of V)
((pr1 (u,v,u1)) * u) + ((pr2 (u,v,u1)) * v) is M2( the carrier of V)
- (((pr1 (u,v,u1)) * u) + ((pr2 (u,v,u1)) * v)) is M2( the carrier of V)
V is non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is V4() set
u is M2( the carrier of V)
v is M2( the carrier of V)
u1 is M2( the carrier of V)
(V,u,v,u1) is M2( the carrier of V)
pr2 (u,v,u1) is V17() V27() V28() M2( REAL )
(pr2 (u,v,u1))