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)
c21 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