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

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