:: ANALORT semantic presentation

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)) * 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)
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,(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)
- (V,u,v,(V,u,v,u1)) is M2( the carrier of V)
- u1 is M2( the carrier of V)
- (- 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
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)
x is M2( the carrier of V)
(V,u,v,x) is M2( the carrier of V)
pr2 (u,v,x) is V17() V27() V28() M2( REAL )
(pr2 (u,v,x)) * u is M2( the carrier of V)
pr1 (u,v,x) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,x)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,x))) * v is M2( the carrier of V)
((pr2 (u,v,x)) * u) + ((- (pr1 (u,v,x))) * v) is M2( the carrier of V)
y is M2( the carrier of V)
(V,u,v,y) is M2( the carrier of V)
pr2 (u,v,y) is V17() V27() V28() M2( REAL )
(pr2 (u,v,y)) * u is M2( the carrier of V)
pr1 (u,v,y) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,y)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,y))) * v is M2( the carrier of V)
((pr2 (u,v,y)) * u) + ((- (pr1 (u,v,y))) * v) is M2( the carrier of V)
v1 - u1 is M2( the carrier of V)
- u1 is M2( the carrier of V)
v1 + (- u1) is M2( the carrier of V)
y - x is M2( the carrier of V)
- x is M2( the carrier of V)
y + (- x) is M2( the carrier of V)
p is V17() V27() V28() M2( REAL )
q is V17() V27() V28() M2( REAL )
p * (v1 - u1) is M2( the carrier of V)
q * (y - x) is M2( the carrier of V)
(V,u,v,v1) - (V,u,v,u1) is M2( the carrier of V)
- (V,u,v,u1) is M2( the carrier of V)
(V,u,v,v1) + (- (V,u,v,u1)) is M2( the carrier of V)
p * ((V,u,v,v1) - (V,u,v,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)
p * (V,u,v,(v1 - u1)) is M2( the carrier of V)
(V,u,v,(q * (y - x))) is M2( the carrier of V)
pr2 (u,v,(q * (y - x))) is V17() V27() V28() M2( REAL )
(pr2 (u,v,(q * (y - x)))) * u is M2( the carrier of V)
pr1 (u,v,(q * (y - x))) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,(q * (y - x)))) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,(q * (y - x))))) * v is M2( the carrier of V)
((pr2 (u,v,(q * (y - x)))) * u) + ((- (pr1 (u,v,(q * (y - x))))) * v) is M2( the carrier of V)
(V,u,v,(y - x)) is M2( the carrier of V)
pr2 (u,v,(y - x)) is V17() V27() V28() M2( REAL )
(pr2 (u,v,(y - x))) * u is M2( the carrier of V)
pr1 (u,v,(y - x)) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,(y - x))) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,(y - x)))) * v is M2( the carrier of V)
((pr2 (u,v,(y - x))) * u) + ((- (pr1 (u,v,(y - x)))) * v) is M2( the carrier of V)
q * (V,u,v,(y - x)) is M2( the carrier of V)
(V,u,v,y) - (V,u,v,x) is M2( the carrier of V)
- (V,u,v,x) is M2( the carrier of V)
(V,u,v,y) + (- (V,u,v,x)) is M2( the carrier of V)
q * ((V,u,v,y) - (V,u,v,x)) 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)
x is M2( the carrier of V)
(V,u,v,x) is M2( the carrier of V)
pr1 (u,v,x) is V17() V27() V28() M2( REAL )
(pr1 (u,v,x)) * u is M2( the carrier of V)
pr2 (u,v,x) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,x)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,x))) * v is M2( the carrier of V)
((pr1 (u,v,x)) * u) + ((- (pr2 (u,v,x))) * v) is M2( the carrier of V)
y is M2( the carrier of V)
(V,u,v,y) is M2( the carrier of V)
pr1 (u,v,y) is V17() V27() V28() M2( REAL )
(pr1 (u,v,y)) * u is M2( the carrier of V)
pr2 (u,v,y) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,y)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,y))) * v is M2( the carrier of V)
((pr1 (u,v,y)) * u) + ((- (pr2 (u,v,y))) * v) is M2( the carrier of V)
v1 - u1 is M2( the carrier of V)
- u1 is M2( the carrier of V)
v1 + (- u1) is M2( the carrier of V)
y - x is M2( the carrier of V)
- x is M2( the carrier of V)
y + (- x) is M2( the carrier of V)
p is V17() V27() V28() M2( REAL )
q is V17() V27() V28() M2( REAL )
p * (v1 - u1) is M2( the carrier of V)
q * (y - x) is M2( the carrier of V)
(V,u,v,v1) - (V,u,v,u1) is M2( the carrier of V)
- (V,u,v,u1) is M2( the carrier of V)
(V,u,v,v1) + (- (V,u,v,u1)) is M2( the carrier of V)
p * ((V,u,v,v1) - (V,u,v,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)
p * (V,u,v,(v1 - u1)) is M2( the carrier of V)
(V,u,v,(q * (y - x))) is M2( the carrier of V)
pr1 (u,v,(q * (y - x))) is V17() V27() V28() M2( REAL )
(pr1 (u,v,(q * (y - x)))) * u is M2( the carrier of V)
pr2 (u,v,(q * (y - x))) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,(q * (y - x)))) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,(q * (y - x))))) * v is M2( the carrier of V)
((pr1 (u,v,(q * (y - x)))) * u) + ((- (pr2 (u,v,(q * (y - x))))) * v) is M2( the carrier of V)
(V,u,v,(y - x)) is M2( the carrier of V)
pr1 (u,v,(y - x)) is V17() V27() V28() M2( REAL )
(pr1 (u,v,(y - x))) * u is M2( the carrier of V)
pr2 (u,v,(y - x)) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,(y - x))) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,(y - x)))) * v is M2( the carrier of V)
((pr1 (u,v,(y - x))) * u) + ((- (pr2 (u,v,(y - x)))) * v) is M2( the carrier of V)
q * (V,u,v,(y - x)) is M2( the carrier of V)
(V,u,v,y) - (V,u,v,x) is M2( the carrier of V)
- (V,u,v,x) is M2( the carrier of V)
(V,u,v,y) + (- (V,u,v,x)) is M2( the carrier of V)
q * ((V,u,v,y) - (V,u,v,x)) 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 M2( the carrier of V)
x is M2( the carrier of V)
y 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,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,x) is M2( the carrier of V)
pr2 (u,v,x) is V17() V27() V28() M2( REAL )
(pr2 (u,v,x)) * u is M2( the carrier of V)
pr1 (u,v,x) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,x)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,x))) * v is M2( the carrier of V)
((pr2 (u,v,x)) * u) + ((- (pr1 (u,v,x))) * v) is M2( the carrier of V)
(V,u,v,y) is M2( the carrier of V)
pr2 (u,v,y) is V17() V27() V28() M2( REAL )
(pr2 (u,v,y)) * u is M2( the carrier of V)
pr1 (u,v,y) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,y)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,y))) * v is M2( the carrier of V)
((pr2 (u,v,y)) * u) + ((- (pr1 (u,v,y))) * 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)
(V,u,v,(V,u,v,v1)) is M2( the carrier of V)
pr2 (u,v,(V,u,v,v1)) is V17() V27() V28() M2( REAL )
(pr2 (u,v,(V,u,v,v1))) * u is M2( the carrier of V)
pr1 (u,v,(V,u,v,v1)) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,(V,u,v,v1))) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,(V,u,v,v1)))) * v is M2( the carrier of V)
((pr2 (u,v,(V,u,v,v1))) * u) + ((- (pr1 (u,v,(V,u,v,v1)))) * v) is M2( the carrier of V)
- u1 is M2( the carrier of V)
- v1 is M2( the carrier of V)
(- v1) - (- u1) is M2( the carrier of V)
- (- u1) is M2( the carrier of V)
(- v1) + (- (- u1)) is M2( the carrier of V)
u1 + (- v1) is M2( the carrier of V)
u1 - v1 is M2( the carrier of V)
u1 + (- v1) is M2( the carrier of 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)
v1 is M2( the carrier of V)
x is M2( the carrier of V)
y 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,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,x) is M2( the carrier of V)
pr1 (u,v,x) is V17() V27() V28() M2( REAL )
(pr1 (u,v,x)) * u is M2( the carrier of V)
pr2 (u,v,x) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,x)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,x))) * v is M2( the carrier of V)
((pr1 (u,v,x)) * u) + ((- (pr2 (u,v,x))) * v) is M2( the carrier of V)
(V,u,v,y) is M2( the carrier of V)
pr1 (u,v,y) is V17() V27() V28() M2( REAL )
(pr1 (u,v,y)) * u is M2( the carrier of V)
pr2 (u,v,y) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,y)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,y))) * v is M2( the carrier of V)
((pr1 (u,v,y)) * u) + ((- (pr2 (u,v,y))) * 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,u,v,(V,u,v,v1)) is M2( the carrier of V)
pr1 (u,v,(V,u,v,v1)) is V17() V27() V28() M2( REAL )
(pr1 (u,v,(V,u,v,v1))) * u is M2( the carrier of V)
pr2 (u,v,(V,u,v,v1)) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,(V,u,v,v1))) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,(V,u,v,v1)))) * v is M2( the carrier of V)
((pr1 (u,v,(V,u,v,v1))) * u) + ((- (pr2 (u,v,(V,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)
v1 is M2( the carrier of V)
x is M2( the carrier of V)
(V,v1,x,u) is M2( the carrier of V)
pr2 (v1,x,u) is V17() V27() V28() M2( REAL )
(pr2 (v1,x,u)) * v1 is M2( the carrier of V)
pr1 (v1,x,u) is V17() V27() V28() M2( REAL )
- (pr1 (v1,x,u)) is V17() V27() V28() M2( REAL )
(- (pr1 (v1,x,u))) * x is M2( the carrier of V)
((pr2 (v1,x,u)) * v1) + ((- (pr1 (v1,x,u))) * x) 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 M2( the carrier of V)
x is M2( the carrier of V)
(V,v1,x,u) is M2( the carrier of V)
pr1 (v1,x,u) is V17() V27() V28() M2( REAL )
(pr1 (v1,x,u)) * v1 is M2( the carrier of V)
pr2 (v1,x,u) is V17() V27() V28() M2( REAL )
- (pr2 (v1,x,u)) is V17() V27() V28() M2( REAL )
(- (pr2 (v1,x,u))) * x is M2( the carrier of V)
((pr1 (v1,x,u)) * v1) + ((- (pr2 (v1,x,u))) * x) 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 M2( the carrier of V)
x is M2( the carrier of V)
(V,v1,x,u) is M2( the carrier of V)
pr2 (v1,x,u) is V17() V27() V28() M2( REAL )
(pr2 (v1,x,u)) * v1 is M2( the carrier of V)
pr1 (v1,x,u) is V17() V27() V28() M2( REAL )
- (pr1 (v1,x,u)) is V17() V27() V28() M2( REAL )
(- (pr1 (v1,x,u))) * x is M2( the carrier of V)
((pr2 (v1,x,u)) * v1) + ((- (pr1 (v1,x,u))) * x) is M2( the carrier of V)
(V,v1,x,v) is M2( the carrier of V)
pr2 (v1,x,v) is V17() V27() V28() M2( REAL )
(pr2 (v1,x,v)) * v1 is M2( the carrier of V)
pr1 (v1,x,v) is V17() V27() V28() M2( REAL )
- (pr1 (v1,x,v)) is V17() V27() V28() M2( REAL )
(- (pr1 (v1,x,v))) * x is M2( the carrier of V)
((pr2 (v1,x,v)) * v1) + ((- (pr1 (v1,x,v))) * x) 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 M2( the carrier of V)
x is M2( the carrier of V)
(V,v1,x,u) is M2( the carrier of V)
pr1 (v1,x,u) is V17() V27() V28() M2( REAL )
(pr1 (v1,x,u)) * v1 is M2( the carrier of V)
pr2 (v1,x,u) is V17() V27() V28() M2( REAL )
- (pr2 (v1,x,u)) is V17() V27() V28() M2( REAL )
(- (pr2 (v1,x,u))) * x is M2( the carrier of V)
((pr1 (v1,x,u)) * v1) + ((- (pr2 (v1,x,u))) * x) is M2( the carrier of V)
(V,v1,x,v) is M2( the carrier of V)
pr1 (v1,x,v) is V17() V27() V28() M2( REAL )
(pr1 (v1,x,v)) * v1 is M2( the carrier of V)
pr2 (v1,x,v) is V17() V27() V28() M2( REAL )
- (pr2 (v1,x,v)) is V17() V27() V28() M2( REAL )
(- (pr2 (v1,x,v))) * x is M2( the carrier of V)
((pr1 (v1,x,v)) * v1) + ((- (pr2 (v1,x,v))) * x) 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)
(V,u,v,v1) - (V,u,v,u1) is M2( the carrier of V)
- (V,u,v,u1) is M2( the carrier of V)
(V,u,v,v1) + (- (V,u,v,u1)) is M2( the carrier of V)
v1 - u1 is M2( the carrier of V)
- u1 is M2( the carrier of V)
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)
PProJ (u,v,(v1 - u1),((V,u,v,v1) - (V,u,v,u1))) is V17() V27() V28() M2( REAL )
pr1 (u,v,((V,u,v,v1) - (V,u,v,u1))) is V17() V27() V28() M2( REAL )
(pr1 (u,v,(v1 - u1))) * (pr1 (u,v,((V,u,v,v1) - (V,u,v,u1)))) is V17() V27() V28() M2( REAL )
pr2 (u,v,((V,u,v,v1) - (V,u,v,u1))) is V17() V27() V28() M2( REAL )
(pr2 (u,v,(v1 - u1))) * (pr2 (u,v,((V,u,v,v1) - (V,u,v,u1)))) is V17() V27() V28() M2( REAL )
((pr1 (u,v,(v1 - u1))) * (pr1 (u,v,((V,u,v,v1) - (V,u,v,u1))))) + ((pr2 (u,v,(v1 - u1))) * (pr2 (u,v,((V,u,v,v1) - (V,u,v,u1))))) is V17() V27() V28() M2( REAL )
(pr1 (u,v,(v1 - u1))) * (pr2 (u,v,(v1 - u1))) is V17() V27() V28() M2( REAL )
((pr1 (u,v,(v1 - u1))) * (pr2 (u,v,(v1 - u1)))) + ((pr2 (u,v,(v1 - u1))) * (pr2 (u,v,((V,u,v,v1) - (V,u,v,u1))))) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,(v1 - u1)))) * (pr2 (u,v,(v1 - u1))) is V17() V27() V28() M2( REAL )
((pr1 (u,v,(v1 - u1))) * (pr2 (u,v,(v1 - u1)))) + ((- (pr1 (u,v,(v1 - u1)))) * (pr2 (u,v,(v1 - u1)))) 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
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)
(V,u1,v1,u) is M2( the carrier of V)
pr2 (u1,v1,u) is V17() V27() V28() M2( REAL )
(pr2 (u1,v1,u)) * u1 is M2( the carrier of V)
pr1 (u1,v1,u) is V17() V27() V28() M2( REAL )
- (pr1 (u1,v1,u)) is V17() V27() V28() M2( REAL )
(- (pr1 (u1,v1,u))) * v1 is M2( the carrier of V)
((pr2 (u1,v1,u)) * u1) + ((- (pr1 (u1,v1,u))) * v1) is M2( the carrier of V)
(V,u1,v1,v) is M2( the carrier of V)
pr2 (u1,v1,v) is V17() V27() V28() M2( REAL )
(pr2 (u1,v1,v)) * u1 is M2( the carrier of V)
pr1 (u1,v1,v) is V17() V27() V28() M2( REAL )
- (pr1 (u1,v1,v)) is V17() V27() V28() M2( REAL )
(- (pr1 (u1,v1,v))) * v1 is M2( the carrier of V)
((pr2 (u1,v1,v)) * u1) + ((- (pr1 (u1,v1,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)
v1 is M2( the carrier of V)
(V,u1,v1,u) is M2( the carrier of V)
pr1 (u1,v1,u) is V17() V27() V28() M2( REAL )
(pr1 (u1,v1,u)) * u1 is M2( the carrier of V)
pr2 (u1,v1,u) is V17() V27() V28() M2( REAL )
- (pr2 (u1,v1,u)) is V17() V27() V28() M2( REAL )
(- (pr2 (u1,v1,u))) * v1 is M2( the carrier of V)
((pr1 (u1,v1,u)) * u1) + ((- (pr2 (u1,v1,u))) * v1) is M2( the carrier of V)
(V,u1,v1,v) is M2( the carrier of V)
pr1 (u1,v1,v) is V17() V27() V28() M2( REAL )
(pr1 (u1,v1,v)) * u1 is M2( the carrier of V)
pr2 (u1,v1,v) is V17() V27() V28() M2( REAL )
- (pr2 (u1,v1,v)) is V17() V27() V28() M2( REAL )
(- (pr2 (u1,v1,v))) * v1 is M2( the carrier of V)
((pr1 (u1,v1,v)) * u1) + ((- (pr2 (u1,v1,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)
v1 is M2( the carrier of V)
x is M2( the carrier of V)
y 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)
p is V60(V) M2( the carrier of V)
(V,u,v,p) is M2( the carrier of V)
pr2 (u,v,p) is V17() V27() V28() M2( REAL )
(pr2 (u,v,p)) * u is M2( the carrier of V)
pr1 (u,v,p) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,p)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,p))) * v is M2( the carrier of V)
((pr2 (u,v,p)) * u) + ((- (pr1 (u,v,p))) * v) is M2( the carrier of V)
q is M2( the carrier of V)
(V,u,v,q) is M2( the carrier of V)
pr2 (u,v,q) is V17() V27() V28() M2( REAL )
(pr2 (u,v,q)) * u is M2( the carrier of V)
pr1 (u,v,q) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,q)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,q))) * v is M2( the carrier of V)
((pr2 (u,v,q)) * u) + ((- (pr1 (u,v,q))) * v) is M2( the carrier of V)
p is M2( the carrier of V)
(V,u,v,p) is M2( the carrier of V)
pr2 (u,v,p) is V17() V27() V28() M2( REAL )
(pr2 (u,v,p)) * u is M2( the carrier of V)
pr1 (u,v,p) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,p)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,p))) * v is M2( the carrier of V)
((pr2 (u,v,p)) * u) + ((- (pr1 (u,v,p))) * v) is M2( the carrier of V)
q is M2( the carrier of V)
(V,u,v,q) is M2( the carrier of V)
pr2 (u,v,q) is V17() V27() V28() M2( REAL )
(pr2 (u,v,q)) * u is M2( the carrier of V)
pr1 (u,v,q) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,q)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,q))) * v is M2( the carrier of V)
((pr2 (u,v,q)) * u) + ((- (pr1 (u,v,q))) * v) is M2( the carrier of V)
p is M2( the carrier of V)
(V,u,v,p) is M2( the carrier of V)
pr2 (u,v,p) is V17() V27() V28() M2( REAL )
(pr2 (u,v,p)) * u is M2( the carrier of V)
pr1 (u,v,p) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,p)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,p))) * v is M2( the carrier of V)
((pr2 (u,v,p)) * u) + ((- (pr1 (u,v,p))) * v) is M2( the carrier of V)
q is M2( the carrier of V)
(V,u,v,q) is M2( the carrier of V)
pr2 (u,v,q) is V17() V27() V28() M2( REAL )
(pr2 (u,v,q)) * u is M2( the carrier of V)
pr1 (u,v,q) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,q)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,q))) * v is M2( the carrier of V)
((pr2 (u,v,q)) * u) + ((- (pr1 (u,v,q))) * v) is M2( the carrier of V)
p is M2( the carrier of V)
q is M2( the carrier of V)
u19 is M2( the carrier of V)
u29 is M2( the carrier of V)
v19 is M2( the carrier of V)
v29 is M2( the carrier of V)
p is M2( the carrier of V)
q is M2( the carrier of V)
(V,u,v,p) is M2( the carrier of V)
pr2 (u,v,p) is V17() V27() V28() M2( REAL )
(pr2 (u,v,p)) * u is M2( the carrier of V)
pr1 (u,v,p) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,p)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,p))) * v is M2( the carrier of V)
((pr2 (u,v,p)) * u) + ((- (pr1 (u,v,p))) * v) is M2( the carrier of V)
(V,u,v,q) is M2( the carrier of V)
pr2 (u,v,q) is V17() V27() V28() M2( REAL )
(pr2 (u,v,q)) * u is M2( the carrier of V)
pr1 (u,v,q) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,q)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,q))) * v is M2( the carrier of V)
((pr2 (u,v,q)) * u) + ((- (pr1 (u,v,q))) * v) is M2( the carrier of V)
p is M2( the carrier of V)
q is M2( the carrier of V)
r is M2( the carrier of V)
s 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 M2( the carrier of V)
x is M2( the carrier of V)
y 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)
p is V60(V) M2( the carrier of V)
(V,u,v,p) is M2( the carrier of V)
pr1 (u,v,p) is V17() V27() V28() M2( REAL )
(pr1 (u,v,p)) * u is M2( the carrier of V)
pr2 (u,v,p) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,p)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,p))) * v is M2( the carrier of V)
((pr1 (u,v,p)) * u) + ((- (pr2 (u,v,p))) * v) is M2( the carrier of V)
q is M2( the carrier of V)
(V,u,v,q) is M2( the carrier of V)
pr1 (u,v,q) is V17() V27() V28() M2( REAL )
(pr1 (u,v,q)) * u is M2( the carrier of V)
pr2 (u,v,q) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,q)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,q))) * v is M2( the carrier of V)
((pr1 (u,v,q)) * u) + ((- (pr2 (u,v,q))) * v) is M2( the carrier of V)
p is M2( the carrier of V)
(V,u,v,p) is M2( the carrier of V)
pr1 (u,v,p) is V17() V27() V28() M2( REAL )
(pr1 (u,v,p)) * u is M2( the carrier of V)
pr2 (u,v,p) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,p)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,p))) * v is M2( the carrier of V)
((pr1 (u,v,p)) * u) + ((- (pr2 (u,v,p))) * v) is M2( the carrier of V)
q is M2( the carrier of V)
(V,u,v,q) is M2( the carrier of V)
pr1 (u,v,q) is V17() V27() V28() M2( REAL )
(pr1 (u,v,q)) * u is M2( the carrier of V)
pr2 (u,v,q) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,q)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,q))) * v is M2( the carrier of V)
((pr1 (u,v,q)) * u) + ((- (pr2 (u,v,q))) * v) is M2( the carrier of V)
p is M2( the carrier of V)
(V,u,v,p) is M2( the carrier of V)
pr1 (u,v,p) is V17() V27() V28() M2( REAL )
(pr1 (u,v,p)) * u is M2( the carrier of V)
pr2 (u,v,p) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,p)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,p))) * v is M2( the carrier of V)
((pr1 (u,v,p)) * u) + ((- (pr2 (u,v,p))) * v) is M2( the carrier of V)
q is M2( the carrier of V)
(V,u,v,q) is M2( the carrier of V)
pr1 (u,v,q) is V17() V27() V28() M2( REAL )
(pr1 (u,v,q)) * u is M2( the carrier of V)
pr2 (u,v,q) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,q)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,q))) * v is M2( the carrier of V)
((pr1 (u,v,q)) * u) + ((- (pr2 (u,v,q))) * v) is M2( the carrier of V)
p is M2( the carrier of V)
q is M2( the carrier of V)
u19 is M2( the carrier of V)
u29 is M2( the carrier of V)
v19 is M2( the carrier of V)
v29 is M2( the carrier of V)
p is M2( the carrier of V)
q is M2( the carrier of V)
(V,u,v,p) is M2( the carrier of V)
pr1 (u,v,p) is V17() V27() V28() M2( REAL )
(pr1 (u,v,p)) * u is M2( the carrier of V)
pr2 (u,v,p) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,p)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,p))) * v is M2( the carrier of V)
((pr1 (u,v,p)) * u) + ((- (pr2 (u,v,p))) * v) is M2( the carrier of V)
(V,u,v,q) is M2( the carrier of V)
pr1 (u,v,q) is V17() V27() V28() M2( REAL )
(pr1 (u,v,q)) * u is M2( the carrier of V)
pr2 (u,v,q) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,q)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,q))) * v is M2( the carrier of V)
((pr1 (u,v,q)) * u) + ((- (pr2 (u,v,q))) * v) is M2( the carrier of V)
p is M2( the carrier of V)
q is M2( the carrier of V)
r is M2( the carrier of V)
s 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 M2( the carrier of V)
x is M2( the carrier of V)
y is M2( the carrier of V)
v1 - u1 is M2( the carrier of V)
- u1 is M2( the carrier of V)
v1 + (- u1) 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)
y - x is M2( the carrier of V)
- x is M2( the carrier of V)
y + (- x) 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,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,v1) - (V,u,v,u1) is M2( the carrier of V)
- (V,u,v,u1) is M2( the carrier of V)
(V,u,v,v1) + (- (V,u,v,u1)) is M2( the carrier of V)
r is V17() V27() V28() M2( REAL )
r * ((V,u,v,v1) - (V,u,v,u1)) is M2( the carrier of V)
s is V17() V27() V28() M2( REAL )
s * (y - x) is M2( the carrier of V)
r is V17() V27() V28() M2( REAL )
r * ((V,u,v,v1) - (V,u,v,u1)) is M2( the carrier of V)
s is V17() V27() V28() M2( REAL )
s * (y - x) is M2( the carrier of V)
s " is V17() V27() V28() M2( REAL )
(s ") * r is V17() V27() V28() M2( REAL )
((s ") * r) * ((V,u,v,v1) - (V,u,v,u1)) is M2( the carrier of V)
(s ") * (s * (y - x)) is M2( the carrier of V)
(s ") * s is V17() V27() V28() M2( REAL )
((s ") * s) * (y - x) is M2( the carrier of V)
1 * (y - x) 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 M2( the carrier of V)
x is M2( the carrier of V)
y 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,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 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)
x is M2( the carrier of V)
y 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,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 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)
x is M2( the carrier of V)
y is M2( the carrier of V)
p 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,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 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)
x is M2( the carrier of V)
y is M2( the carrier of V)
p 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,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 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)
x is M2( the carrier of V)
y is M2( the carrier of V)
(V,x,y,u) is M2( the carrier of V)
pr2 (x,y,u) is V17() V27() V28() M2( REAL )
(pr2 (x,y,u)) * x is M2( the carrier of V)
pr1 (x,y,u) is V17() V27() V28() M2( REAL )
- (pr1 (x,y,u)) is V17() V27() V28() M2( REAL )
(- (pr1 (x,y,u))) * y is M2( the carrier of V)
((pr2 (x,y,u)) * x) + ((- (pr1 (x,y,u))) * y) is M2( the carrier of V)
(V,x,y,v) is M2( the carrier of V)
pr2 (x,y,v) is V17() V27() V28() M2( REAL )
(pr2 (x,y,v)) * x is M2( the carrier of V)
pr1 (x,y,v) is V17() V27() V28() M2( REAL )
- (pr1 (x,y,v)) is V17() V27() V28() M2( REAL )
(- (pr1 (x,y,v))) * y is M2( the carrier of V)
((pr2 (x,y,v)) * x) + ((- (pr1 (x,y,v))) * y) 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 M2( the carrier of V)
x is M2( the carrier of V)
y is M2( the carrier of V)
(V,x,y,u) is M2( the carrier of V)
pr1 (x,y,u) is V17() V27() V28() M2( REAL )
(pr1 (x,y,u)) * x is M2( the carrier of V)
pr2 (x,y,u) is V17() V27() V28() M2( REAL )
- (pr2 (x,y,u)) is V17() V27() V28() M2( REAL )
(- (pr2 (x,y,u))) * y is M2( the carrier of V)
((pr1 (x,y,u)) * x) + ((- (pr2 (x,y,u))) * y) is M2( the carrier of V)
(V,x,y,v) is M2( the carrier of V)
pr1 (x,y,v) is V17() V27() V28() M2( REAL )
(pr1 (x,y,v)) * x is M2( the carrier of V)
pr2 (x,y,v) is V17() V27() V28() M2( REAL )
- (pr2 (x,y,v)) is V17() V27() V28() M2( REAL )
(- (pr2 (x,y,v))) * y is M2( the carrier of V)
((pr1 (x,y,v)) * x) + ((- (pr2 (x,y,v))) * y) 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 M2( the carrier of V)
x is M2( the carrier of V)
y is M2( the carrier of V)
p 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,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 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)
x is M2( the carrier of V)
y is M2( the carrier of V)
p 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,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 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)
x is M2( the carrier of V)
x + u is M2( the carrier of V)
(V,u,v,x) is M2( the carrier of V)
pr2 (u,v,x) is V17() V27() V28() M2( REAL )
(pr2 (u,v,x)) * u is M2( the carrier of V)
pr1 (u,v,x) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,x)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,x))) * v is M2( the carrier of V)
((pr2 (u,v,x)) * u) + ((- (pr1 (u,v,x))) * v) is M2( the carrier of V)
y is M2( the carrier of V)
(V,u,v,y) is M2( the carrier of V)
pr2 (u,v,y) is V17() V27() V28() M2( REAL )
(pr2 (u,v,y)) * u is M2( the carrier of V)
pr1 (u,v,y) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,y)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,y))) * v is M2( the carrier of V)
((pr2 (u,v,y)) * u) + ((- (pr1 (u,v,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)
y is M2( the carrier of V)
(V,u,v,y) is M2( the carrier of V)
pr2 (u,v,y) is V17() V27() V28() M2( REAL )
(pr2 (u,v,y)) * u is M2( the carrier of V)
pr1 (u,v,y) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,y)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,y))) * v is M2( the carrier of V)
((pr2 (u,v,y)) * u) + ((- (pr1 (u,v,y))) * v) is M2( the carrier of V)
p is M2( the carrier of V)
(V,u,v,p) is M2( the carrier of V)
pr2 (u,v,p) is V17() V27() V28() M2( REAL )
(pr2 (u,v,p)) * u is M2( the carrier of V)
pr1 (u,v,p) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,p)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,p))) * v is M2( the carrier of V)
((pr2 (u,v,p)) * u) + ((- (pr1 (u,v,p))) * v) is M2( the carrier of V)
p + x is M2( the carrier of V)
(p + x) - y is M2( the carrier of V)
- y is M2( the carrier of V)
(p + x) + (- y) is M2( the carrier of V)
q is M2( the carrier of V)
(V,u,v,q) is M2( the carrier of V)
pr2 (u,v,q) is V17() V27() V28() M2( REAL )
(pr2 (u,v,q)) * u is M2( the carrier of V)
pr1 (u,v,q) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,q)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,q))) * v is M2( the carrier of V)
((pr2 (u,v,q)) * u) + ((- (pr1 (u,v,q))) * v) is M2( the carrier of V)
p - y is M2( the carrier of V)
p + (- y) is M2( the carrier of V)
x + (p - y) is M2( the carrier of V)
p is M2( the carrier of V)
r 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 M2( the carrier of V)
x is M2( the carrier of V)
x + u is M2( the carrier of V)
(V,u,v,x) is M2( the carrier of V)
pr1 (u,v,x) is V17() V27() V28() M2( REAL )
(pr1 (u,v,x)) * u is M2( the carrier of V)
pr2 (u,v,x) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,x)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,x))) * v is M2( the carrier of V)
((pr1 (u,v,x)) * u) + ((- (pr2 (u,v,x))) * v) is M2( the carrier of V)
y is M2( the carrier of V)
(V,u,v,y) is M2( the carrier of V)
pr1 (u,v,y) is V17() V27() V28() M2( REAL )
(pr1 (u,v,y)) * u is M2( the carrier of V)
pr2 (u,v,y) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,y)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,y))) * v is M2( the carrier of V)
((pr1 (u,v,y)) * u) + ((- (pr2 (u,v,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)
y is M2( the carrier of V)
(V,u,v,y) is M2( the carrier of V)
pr1 (u,v,y) is V17() V27() V28() M2( REAL )
(pr1 (u,v,y)) * u is M2( the carrier of V)
pr2 (u,v,y) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,y)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,y))) * v is M2( the carrier of V)
((pr1 (u,v,y)) * u) + ((- (pr2 (u,v,y))) * v) is M2( the carrier of V)
p is M2( the carrier of V)
(V,u,v,p) is M2( the carrier of V)
pr1 (u,v,p) is V17() V27() V28() M2( REAL )
(pr1 (u,v,p)) * u is M2( the carrier of V)
pr2 (u,v,p) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,p)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,p))) * v is M2( the carrier of V)
((pr1 (u,v,p)) * u) + ((- (pr2 (u,v,p))) * v) is M2( the carrier of V)
p + x is M2( the carrier of V)
(p + x) - y is M2( the carrier of V)
- y is M2( the carrier of V)
(p + x) + (- y) is M2( the carrier of V)
q is M2( the carrier of V)
(V,u,v,q) is M2( the carrier of V)
pr1 (u,v,q) is V17() V27() V28() M2( REAL )
(pr1 (u,v,q)) * u is M2( the carrier of V)
pr2 (u,v,q) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,q)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,q))) * v is M2( the carrier of V)
((pr1 (u,v,q)) * u) + ((- (pr2 (u,v,q))) * v) is M2( the carrier of V)
p - y is M2( the carrier of V)
p + (- y) is M2( the carrier of V)
x + (p - y) is M2( the carrier of V)
p is M2( the carrier of V)
r 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 M2( the carrier of V)
x is M2( the carrier of V)
x + u 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,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)
y 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)
y is M2( the carrier of V)
(V,u,v,y) is M2( the carrier of V)
pr2 (u,v,y) is V17() V27() V28() M2( REAL )
(pr2 (u,v,y)) * u is M2( the carrier of V)
pr1 (u,v,y) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,y)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,y))) * v is M2( the carrier of V)
((pr2 (u,v,y)) * u) + ((- (pr1 (u,v,y))) * v) is M2( the carrier of V)
p is M2( the carrier of V)
(V,u,v,p) is M2( the carrier of V)
pr2 (u,v,p) is V17() V27() V28() M2( REAL )
(pr2 (u,v,p)) * u is M2( the carrier of V)
pr1 (u,v,p) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,p)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,p))) * v is M2( the carrier of V)
((pr2 (u,v,p)) * u) + ((- (pr1 (u,v,p))) * v) is M2( the carrier of V)
y + x is M2( the carrier of V)
(y + x) - p is M2( the carrier of V)
- p is M2( the carrier of V)
(y + x) + (- p) is M2( the carrier of V)
q is M2( the carrier of V)
(V,u,v,x) is M2( the carrier of V)
pr2 (u,v,x) is V17() V27() V28() M2( REAL )
(pr2 (u,v,x)) * u is M2( the carrier of V)
pr1 (u,v,x) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,x)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,x))) * v is M2( the carrier of V)
((pr2 (u,v,x)) * u) + ((- (pr1 (u,v,x))) * v) is M2( the carrier of V)
(V,u,v,q) is M2( the carrier of V)
pr2 (u,v,q) is V17() V27() V28() M2( REAL )
(pr2 (u,v,q)) * u is M2( the carrier of V)
pr1 (u,v,q) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,q)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,q))) * v is M2( the carrier of V)
((pr2 (u,v,q)) * u) + ((- (pr1 (u,v,q))) * v) is M2( the carrier of V)
y - p is M2( the carrier of V)
y + (- p) is M2( the carrier of V)
x + (y - p) is M2( the carrier of V)
p is M2( the carrier of V)
r 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 M2( the carrier of V)
x is M2( the carrier of V)
x + u is M2( the carrier of V)
(V,u,v,x) is M2( the carrier of V)
pr1 (u,v,x) is V17() V27() V28() M2( REAL )
(pr1 (u,v,x)) * u is M2( the carrier of V)
pr2 (u,v,x) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,x)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,x))) * v is M2( the carrier of V)
((pr1 (u,v,x)) * u) + ((- (pr2 (u,v,x))) * v) is M2( the carrier of V)
y is M2( the carrier of V)
(V,u,v,y) is M2( the carrier of V)
pr1 (u,v,y) is V17() V27() V28() M2( REAL )
(pr1 (u,v,y)) * u is M2( the carrier of V)
pr2 (u,v,y) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,y)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,y))) * v is M2( the carrier of V)
((pr1 (u,v,y)) * u) + ((- (pr2 (u,v,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)
y is M2( the carrier of V)
(V,u,v,y) is M2( the carrier of V)
pr1 (u,v,y) is V17() V27() V28() M2( REAL )
(pr1 (u,v,y)) * u is M2( the carrier of V)
pr2 (u,v,y) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,y)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,y))) * v is M2( the carrier of V)
((pr1 (u,v,y)) * u) + ((- (pr2 (u,v,y))) * v) is M2( the carrier of V)
p is M2( the carrier of V)
(V,u,v,p) is M2( the carrier of V)
pr1 (u,v,p) is V17() V27() V28() M2( REAL )
(pr1 (u,v,p)) * u is M2( the carrier of V)
pr2 (u,v,p) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,p)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,p))) * v is M2( the carrier of V)
((pr1 (u,v,p)) * u) + ((- (pr2 (u,v,p))) * v) is M2( the carrier of V)
p + x is M2( the carrier of V)
(p + x) - y is M2( the carrier of V)
- y is M2( the carrier of V)
(p + x) + (- y) is M2( the carrier of V)
q is M2( the carrier of V)
(V,u,v,q) is M2( the carrier of V)
pr1 (u,v,q) is V17() V27() V28() M2( REAL )
(pr1 (u,v,q)) * u is M2( the carrier of V)
pr2 (u,v,q) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,q)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,q))) * v is M2( the carrier of V)
((pr1 (u,v,q)) * u) + ((- (pr2 (u,v,q))) * v) is M2( the carrier of V)
p - y is M2( the carrier of V)
p + (- y) is M2( the carrier of V)
x + (p - y) 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)
p is M2( the carrier of V)
r 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 M2( the carrier of V)
x is M2( the carrier of V)
y is M2( the carrier of V)
p is M2( the carrier of V)
q is M2( the carrier of V)
r is M2( the carrier of V)
s 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,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,p) is M2( the carrier of V)
pr2 (u,v,p) is V17() V27() V28() M2( REAL )
(pr2 (u,v,p)) * u is M2( the carrier of V)
pr1 (u,v,p) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,p)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,p))) * v is M2( the carrier of V)
((pr2 (u,v,p)) * u) + ((- (pr1 (u,v,p))) * v) is M2( the carrier of V)
(V,u,v,q) is M2( the carrier of V)
pr2 (u,v,q) is V17() V27() V28() M2( REAL )
(pr2 (u,v,q)) * u is M2( the carrier of V)
pr1 (u,v,q) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,q)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,q))) * v is M2( the carrier of V)
((pr2 (u,v,q)) * u) + ((- (pr1 (u,v,q))) * 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)
v1 is M2( the carrier of V)
x is M2( the carrier of V)
y is M2( the carrier of V)
p is M2( the carrier of V)
q is M2( the carrier of V)
r is M2( the carrier of V)
s 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,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,p) is M2( the carrier of V)
pr1 (u,v,p) is V17() V27() V28() M2( REAL )
(pr1 (u,v,p)) * u is M2( the carrier of V)
pr2 (u,v,p) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,p)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,p))) * v is M2( the carrier of V)
((pr1 (u,v,p)) * u) + ((- (pr2 (u,v,p))) * v) is M2( the carrier of V)
(V,u,v,q) is M2( the carrier of V)
pr1 (u,v,q) is V17() V27() V28() M2( REAL )
(pr1 (u,v,q)) * u is M2( the carrier of V)
pr2 (u,v,q) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,q)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,q))) * v is M2( the carrier of V)
((pr1 (u,v,q)) * u) + ((- (pr2 (u,v,q))) * 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)
v1 is M2( the carrier of V)
x is M2( the carrier of V)
y is M2( the carrier of V)
p is M2( the carrier of V)
q is M2( the carrier of V)
r is M2( the carrier of V)
s is M2( the carrier of V)
(V,u,v,x) is M2( the carrier of V)
pr2 (u,v,x) is V17() V27() V28() M2( REAL )
(pr2 (u,v,x)) * u is M2( the carrier of V)
pr1 (u,v,x) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,x)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,x))) * v is M2( the carrier of V)
((pr2 (u,v,x)) * u) + ((- (pr1 (u,v,x))) * v) is M2( the carrier of V)
(V,u,v,y) is M2( the carrier of V)
pr2 (u,v,y) is V17() V27() V28() M2( REAL )
(pr2 (u,v,y)) * u is M2( the carrier of V)
pr1 (u,v,y) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,y)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,y))) * v is M2( the carrier of V)
((pr2 (u,v,y)) * u) + ((- (pr1 (u,v,y))) * v) is M2( the carrier of V)
(V,u,v,r) is M2( the carrier of V)
pr2 (u,v,r) is V17() V27() V28() M2( REAL )
(pr2 (u,v,r)) * u is M2( the carrier of V)
pr1 (u,v,r) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,r)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,r))) * v is M2( the carrier of V)
((pr2 (u,v,r)) * u) + ((- (pr1 (u,v,r))) * v) is M2( the carrier of V)
(V,u,v,s) is M2( the carrier of V)
pr2 (u,v,s) is V17() V27() V28() M2( REAL )
(pr2 (u,v,s)) * u is M2( the carrier of V)
pr1 (u,v,s) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,s)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,s))) * v is M2( the carrier of V)
((pr2 (u,v,s)) * u) + ((- (pr1 (u,v,s))) * 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)
v1 is M2( the carrier of V)
x is M2( the carrier of V)
y is M2( the carrier of V)
p is M2( the carrier of V)
q is M2( the carrier of V)
r is M2( the carrier of V)
s 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,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,p) is M2( the carrier of V)
pr1 (u,v,p) is V17() V27() V28() M2( REAL )
(pr1 (u,v,p)) * u is M2( the carrier of V)
pr2 (u,v,p) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,p)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,p))) * v is M2( the carrier of V)
((pr1 (u,v,p)) * u) + ((- (pr2 (u,v,p))) * v) is M2( the carrier of V)
(V,u,v,q) is M2( the carrier of V)
pr1 (u,v,q) is V17() V27() V28() M2( REAL )
(pr1 (u,v,q)) * u is M2( the carrier of V)
pr2 (u,v,q) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,q)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,q))) * v is M2( the carrier of V)
((pr1 (u,v,q)) * u) + ((- (pr2 (u,v,q))) * 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)
v1 is M2( the carrier of V)
x is M2( the carrier of V)
y is M2( the carrier of V)
p is M2( the carrier of V)
q is M2( the carrier of V)
r is M2( the carrier of V)
s 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,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,x) is M2( the carrier of V)
pr2 (u,v,x) is V17() V27() V28() M2( REAL )
(pr2 (u,v,x)) * u is M2( the carrier of V)
pr1 (u,v,x) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,x)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,x))) * v is M2( the carrier of V)
((pr2 (u,v,x)) * u) + ((- (pr1 (u,v,x))) * v) is M2( the carrier of V)
(V,u,v,y) is M2( the carrier of V)
pr2 (u,v,y) is V17() V27() V28() M2( REAL )
(pr2 (u,v,y)) * u is M2( the carrier of V)
pr1 (u,v,y) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,y)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,y))) * v is M2( the carrier of V)
((pr2 (u,v,y)) * u) + ((- (pr1 (u,v,y))) * v) is M2( the carrier of V)
(V,u,v,r) is M2( the carrier of V)
pr2 (u,v,r) is V17() V27() V28() M2( REAL )
(pr2 (u,v,r)) * u is M2( the carrier of V)
pr1 (u,v,r) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,r)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,r))) * v is M2( the carrier of V)
((pr2 (u,v,r)) * u) + ((- (pr1 (u,v,r))) * v) is M2( the carrier of V)
(V,u,v,s) is M2( the carrier of V)
pr2 (u,v,s) is V17() V27() V28() M2( REAL )
(pr2 (u,v,s)) * u is M2( the carrier of V)
pr1 (u,v,s) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,s)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,s))) * v is M2( the carrier of V)
((pr2 (u,v,s)) * u) + ((- (pr1 (u,v,s))) * 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)
v1 is M2( the carrier of V)
x is M2( the carrier of V)
y is M2( the carrier of V)
p is M2( the carrier of V)
q is M2( the carrier of V)
r is M2( the carrier of V)
s 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,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,x) is M2( the carrier of V)
pr1 (u,v,x) is V17() V27() V28() M2( REAL )
(pr1 (u,v,x)) * u is M2( the carrier of V)
pr2 (u,v,x) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,x)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,x))) * v is M2( the carrier of V)
((pr1 (u,v,x)) * u) + ((- (pr2 (u,v,x))) * v) is M2( the carrier of V)
(V,u,v,y) is M2( the carrier of V)
pr1 (u,v,y) is V17() V27() V28() M2( REAL )
(pr1 (u,v,y)) * u is M2( the carrier of V)
pr2 (u,v,y) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,y)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,y))) * v is M2( the carrier of V)
((pr1 (u,v,y)) * u) + ((- (pr2 (u,v,y))) * v) is M2( the carrier of V)
(V,u,v,r) is M2( the carrier of V)
pr1 (u,v,r) is V17() V27() V28() M2( REAL )
(pr1 (u,v,r)) * u is M2( the carrier of V)
pr2 (u,v,r) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,r)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,r))) * v is M2( the carrier of V)
((pr1 (u,v,r)) * u) + ((- (pr2 (u,v,r))) * v) is M2( the carrier of V)
(V,u,v,s) is M2( the carrier of V)
pr1 (u,v,s) is V17() V27() V28() M2( REAL )
(pr1 (u,v,s)) * u is M2( the carrier of V)
pr2 (u,v,s) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,s)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,s))) * v is M2( the carrier of V)
((pr1 (u,v,s)) * u) + ((- (pr2 (u,v,s))) * 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)
v1 is M2( the carrier of V)
x is M2( the carrier of V)
y is M2( the carrier of V)
p is M2( the carrier of V)
q 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,y) is M2( the carrier of V)
pr2 (u,v,y) is V17() V27() V28() M2( REAL )
(pr2 (u,v,y)) * u is M2( the carrier of V)
pr1 (u,v,y) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,y)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,y))) * v is M2( the carrier of V)
((pr2 (u,v,y)) * u) + ((- (pr1 (u,v,y))) * v) is M2( the carrier of V)
(V,u,v,x) is M2( the carrier of V)
pr2 (u,v,x) is V17() V27() V28() M2( REAL )
(pr2 (u,v,x)) * u is M2( the carrier of V)
pr1 (u,v,x) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,x)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,x))) * v is M2( the carrier of V)
((pr2 (u,v,x)) * u) + ((- (pr1 (u,v,x))) * v) is M2( the carrier of V)
(V,u,v,p) is M2( the carrier of V)
pr2 (u,v,p) is V17() V27() V28() M2( REAL )
(pr2 (u,v,p)) * u is M2( the carrier of V)
pr1 (u,v,p) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,p)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,p))) * v is M2( the carrier of V)
((pr2 (u,v,p)) * u) + ((- (pr1 (u,v,p))) * v) is M2( the carrier of V)
r is M2( the carrier of V)
r is M2( the carrier of V)
s is M2( the carrier of V)
r 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)
0. V is V60(V) M2( the carrier of V)
the ZeroF of V is M2( the carrier of V)
u1 is M2( the carrier of V)
v1 is M2( the carrier of V)
u1 is M2( the carrier of V)
v1 is M2( the carrier of V)
x 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,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)
y is M2( the carrier of V)
p is M2( the carrier of V)
(V,u,v,y) is M2( the carrier of V)
pr2 (u,v,y) is V17() V27() V28() M2( REAL )
(pr2 (u,v,y)) * u is M2( the carrier of V)
pr1 (u,v,y) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,y)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,y))) * v is M2( the carrier of V)
((pr2 (u,v,y)) * u) + ((- (pr1 (u,v,y))) * v) is M2( the carrier of V)
(V,u,v,p) is M2( the carrier of V)
pr2 (u,v,p) is V17() V27() V28() M2( REAL )
(pr2 (u,v,p)) * u is M2( the carrier of V)
pr1 (u,v,p) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,p)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,p))) * v is M2( the carrier of V)
((pr2 (u,v,p)) * u) + ((- (pr1 (u,v,p))) * v) is M2( the carrier of V)
(V,u,v,x) is M2( the carrier of V)
pr2 (u,v,x) is V17() V27() V28() M2( REAL )
(pr2 (u,v,x)) * u is M2( the carrier of V)
pr1 (u,v,x) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,x)) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,x))) * v is M2( the carrier of V)
((pr2 (u,v,x)) * u) + ((- (pr1 (u,v,x))) * v) is M2( the carrier of V)
x - u1 is M2( the carrier of V)
- u1 is M2( the carrier of V)
x + (- u1) is M2( the carrier of V)
(V,u,v,x) - (V,u,v,u1) is M2( the carrier of V)
- (V,u,v,u1) is M2( the carrier of V)
(V,u,v,x) + (- (V,u,v,u1)) is M2( the carrier of V)
q is V17() V27() V28() M2( REAL )
q * (x - u1) is M2( the carrier of V)
r is V17() V27() V28() M2( REAL )
r * ((V,u,v,x) - (V,u,v,u1)) is M2( the carrier of V)
s is V17() V27() V28() M2( REAL )
s * (x - u1) is M2( the carrier of V)
(V,u,v,(x - u1)) is M2( the carrier of V)
pr2 (u,v,(x - u1)) is V17() V27() V28() M2( REAL )
(pr2 (u,v,(x - u1))) * u is M2( the carrier of V)
pr1 (u,v,(x - u1)) is V17() V27() V28() M2( REAL )
- (pr1 (u,v,(x - u1))) is V17() V27() V28() M2( REAL )
(- (pr1 (u,v,(x - u1)))) * v is M2( the carrier of V)
((pr2 (u,v,(x - u1))) * u) + ((- (pr1 (u,v,(x - u1)))) * v) is M2( the carrier of V)
u19 is V17() V27() V28() M2( REAL )
u19 * (V,u,v,(x - u1)) is M2( the carrier of V)
(pr1 (u,v,(x - u1))) * u is M2( the carrier of V)
(pr2 (u,v,(x - u1))) * v is M2( the carrier of V)
((pr1 (u,v,(x - u1))) * u) + ((pr2 (u,v,(x - u1))) * v) is M2( the carrier of V)
s * (((pr1 (u,v,(x - u1))) * u) + ((pr2 (u,v,(x - u1))) * v)) is M2( the carrier of V)
u19 * 0 is V17() V27() V28() M2( REAL )
(u19 * 0) * u is M2( the carrier of V)
u19 * (- (pr1 (u,v,(x - u1)))) is V17() V27() V28() M2( REAL )
(u19 * (- (pr1 (u,v,(x - u1))))) * v is M2( the carrier of V)
((u19 * 0) * u) + ((u19 * (- (pr1 (u,v,(x - u1))))) * v) is M2( the carrier of V)
s * (pr1 (u,v,(x - u1))) is V17() V27() V28() M2( REAL )
(s * (pr1 (u,v,(x - u1)))) * u is M2( the carrier of V)
s * (pr2 (u,v,(x - u1))) is V17() V27() V28() M2( REAL )
(s * (pr2 (u,v,(x - u1)))) * v is M2( the carrier of V)
((s * (pr1 (u,v,(x - u1)))) * u) + ((s * (pr2 (u,v,(x - u1)))) * v) is M2( the carrier of V)
0 * u is M2( the carrier of V)
0 * v is M2( the carrier of V)
(0 * u) + (0 * 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)
(0. V) + (0 * v) is M2( the carrier of V)
(0. V) + (0. V) is M2( the carrier of V)
s " is V17() V27() V28() M2( REAL )
(s ") * s is V17() V27() V28() M2( REAL )
((s ") * s) * (((pr1 (u,v,(x - u1))) * u) + ((pr2 (u,v,(x - u1))) * v)) is M2( the carrier of V)
u19 * (((pr2 (u,v,(x - u1))) * u) + ((- (pr1 (u,v,(x - u1)))) * v)) is M2( the carrier of V)
(s ") * (u19 * (((pr2 (u,v,(x - u1))) * u) + ((- (pr1 (u,v,(x - u1)))) * v))) is M2( the carrier of V)
(s ") * u19 is V17() V27() V28() M2( REAL )
((s ") * u19) * (((pr2 (u,v,(x - u1))) * u) + ((- (pr1 (u,v,(x - u1)))) * v)) is M2( the carrier of V)
1 * (((pr1 (u,v,(x - u1))) * u) + ((pr2 (u,v,(x - u1))) * v)) is M2( the carrier of V)
((s ") * u19) * (pr2 (u,v,(x - u1))) is V17() V27() V28() M2( REAL )
(((s ") * u19) * (pr2 (u,v,(x - u1)))) * u is M2( the carrier of V)
((s ") * u19) * (- (pr1 (u,v,(x - u1)))) is V17() V27() V28() M2( REAL )
(((s ") * u19) * (- (pr1 (u,v,(x - u1))))) * v is M2( the carrier of V)
((((s ") * u19) * (pr2 (u,v,(x - u1)))) * u) + ((((s ") * u19) * (- (pr1 (u,v,(x - u1))))) * v) is M2( the carrier of V)
((s ") * u19) * (((s ") * u19) * (pr2 (u,v,(x - u1)))) is V17() V27() V28() M2( REAL )
- (((s ") * u19) * (((s ") * u19) * (pr2 (u,v,(x - u1))))) is V17() V27() V28() M2( REAL )
(pr2 (u,v,(x - u1))) " is V17() V27() V28() M2( REAL )
((pr2 (u,v,(x - u1))) ") * (pr2 (u,v,(x - u1))) is V17() V27() V28() M2( REAL )
- (((pr2 (u,v,(x - u1))) ") * (pr2 (u,v,(x - u1)))) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,(x - u1))) is V17() V27() V28() M2( REAL )
((pr2 (u,v,(x - u1))) ") * (- (pr2 (u,v,(x - u1)))) is V17() V27() V28() M2( REAL )
((pr2 (u,v,(x - u1))) ") * (((s ") * u19) * (((s ") * u19) * (pr2 (u,v,(x - u1))))) is V17() V27() V28() M2( REAL )
- 1 is V17() V27() V28() M2( REAL )
((s ") * u19) * ((s ") * u19) is V17() V27() V28() M2( REAL )
(((pr2 (u,v,(x - u1))) ") * (pr2 (u,v,(x - u1)))) * (((s ") * u19) * ((s ") * u19)) is V17() V27() V28() M2( REAL )
1 * (((s ") * u19) * ((s ") * u19)) is V17() V27() V28() M2( REAL )
0 * v is M2( the carrier of V)
((pr1 (u,v,(x - u1))) * u) + (0 * v) is M2( the carrier of V)
s * (((pr1 (u,v,(x - u1))) * u) + (0 * v)) is M2( the carrier of V)
u19 * 0 is V17() V27() V28() M2( REAL )
(u19 * 0) * u is M2( the carrier of V)
u19 * (- (pr1 (u,v,(x - u1)))) is V17() V27() V28() M2( REAL )
(u19 * (- (pr1 (u,v,(x - u1))))) * v is M2( the carrier of V)
((u19 * 0) * u) + ((u19 * (- (pr1 (u,v,(x - u1))))) * v) is M2( the carrier of V)
s * (pr1 (u,v,(x - u1))) is V17() V27() V28() M2( REAL )
(s * (pr1 (u,v,(x - u1)))) * u is M2( the carrier of V)
s * 0 is V17() V27() V28() M2( REAL )
(s * 0) * v is M2( the carrier of V)
((s * (pr1 (u,v,(x - u1)))) * u) + ((s * 0) * v) is M2( the carrier of V)
0 * u is M2( the carrier of V)
- 0 is V17() V27() V28() M2( REAL )
(- 0) * v is M2( the carrier of V)
(0 * u) + ((- 0) * 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)
(0. V) + (0 * v) is M2( the carrier of V)
(0. V) + (0. V) is M2( the carrier of V)
u19 " is V17() V27() V28() M2( REAL )
(u19 ") * (s * (((pr1 (u,v,(x - u1))) * u) + ((pr2 (u,v,(x - u1))) * v))) is M2( the carrier of V)
(u19 ") * u19 is V17() V27() V28() M2( REAL )
((u19 ") * u19) * (((pr2 (u,v,(x - u1))) * u) + ((- (pr1 (u,v,(x - u1)))) * v)) is M2( the carrier of V)
(u19 ") * s is V17() V27() V28() M2( REAL )
((u19 ") * s) * (((pr1 (u,v,(x - u1))) * u) + ((pr2 (u,v,(x - u1))) * v)) is M2( the carrier of V)
1 * (((pr2 (u,v,(x - u1))) * u) + ((- (pr1 (u,v,(x - u1)))) * v)) is M2( the carrier of V)
((u19 ") * s) * (pr1 (u,v,(x - u1))) is V17() V27() V28() M2( REAL )
(((u19 ") * s) * (pr1 (u,v,(x - u1)))) * u is M2( the carrier of V)
((u19 ") * s) * (pr2 (u,v,(x - u1))) is V17() V27() V28() M2( REAL )
(((u19 ") * s) * (pr2 (u,v,(x - u1)))) * v is M2( the carrier of V)
((((u19 ") * s) * (pr1 (u,v,(x - u1)))) * u) + ((((u19 ") * s) * (pr2 (u,v,(x - u1)))) * v) is M2( the carrier of V)
- (((u19 ") * s) * (pr2 (u,v,(x - u1)))) is V17() V27() V28() M2( REAL )
((u19 ") * s) * (- (((u19 ") * s) * (pr2 (u,v,(x - u1))))) is V17() V27() V28() M2( REAL )
((u19 ") * s) * (((u19 ") * s) * (pr2 (u,v,(x - u1)))) is V17() V27() V28() M2( REAL )
((pr2 (u,v,(x - u1))) ") * (((u19 ") * s) * (((u19 ") * s) * (pr2 (u,v,(x - u1))))) is V17() V27() V28() M2( REAL )
((u19 ") * s) * ((u19 ") * s) is V17() V27() V28() M2( REAL )
(((pr2 (u,v,(x - u1))) ") * (pr2 (u,v,(x - u1)))) * (((u19 ") * s) * ((u19 ") * s)) is V17() V27() V28() M2( REAL )
1 * (((u19 ") * s) * ((u19 ") * s)) 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
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)
x is M2( the carrier of V)
y is M2( the carrier of V)
p is M2( the carrier of V)
q 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,y) is M2( the carrier of V)
pr1 (u,v,y) is V17() V27() V28() M2( REAL )
(pr1 (u,v,y)) * u is M2( the carrier of V)
pr2 (u,v,y) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,y)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,y))) * v is M2( the carrier of V)
((pr1 (u,v,y)) * u) + ((- (pr2 (u,v,y))) * v) is M2( the carrier of V)
(V,u,v,x) is M2( the carrier of V)
pr1 (u,v,x) is V17() V27() V28() M2( REAL )
(pr1 (u,v,x)) * u is M2( the carrier of V)
pr2 (u,v,x) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,x)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,x))) * v is M2( the carrier of V)
((pr1 (u,v,x)) * u) + ((- (pr2 (u,v,x))) * v) is M2( the carrier of V)
(V,u,v,p) is M2( the carrier of V)
pr1 (u,v,p) is V17() V27() V28() M2( REAL )
(pr1 (u,v,p)) * u is M2( the carrier of V)
pr2 (u,v,p) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,p)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,p))) * v is M2( the carrier of V)
((pr1 (u,v,p)) * u) + ((- (pr2 (u,v,p))) * v) is M2( the carrier of V)
r is M2( the carrier of V)
r is M2( the carrier of V)
s is M2( the carrier of V)
r 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)
0 * u is M2( the carrier of V)
0 * v is M2( the carrier of V)
(0 * u) + (0 * v) is M2( the carrier of V)
u1 is M2( the carrier of V)
1 * u is M2( the carrier of V)
1 * v is M2( the carrier of V)
(1 * u) + (1 * v) is M2( the carrier of V)
v1 is M2( the carrier of V)
- 1 is V17() V27() V28() M2( REAL )
(- 1) * v is M2( the carrier of V)
(1 * u) + ((- 1) * v) is M2( the carrier of V)
x 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 )
pr1 (u,v,v1) is V17() V27() V28() M2( REAL )
pr2 (u,v,v1) is V17() V27() V28() M2( REAL )
(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)) 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,v1) is M2( the carrier of V)
(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))) * v is M2( the carrier of V)
((pr1 (u,v,v1)) * u) + ((- (pr2 (u,v,v1))) * v) is M2( the carrier of V)
y is M2( the carrier of V)
p is M2( the carrier of V)
(V,u,v,y) is M2( the carrier of V)
pr1 (u,v,y) is V17() V27() V28() M2( REAL )
(pr1 (u,v,y)) * u is M2( the carrier of V)
pr2 (u,v,y) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,y)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,y))) * v is M2( the carrier of V)
((pr1 (u,v,y)) * u) + ((- (pr2 (u,v,y))) * v) is M2( the carrier of V)
(V,u,v,p) is M2( the carrier of V)
pr1 (u,v,p) is V17() V27() V28() M2( REAL )
(pr1 (u,v,p)) * u is M2( the carrier of V)
pr2 (u,v,p) is V17() V27() V28() M2( REAL )
- (pr2 (u,v,p)) is V17() V27() V28() M2( REAL )
(- (pr2 (u,v,p))) * v is M2( the carrier of V)
((pr1 (u,v,p)) * u) + ((- (pr2 (u,v,p))) * v) is M2( the carrier of V)
v1 - u1 is M2( the carrier of V)
- u1 is M2( the carrier of V)
v1 + (- u1) is M2( the carrier of V)
x - u1 is M2( the carrier of V)
x + (- u1) is M2( the carrier of V)
q is V17() V27() V28() M2( REAL )
q * (v1 - u1) is M2( the carrier of V)
r is V17() V27() V28() M2( REAL )
r * (x - u1) 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)
(0. V) + (0 * v) is M2( the carrier of V)
(0. V) + (0. V) is M2( the carrier of V)
s is V17() V27() V28() M2( REAL )
s * v1 is M2( the carrier of V)
x - (0. V) is M2( the carrier of V)
- (0. V) is M2( the carrier of V)
x + (- (0. V)) is M2( the carrier of V)
u19 is V17() V27() V28() M2( REAL )
u19 * (x - (0. V)) is M2( the carrier of V)
u19 * x is M2( the carrier of V)
s " is V17() V27() V28() M2( REAL )
(s ") * s is V17() V27() V28() M2( REAL )
((s ") * s) * v1 is M2( the carrier of V)
(s ") * (u19 * x) is M2( the carrier of V)
(s ") * u19 is V17() V27() V28() M2( REAL )
((s ") * u19) * x is M2( the carrier of V)
1 * v1 is M2( the carrier of V)
((s ") * u19) * 1 is V17() V27() V28() M2( REAL )
(((s ") * u19) * 1) * u is M2( the carrier of V)
((s ") * u19) * (- 1) is V17() V27() V28() M2( REAL )
(((s ") * u19) * (- 1)) * v is M2( the carrier of V)
((((s ") * u19) * 1) * u) + ((((s ") * u19) * (- 1)) * v) is M2( the carrier of V)
1 * 1 is V17() V27() V28() M2( REAL )
(1 * 1) * u is M2( the carrier of V)
(1 * 1) * v is M2( the carrier of V)
((1 * 1) * u) + ((1 * 1) * v) is M2( the carrier of V)
s * 1 is V17() V27() V28() M2( REAL )
u19 * 1 is V17() V27() V28() M2( REAL )
(s ") * (u19 * 1) is V17() V27() V28() M2( REAL )
s * ((s ") * (u19 * 1)) is V17() V27() V28() M2( REAL )
s * (s ") is V17() V27() V28() M2( REAL )
(s * (s ")) * (u19 * 1) is V17() V27() V28() M2( REAL )
((s ") * s) * (- 1) is V17() V27() V28() M2( REAL )
u19 " is V17() V27() V28() M2( REAL )
(u19 ") * s is V17() V27() V28() M2( REAL )
((u19 ") * s) * v1 is M2( the carrier of V)
(u19 ") * (u19 * x) is M2( the carrier of V)
(u19 ") * u19 is V17() V27() V28() M2( REAL )
((u19 ") * u19) * x is M2( the carrier of V)
1 * x is M2( the carrier of V)
((u19 ") * s) * 1 is V17() V27() V28() M2( REAL )
(((u19 ") * s) * 1) * u is M2( the carrier of V)
(((u19 ") * s) * 1) * v is M2( the carrier of V)
((((u19 ") * s) * 1) * u) + ((((u19 ") * s) * 1) * v) is M2( the carrier of V)
1 * (- 1) is V17() V27() V28() M2( REAL )
(1 * (- 1)) * v is M2( the carrier of V)
((1 * 1) * u) + ((1 * (- 1)) * v) is M2( the carrier of V)
(u19 ") * (s * 1) is V17() V27() V28() M2( REAL )
u19 * ((u19 ") * (s * 1)) is V17() V27() V28() M2( REAL )
u19 * (u19 ") is V17() V27() V28() M2( REAL )
(u19 * (u19 ")) * (s * 1) is V17() V27() V28() M2( REAL )
((u19 ") * u19) * 1 is V17() V27() V28() M2( REAL )
y is M2( the carrier of V)
p 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
[: the carrier of V, the carrier of V:] is set
[:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is set
bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is set
u is M2( the carrier of V)
v is M2( the carrier of V)
v1 is V7() V10([: the carrier of V, the carrier of V:]) V11([: the carrier of V, the carrier of V:]) M2( bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:])
x is set
y is set
[x,y] is set
p is M2( the carrier of V)
q is M2( the carrier of V)
[p,q] is set
r is M2( the carrier of V)
s is M2( the carrier of V)
[r,s] is set
p is M2( the carrier of V)
q is M2( the carrier of V)
[p,q] is set
r is M2( the carrier of V)
s is M2( the carrier of V)
[r,s] is set
p is M2( the carrier of V)
q is M2( the carrier of V)
[p,q] is set
r is M2( the carrier of V)
s is M2( the carrier of V)
[r,s] is set
u1 is V7() V10([: the carrier of V, the carrier of V:]) V11([: the carrier of V, the carrier of V:]) M2( bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:])
v1 is V7() V10([: the carrier of V, the carrier of V:]) V11([: the carrier of V, the carrier of V:]) M2( bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:])
x is set
y is set
[x,y] is set
p is M2( the carrier of V)
q is M2( the carrier of V)
[p,q] is set
r is M2( the carrier of V)
s is M2( the carrier of V)
[r,s] is set
p is M2( the carrier of V)
q is M2( the carrier of V)
[p,q] is set
r is M2( the carrier of V)
s is M2( the carrier of V)
[r,s] is set
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
[: the carrier of V, the carrier of V:] is set
[:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is set
bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is set
u is M2( the carrier of V)
v is M2( the carrier of V)
v1 is V7() V10([: the carrier of V, the carrier of V:]) V11([: the carrier of V, the carrier of V:]) M2( bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:])
x is set
y is set
[x,y] is set
p is M2( the carrier of V)
q is M2( the carrier of V)
[p,q] is set
r is M2( the carrier of V)
s is M2( the carrier of V)
[r,s] is set
p is M2( the carrier of V)
q is M2( the carrier of V)
[p,q] is set
r is M2( the carrier of V)
s is M2( the carrier of V)
[r,s] is set
p is M2( the carrier of V)
q is M2( the carrier of V)
[p,q] is set
r is M2( the carrier of V)
s is M2( the carrier of V)
[r,s] is set
u1 is V7() V10([: the carrier of V, the carrier of V:]) V11([: the carrier of V, the carrier of V:]) M2( bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:])
v1 is V7() V10([: the carrier of V, the carrier of V:]) V11([: the carrier of V, the carrier of V:]) M2( bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:])
x is set
y is set
[x,y] is set
p is M2( the carrier of V)
q is M2( the carrier of V)
[p,q] is set
r is M2( the carrier of V)
s is M2( the carrier of V)
[r,s] is set
p is M2( the carrier of V)
q is M2( the carrier of V)
[p,q] is set
r is M2( the carrier of V)
s is M2( the carrier of V)
[r,s] is set
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)
(V,u,v) is V7() V10([: the carrier of V, the carrier of V:]) V11([: the carrier of V, the carrier of V:]) M2( bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:])
[: the carrier of V, the carrier of V:] is set
[:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is set
bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is set
AffinStruct(# the carrier of V,(V,u,v) #) is strict AffinStruct
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)
(V,u,v) is strict AffinStruct
(V,u,v) is V7() V10([: the carrier of V, the carrier of V:]) V11([: the carrier of V, the carrier of V:]) M2( bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:])
[: the carrier of V, the carrier of V:] is set
[:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is set
bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is set
AffinStruct(# the carrier of V,(V,u,v) #) is strict AffinStruct
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)
(V,u,v) is V7() V10([: the carrier of V, the carrier of V:]) V11([: the carrier of V, the carrier of V:]) M2( bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:])
[: the carrier of V, the carrier of V:] is set
[:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is set
bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is set
AffinStruct(# the carrier of V,(V,u,v) #) is strict AffinStruct
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)
(V,u,v) is strict AffinStruct
(V,u,v) is V7() V10([: the carrier of V, the carrier of V:]) V11([: the carrier of V, the carrier of V:]) M2( bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:])
[: the carrier of V, the carrier of V:] is set
[:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is set
bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is set
AffinStruct(# the carrier of V,(V,u,v) #) is strict AffinStruct
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
v1 is non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of v1 is V4() set
u1 is set
u is M2( the carrier of V)
v is M2( the carrier of V)
(V,u,v) is non empty strict AffinStruct
(V,u,v) is V7() V10([: the carrier of V, the carrier of V:]) V11([: the carrier of V, the carrier of V:]) M2( bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:])
[: the carrier of V, the carrier of V:] is set
[:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is set
bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is set
AffinStruct(# the carrier of V,(V,u,v) #) is strict AffinStruct
the carrier of (V,u,v) is V4() set
p is set
x is M2( the carrier of v1)
y is M2( the carrier of v1)
(v1,x,y) is non empty strict AffinStruct
(v1,x,y) is V7() V10([: the carrier of v1, the carrier of v1:]) V11([: the carrier of v1, the carrier of v1:]) M2( bool [:[: the carrier of v1, the carrier of v1:],[: the carrier of v1, the carrier of v1:]:])
[: the carrier of v1, the carrier of v1:] is set
[:[: the carrier of v1, the carrier of v1:],[: the carrier of v1, the carrier of v1:]:] is set
bool [:[: the carrier of v1, the carrier of v1:],[: the carrier of v1, the carrier of v1:]:] is set
AffinStruct(# the carrier of v1,(v1,x,y) #) is strict AffinStruct
the carrier of (v1,x,y) is V4() set
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
v1 is non empty V79() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of v1 is V4() set
u1 is set
u is M2( the carrier of V)
v is M2( the carrier of V)
(V,u,v) is non empty strict AffinStruct
(V,u,v) is V7() V10([: the carrier of V, the carrier of V:]) V11([: the carrier of V, the carrier of V:]) M2( bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:])
[: the carrier of V, the carrier of V:] is set
[:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is set
bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is set
AffinStruct(# the carrier of V,(V,u,v) #) is strict AffinStruct
the carrier of (V,u,v) is V4() set
p is set
x is M2( the carrier of v1)
y is M2( the carrier of v1)
(v1,x,y) is non empty strict AffinStruct
(v1,x,y) is V7() V10([: the carrier of v1, the carrier of v1:]) V11([: the carrier of v1, the carrier of v1:]) M2( bool [:[: the carrier of v1, the carrier of v1:],[: the carrier of v1, the carrier of v1:]:])
[: the carrier of v1, the carrier of v1:] is set
[:[: the carrier of v1, the carrier of v1:],[: the carrier of v1, the carrier of v1:]:] is set
bool [:[: the carrier of v1, the carrier of v1:],[: the carrier of v1, the carrier of v1:]:] is set
AffinStruct(# the carrier of v1,(v1,x,y) #) is strict AffinStruct
the carrier of (v1,x,y) is V4() set
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)
x is M2( the carrier of V)
y is M2( the carrier of V)
(V,x,y) is non empty strict AffinStruct
(V,x,y) is V7() V10([: the carrier of V, the carrier of V:]) V11([: the carrier of V, the carrier of V:]) M2( bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:])
[: the carrier of V, the carrier of V:] is set
[:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is set
bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is set
AffinStruct(# the carrier of V,(V,x,y) #) is strict AffinStruct
the carrier of (V,x,y) is V4() set
p is M2( the carrier of (V,x,y))
q is M2( the carrier of (V,x,y))
r is M2( the carrier of (V,x,y))
s is M2( the carrier of (V,x,y))
[p,q] is set
[r,s] is set
[[p,q],[r,s]] is set
the CONGR of (V,x,y) is V7() V10([: the carrier of (V,x,y), the carrier of (V,x,y):]) V11([: the carrier of (V,x,y), the carrier of (V,x,y):]) M2( bool [:[: the carrier of (V,x,y), the carrier of (V,x,y):],[: the carrier of (V,x,y), the carrier of (V,x,y):]:])
[: the carrier of (V,x,y), the carrier of (V,x,y):] is set
[:[: the carrier of (V,x,y), the carrier of (V,x,y):],[: the carrier of (V,x,y), the carrier of (V,x,y):]:] is set
bool [:[: the carrier of (V,x,y), the carrier of (V,x,y):],[: the carrier of (V,x,y), the carrier of (V,x,y):]:] is set
[u,v] is set
[u1,v1] is set
u19 is M2( the carrier of V)
u29 is M2( the carrier of V)
[u19,u29] is set
v19 is M2( the carrier of V)
v29 is M2( the carrier of V)
[v19,v29] is set
[u,v] is set
[u1,v1] is set
[[u,v],[u1,v1]] is set
the CONGR of AffinStruct(# the carrier of V,(V,x,y) #) is V7() V10([: the carrier of AffinStruct(# the carrier of V,(V,x,y) #), the carrier of AffinStruct(# the carrier of V,(V,x,y) #):]) V11([: the carrier of AffinStruct(# the carrier of V,(V,x,y) #), the carrier of AffinStruct(# the carrier of V,(V,x,y) #):]) M2( bool [:[: the carrier of AffinStruct(# the carrier of V,(V,x,y) #), the carrier of AffinStruct(# the carrier of V,(V,x,y) #):],[: the carrier of AffinStruct(# the carrier of V,(V,x,y) #), the carrier of AffinStruct(# the carrier of V,(V,x,y) #):]:])
the carrier of AffinStruct(# the carrier of V,(V,x,y) #) is set
[: the carrier of AffinStruct(# the carrier of V,(V,x,y) #), the carrier of AffinStruct(# the carrier of V,(V,x,y) #):] is set
[:[: the carrier of AffinStruct(# the carrier of V,(V,x,y) #), the carrier of AffinStruct(# the carrier of V,(V,x,y) #):],[: the carrier of AffinStruct(# the carrier of V,(V,x,y) #), the carrier of AffinStruct(# the carrier of V,(V,x,y) #):]:] is set
bool [:[: the carrier of AffinStruct(# the carrier of V,(V,x,y) #), the carrier of AffinStruct(# the carrier of V,(V,x,y) #):],[: the carrier of AffinStruct(# the carrier of V,(V,x,y) #), the carrier of AffinStruct(# the carrier of V,(V,x,y) #):]:] is set
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)
x is M2( the carrier of V)
y is M2( the carrier of V)
(V,x,y) is non empty strict AffinStruct
(V,x,y) is V7() V10([: the carrier of V, the carrier of V:]) V11([: the carrier of V, the carrier of V:]) M2( bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:])
[: the carrier of V, the carrier of V:] is set
[:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is set
bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is set
AffinStruct(# the carrier of V,(V,x,y) #) is strict AffinStruct
the carrier of (V,x,y) is V4() set
p is M2( the carrier of (V,x,y))
q is M2( the carrier of (V,x,y))
r is M2( the carrier of (V,x,y))
s is M2( the carrier of (V,x,y))
[p,q] is set
[r,s] is set
[[p,q],[r,s]] is set
the CONGR of (V,x,y) is V7() V10([: the carrier of (V,x,y), the carrier of (V,x,y):]) V11([: the carrier of (V,x,y), the carrier of (V,x,y):]) M2( bool [:[: the carrier of (V,x,y), the carrier of (V,x,y):],[: the carrier of (V,x,y), the carrier of (V,x,y):]:])
[: the carrier of (V,x,y), the carrier of (V,x,y):] is set
[:[: the carrier of (V,x,y), the carrier of (V,x,y):],[: the carrier of (V,x,y), the carrier of (V,x,y):]:] is set
bool [:[: the carrier of (V,x,y), the carrier of (V,x,y):],[: the carrier of (V,x,y), the carrier of (V,x,y):]:] is set
[u,v] is set
[u1,v1] is set
u19 is M2( the carrier of V)
u29 is M2( the carrier of V)
[u19,u29] is set
v19 is M2( the carrier of V)
v29 is M2( the carrier of V)
[v19,v29] is set
[u,v] is set
[u1,v1] is set
[[u,v],[u1,v1]] is set
the CONGR of AffinStruct(# the carrier of V,(V,x,y) #) is V7() V10([: the carrier of AffinStruct(# the carrier of V,(V,x,y) #), the carrier of AffinStruct(# the carrier of V,(V,x,y) #):]) V11([: the carrier of AffinStruct(# the carrier of V,(V,x,y) #), the carrier of AffinStruct(# the carrier of V,(V,x,y) #):]) M2( bool [:[: the carrier of AffinStruct(# the carrier of V,(V,x,y) #), the carrier of AffinStruct(# the carrier of V,(V,x,y) #):],[: the carrier of AffinStruct(# the carrier of V,(V,x,y) #), the carrier of AffinStruct(# the carrier of V,(V,x,y) #):]:])
the carrier of AffinStruct(# the carrier of V,(V,x,y) #) is set
[: the carrier of AffinStruct(# the carrier of V,(V,x,y) #), the carrier of AffinStruct(# the carrier of V,(V,x,y) #):] is set
[:[: the carrier of AffinStruct(# the carrier of V,(V,x,y) #), the carrier of AffinStruct(# the carrier of V,(V,x,y) #):],[: the carrier of AffinStruct(# the carrier of V,(V,x,y) #), the carrier of AffinStruct(# the carrier of V,(V,x,y) #):]:] is set
bool [:[: the carrier of AffinStruct(# the carrier of V,(V,x,y) #), the carrier of AffinStruct(# the carrier of V,(V,x,y) #):],[: the carrier of AffinStruct(# the carrier of V,(V,x,y) #), the carrier of AffinStruct(# the carrier of V,(V,x,y) #):]:] is set