:: ANALOAF semantic presentation

REAL is V16() V17() V18() V22() set
NAT is V16() V17() V18() V19() V20() V21() V22() M2( bool REAL)
bool REAL is non empty set
NAT is V16() V17() V18() V19() V20() V21() V22() set
bool NAT is non empty set
bool NAT is non empty set
{} is empty trivial V16() V17() V18() V19() V20() V21() V22() set
1 is V1() V2() V3() non empty V13() V14() V15() V16() V17() V18() V19() V20() V21() M3( REAL , NAT )
0 is V1() V2() V3() empty trivial V13() V14() V15() V16() V17() V18() V19() V20() V21() V22() M3( REAL , NAT )
- 1 is V1() V14() V15() M2( REAL )
K44(0) is V14() set
V is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
V is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
S - v is M2( the carrier of V)
- v is M2( the carrier of V)
K176(V,S,(- v)) is M2( the carrier of V)
b is M2( the carrier of V)
v - b is M2( the carrier of V)
- b is M2( the carrier of V)
K176(V,v,(- b)) is M2( the carrier of V)
(S - v) + (v - b) is M2( the carrier of V)
S - b is M2( the carrier of V)
K176(V,S,(- b)) is M2( the carrier of V)
v - (v - b) is M2( the carrier of V)
- (v - b) is M2( the carrier of V)
K176(V,v,(- (v - b))) is M2( the carrier of V)
S - (v - (v - b)) is M2( the carrier of V)
- (v - (v - b)) is M2( the carrier of V)
K176(V,S,(- (v - (v - b)))) is M2( the carrier of V)
v - v is M2( the carrier of V)
K176(V,v,(- v)) is M2( the carrier of V)
(v - v) + b is M2( the carrier of V)
S - ((v - v) + b) is M2( the carrier of V)
- ((v - v) + b) is M2( the carrier of V)
K176(V,S,(- ((v - v) + b))) is M2( the carrier of V)
0. V is V59(V) M2( the carrier of V)
the ZeroF of V is M2( the carrier of V)
(0. V) + b is M2( the carrier of V)
S - ((0. V) + b) is M2( the carrier of V)
- ((0. V) + b) is M2( the carrier of V)
K176(V,S,(- ((0. V) + b))) is M2( the carrier of V)
V is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
S + v is M2( the carrier of V)
b is M2( the carrier of V)
b - v is M2( the carrier of V)
- v is M2( the carrier of V)
K176(V,b,(- v)) is M2( the carrier of V)
c is M2( the carrier of V)
b + c is M2( the carrier of V)
S - c is M2( the carrier of V)
- c is M2( the carrier of V)
K176(V,S,(- c)) is M2( the carrier of V)
0. V is V59(V) M2( the carrier of V)
the ZeroF of V is M2( the carrier of V)
S + (0. V) is M2( the carrier of V)
(S + (0. V)) - c is M2( the carrier of V)
K176(V,(S + (0. V)),(- c)) is M2( the carrier of V)
v - v is M2( the carrier of V)
K176(V,v,(- v)) is M2( the carrier of V)
S + (v - v) is M2( the carrier of V)
(S + (v - v)) - c is M2( the carrier of V)
K176(V,(S + (v - v)),(- c)) is M2( the carrier of V)
(b + c) + (- v) is M2( the carrier of V)
((b + c) + (- v)) - c is M2( the carrier of V)
K176(V,((b + c) + (- v)),(- c)) is M2( the carrier of V)
(b + c) - c is M2( the carrier of V)
K176(V,(b + c),(- c)) is M2( the carrier of V)
(- v) + ((b + c) - c) is M2( the carrier of V)
V is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
S - v is M2( the carrier of V)
- v is M2( the carrier of V)
K176(V,S,(- v)) is M2( the carrier of V)
v - S is M2( the carrier of V)
- S is M2( the carrier of V)
K176(V,v,(- S)) is M2( the carrier of V)
b is V1() V14() V15() M2( REAL )
b * (S - v) is M2( the carrier of V)
b * (v - S) is M2( the carrier of V)
- (b * (v - S)) is M2( the carrier of V)
(b * (v - S)) + (b * (S - v)) is M2( the carrier of V)
- (v - S) is M2( the carrier of V)
b * (- (v - S)) is M2( the carrier of V)
(b * (v - S)) + (b * (- (v - S))) is M2( the carrier of V)
(b * (v - S)) - (b * (v - S)) is M2( the carrier of V)
K176(V,(b * (v - S)),(- (b * (v - S)))) is M2( the carrier of V)
0. V is V59(V) M2( the carrier of V)
the ZeroF of V is M2( the carrier of V)
V is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
S - v is M2( the carrier of V)
- v is M2( the carrier of V)
K176(V,S,(- v)) is M2( the carrier of V)
v - S is M2( the carrier of V)
- S is M2( the carrier of V)
K176(V,v,(- S)) is M2( the carrier of V)
b is V1() V14() V15() M2( REAL )
c is V1() V14() V15() M2( REAL )
b - c is V1() V14() V15() M2( REAL )
(b - c) * (S - v) is M2( the carrier of V)
c - b is V1() V14() V15() M2( REAL )
(c - b) * (v - S) is M2( the carrier of V)
- (v - S) is M2( the carrier of V)
- (c - b) is V1() V14() V15() M2( REAL )
(- (c - b)) * (- (v - S)) is M2( the carrier of V)
V is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
b is V1() V14() V15() M2( REAL )
b * S is M2( the carrier of V)
b " is V1() V14() V15() M2( REAL )
(b ") * v is M2( the carrier of V)
1 * S is M2( the carrier of V)
(b ") * b is V1() V14() V15() M2( REAL )
((b ") * b) * S is M2( the carrier of V)
V is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
b is V1() V14() V15() M2( REAL )
b * S is M2( the carrier of V)
b " is V1() V14() V15() M2( REAL )
(b ") * v is M2( the carrier of V)
(b ") " is V1() V14() V15() M2( REAL )
((b ") ") * S is M2( the carrier of V)
V is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
v - S is M2( the carrier of V)
- S is M2( the carrier of V)
K176(V,v,(- S)) is M2( the carrier of V)
b is M2( the carrier of V)
c is M2( the carrier of V)
c - b is M2( the carrier of V)
- b is M2( the carrier of V)
K176(V,c,(- b)) is M2( the carrier of V)
d is V1() V14() V15() M2( REAL )
a9 is V1() V14() V15() M2( REAL )
d * (v - S) is M2( the carrier of V)
a9 * (c - b) is M2( the carrier of V)
V is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
v - S is M2( the carrier of V)
- S is M2( the carrier of V)
K176(V,v,(- S)) is M2( the carrier of V)
1 * (v - S) is M2( the carrier of V)
V is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
c is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of c is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
b is M2( the carrier of V)
d is M2( the carrier of c)
a9 is M2( the carrier of c)
b9 is M2( the carrier of c)
V is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
v - S is M2( the carrier of V)
- S is M2( the carrier of V)
K176(V,v,(- S)) is M2( the carrier of V)
S - v is M2( the carrier of V)
- v is M2( the carrier of V)
K176(V,S,(- v)) is M2( the carrier of V)
b is V1() V14() V15() M2( REAL )
b * (v - S) is M2( the carrier of V)
c is V1() V14() V15() M2( REAL )
c * (S - v) is M2( the carrier of V)
c * (v - S) is M2( the carrier of V)
- (c * (v - S)) is M2( the carrier of V)
(c * (v - S)) + (b * (v - S)) is M2( the carrier of V)
0. V is V59(V) M2( the carrier of V)
the ZeroF of V is M2( the carrier of V)
c + b is V1() V14() V15() M2( REAL )
(c + b) * (v - S) is M2( the carrier of V)
(- S) + v is M2( the carrier of V)
- (- S) is M2( the carrier of V)
V is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
b is M2( the carrier of V)
c is M2( the carrier of V)
d is M2( the carrier of V)
a9 is M2( the carrier of V)
v - S is M2( the carrier of V)
- S is M2( the carrier of V)
K176(V,v,(- S)) is M2( the carrier of V)
c - b is M2( the carrier of V)
- b is M2( the carrier of V)
K176(V,c,(- b)) is M2( the carrier of V)
b9 is V1() V14() V15() M2( REAL )
b9 * (v - S) is M2( the carrier of V)
c9 is V1() V14() V15() M2( REAL )
c9 * (c - b) is M2( the carrier of V)
b9 " is V1() V14() V15() M2( REAL )
(b9 ") * c9 is V1() V14() V15() M2( REAL )
a9 - d is M2( the carrier of V)
- d is M2( the carrier of V)
K176(V,a9,(- d)) is M2( the carrier of V)
d9 is V1() V14() V15() M2( REAL )
d9 * (v - S) is M2( the carrier of V)
t9 is V1() V14() V15() M2( REAL )
t9 * (a9 - d) is M2( the carrier of V)
d9 " is V1() V14() V15() M2( REAL )
(d9 ") * (t9 * (a9 - d)) is M2( the carrier of V)
(d9 ") * t9 is V1() V14() V15() M2( REAL )
((d9 ") * t9) * (a9 - d) is M2( the carrier of V)
(b9 ") * (c9 * (c - b)) is M2( the carrier of V)
((b9 ") * c9) * (c - b) is M2( the carrier of V)
V is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
b is M2( the carrier of V)
c is M2( the carrier of V)
v - S is M2( the carrier of V)
- S is M2( the carrier of V)
K176(V,v,(- S)) is M2( the carrier of V)
c - b is M2( the carrier of V)
- b is M2( the carrier of V)
K176(V,c,(- b)) is M2( the carrier of V)
d is V1() V14() V15() M2( REAL )
d * (v - S) is M2( the carrier of V)
a9 is V1() V14() V15() M2( REAL )
a9 * (c - b) is M2( the carrier of V)
S - v is M2( the carrier of V)
- v is M2( the carrier of V)
K176(V,S,(- v)) is M2( the carrier of V)
d * (S - v) is M2( the carrier of V)
- (a9 * (c - b)) is M2( the carrier of V)
b - c is M2( the carrier of V)
- c is M2( the carrier of V)
K176(V,b,(- c)) is M2( the carrier of V)
a9 * (b - c) is M2( the carrier of V)
V is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
b is M2( the carrier of V)
v - S is M2( the carrier of V)
- S is M2( the carrier of V)
K176(V,v,(- S)) is M2( the carrier of V)
b - v is M2( the carrier of V)
- v is M2( the carrier of V)
K176(V,b,(- v)) is M2( the carrier of V)
c is V1() V14() V15() M2( REAL )
c * (v - S) is M2( the carrier of V)
d is V1() V14() V15() M2( REAL )
d * (b - v) is M2( the carrier of V)
c + d is V1() V14() V15() M2( REAL )
b - S is M2( the carrier of V)
K176(V,b,(- S)) is M2( the carrier of V)
d * (b - S) is M2( the carrier of V)
(b - v) + (v - S) is M2( the carrier of V)
d * ((b - v) + (v - S)) is M2( the carrier of V)
d * (v - S) is M2( the carrier of V)
(c * (v - S)) + (d * (v - S)) is M2( the carrier of V)
(c + d) * (v - S) is M2( the carrier of V)
V is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
b is M2( the carrier of V)
v - S is M2( the carrier of V)
- S is M2( the carrier of V)
K176(V,v,(- S)) is M2( the carrier of V)
b - S is M2( the carrier of V)
K176(V,b,(- S)) is M2( the carrier of V)
c is V1() V14() V15() M2( REAL )
c * (v - S) is M2( the carrier of V)
d is V1() V14() V15() M2( REAL )
d * (b - S) is M2( the carrier of V)
b - v is M2( the carrier of V)
- v is M2( the carrier of V)
K176(V,b,(- v)) is M2( the carrier of V)
S - v is M2( the carrier of V)
K176(V,S,(- v)) is M2( the carrier of V)
(b - S) + (S - v) is M2( the carrier of V)
(b - S) - (v - S) is M2( the carrier of V)
- (v - S) is M2( the carrier of V)
K176(V,(b - S),(- (v - S))) is M2( the carrier of V)
c * (b - v) is M2( the carrier of V)
c * (b - S) is M2( the carrier of V)
(c * (b - S)) - (d * (b - S)) is M2( the carrier of V)
- (d * (b - S)) is M2( the carrier of V)
K176(V,(c * (b - S)),(- (d * (b - S)))) is M2( the carrier of V)
c - d is V1() V14() V15() M2( REAL )
(c - d) * (b - S) is M2( the carrier of V)
S - b is M2( the carrier of V)
- b is M2( the carrier of V)
K176(V,S,(- b)) is M2( the carrier of V)
d - c is V1() V14() V15() M2( REAL )
(d - c) * (S - b) is M2( the carrier of V)
v - b is M2( the carrier of V)
K176(V,v,(- b)) is M2( the carrier of V)
(v - S) + (S - b) is M2( the carrier of V)
(v - S) - (b - S) is M2( the carrier of V)
- (b - S) is M2( the carrier of V)
K176(V,(v - S),(- (b - S))) is M2( the carrier of V)
d * (v - b) is M2( the carrier of V)
d * (v - S) is M2( the carrier of V)
(d * (v - S)) - (c * (v - S)) is M2( the carrier of V)
- (c * (v - S)) is M2( the carrier of V)
K176(V,(d * (v - S)),(- (c * (v - S)))) is M2( the carrier of V)
(d - c) * (v - S) is M2( the carrier of V)
(c - d) * (S - v) is M2( the carrier of V)
(- S) + v is M2( the carrier of V)
(- S) + b is M2( the carrier of V)
V is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
S - v is M2( the carrier of V)
- v is M2( the carrier of V)
K176(V,S,(- v)) is M2( the carrier of V)
b is M2( the carrier of V)
c is M2( the carrier of V)
b - c is M2( the carrier of V)
- c is M2( the carrier of V)
K176(V,b,(- c)) is M2( the carrier of V)
1 * (S - v) is M2( the carrier of V)
1 * (b - c) is M2( the carrier of V)
V is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
b is M2( the carrier of V)
v + b is M2( the carrier of V)
c is M2( the carrier of V)
(v + b) - c is M2( the carrier of V)
- c is M2( the carrier of V)
K176(V,(v + b),(- c)) is M2( the carrier of V)
((v + b) - c) + c is M2( the carrier of V)
((v + b) - c) - v is M2( the carrier of V)
- v is M2( the carrier of V)
K176(V,((v + b) - c),(- v)) is M2( the carrier of V)
b - c is M2( the carrier of V)
K176(V,b,(- c)) is M2( the carrier of V)
((v + b) - c) - b is M2( the carrier of V)
- b is M2( the carrier of V)
K176(V,((v + b) - c),(- b)) is M2( the carrier of V)
v - c is M2( the carrier of V)
K176(V,v,(- c)) is M2( the carrier of V)
V is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
b is M2( the carrier of V)
c is M2( the carrier of V)
d is M2( the carrier of V)
c + d is M2( the carrier of V)
(c + d) - b is M2( the carrier of V)
- b is M2( the carrier of V)
K176(V,(c + d),(- b)) is M2( the carrier of V)
a9 is M2( the carrier of V)
d - b is M2( the carrier of V)
K176(V,d,(- b)) is M2( the carrier of V)
c + (d - b) is M2( the carrier of V)
0. V is V59(V) M2( the carrier of V)
the ZeroF of V is M2( the carrier of V)
a9 is M2( the carrier of V)
a9 is M2( the carrier of V)
c9 is M2( the carrier of V)
V is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
b is M2( the carrier of V)
c is M2( the carrier of V)
S - v is M2( the carrier of V)
- v is M2( the carrier of V)
K176(V,S,(- v)) is M2( the carrier of V)
b - S is M2( the carrier of V)
- S is M2( the carrier of V)
K176(V,b,(- S)) is M2( the carrier of V)
d is V1() V14() V15() M2( REAL )
d * (S - v) is M2( the carrier of V)
a9 is V1() V14() V15() M2( REAL )
a9 * (b - S) is M2( the carrier of V)
S - c is M2( the carrier of V)
- c is M2( the carrier of V)
K176(V,S,(- c)) is M2( the carrier of V)
a9 " is V1() V14() V15() M2( REAL )
(a9 ") * d is V1() V14() V15() M2( REAL )
((a9 ") * d) * (S - c) is M2( the carrier of V)
(((a9 ") * d) * (S - c)) + S is M2( the carrier of V)
((((a9 ") * d) * (S - c)) + S) - S is M2( the carrier of V)
K176(V,((((a9 ") * d) * (S - c)) + S),(- S)) is M2( the carrier of V)
d * (S - c) is M2( the carrier of V)
(a9 ") * (d * (S - c)) is M2( the carrier of V)
((((a9 ") * d) * (S - c)) + S) - b is M2( the carrier of V)
- b is M2( the carrier of V)
K176(V,((((a9 ") * d) * (S - c)) + S),(- b)) is M2( the carrier of V)
S - b is M2( the carrier of V)
K176(V,S,(- b)) is M2( the carrier of V)
(((((a9 ") * d) * (S - c)) + S) - S) + (S - b) is M2( the carrier of V)
(((((a9 ") * d) * (S - c)) + S) - S) - (b - S) is M2( the carrier of V)
- (b - S) is M2( the carrier of V)
K176(V,(((((a9 ") * d) * (S - c)) + S) - S),(- (b - S))) is M2( the carrier of V)
v - c is M2( the carrier of V)
K176(V,v,(- c)) is M2( the carrier of V)
v - S is M2( the carrier of V)
K176(V,v,(- S)) is M2( the carrier of V)
(S - c) + (v - S) is M2( the carrier of V)
(S - c) - (S - v) is M2( the carrier of V)
- (S - v) is M2( the carrier of V)
K176(V,(S - c),(- (S - v))) is M2( the carrier of V)
d * (v - c) is M2( the carrier of V)
(d * (S - c)) - (d * (S - v)) is M2( the carrier of V)
- (d * (S - v)) is M2( the carrier of V)
K176(V,(d * (S - c)),(- (d * (S - v)))) is M2( the carrier of V)
a9 * (((((a9 ") * d) * (S - c)) + S) - S) is M2( the carrier of V)
(a9 * (((((a9 ") * d) * (S - c)) + S) - S)) - (a9 * (b - S)) is M2( the carrier of V)
- (a9 * (b - S)) is M2( the carrier of V)
K176(V,(a9 * (((((a9 ") * d) * (S - c)) + S) - S)),(- (a9 * (b - S)))) is M2( the carrier of V)
a9 * (((((a9 ") * d) * (S - c)) + S) - b) is M2( the carrier of V)
1 * (((((a9 ") * d) * (S - c)) + S) - S) is M2( the carrier of V)
d is M2( the carrier of V)
d is M2( the carrier of V)
a9 is M2( the carrier of V)
V is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
0. V is V59(V) M2( the carrier of V)
the ZeroF of V is M2( the carrier of V)
S is M2( the carrier of V)
v is M2( the carrier of V)
S - v is M2( the carrier of V)
- v is M2( the carrier of V)
K176(V,S,(- v)) is M2( the carrier of V)
1 * S is M2( the carrier of V)
(1 * S) + (- v) is M2( the carrier of V)
(- 1) * v is M2( the carrier of V)
(1 * S) + ((- 1) * v) is M2( the carrier of V)
1 * S is M2( the carrier of V)
(1 * S) + (0. V) is M2( the carrier of V)
0 * v is M2( the carrier of V)
(1 * S) + (0 * v) is M2( the carrier of V)
1 * v is M2( the carrier of V)
(0. V) + (1 * v) is M2( the carrier of V)
0 * S is M2( the carrier of V)
(0 * S) + (1 * v) is M2( the carrier of V)
V is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
0. V is V59(V) M2( the carrier of V)
the ZeroF of V is M2( the carrier of V)
S is M2( the carrier of V)
v is M2( the carrier of V)
S - (0. V) is M2( the carrier of V)
- (0. V) is M2( the carrier of V)
K176(V,S,(- (0. V))) is M2( the carrier of V)
(0. V) - v is M2( the carrier of V)
- v is M2( the carrier of V)
K176(V,(0. V),(- v)) is M2( the carrier of V)
b is V1() V14() V15() M2( REAL )
c is V1() V14() V15() M2( REAL )
b * (S - (0. V)) is M2( the carrier of V)
c * ((0. V) - v) is M2( the carrier of V)
b * S is M2( the carrier of V)
c * (- v) is M2( the carrier of V)
c * v is M2( the carrier of V)
- (c * v) is M2( the carrier of V)
(b * S) + (c * v) is M2( the carrier of V)
S - (0. V) is M2( the carrier of V)
- (0. V) is M2( the carrier of V)
K176(V,S,(- (0. V))) is M2( the carrier of V)
v - (0. V) is M2( the carrier of V)
K176(V,v,(- (0. V))) is M2( the carrier of V)
b is V1() V14() V15() M2( REAL )
c is V1() V14() V15() M2( REAL )
b * (S - (0. V)) is M2( the carrier of V)
c * (v - (0. V)) is M2( the carrier of V)
b * S is M2( the carrier of V)
c * v is M2( the carrier of V)
(b * S) - (c * v) is M2( the carrier of V)
- (c * v) is M2( the carrier of V)
K176(V,(b * S),(- (c * v))) is M2( the carrier of V)
- v is M2( the carrier of V)
c * (- v) is M2( the carrier of V)
(b * S) + (c * (- v)) is M2( the carrier of V)
- c is V1() V14() V15() M2( REAL )
(- c) * v is M2( the carrier of V)
(b * S) + ((- c) * v) is M2( the carrier of V)
V is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
S - v is M2( the carrier of V)
- v is M2( the carrier of V)
K176(V,S,(- v)) is M2( the carrier of V)
b is M2( the carrier of V)
c is M2( the carrier of V)
b - c is M2( the carrier of V)
- c is M2( the carrier of V)
K176(V,b,(- c)) is M2( the carrier of V)
d is V1() V14() V15() M2( REAL )
d * (S - v) is M2( the carrier of V)
a9 is V1() V14() V15() M2( REAL )
a9 * (b - c) is M2( the carrier of V)
0. V is V59(V) M2( the carrier of V)
the ZeroF of V is M2( the carrier of V)
- (a9 * (b - c)) is M2( the carrier of V)
- (- (a9 * (b - c))) is M2( the carrier of V)
- (b - c) is M2( the carrier of V)
a9 * (- (b - c)) is M2( the carrier of V)
- (a9 * (- (b - c))) is M2( the carrier of V)
c - b is M2( the carrier of V)
- b is M2( the carrier of V)
K176(V,c,(- b)) is M2( the carrier of V)
a9 * (c - b) is M2( the carrier of V)
- (a9 * (c - b)) is M2( the carrier of V)
- (c - b) is M2( the carrier of V)
a9 * (- (c - b)) is M2( the carrier of V)
- a9 is V1() V14() V15() M2( REAL )
(- a9) * (c - b) is M2( the carrier of V)
- d is V1() V14() V15() M2( REAL )
(- d) * (S - v) is M2( the carrier of V)
- (S - v) is M2( the carrier of V)
d * (- (S - v)) is M2( the carrier of V)
(- a9) * (b - c) is M2( the carrier of V)
V is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
b is M2( the carrier of V)
c is M2( the carrier of V)
d is M2( the carrier of V)
a9 is M2( the carrier of V)
c - b is M2( the carrier of V)
- b is M2( the carrier of V)
K176(V,c,(- b)) is M2( the carrier of V)
b9 is V1() V14() V15() M2( REAL )
b9 * S is M2( the carrier of V)
c9 is V1() V14() V15() M2( REAL )
c9 * v is M2( the carrier of V)
(b9 * S) + (c9 * v) is M2( the carrier of V)
a9 - d is M2( the carrier of V)
- d is M2( the carrier of V)
K176(V,a9,(- d)) is M2( the carrier of V)
d9 is V1() V14() V15() M2( REAL )
d9 * S is M2( the carrier of V)
t9 is V1() V14() V15() M2( REAL )
t9 * v is M2( the carrier of V)
(d9 * S) + (t9 * v) is M2( the carrier of V)
b9 * t9 is V1() V14() V15() M2( REAL )
d9 * c9 is V1() V14() V15() M2( REAL )
(b9 * t9) - (d9 * c9) is V1() V14() V15() M2( REAL )
0. V is V59(V) M2( the carrier of V)
the ZeroF of 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)
0. V is V59(V) M2( the carrier of V)
the ZeroF of 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)
0. V is V59(V) M2( the carrier of V)
the ZeroF of 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)
0. V is V59(V) M2( the carrier of V)
the ZeroF of V is M2( the carrier of V)
(0. V) + (t9 * v) is M2( the carrier of V)
t9 " is V1() V14() V15() M2( REAL )
(t9 ") * (a9 - d) is M2( the carrier of V)
(t9 ") * t9 is V1() V14() V15() M2( REAL )
((t9 ") * t9) * v is M2( the carrier of V)
1 * v is M2( the carrier of V)
(0. V) + (c9 * v) is M2( the carrier of V)
c9 " is V1() V14() V15() M2( REAL )
(c9 ") * (c - b) is M2( the carrier of V)
(c9 ") * c9 is V1() V14() V15() M2( REAL )
((c9 ") * c9) * v is M2( the carrier of V)
(b9 * S) + (0. V) is M2( the carrier of V)
b9 " is V1() V14() V15() M2( REAL )
(b9 ") * (c - b) is M2( the carrier of V)
(b9 ") * b9 is V1() V14() V15() M2( REAL )
((b9 ") * b9) * S is M2( the carrier of V)
1 * S is M2( the carrier of V)
(d9 * S) + (0. V) is M2( the carrier of V)
d9 " is V1() V14() V15() M2( REAL )
(d9 ") * (a9 - d) is M2( the carrier of V)
(d9 ") * d9 is V1() V14() V15() M2( REAL )
((d9 ") * d9) * S is M2( the carrier of V)
d9 * (c - b) is M2( the carrier of V)
d9 * (b9 * S) is M2( the carrier of V)
d9 * (c9 * v) is M2( the carrier of V)
(d9 * (b9 * S)) + (d9 * (c9 * v)) is M2( the carrier of V)
d9 * b9 is V1() V14() V15() M2( REAL )
(d9 * b9) * S is M2( the carrier of V)
((d9 * b9) * S) + (d9 * (c9 * v)) is M2( the carrier of V)
b9 * d9 is V1() V14() V15() M2( REAL )
(b9 * d9) * S is M2( the carrier of V)
(b9 * t9) * v is M2( the carrier of V)
((b9 * d9) * S) + ((b9 * t9) * v) is M2( the carrier of V)
b9 * (d9 * S) is M2( the carrier of V)
(b9 * (d9 * S)) + ((b9 * t9) * v) is M2( the carrier of V)
b9 * (t9 * v) is M2( the carrier of V)
(b9 * (d9 * S)) + (b9 * (t9 * v)) is M2( the carrier of V)
b9 * (a9 - d) is M2( the carrier of V)
b - d is M2( the carrier of V)
K176(V,b,(- d)) is M2( the carrier of V)
d9 is V1() V14() V15() M2( REAL )
d9 * S is M2( the carrier of V)
d is V1() V14() V15() M2( REAL )
d * v is M2( the carrier of V)
(d9 * S) + (d * v) is M2( the carrier of V)
d9 * d is V1() V14() V15() M2( REAL )
d9 * t9 is V1() V14() V15() M2( REAL )
(d9 * d) - (d9 * t9) is V1() V14() V15() M2( REAL )
b9 * d is V1() V14() V15() M2( REAL )
d9 * c9 is V1() V14() V15() M2( REAL )
(b9 * d) - (d9 * c9) is V1() V14() V15() M2( REAL )
((b9 * d) - (d9 * c9)) * d9 is V1() V14() V15() M2( REAL )
b9 * ((d9 * d) - (d9 * t9)) is V1() V14() V15() M2( REAL )
d9 * ((b9 * t9) - (d9 * c9)) is V1() V14() V15() M2( REAL )
(b9 * ((d9 * d) - (d9 * t9))) + (d9 * ((b9 * t9) - (d9 * c9))) is V1() V14() V15() M2( REAL )
((b9 * t9) - (d9 * c9)) " is V1() V14() V15() M2( REAL )
(((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9)) is V1() V14() V15() M2( REAL )
((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9))) * (c - b) is M2( the carrier of V)
b + (((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9))) * (c - b)) is M2( the carrier of V)
(b + (((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9))) * (c - b))) - b is M2( the carrier of V)
K176(V,(b + (((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9))) * (c - b))),(- b)) is M2( the carrier of V)
((b9 * t9) - (d9 * c9)) * ((b + (((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9))) * (c - b))) - b) is M2( the carrier of V)
((b9 * t9) - (d9 * c9)) * (b + (((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9))) * (c - b))) is M2( the carrier of V)
((b9 * t9) - (d9 * c9)) * b is M2( the carrier of V)
(((b9 * t9) - (d9 * c9)) * (b + (((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9))) * (c - b)))) - (((b9 * t9) - (d9 * c9)) * b) is M2( the carrier of V)
- (((b9 * t9) - (d9 * c9)) * b) is M2( the carrier of V)
K176(V,(((b9 * t9) - (d9 * c9)) * (b + (((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9))) * (c - b)))),(- (((b9 * t9) - (d9 * c9)) * b))) is M2( the carrier of V)
((b9 * t9) - (d9 * c9)) * (((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9))) * (c - b)) is M2( the carrier of V)
(((b9 * t9) - (d9 * c9)) * b) + (((b9 * t9) - (d9 * c9)) * (((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9))) * (c - b))) is M2( the carrier of V)
((((b9 * t9) - (d9 * c9)) * b) + (((b9 * t9) - (d9 * c9)) * (((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9))) * (c - b)))) - (((b9 * t9) - (d9 * c9)) * b) is M2( the carrier of V)
K176(V,((((b9 * t9) - (d9 * c9)) * b) + (((b9 * t9) - (d9 * c9)) * (((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9))) * (c - b)))),(- (((b9 * t9) - (d9 * c9)) * b))) is M2( the carrier of V)
((b9 * t9) - (d9 * c9)) * ((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9))) is V1() V14() V15() M2( REAL )
(((b9 * t9) - (d9 * c9)) * ((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9)))) * (c - b) is M2( the carrier of V)
(((b9 * t9) - (d9 * c9)) * b) + ((((b9 * t9) - (d9 * c9)) * ((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9)))) * (c - b)) is M2( the carrier of V)
((((b9 * t9) - (d9 * c9)) * b) + ((((b9 * t9) - (d9 * c9)) * ((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9)))) * (c - b))) - (((b9 * t9) - (d9 * c9)) * b) is M2( the carrier of V)
K176(V,((((b9 * t9) - (d9 * c9)) * b) + ((((b9 * t9) - (d9 * c9)) * ((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9)))) * (c - b))),(- (((b9 * t9) - (d9 * c9)) * b))) is M2( the carrier of V)
((b9 * t9) - (d9 * c9)) * (((b9 * t9) - (d9 * c9)) ") is V1() V14() V15() M2( REAL )
(((b9 * t9) - (d9 * c9)) * (((b9 * t9) - (d9 * c9)) ")) * ((d9 * d) - (d9 * t9)) is V1() V14() V15() M2( REAL )
((((b9 * t9) - (d9 * c9)) * (((b9 * t9) - (d9 * c9)) ")) * ((d9 * d) - (d9 * t9))) * (c - b) is M2( the carrier of V)
(((b9 * t9) - (d9 * c9)) * b) + (((((b9 * t9) - (d9 * c9)) * (((b9 * t9) - (d9 * c9)) ")) * ((d9 * d) - (d9 * t9))) * (c - b)) is M2( the carrier of V)
((((b9 * t9) - (d9 * c9)) * b) + (((((b9 * t9) - (d9 * c9)) * (((b9 * t9) - (d9 * c9)) ")) * ((d9 * d) - (d9 * t9))) * (c - b))) - (((b9 * t9) - (d9 * c9)) * b) is M2( the carrier of V)
K176(V,((((b9 * t9) - (d9 * c9)) * b) + (((((b9 * t9) - (d9 * c9)) * (((b9 * t9) - (d9 * c9)) ")) * ((d9 * d) - (d9 * t9))) * (c - b))),(- (((b9 * t9) - (d9 * c9)) * b))) is M2( the carrier of V)
1 * ((d9 * d) - (d9 * t9)) is V1() V14() V15() M2( REAL )
(1 * ((d9 * d) - (d9 * t9))) * (c - b) is M2( the carrier of V)
(((b9 * t9) - (d9 * c9)) * b) + ((1 * ((d9 * d) - (d9 * t9))) * (c - b)) is M2( the carrier of V)
((((b9 * t9) - (d9 * c9)) * b) + ((1 * ((d9 * d) - (d9 * t9))) * (c - b))) - (((b9 * t9) - (d9 * c9)) * b) is M2( the carrier of V)
K176(V,((((b9 * t9) - (d9 * c9)) * b) + ((1 * ((d9 * d) - (d9 * t9))) * (c - b))),(- (((b9 * t9) - (d9 * c9)) * b))) is M2( the carrier of V)
((d9 * d) - (d9 * t9)) * (c - b) is M2( the carrier of V)
(((b9 * t9) - (d9 * c9)) * b) - (((b9 * t9) - (d9 * c9)) * b) is M2( the carrier of V)
K176(V,(((b9 * t9) - (d9 * c9)) * b),(- (((b9 * t9) - (d9 * c9)) * b))) is M2( the carrier of V)
(((d9 * d) - (d9 * t9)) * (c - b)) + ((((b9 * t9) - (d9 * c9)) * b) - (((b9 * t9) - (d9 * c9)) * b)) is M2( the carrier of V)
(((d9 * d) - (d9 * t9)) * (c - b)) + (0. V) is M2( the carrier of V)
(b + (((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9))) * (c - b))) - d is M2( the carrier of V)
K176(V,(b + (((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9))) * (c - b))),(- d)) is M2( the carrier of V)
((b9 * t9) - (d9 * c9)) * ((b + (((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9))) * (c - b))) - d) is M2( the carrier of V)
((b9 * t9) - (d9 * c9)) * d is M2( the carrier of V)
(((b9 * t9) - (d9 * c9)) * (b + (((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9))) * (c - b)))) - (((b9 * t9) - (d9 * c9)) * d) is M2( the carrier of V)
- (((b9 * t9) - (d9 * c9)) * d) is M2( the carrier of V)
K176(V,(((b9 * t9) - (d9 * c9)) * (b + (((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9))) * (c - b)))),(- (((b9 * t9) - (d9 * c9)) * d))) is M2( the carrier of V)
((((b9 * t9) - (d9 * c9)) * b) + (((b9 * t9) - (d9 * c9)) * (((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9))) * (c - b)))) - (((b9 * t9) - (d9 * c9)) * d) is M2( the carrier of V)
K176(V,((((b9 * t9) - (d9 * c9)) * b) + (((b9 * t9) - (d9 * c9)) * (((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9))) * (c - b)))),(- (((b9 * t9) - (d9 * c9)) * d))) is M2( the carrier of V)
((((b9 * t9) - (d9 * c9)) * b) + ((((b9 * t9) - (d9 * c9)) * ((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9)))) * (c - b))) - (((b9 * t9) - (d9 * c9)) * d) is M2( the carrier of V)
K176(V,((((b9 * t9) - (d9 * c9)) * b) + ((((b9 * t9) - (d9 * c9)) * ((((b9 * t9) - (d9 * c9)) ") * ((d9 * d) - (d9 * t9)))) * (c - b))),(- (((b9 * t9) - (d9 * c9)) * d))) is M2( the carrier of V)
((((b9 * t9) - (d9 * c9)) * b) + (((((b9 * t9) - (d9 * c9)) * (((b9 * t9) - (d9 * c9)) ")) * ((d9 * d) - (d9 * t9))) * (c - b))) - (((b9 * t9) - (d9 * c9)) * d) is M2( the carrier of V)
K176(V,((((b9 * t9) - (d9 * c9)) * b) + (((((b9 * t9) - (d9 * c9)) * (((b9 * t9) - (d9 * c9)) ")) * ((d9 * d) - (d9 * t9))) * (c - b))),(- (((b9 * t9) - (d9 * c9)) * d))) is M2( the carrier of V)
((((b9 * t9) - (d9 * c9)) * b) + ((1 * ((d9 * d) - (d9 * t9))) * (c - b))) - (((b9 * t9) - (d9 * c9)) * d) is M2( the carrier of V)
K176(V,((((b9 * t9) - (d9 * c9)) * b) + ((1 * ((d9 * d) - (d9 * t9))) * (c - b))),(- (((b9 * t9) - (d9 * c9)) * d))) is M2( the carrier of V)
(((b9 * t9) - (d9 * c9)) * b) - (((b9 * t9) - (d9 * c9)) * d) is M2( the carrier of V)
K176(V,(((b9 * t9) - (d9 * c9)) * b),(- (((b9 * t9) - (d9 * c9)) * d))) is M2( the carrier of V)
(((d9 * d) - (d9 * t9)) * (c - b)) + ((((b9 * t9) - (d9 * c9)) * b) - (((b9 * t9) - (d9 * c9)) * d)) is M2( the carrier of V)
((d9 * d) - (d9 * t9)) * ((b9 * S) + (c9 * v)) is M2( the carrier of V)
((b9 * t9) - (d9 * c9)) * ((d9 * S) + (d * v)) is M2( the carrier of V)
(((d9 * d) - (d9 * t9)) * ((b9 * S) + (c9 * v))) + (((b9 * t9) - (d9 * c9)) * ((d9 * S) + (d * v))) is M2( the carrier of V)
((d9 * d) - (d9 * t9)) * (b9 * S) is M2( the carrier of V)
((d9 * d) - (d9 * t9)) * (c9 * v) is M2( the carrier of V)
(((d9 * d) - (d9 * t9)) * (b9 * S)) + (((d9 * d) - (d9 * t9)) * (c9 * v)) is M2( the carrier of V)
((((d9 * d) - (d9 * t9)) * (b9 * S)) + (((d9 * d) - (d9 * t9)) * (c9 * v))) + (((b9 * t9) - (d9 * c9)) * ((d9 * S) + (d * v))) is M2( the carrier of V)
((b9 * t9) - (d9 * c9)) * (d9 * S) is M2( the carrier of V)
((b9 * t9) - (d9 * c9)) * (d * v) is M2( the carrier of V)
(((b9 * t9) - (d9 * c9)) * (d9 * S)) + (((b9 * t9) - (d9 * c9)) * (d * v)) is M2( the carrier of V)
((((d9 * d) - (d9 * t9)) * (b9 * S)) + (((d9 * d) - (d9 * t9)) * (c9 * v))) + ((((b9 * t9) - (d9 * c9)) * (d9 * S)) + (((b9 * t9) - (d9 * c9)) * (d * v))) is M2( the carrier of V)
((d9 * d) - (d9 * t9)) * b9 is V1() V14() V15() M2( REAL )
(((d9 * d) - (d9 * t9)) * b9) * S is M2( the carrier of V)
((((d9 * d) - (d9 * t9)) * b9) * S) + (((d9 * d) - (d9 * t9)) * (c9 * v)) is M2( the carrier of V)
(((((d9 * d) - (d9 * t9)) * b9) * S) + (((d9 * d) - (d9 * t9)) * (c9 * v))) + ((((b9 * t9) - (d9 * c9)) * (d9 * S)) + (((b9 * t9) - (d9 * c9)) * (d * v))) is M2( the carrier of V)
((d9 * d) - (d9 * t9)) * c9 is V1() V14() V15() M2( REAL )
(((d9 * d) - (d9 * t9)) * c9) * v is M2( the carrier of V)
((((d9 * d) - (d9 * t9)) * b9) * S) + ((((d9 * d) - (d9 * t9)) * c9) * v) is M2( the carrier of V)
(((((d9 * d) - (d9 * t9)) * b9) * S) + ((((d9 * d) - (d9 * t9)) * c9) * v)) + ((((b9 * t9) - (d9 * c9)) * (d9 * S)) + (((b9 * t9) - (d9 * c9)) * (d * v))) is M2( the carrier of V)
((b9 * t9) - (d9 * c9)) * d9 is V1() V14() V15() M2( REAL )
(((b9 * t9) - (d9 * c9)) * d9) * S is M2( the carrier of V)
((((b9 * t9) - (d9 * c9)) * d9) * S) + (((b9 * t9) - (d9 * c9)) * (d * v)) is M2( the carrier of V)
(((((d9 * d) - (d9 * t9)) * b9) * S) + ((((d9 * d) - (d9 * t9)) * c9) * v)) + (((((b9 * t9) - (d9 * c9)) * d9) * S) + (((b9 * t9) - (d9 * c9)) * (d * v))) is M2( the carrier of V)
((b9 * t9) - (d9 * c9)) * d is V1() V14() V15() M2( REAL )
(((b9 * t9) - (d9 * c9)) * d) * v is M2( the carrier of V)
((((b9 * t9) - (d9 * c9)) * d) * v) + ((((b9 * t9) - (d9 * c9)) * d9) * S) is M2( the carrier of V)
(((((d9 * d) - (d9 * t9)) * b9) * S) + ((((d9 * d) - (d9 * t9)) * c9) * v)) + (((((b9 * t9) - (d9 * c9)) * d) * v) + ((((b9 * t9) - (d9 * c9)) * d9) * S)) is M2( the carrier of V)
(((((d9 * d) - (d9 * t9)) * b9) * S) + ((((d9 * d) - (d9 * t9)) * c9) * v)) + ((((b9 * t9) - (d9 * c9)) * d) * v) is M2( the carrier of V)
((((((d9 * d) - (d9 * t9)) * b9) * S) + ((((d9 * d) - (d9 * t9)) * c9) * v)) + ((((b9 * t9) - (d9 * c9)) * d) * v)) + ((((b9 * t9) - (d9 * c9)) * d9) * S) is M2( the carrier of V)
((((d9 * d) - (d9 * t9)) * c9) * v) + ((((b9 * t9) - (d9 * c9)) * d) * v) is M2( the carrier of V)
(((((d9 * d) - (d9 * t9)) * c9) * v) + ((((b9 * t9) - (d9 * c9)) * d) * v)) + ((((d9 * d) - (d9 * t9)) * b9) * S) is M2( the carrier of V)
((((((d9 * d) - (d9 * t9)) * c9) * v) + ((((b9 * t9) - (d9 * c9)) * d) * v)) + ((((d9 * d) - (d9 * t9)) * b9) * S)) + ((((b9 * t9) - (d9 * c9)) * d9) * S) is M2( the carrier of V)
((((d9 * d) - (d9 * t9)) * b9) * S) + ((((b9 * t9) - (d9 * c9)) * d9) * S) is M2( the carrier of V)
(((((d9 * d) - (d9 * t9)) * c9) * v) + ((((b9 * t9) - (d9 * c9)) * d) * v)) + (((((d9 * d) - (d9 * t9)) * b9) * S) + ((((b9 * t9) - (d9 * c9)) * d9) * S)) is M2( the carrier of V)
(((d9 * d) - (d9 * t9)) * c9) + (((b9 * t9) - (d9 * c9)) * d) is V1() V14() V15() M2( REAL )
((((d9 * d) - (d9 * t9)) * c9) + (((b9 * t9) - (d9 * c9)) * d)) * v is M2( the carrier of V)
(((((d9 * d) - (d9 * t9)) * c9) + (((b9 * t9) - (d9 * c9)) * d)) * v) + (((((d9 * d) - (d9 * t9)) * b9) * S) + ((((b9 * t9) - (d9 * c9)) * d9) * S)) is M2( the carrier of V)
((b9 * d) - (d9 * c9)) * t9 is V1() V14() V15() M2( REAL )
(((b9 * d) - (d9 * c9)) * t9) * v is M2( the carrier of V)
(((b9 * d) - (d9 * c9)) * d9) * S is M2( the carrier of V)
((((b9 * d) - (d9 * c9)) * t9) * v) + ((((b9 * d) - (d9 * c9)) * d9) * S) is M2( the carrier of V)
((b9 * d) - (d9 * c9)) * (t9 * v) is M2( the carrier of V)
(((b9 * d) - (d9 * c9)) * (t9 * v)) + ((((b9 * d) - (d9 * c9)) * d9) * S) is M2( the carrier of V)
((b9 * d) - (d9 * c9)) * (d9 * S) is M2( the carrier of V)
(((b9 * d) - (d9 * c9)) * (t9 * v)) + (((b9 * d) - (d9 * c9)) * (d9 * S)) is M2( the carrier of V)
((b9 * d) - (d9 * c9)) * (a9 - d) is M2( the carrier of V)
c9 * ((d9 * d) - (d9 * t9)) is V1() V14() V15() M2( REAL )
d * ((b9 * t9) - (d9 * c9)) is V1() V14() V15() M2( REAL )
(c9 * ((d9 * d) - (d9 * t9))) + (d * ((b9 * t9) - (d9 * c9))) is V1() V14() V15() M2( REAL )
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)
q9 is M2( the carrier of V)
r9 is M2( the carrier of V)
s9 is M2( the carrier of V)
c₂₁ is M2( the carrier of V)
the non empty non trivial set is non empty non trivial set
[: the non empty non trivial set , the non empty non trivial set :] is non empty set
[:[: the non empty non trivial set , the non empty non trivial set :],[: the non empty non trivial set , the non empty non trivial set :]:] is non empty set
bool [:[: the non empty non trivial set , the non empty non trivial set :],[: the non empty non trivial set , the non empty non trivial set :]:] is non empty set
the V26() V29([: the non empty non trivial set , the non empty non trivial set :]) V30([: the non empty non trivial set , the non empty non trivial set :]) M2( bool [:[: the non empty non trivial set , the non empty non trivial set :],[: the non empty non trivial set , the non empty non trivial set :]:]) is V26() V29([: the non empty non trivial set , the non empty non trivial set :]) V30([: the non empty non trivial set , the non empty non trivial set :]) M2( bool [:[: the non empty non trivial set , the non empty non trivial set :],[: the non empty non trivial set , the non empty non trivial set :]:])
( the non empty non trivial set , the V26() V29([: the non empty non trivial set , the non empty non trivial set :]) V30([: the non empty non trivial set , the non empty non trivial set :]) M2( bool [:[: the non empty non trivial set , the non empty non trivial set :],[: the non empty non trivial set , the non empty non trivial set :]:])) is () ()
V is non empty ()
the carrier of V is non empty set
V is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
[: the carrier of V, the carrier of V:] is non empty set
[:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is non empty set
bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is non empty set
v is V26() V29([: the carrier of V, the carrier of V:]) V30([: 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:]:])
b is set
c is set
[b,c] is non empty set
d is M2( the carrier of V)
a9 is M2( the carrier of V)
[d,a9] is non empty M2([: the carrier of V, the carrier of V:])
b9 is M2( the carrier of V)
c9 is M2( the carrier of V)
[b9,c9] is non empty M2([: the carrier of V, the carrier of V:])
S is V26() V29([: the carrier of V, the carrier of V:]) V30([: 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:]:])
v is V26() V29([: the carrier of V, the carrier of V:]) V30([: 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:]:])
b is set
c is set
[b,c] is non empty set
d is M2( the carrier of V)
a9 is M2( the carrier of V)
[d,a9] is non empty M2([: the carrier of V, the carrier of V:])
b9 is M2( the carrier of V)
c9 is M2( the carrier of V)
[b9,c9] is non empty M2([: the carrier of V, the carrier of V:])
d is M2( the carrier of V)
a9 is M2( the carrier of V)
[d,a9] is non empty M2([: the carrier of V, the carrier of V:])
b9 is M2( the carrier of V)
c9 is M2( the carrier of V)
[b9,c9] is non empty M2([: the carrier of V, the carrier of V:])
V is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
[: the carrier of V, the carrier of V:] is non empty set
(V) is V26() V29([: the carrier of V, the carrier of V:]) V30([: 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:],[: the carrier of V, the carrier of V:]:] is non empty set
bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
[S,v] is non empty M2([: the carrier of V, the carrier of V:])
b is M2( the carrier of V)
c is M2( the carrier of V)
[b,c] is non empty M2([: the carrier of V, the carrier of V:])
[[S,v],[b,c]] is non empty M2([:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:])
d is M2( the carrier of V)
a9 is M2( the carrier of V)
[d,a9] is non empty M2([: the carrier of V, the carrier of V:])
b9 is M2( the carrier of V)
c9 is M2( the carrier of V)
[b9,c9] is non empty M2([: the carrier of V, the carrier of V:])
V is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
(V) is V26() V29([: the carrier of V, the carrier of V:]) V30([: 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 non empty set
[:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is non empty set
bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is non empty set
( the carrier of V,(V)) is () ()
V is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
(V) is () ()
the carrier of V is non empty set
(V) is V26() V29([: the carrier of V, the carrier of V:]) V30([: 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 non empty set
[:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is non empty set
bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is non empty set
( the carrier of V,(V)) is () ()
V is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
0. V is V59(V) M2( the carrier of V)
the ZeroF of V is M2( the carrier of V)
(V) is non empty () ()
(V) is V26() V29([: the carrier of V, the carrier of V:]) V30([: 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 non empty set
[:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is non empty set
bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is non empty set
( the carrier of V,(V)) is () ()
the carrier of (V) is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
c is M2( the carrier of (V))
d is M2( the carrier of (V))
a9 is M2( the carrier of (V))
c9 is M2( the carrier of (V))
d9 is M2( the carrier of (V))
t9 is M2( the carrier of (V))
t is M2( the carrier of (V))
b9 is M2( the carrier of (V))
d9 is M2( the carrier of V)
d is M2( the carrier of V)
c9 is M2( the carrier of V)
[: the carrier of (V), the carrier of (V):] is non empty set
[c,d] is non empty M2([: the carrier of (V), the carrier of (V):])
[a9,a9] is non empty M2([: the carrier of (V), the carrier of (V):])
[[c,d],[a9,a9]] is non empty M2([:[: the carrier of (V), the carrier of (V):],[: 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 non empty set
the of (V) is V26() V29([: the carrier of (V), the carrier of (V):]) V30([: 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):]:])
bool [:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:] is non empty set
[d,c] is non empty M2([: the carrier of (V), the carrier of (V):])
[[c,d],[d,c]] is non empty M2([:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:])
[c9,d9] is non empty M2([: the carrier of (V), the carrier of (V):])
[[c,d],[c9,d9]] is non empty M2([:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:])
[t9,t] is non empty M2([: the carrier of (V), the carrier of (V):])
[[c,d],[t9,t]] is non empty M2([:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:])
p9 is M2( the carrier of V)
q9 is M2( the carrier of V)
r9 is M2( the carrier of V)
s9 is M2( the carrier of V)
[[c9,d9],[t9,t]] is non empty M2([:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:])
[a9,b9] is non empty M2([: the carrier of (V), the carrier of (V):])
[[c,d],[a9,b9]] is non empty M2([:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:])
d9 is M2( the carrier of V)
[d,c] is non empty M2([: the carrier of (V), the carrier of (V):])
[b9,a9] is non empty M2([: the carrier of (V), the carrier of (V):])
[[d,c],[b9,a9]] is non empty M2([:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:])
[d,a9] is non empty M2([: the carrier of (V), the carrier of (V):])
[[c,d],[d,a9]] is non empty M2([:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:])
[c,a9] is non empty M2([: the carrier of (V), the carrier of (V):])
[[c,d],[c,a9]] is non empty M2([:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:])
[c,a9] is non empty M2([: the carrier of (V), the carrier of (V):])
[[c,d],[c,a9]] is non empty M2([:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:])
[d,a9] is non empty M2([: the carrier of (V), the carrier of (V):])
[[c,d],[d,a9]] is non empty M2([:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:])
[a9,d] is non empty M2([: the carrier of (V), the carrier of (V):])
[[c,a9],[a9,d]] is non empty M2([:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:])
c is M2( the carrier of V)
d is M2( the carrier of V)
a9 is M2( the carrier of V)
b9 is M2( the carrier of V)
[: the carrier of (V), the carrier of (V):] is non empty set
c9 is M2( the carrier of (V))
d9 is M2( the carrier of (V))
[c9,d9] is non empty M2([: the carrier of (V), the carrier of (V):])
t is M2( the carrier of (V))
t9 is M2( the carrier of (V))
[t,t9] is non empty M2([: the carrier of (V), the carrier of (V):])
[[c9,d9],[t,t9]] is non empty M2([:[: the carrier of (V), the carrier of (V):],[: 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 non empty set
the of (V) is V26() V29([: the carrier of (V), the carrier of (V):]) V30([: 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):]:])
bool [:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:] is non empty set
[t9,t] is non empty M2([: the carrier of (V), the carrier of (V):])
[[c9,d9],[t9,t]] is non empty M2([:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:])
c is M2( the carrier of (V))
d is M2( the carrier of (V))
a9 is M2( the carrier of (V))
b9 is M2( the carrier of V)
c9 is M2( the carrier of V)
d9 is M2( the carrier of V)
t9 is M2( the carrier of V)
[: the carrier of (V), the carrier of (V):] is non empty set
[c,a9] is non empty M2([: the carrier of (V), the carrier of (V):])
t is M2( the carrier of (V))
[d,t] is non empty M2([: the carrier of (V), the carrier of (V):])
[[c,a9],[d,t]] is non empty M2([:[: the carrier of (V), the carrier of (V):],[: 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 non empty set
the of (V) is V26() V29([: the carrier of (V), the carrier of (V):]) V30([: 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):]:])
bool [:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:] is non empty set
[c,d] is non empty M2([: the carrier of (V), the carrier of (V):])
[a9,t] is non empty M2([: the carrier of (V), the carrier of (V):])
[[c,d],[a9,t]] is non empty M2([:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:])
c is M2( the carrier of (V))
a9 is M2( the carrier of (V))
b9 is M2( the carrier of (V))
d is M2( the carrier of (V))
[: the carrier of (V), the carrier of (V):] is non empty set
[a9,c] is non empty M2([: the carrier of (V), the carrier of (V):])
[c,b9] is non empty M2([: the carrier of (V), the carrier of (V):])
[[a9,c],[c,b9]] is non empty M2([:[: the carrier of (V), the carrier of (V):],[: 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 non empty set
the of (V) is V26() V29([: the carrier of (V), the carrier of (V):]) V30([: 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):]:])
bool [:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:] is non empty set
t9 is M2( the carrier of V)
c9 is M2( the carrier of V)
t is M2( the carrier of V)
d9 is M2( the carrier of V)
d9 is M2( the carrier of V)
[d,a9] is non empty M2([: the carrier of (V), the carrier of (V):])
d is M2( the carrier of (V))
[b9,d] is non empty M2([: the carrier of (V), the carrier of (V):])
[[d,a9],[b9,d]] is non empty M2([:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:])
[d,c] is non empty M2([: the carrier of (V), the carrier of (V):])
[c,d] is non empty M2([: the carrier of (V), the carrier of (V):])
[[d,c],[c,d]] is non empty M2([:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:])
V is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
(V) is non empty () ()
(V) is V26() V29([: the carrier of V, the carrier of V:]) V30([: 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 non empty set
[:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is non empty set
bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is non empty set
( the carrier of V,(V)) is () ()
the carrier of (V) is non empty set
v is M2( the carrier of (V))
b is M2( the carrier of (V))
c is M2( the carrier of (V))
d is M2( the carrier of (V))
[: the carrier of (V), the carrier of (V):] is non empty set
[v,b] is non empty M2([: the carrier of (V), the carrier of (V):])
[c,d] is non empty M2([: the carrier of (V), the carrier of (V):])
[[v,b],[c,d]] is non empty M2([:[: the carrier of (V), the carrier of (V):],[: 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 non empty set
the of (V) is V26() V29([: the carrier of (V), the carrier of (V):]) V30([: 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):]:])
bool [:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:] is non empty set
[d,c] is non empty M2([: the carrier of (V), the carrier of (V):])
[[v,b],[d,c]] is non empty M2([:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:])
a9 is M2( the carrier of V)
b9 is M2( the carrier of V)
c9 is M2( the carrier of V)
d9 is M2( the carrier of V)
t9 is M2( the carrier of V)
t is M2( the carrier of V)
t9 is M2( the carrier of V)
t is M2( the carrier of (V))
[c,t] is non empty M2([: the carrier of (V), the carrier of (V):])
[[c,d],[c,t]] is non empty M2([:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:])
[t,c] is non empty M2([: the carrier of (V), the carrier of (V):])
[[c,d],[t,c]] is non empty M2([:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:])
[v,t] is non empty M2([: the carrier of (V), the carrier of (V):])
[[v,b],[v,t]] is non empty M2([:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:])
[t,v] is non empty M2([: the carrier of (V), the carrier of (V):])
[[v,b],[t,v]] is non empty M2([:[: the carrier of (V), the carrier of (V):],[: the carrier of (V), the carrier of (V):]:])
V is non empty V78() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
0. V is V59(V) M2( the carrier of V)
the ZeroF of V is M2( the carrier of V)
V is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
0. V is V59(V) M2( the carrier of V)
the ZeroF of V is M2( the carrier of V)
(V) is non empty () ()
(V) is V26() V29([: the carrier of V, the carrier of V:]) V30([: 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 non empty set
[:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is non empty set
bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is non empty set
( the carrier of V,(V)) is () ()
the carrier of (V) is non empty set
b is M2( the carrier of (V))
c is M2( the carrier of (V))
d is M2( the carrier of (V))
b is M2( the carrier of (V))
d is M2( the carrier of (V))
a9 is M2( the carrier of (V))
c is M2( the carrier of (V))
b is M2( the carrier of (V))
c is M2( the carrier of (V))
d is M2( the carrier of (V))
a9 is M2( the carrier of (V))
b9 is M2( the carrier of (V))
c9 is M2( the carrier of (V))
d9 is M2( the carrier of (V))
t9 is M2( the carrier of (V))
t is M2( the carrier of (V))
d9 is M2( the carrier of (V))
d is M2( the carrier of (V))
c9 is M2( the carrier of (V))
d9 is M2( the carrier of (V))
p9 is M2( the carrier of (V))
q9 is M2( the carrier of (V))
r9 is M2( the carrier of (V))
s9 is M2( the carrier of (V))
c₂₁ is M2( the carrier of (V))
c₂₂ is M2( the carrier of (V))
c₂₃ is M2( the carrier of (V))
c₂₄ is M2( the carrier of (V))
b is M2( the carrier of (V))
c is M2( the carrier of (V))
d is M2( the carrier of (V))
a9 is M2( the carrier of (V))
b9 is M2( the carrier of (V))
c9 is M2( the carrier of (V))
V is non empty ()
the carrier of V is non empty set
b9 is non empty ()
the carrier of b9 is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
b is M2( the carrier of V)
c is M2( the carrier of V)
d is M2( the carrier of V)
a9 is M2( the carrier of V)
c9 is M2( the carrier of b9)
d9 is M2( the carrier of b9)
t9 is M2( the carrier of b9)
t is M2( the carrier of b9)
d9 is M2( the carrier of b9)
d is M2( the carrier of b9)
c9 is M2( the carrier of b9)
d9 is M2( the carrier of b9)
p9 is M2( the carrier of b9)
q9 is M2( the carrier of b9)
r9 is M2( the carrier of b9)
s9 is M2( the carrier of b9)
c₂₁ is M2( the carrier of b9)
c₂₂ is M2( the carrier of b9)
c₂₃ is M2( the carrier of b9)
c₂₄ is M2( the carrier of b9)
c₂₅ is M2( the carrier of b9)
c₂₆ is M2( the carrier of b9)
c₂₇ is M2( the carrier of b9)
c₂₈ is M2( the carrier of b9)
c₂₉ is M2( the carrier of b9)
c₃₀ is M2( the carrier of b9)
c₃₁ is M2( the carrier of b9)
c₃₂ is M2( the carrier of b9)
c₃₃ is M2( the carrier of b9)
c₃₅ is M2( the carrier of b9)
c₃₆ is M2( the carrier of b9)
c₃₄ is M2( the carrier of b9)
V is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
0. V is V59(V) M2( the carrier of V)
the ZeroF of V is M2( the carrier of V)
(V) is non empty () ()
(V) is V26() V29([: the carrier of V, the carrier of V:]) V30([: 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 non empty set
[:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is non empty set
bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is non empty set
( the carrier of V,(V)) is () ()
the carrier of (V) is non empty set
S is M2( the carrier of (V))
v is M2( the carrier of (V))
b is M2( the carrier of (V))
c is M2( the carrier of V)
d is M2( the carrier of V)
S is M2( the carrier of (V))
b is M2( the carrier of (V))
c is M2( the carrier of (V))
v is M2( the carrier of (V))
d is M2( the carrier of V)
a9 is M2( the carrier of V)
S is M2( the carrier of (V))
v is M2( the carrier of (V))
b is M2( the carrier of (V))
c is M2( the carrier of (V))
d is M2( the carrier of (V))
a9 is M2( the carrier of (V))
b9 is M2( the carrier of (V))
c9 is M2( the carrier of (V))
d9 is M2( the carrier of (V))
t9 is M2( the carrier of (V))
t is M2( the carrier of (V))
d9 is M2( the carrier of (V))
d is M2( the carrier of (V))
c9 is M2( the carrier of (V))
d9 is M2( the carrier of (V))
p9 is M2( the carrier of (V))
q9 is M2( the carrier of (V))
r9 is M2( the carrier of (V))
s9 is M2( the carrier of (V))
c₂₁ is M2( the carrier of (V))
c₂₂ is M2( the carrier of (V))
c₂₃ is M2( the carrier of V)
c₂₄ is M2( the carrier of V)
S is M2( the carrier of (V))
v is M2( the carrier of (V))
b is M2( the carrier of (V))
c is M2( the carrier of (V))
d is M2( the carrier of (V))
a9 is M2( the carrier of (V))
V is non empty V78() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
0. V is V59(V) M2( the carrier of V)
the ZeroF of V is M2( the carrier of V)
V is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
0. V is V59(V) M2( the carrier of V)
the ZeroF of V is M2( the carrier of V)
(V) is non empty () ()
(V) is V26() V29([: the carrier of V, the carrier of V:]) V30([: 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 non empty set
[:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is non empty set
bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is non empty set
( the carrier of V,(V)) is () ()
v is M2( the carrier of V)
b is M2( the carrier of V)
S is non empty non trivial () ()
the carrier of S is non empty non trivial set
v is M2( the carrier of S)
b is M2( the carrier of S)
c is M2( the carrier of S)
d is M2( the carrier of S)
a9 is M2( the carrier of V)
b9 is M2( the carrier of V)
V is non empty ()
the carrier of V is non empty set
b9 is non empty ()
the carrier of b9 is non empty set
S is M2( the carrier of V)
v is M2( the carrier of V)
b is M2( the carrier of V)
c is M2( the carrier of V)
d is M2( the carrier of V)
a9 is M2( the carrier of V)
c9 is M2( the carrier of b9)
d9 is M2( the carrier of b9)
t9 is M2( the carrier of b9)
t is M2( the carrier of b9)
d9 is M2( the carrier of b9)
d is M2( the carrier of b9)
c9 is M2( the carrier of b9)
d9 is M2( the carrier of b9)
p9 is M2( the carrier of b9)
q9 is M2( the carrier of b9)
r9 is M2( the carrier of b9)
s9 is M2( the carrier of b9)
c₂₁ is M2( the carrier of b9)
c₂₂ is M2( the carrier of b9)
c₂₃ is M2( the carrier of b9)
c₂₄ is M2( the carrier of b9)
c₂₅ is M2( the carrier of b9)
c₂₆ is M2( the carrier of b9)
c₂₇ is M2( the carrier of b9)
c₂₈ is M2( the carrier of b9)
c₂₉ is M2( the carrier of b9)
c₃₀ is M2( the carrier of b9)
c₃₁ is M2( the carrier of b9)
c₃₂ is M2( the carrier of b9)
c₃₃ is M2( the carrier of b9)
c₃₅ is M2( the carrier of b9)
c₃₆ is M2( the carrier of b9)
c₃₄ is M2( the carrier of b9)
c₃₇ is M2( the carrier of b9)
c₃₈ is M2( the carrier of b9)
c₃₉ is M2( the carrier of b9)
c₄₀ is M2( the carrier of b9)
V is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
0. V is V59(V) M2( the carrier of V)
the ZeroF of V is M2( the carrier of V)
(V) is non empty () ()
(V) is V26() V29([: the carrier of V, the carrier of V:]) V30([: 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 non empty set
[:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is non empty set
bool [:[: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:]:] is non empty set
( the carrier of V,(V)) is () ()
the carrier of (V) is non empty set
v is M2( the carrier of (V))
b is M2( the carrier of (V))
c is M2( the carrier of (V))
d is M2( the carrier of (V))
a9 is M2( the carrier of V)
b9 is M2( the carrier of V)
v is M2( the carrier of V)
b is M2( the carrier of V)