REAL is V16() V17() V18() V22() set
NAT is V16() V17() V18() V19() V20() V21() V22() M2(K11(REAL))
K11(REAL) is set
NAT is V16() V17() V18() V19() V20() V21() V22() set
K11(NAT) is set
K11(NAT) is set
0 is set
1 is V1() V2() V4() V13() V14() V15() V16() V17() V18() V19() V20() V21() M3( REAL , NAT )
0 is V1() V13() V14() V15() V16() V17() V18() V19() V20() V21() M3( REAL , NAT )
K44(0) is V14() set
OAS is V52() non trivial OAffinSpace-like AffinStruct
Lambda OAS is V52() strict AffinStruct
OAS is V52() non trivial OAffinSpace-like 2-dimensional AffinStruct
Lambda OAS is V52() non trivial strict AffinSpace-like AffinStruct
OAS is V52() non trivial OAffinSpace-like AffinStruct
the carrier of OAS is V4() V5() set
Lambda OAS is V52() non trivial strict AffinSpace-like AffinStruct
the carrier of (Lambda OAS) is V4() V5() set
K11( the carrier of OAS) is set
K11( the carrier of (Lambda OAS)) is set
the CONGR of OAS is M2(K11(K12(K12( the carrier of OAS, the carrier of OAS),K12( the carrier of OAS, the carrier of OAS))))
K12( the carrier of OAS, the carrier of OAS) is set
K12(K12( the carrier of OAS, the carrier of OAS),K12( the carrier of OAS, the carrier of OAS)) is set
K11(K12(K12( the carrier of OAS, the carrier of OAS),K12( the carrier of OAS, the carrier of OAS))) is set
lambda the CONGR of OAS is M2(K11(K12(K12( the carrier of OAS, the carrier of OAS),K12( the carrier of OAS, the carrier of OAS))))
AffinStruct(# the carrier of OAS,(lambda the CONGR of OAS) #) is strict AffinStruct
X is set
c3 is set
b is set
c is set
OAS is V52() non trivial OAffinSpace-like AffinStruct
the carrier of OAS is V4() V5() set
Lambda OAS is V52() non trivial strict AffinSpace-like AffinStruct
the carrier of (Lambda OAS) is V4() V5() set
X is M2( the carrier of OAS)
c3 is M2( the carrier of OAS)
b is M2( the carrier of OAS)
c is M2( the carrier of (Lambda OAS))
d is M2( the carrier of (Lambda OAS))
a1 is M2( the carrier of (Lambda OAS))
OAS is V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
OASpace OAS is strict AffinStruct
the carrier of (OASpace OAS) is set
the carrier of OAS is V4() set
X is set
DirPar OAS is M2(K11(K12(K12( the carrier of OAS, the carrier of OAS),K12( the carrier of OAS, the carrier of OAS))))
K12( the carrier of OAS, the carrier of OAS) is set
K12(K12( the carrier of OAS, the carrier of OAS),K12( the carrier of OAS, the carrier of OAS)) is set
K11(K12(K12( the carrier of OAS, the carrier of OAS),K12( the carrier of OAS, the carrier of OAS))) is set
AffinStruct(# the carrier of OAS,(DirPar OAS) #) is strict AffinStruct
OAS is V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
OASpace OAS is strict AffinStruct
the carrier of OAS is V4() set
X is V52() non trivial OAffinSpace-like AffinStruct
the carrier of X is V4() V5() set
c3 is M2( the carrier of X)
b is M2( the carrier of X)
c is M2( the carrier of X)
d is M2( the carrier of X)
a1 is M2( the carrier of OAS)
b1 is M2( the carrier of OAS)
c1 is M2( the carrier of OAS)
d1 is M2( the carrier of OAS)
OAS is V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
OASpace OAS is strict AffinStruct
the carrier of OAS is V4() set
0. OAS is V59(OAS) M2( the carrier of OAS)
X is V52() non trivial OAffinSpace-like AffinStruct
the carrier of X is V4() V5() set
c3 is M2( the carrier of X)
b is M2( the carrier of X)
c is M2( the carrier of X)
d is M2( the carrier of X)
b1 is M2( the carrier of OAS)
a1 is M2( the carrier of OAS)
b1 - a1 is M2( the carrier of OAS)
- a1 is M2( the carrier of OAS)
K151(OAS,b1,(- a1)) is M2( the carrier of OAS)
P is M2( the carrier of OAS)
d1 is M2( the carrier of OAS)
c1 is M2( the carrier of OAS)
d1 - c1 is M2( the carrier of OAS)
- c1 is M2( the carrier of OAS)
K151(OAS,d1,(- c1)) is M2( the carrier of OAS)
Q is M2( the carrier of OAS)
x1 is V1() V14() V15() M2( REAL )
x1 * P is M2( the carrier of OAS)
x is V1() V14() V15() M2( REAL )
x * Q is M2( the carrier of OAS)
(x1 * P) + (x * Q) is M2( the carrier of OAS)
- (x * Q) is M2( the carrier of OAS)
- Q is M2( the carrier of OAS)
x * (- Q) is M2( the carrier of OAS)
- x is V1() V14() V15() M2( REAL )
(- x) * Q is M2( the carrier of OAS)
x1 is V1() V14() V15() M2( REAL )
x1 * P is M2( the carrier of OAS)
x is V1() V14() V15() M2( REAL )
x * Q is M2( the carrier of OAS)
(x1 * P) + (x * Q) is M2( the carrier of OAS)
OAS is V52() non trivial AffinSpace-like AffinStruct
the carrier of OAS is V4() V5() set
X is M2( the carrier of OAS)
c3 is M2( the carrier of OAS)
b is M2( the carrier of OAS)
c is M2( the carrier of OAS)
X is M2( the carrier of OAS)
c3 is M2( the carrier of OAS)
b is M2( the carrier of OAS)
c is M2( the carrier of OAS)
OAS is V52() non trivial OAffinSpace-like AffinStruct
the carrier of OAS is V4() V5() set
X is M2( the carrier of OAS)
c3 is M2( the carrier of OAS)
d is M2( the carrier of OAS)
b is M2( the carrier of OAS)
a1 is M2( the carrier of OAS)
c is M2( the carrier of OAS)
b1 is M2( the carrier of OAS)
c1 is M2( the carrier of OAS)
d1 is M2( the carrier of OAS)
P is M2( the carrier of OAS)
OAS is V52() non trivial OAffinSpace-like AffinStruct
the carrier of OAS is V4() V5() set
X is M2( the carrier of OAS)
c3 is M2( the carrier of OAS)
b is M2( the carrier of OAS)
c is M2( the carrier of OAS)
d is M2( the carrier of OAS)
OAS is V52() non trivial OAffinSpace-like AffinStruct
the carrier of OAS is V4() V5() set
X is M2( the carrier of OAS)
c3 is M2( the carrier of OAS)
b is M2( the carrier of OAS)
c is M2( the carrier of OAS)
d is M2( the carrier of OAS)
a1 is M2( the carrier of OAS)
b1 is M2( the carrier of OAS)
OAS is V52() non trivial OAffinSpace-like AffinStruct
Lambda OAS is V52() non trivial strict AffinSpace-like AffinStruct
the carrier of (Lambda OAS) is V4() V5() set
K11( the carrier of (Lambda OAS)) is set
c3 is M2(K11( the carrier of (Lambda OAS)))
b is M2(K11( the carrier of (Lambda OAS)))
c is M2(K11( the carrier of (Lambda OAS)))
d is M2( the carrier of (Lambda OAS))
a1 is M2( the carrier of (Lambda OAS))
b1 is M2( the carrier of (Lambda OAS))
c1 is M2( the carrier of (Lambda OAS))
d1 is M2( the carrier of (Lambda OAS))
P is M2( the carrier of (Lambda OAS))
Q is M2( the carrier of (Lambda OAS))
the carrier of OAS is V4() V5() set
x1 is M2( the carrier of OAS)
c1 is M2( the carrier of OAS)
c19 is M2( the carrier of OAS)
x is M2( the carrier of OAS)
a19 is M2( the carrier of OAS)
v is M2(K11( the carrier of (Lambda OAS)))
v is M2(K11( the carrier of (Lambda OAS)))
u is M2( the carrier of OAS)
b19 is M2( the carrier of OAS)
OAS is V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of OAS is V4() set
X is M2( the carrier of OAS)
c3 is M2( the carrier of OAS)
X - c3 is M2( the carrier of OAS)
- c3 is M2( the carrier of OAS)
K151(OAS,X,(- c3)) is M2( the carrier of OAS)
c is M2( the carrier of OAS)
c - X is M2( the carrier of OAS)
- X is M2( the carrier of OAS)
K151(OAS,c,(- X)) is M2( the carrier of OAS)
b is M2( the carrier of OAS)
d is M2( the carrier of OAS)
b - c3 is M2( the carrier of OAS)
K151(OAS,b,(- c3)) is M2( the carrier of OAS)
b - X is M2( the carrier of OAS)
K151(OAS,b,(- X)) is M2( the carrier of OAS)
d - c is M2( the carrier of OAS)
- c is M2( the carrier of OAS)
K151(OAS,d,(- c)) is M2( the carrier of OAS)
a1 is V1() V14() V15() M2( REAL )
a1 * (c - X) is M2( the carrier of OAS)
- a1 is V1() V14() V15() M2( REAL )
(- a1) " is V1() V14() V15() M2( REAL )
((- a1) ") * (b - c3) is M2( the carrier of OAS)
c + (((- a1) ") * (b - c3)) is M2( the carrier of OAS)
((- a1) ") * (b - X) is M2( the carrier of OAS)
X + (((- a1) ") * (b - X)) is M2( the carrier of OAS)
(- a1) * (d - c) is M2( the carrier of OAS)
c3 - X is M2( the carrier of OAS)
K151(OAS,c3,(- X)) is M2( the carrier of OAS)
0. OAS is V59(OAS) M2( the carrier of OAS)
b1 is V1() V14() V15() M2( REAL )
b1 * (c3 - X) is M2( the carrier of OAS)
c1 is V1() V14() V15() M2( REAL )
c1 * (b - X) is M2( the carrier of OAS)
(b1 * (c3 - X)) + (c1 * (b - X)) is M2( the carrier of OAS)
- (c1 * (b - X)) is M2( the carrier of OAS)
- (b - X) is M2( the carrier of OAS)
c1 * (- (b - X)) is M2( the carrier of OAS)
- c1 is V1() V14() V15() M2( REAL )
(- c1) * (b - X) is M2( the carrier of OAS)
OASpace OAS is strict AffinStruct
b1 is V52() non trivial OAffinSpace-like AffinStruct
the carrier of b1 is V4() V5() set
P is M2( the carrier of b1)
x1 is M2( the carrier of b1)
Q is M2( the carrier of b1)
x is M2( the carrier of b1)
d1 is M2( the carrier of b1)
(c + (((- a1) ") * (b - c3))) - c is M2( the carrier of OAS)
K151(OAS,(c + (((- a1) ") * (b - c3))),(- c)) is M2( the carrier of OAS)
(- a1) * ((c + (((- a1) ") * (b - c3))) - c) is M2( the carrier of OAS)
(- a1) * (((- a1) ") * (b - c3)) is M2( the carrier of OAS)
(- a1) * ((- a1) ") is V1() V14() V15() M2( REAL )
((- a1) * ((- a1) ")) * (b - c3) is M2( the carrier of OAS)
1 * (b - c3) is M2( the carrier of OAS)
c1 is M2( the carrier of b1)
X - (c + (((- a1) ") * (b - c3))) is M2( the carrier of OAS)
- (c + (((- a1) ") * (b - c3))) is M2( the carrier of OAS)
K151(OAS,X,(- (c + (((- a1) ") * (b - c3))))) is M2( the carrier of OAS)
(- a1) * (X - (c + (((- a1) ") * (b - c3)))) is M2( the carrier of OAS)
(- a1) * X is M2( the carrier of OAS)
(- a1) * (c + (((- a1) ") * (b - c3))) is M2( the carrier of OAS)
((- a1) * X) - ((- a1) * (c + (((- a1) ") * (b - c3)))) is M2( the carrier of OAS)
- ((- a1) * (c + (((- a1) ") * (b - c3)))) is M2( the carrier of OAS)
K151(OAS,((- a1) * X),(- ((- a1) * (c + (((- a1) ") * (b - c3)))))) is M2( the carrier of OAS)
(- a1) * c is M2( the carrier of OAS)
((- a1) * c) + ((- a1) * (((- a1) ") * (b - c3))) is M2( the carrier of OAS)
((- a1) * X) - (((- a1) * c) + ((- a1) * (((- a1) ") * (b - c3)))) is M2( the carrier of OAS)
- (((- a1) * c) + ((- a1) * (((- a1) ") * (b - c3)))) is M2( the carrier of OAS)
K151(OAS,((- a1) * X),(- (((- a1) * c) + ((- a1) * (((- a1) ") * (b - c3)))))) is M2( the carrier of OAS)
((- a1) * c) + (((- a1) * ((- a1) ")) * (b - c3)) is M2( the carrier of OAS)
((- a1) * X) - (((- a1) * c) + (((- a1) * ((- a1) ")) * (b - c3))) is M2( the carrier of OAS)
- (((- a1) * c) + (((- a1) * ((- a1) ")) * (b - c3))) is M2( the carrier of OAS)
K151(OAS,((- a1) * X),(- (((- a1) * c) + (((- a1) * ((- a1) ")) * (b - c3))))) is M2( the carrier of OAS)
((- a1) * c) + (1 * (b - c3)) is M2( the carrier of OAS)
((- a1) * X) - (((- a1) * c) + (1 * (b - c3))) is M2( the carrier of OAS)
- (((- a1) * c) + (1 * (b - c3))) is M2( the carrier of OAS)
K151(OAS,((- a1) * X),(- (((- a1) * c) + (1 * (b - c3))))) is M2( the carrier of OAS)
((- a1) * c) + (b - c3) is M2( the carrier of OAS)
((- a1) * X) - (((- a1) * c) + (b - c3)) is M2( the carrier of OAS)
- (((- a1) * c) + (b - c3)) is M2( the carrier of OAS)
K151(OAS,((- a1) * X),(- (((- a1) * c) + (b - c3)))) is M2( the carrier of OAS)
((- a1) * X) - ((- a1) * c) is M2( the carrier of OAS)
- ((- a1) * c) is M2( the carrier of OAS)
K151(OAS,((- a1) * X),(- ((- a1) * c))) is M2( the carrier of OAS)
(((- a1) * X) - ((- a1) * c)) - (b - c3) is M2( the carrier of OAS)
- (b - c3) is M2( the carrier of OAS)
K151(OAS,(((- a1) * X) - ((- a1) * c)),(- (b - c3))) is M2( the carrier of OAS)
X - c is M2( the carrier of OAS)
K151(OAS,X,(- c)) is M2( the carrier of OAS)
(- a1) * (X - c) is M2( the carrier of OAS)
((- a1) * (X - c)) - (b - c3) is M2( the carrier of OAS)
K151(OAS,((- a1) * (X - c)),(- (b - c3))) is M2( the carrier of OAS)
- (X - c) is M2( the carrier of OAS)
a1 * (- (X - c)) is M2( the carrier of OAS)
(a1 * (- (X - c))) - (b - c3) is M2( the carrier of OAS)
K151(OAS,(a1 * (- (X - c))),(- (b - c3))) is M2( the carrier of OAS)
(X - c3) - (b - c3) is M2( the carrier of OAS)
K151(OAS,(X - c3),(- (b - c3))) is M2( the carrier of OAS)
(b - c3) + c3 is M2( the carrier of OAS)
X - ((b - c3) + c3) is M2( the carrier of OAS)
- ((b - c3) + c3) is M2( the carrier of OAS)
K151(OAS,X,(- ((b - c3) + c3))) is M2( the carrier of OAS)
X - b is M2( the carrier of OAS)
- b is M2( the carrier of OAS)
K151(OAS,X,(- b)) is M2( the carrier of OAS)
1 * (X - b) is M2( the carrier of OAS)
1 * (c3 - X) is M2( the carrier of OAS)
- (c3 - X) is M2( the carrier of OAS)
- 1 is V1() V14() V15() M2( REAL )
(- 1) * (- (c3 - X)) is M2( the carrier of OAS)
(- 1) * (a1 * (c - X)) is M2( the carrier of OAS)
(- 1) * a1 is V1() V14() V15() M2( REAL )
((- 1) * a1) * (c - X) is M2( the carrier of OAS)
(- a1) * (c - X) is M2( the carrier of OAS)
(c + (((- a1) ") * (b - c3))) - X is M2( the carrier of OAS)
K151(OAS,(c + (((- a1) ") * (b - c3))),(- X)) is M2( the carrier of OAS)
(- a1) * ((c + (((- a1) ") * (b - c3))) - X) is M2( the carrier of OAS)
- ((c + (((- a1) ") * (b - c3))) - X) is M2( the carrier of OAS)
a1 * (- ((c + (((- a1) ") * (b - c3))) - X)) is M2( the carrier of OAS)
a1 * (X - (c + (((- a1) ") * (b - c3)))) is M2( the carrier of OAS)
- (a1 * (X - (c + (((- a1) ") * (b - c3))))) is M2( the carrier of OAS)
- (- (a1 * (X - (c + (((- a1) ") * (b - c3)))))) is M2( the carrier of OAS)
- (X - (c + (((- a1) ") * (b - c3)))) is M2( the carrier of OAS)
a1 * (- (X - (c + (((- a1) ") * (b - c3))))) is M2( the carrier of OAS)
- (a1 * (- (X - (c + (((- a1) ") * (b - c3)))))) is M2( the carrier of OAS)
- (1 * (X - b)) is M2( the carrier of OAS)
- (X - b) is M2( the carrier of OAS)
X + ((c + (((- a1) ") * (b - c3))) - X) is M2( the carrier of OAS)
OAS is V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of OAS is V4() set
X is M2( the carrier of OAS)
c3 is M2( the carrier of OAS)
b is M2( the carrier of OAS)
c3 - X is M2( the carrier of OAS)
- X is M2( the carrier of OAS)
K151(OAS,c3,(- X)) is M2( the carrier of OAS)
b - c3 is M2( the carrier of OAS)
- c3 is M2( the carrier of OAS)
K151(OAS,b,(- c3)) is M2( the carrier of OAS)
c is V1() V14() V15() M2( REAL )
c * (c3 - X) is M2( the carrier of OAS)
d is V1() V14() V15() M2( REAL )
d * (b - c3) is M2( the carrier of OAS)
c " is V1() V14() V15() M2( REAL )
(c ") * d is V1() V14() V15() M2( REAL )
a1 is V1() V14() V15() M2( REAL )
a1 * (b - c3) is M2( the carrier of OAS)
0 * d is V1() V14() V15() M2( REAL )
1 * (c3 - X) is M2( the carrier of OAS)
(c ") * c is V1() V14() V15() M2( REAL )
((c ") * c) * (c3 - X) is M2( the carrier of OAS)
(c ") * (d * (b - c3)) is M2( the carrier of OAS)
OAS is V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
OASpace OAS is strict AffinStruct
X is V52() non trivial OAffinSpace-like AffinStruct
the carrier of X is V4() V5() set
b is M2( the carrier of X)
c3 is M2( the carrier of X)
a1 is M2( the carrier of X)
c is M2( the carrier of X)
b1 is M2( the carrier of X)
d is M2( the carrier of X)
c1 is M2( the carrier of X)
the carrier of OAS is V4() set
d1 is M2( the carrier of OAS)
P is M2( the carrier of OAS)
Q is M2( the carrier of OAS)
x1 is M2( the carrier of OAS)
a19 is M2( the carrier of OAS)
c1 is M2( the carrier of OAS)
x is M2( the carrier of OAS)
d1 - P is M2( the carrier of OAS)
- P is M2( the carrier of OAS)
K151(OAS,d1,(- P)) is M2( the carrier of OAS)
x - d1 is M2( the carrier of OAS)
- d1 is M2( the carrier of OAS)
K151(OAS,x,(- d1)) is M2( the carrier of OAS)
b19 is V1() V14() V15() M2( REAL )
b19 * (x - d1) is M2( the carrier of OAS)
x1 - P is M2( the carrier of OAS)
K151(OAS,x1,(- P)) is M2( the carrier of OAS)
- b19 is V1() V14() V15() M2( REAL )
(- b19) " is V1() V14() V15() M2( REAL )
((- b19) ") * (x1 - P) is M2( the carrier of OAS)
x + (((- b19) ") * (x1 - P)) is M2( the carrier of OAS)
Q - P is M2( the carrier of OAS)
K151(OAS,Q,(- P)) is M2( the carrier of OAS)
((- b19) ") * (Q - P) is M2( the carrier of OAS)
x + (((- b19) ") * (Q - P)) is M2( the carrier of OAS)
a19 - c1 is M2( the carrier of OAS)
- c1 is M2( the carrier of OAS)
K151(OAS,a19,(- c1)) is M2( the carrier of OAS)
1 * (a19 - c1) is M2( the carrier of OAS)
(x + (((- b19) ") * (x1 - P))) - (x + (((- b19) ") * (Q - P))) is M2( the carrier of OAS)
- (x + (((- b19) ") * (Q - P))) is M2( the carrier of OAS)
K151(OAS,(x + (((- b19) ") * (x1 - P))),(- (x + (((- b19) ") * (Q - P))))) is M2( the carrier of OAS)
(((- b19) ") * (x1 - P)) + x is M2( the carrier of OAS)
((((- b19) ") * (x1 - P)) + x) - x is M2( the carrier of OAS)
- x is M2( the carrier of OAS)
K151(OAS,((((- b19) ") * (x1 - P)) + x),(- x)) is M2( the carrier of OAS)
(((((- b19) ") * (x1 - P)) + x) - x) - (((- b19) ") * (Q - P)) is M2( the carrier of OAS)
- (((- b19) ") * (Q - P)) is M2( the carrier of OAS)
K151(OAS,(((((- b19) ") * (x1 - P)) + x) - x),(- (((- b19) ") * (Q - P)))) is M2( the carrier of OAS)
(((- b19) ") * (x1 - P)) - (((- b19) ") * (Q - P)) is M2( the carrier of OAS)
K151(OAS,(((- b19) ") * (x1 - P)),(- (((- b19) ") * (Q - P)))) is M2( the carrier of OAS)
(x1 - P) - (Q - P) is M2( the carrier of OAS)
- (Q - P) is M2( the carrier of OAS)
K151(OAS,(x1 - P),(- (Q - P))) is M2( the carrier of OAS)
((- b19) ") * ((x1 - P) - (Q - P)) is M2( the carrier of OAS)
(Q - P) + P is M2( the carrier of OAS)
x1 - ((Q - P) + P) is M2( the carrier of OAS)
- ((Q - P) + P) is M2( the carrier of OAS)
K151(OAS,x1,(- ((Q - P) + P))) is M2( the carrier of OAS)
((- b19) ") * (x1 - ((Q - P) + P)) is M2( the carrier of OAS)
x1 - Q is M2( the carrier of OAS)
- Q is M2( the carrier of OAS)
K151(OAS,x1,(- Q)) is M2( the carrier of OAS)
((- b19) ") * (x1 - Q) is M2( the carrier of OAS)
b19 " is V1() V14() V15() M2( REAL )
- (b19 ") is V1() V14() V15() M2( REAL )
(- (b19 ")) * (x1 - Q) is M2( the carrier of OAS)
- (x1 - Q) is M2( the carrier of OAS)
(b19 ") * (- (x1 - Q)) is M2( the carrier of OAS)
Q - x1 is M2( the carrier of OAS)
- x1 is M2( the carrier of OAS)
K151(OAS,Q,(- x1)) is M2( the carrier of OAS)
(b19 ") * (Q - x1) is M2( the carrier of OAS)
X is V52() non trivial OAffinSpace-like AffinStruct
OAS is V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
OASpace OAS is strict AffinStruct
OAS is V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of OAS is V4() set
X is M2( the carrier of OAS)
c3 is M2( the carrier of OAS)
b is M2( the carrier of OAS)
c3 - X is M2( the carrier of OAS)
- X is M2( the carrier of OAS)
K151(OAS,c3,(- X)) is M2( the carrier of OAS)
b - X is M2( the carrier of OAS)
K151(OAS,b,(- X)) is M2( the carrier of OAS)
c is V1() V14() V15() M2( REAL )
c * (c3 - X) is M2( the carrier of OAS)
d is V1() V14() V15() M2( REAL )
d * (b - X) is M2( the carrier of OAS)
0. OAS is V59(OAS) M2( the carrier of OAS)
c " is V1() V14() V15() M2( REAL )
(c ") * d is V1() V14() V15() M2( REAL )
a1 is V1() V14() V15() M2( REAL )
a1 * (b - X) is M2( the carrier of OAS)
(c ") * (c * (c3 - X)) is M2( the carrier of OAS)
(c ") * c is V1() V14() V15() M2( REAL )
((c ") * c) * (c3 - X) is M2( the carrier of OAS)
1 * (c3 - X) is M2( the carrier of OAS)
OAS is V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of OAS is V4() set
X is M2( the carrier of OAS)
b is M2( the carrier of OAS)
X - b is M2( the carrier of OAS)
- b is M2( the carrier of OAS)
K151(OAS,X,(- b)) is M2( the carrier of OAS)
c3 is M2( the carrier of OAS)
c3 - b is M2( the carrier of OAS)
K151(OAS,c3,(- b)) is M2( the carrier of OAS)
(X - b) - (c3 - b) is M2( the carrier of OAS)
- (c3 - b) is M2( the carrier of OAS)
K151(OAS,(X - b),(- (c3 - b))) is M2( the carrier of OAS)
X - c3 is M2( the carrier of OAS)
- c3 is M2( the carrier of OAS)
K151(OAS,X,(- c3)) is M2( the carrier of OAS)
(c3 - b) + b is M2( the carrier of OAS)
X - ((c3 - b) + b) is M2( the carrier of OAS)
- ((c3 - b) + b) is M2( the carrier of OAS)
K151(OAS,X,(- ((c3 - b) + b))) is M2( the carrier of OAS)
OAS is V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
OASpace OAS is strict AffinStruct
X is V52() non trivial OAffinSpace-like AffinStruct
Lambda X is V52() non trivial strict AffinSpace-like AffinStruct
the carrier of (Lambda X) is V4() V5() set
K11( the carrier of (Lambda X)) is set
b is M2(K11( the carrier of (Lambda X)))
c is M2(K11( the carrier of (Lambda X)))
d is M2( the carrier of (Lambda X))
a1 is M2( the carrier of (Lambda X))
d1 is M2( the carrier of (Lambda X))
b1 is M2( the carrier of (Lambda X))
P is M2( the carrier of (Lambda X))
c1 is M2( the carrier of (Lambda X))
Q is M2( the carrier of (Lambda X))
the carrier of X is V4() V5() set
the carrier of OAS is V4() set
x1 is M2( the carrier of X)
x is M2( the carrier of X)
c1 is M2( the carrier of X)
a19 is M2( the carrier of X)
b19 is M2( the carrier of X)
c19 is M2( the carrier of X)
u is M2( the carrier of X)
u9 is M2( the carrier of OAS)
c199 is M2( the carrier of OAS)
v99 is M2( the carrier of OAS)
b199 is M2( the carrier of OAS)
v is M2( the carrier of OAS)
w99 is M2( the carrier of OAS)
v99 - v is M2( the carrier of OAS)
- v is M2( the carrier of OAS)
K151(OAS,v99,(- v)) is M2( the carrier of OAS)
u9 - v is M2( the carrier of OAS)
K151(OAS,u9,(- v)) is M2( the carrier of OAS)
r2 is V1() V14() V15() M2( REAL )
r2 * (u9 - v) is M2( the carrier of OAS)
- r2 is V1() V14() V15() M2( REAL )
w is M2( the carrier of OAS)
w - v is M2( the carrier of OAS)
K151(OAS,w,(- v)) is M2( the carrier of OAS)
r1 is V1() V14() V15() M2( REAL )
r1 * (u9 - v) is M2( the carrier of OAS)
v - u9 is M2( the carrier of OAS)
- u9 is M2( the carrier of OAS)
K151(OAS,v,(- u9)) is M2( the carrier of OAS)
- r1 is V1() V14() V15() M2( REAL )
(- r1) * (v - u9) is M2( the carrier of OAS)
- (v - u9) is M2( the carrier of OAS)
r1 * (- (v - u9)) is M2( the carrier of OAS)
(- r2) * (v - u9) is M2( the carrier of OAS)
r2 * (- (v - u9)) is M2( the carrier of OAS)
(- r2) " is V1() V14() V15() M2( REAL )
((- r2) ") * (v99 - v) is M2( the carrier of OAS)
c199 - v is M2( the carrier of OAS)
K151(OAS,c199,(- v)) is M2( the carrier of OAS)
- ((- r2) ") is V1() V14() V15() M2( REAL )
(- ((- r2) ")) " is V1() V14() V15() M2( REAL )
((- ((- r2) ")) ") * (c199 - v) is M2( the carrier of OAS)
v + (((- ((- r2) ")) ") * (c199 - v)) is M2( the carrier of OAS)
r2 " is V1() V14() V15() M2( REAL )
- (r2 ") is V1() V14() V15() M2( REAL )
- (- (r2 ")) is V1() V14() V15() M2( REAL )
(- (- (r2 "))) " is V1() V14() V15() M2( REAL )
((- (- (r2 "))) ") * (c199 - v) is M2( the carrier of OAS)
v + (((- (- (r2 "))) ") * (c199 - v)) is M2( the carrier of OAS)
r2 * (c199 - v) is M2( the carrier of OAS)
v + (r2 * (c199 - v)) is M2( the carrier of OAS)
b199 - v is M2( the carrier of OAS)
K151(OAS,b199,(- v)) is M2( the carrier of OAS)
r1 " is V1() V14() V15() M2( REAL )
(r1 ") * r2 is V1() V14() V15() M2( REAL )
r1 * (r2 ") is V1() V14() V15() M2( REAL )
(r2 ") * (v99 - v) is M2( the carrier of OAS)
r1 * ((r2 ") * (v99 - v)) is M2( the carrier of OAS)
(r1 * (r2 ")) * (v99 - v) is M2( the carrier of OAS)
(- r1) " is V1() V14() V15() M2( REAL )
((- r1) ") * (w - v) is M2( the carrier of OAS)
w99 - v is M2( the carrier of OAS)
K151(OAS,w99,(- v)) is M2( the carrier of OAS)
- ((- r1) ") is V1() V14() V15() M2( REAL )
(- ((- r1) ")) " is V1() V14() V15() M2( REAL )
((- ((- r1) ")) ") * (w99 - v) is M2( the carrier of OAS)
v + (((- ((- r1) ")) ") * (w99 - v)) is M2( the carrier of OAS)
- (r1 ") is V1() V14() V15() M2( REAL )
- (- (r1 ")) is V1() V14() V15() M2( REAL )
(- (- (r1 "))) " is V1() V14() V15() M2( REAL )
((- (- (r1 "))) ") * (w99 - v) is M2( the carrier of OAS)
v + (((- (- (r1 "))) ") * (w99 - v)) is M2( the carrier of OAS)
r1 * (w99 - v) is M2( the carrier of OAS)
v + (r1 * (w99 - v)) is M2( the carrier of OAS)
(r1 ") * (r2 * (c199 - v)) is M2( the carrier of OAS)
((r1 ") * r2) * (c199 - v) is M2( the carrier of OAS)
((r1 ") * r2) " is V1() V14() V15() M2( REAL )
(((r1 ") * r2) ") * (w99 - v) is M2( the carrier of OAS)
(r1 ") " is V1() V14() V15() M2( REAL )
((r1 ") ") * (r2 ") is V1() V14() V15() M2( REAL )
(((r1 ") ") * (r2 ")) * (w99 - v) is M2( the carrier of OAS)
(r1 * (r2 ")) * (w99 - v) is M2( the carrier of OAS)
c199 - w is M2( the carrier of OAS)
- w is M2( the carrier of OAS)
K151(OAS,c199,(- w)) is M2( the carrier of OAS)
1 * (c199 - w) is M2( the carrier of OAS)
((r1 * (r2 ")) * (w99 - v)) - ((r1 * (r2 ")) * (v99 - v)) is M2( the carrier of OAS)
- ((r1 * (r2 ")) * (v99 - v)) is M2( the carrier of OAS)
K151(OAS,((r1 * (r2 ")) * (w99 - v)),(- ((r1 * (r2 ")) * (v99 - v)))) is M2( the carrier of OAS)
(w99 - v) - (v99 - v) is M2( the carrier of OAS)
- (v99 - v) is M2( the carrier of OAS)
K151(OAS,(w99 - v),(- (v99 - v))) is M2( the carrier of OAS)
(r1 * (r2 ")) * ((w99 - v) - (v99 - v)) is M2( the carrier of OAS)
w99 - v99 is M2( the carrier of OAS)
- v99 is M2( the carrier of OAS)
K151(OAS,w99,(- v99)) is M2( the carrier of OAS)
(r1 * (r2 ")) * (w99 - v99) is M2( the carrier of OAS)
X is V52() non trivial OAffinSpace-like AffinStruct
OAS is V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
OASpace OAS is strict AffinStruct
Lambda X is V52() non trivial strict AffinSpace-like AffinStruct
OAS is V52() non trivial AffinSpace-like AffinStruct
the carrier of OAS is V4() V5() set
K11( the carrier of OAS) is set
X is M2(K11( the carrier of OAS))
c3 is M2( the carrier of OAS)
d is M2( the carrier of OAS)
c1 is M2( the carrier of OAS)
b is M2( the carrier of OAS)
c is M2( the carrier of OAS)
a1 is M2( the carrier of OAS)
b1 is M2( the carrier of OAS)
Line (c3,b) is M2(K11( the carrier of OAS))
Line (c3,c) is M2(K11( the carrier of OAS))
OAS is V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
OASpace OAS is strict AffinStruct
X is V52() non trivial OAffinSpace-like AffinStruct
Lambda X is V52() non trivial strict AffinSpace-like AffinStruct
OAS is V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
OASpace OAS is strict AffinStruct
X is V52() non trivial OAffinSpace-like AffinStruct
Lambda X is V52() non trivial strict AffinSpace-like AffinStruct
the carrier of (Lambda X) is V4() V5() set
K11( the carrier of (Lambda X)) is set
b is M2(K11( the carrier of (Lambda X)))
c is M2(K11( the carrier of (Lambda X)))
d is M2(K11( the carrier of (Lambda X)))
a1 is M2( the carrier of (Lambda X))
d1 is M2( the carrier of (Lambda X))
b1 is M2( the carrier of (Lambda X))
P is M2( the carrier of (Lambda X))
c1 is M2( the carrier of (Lambda X))
Q is M2( the carrier of (Lambda X))
the carrier of X is V4() V5() set
the carrier of OAS is V4() set
x1 is M2( the carrier of X)
x is M2( the carrier of X)
c1 is M2( the carrier of X)
a19 is M2( the carrier of X)
c19 is M2( the carrier of X)
b19 is M2( the carrier of X)
u9 is M2( the carrier of OAS)
v is M2( the carrier of OAS)
u9 + v is M2( the carrier of OAS)
u is M2( the carrier of OAS)
(u9 + v) - u is M2( the carrier of OAS)
- u is M2( the carrier of OAS)
K151(OAS,(u9 + v),(- u)) is M2( the carrier of OAS)
w is M2( the carrier of OAS)
u9 + w is M2( the carrier of OAS)
(u9 + w) - u is M2( the carrier of OAS)
K151(OAS,(u9 + w),(- u)) is M2( the carrier of OAS)
((u9 + w) - u) - ((u9 + v) - u) is M2( the carrier of OAS)
- ((u9 + v) - u) is M2( the carrier of OAS)
K151(OAS,((u9 + w) - u),(- ((u9 + v) - u))) is M2( the carrier of OAS)
((u9 + v) - u) + u is M2( the carrier of OAS)
(u9 + w) - (((u9 + v) - u) + u) is M2( the carrier of OAS)
- (((u9 + v) - u) + u) is M2( the carrier of OAS)
K151(OAS,(u9 + w),(- (((u9 + v) - u) + u))) is M2( the carrier of OAS)
(u9 + w) - (u9 + v) is M2( the carrier of OAS)
- (u9 + v) is M2( the carrier of OAS)
K151(OAS,(u9 + w),(- (u9 + v))) is M2( the carrier of OAS)
w + u9 is M2( the carrier of OAS)
(w + u9) - u9 is M2( the carrier of OAS)
- u9 is M2( the carrier of OAS)
K151(OAS,(w + u9),(- u9)) is M2( the carrier of OAS)
((w + u9) - u9) - v is M2( the carrier of OAS)
- v is M2( the carrier of OAS)
K151(OAS,((w + u9) - u9),(- v)) is M2( the carrier of OAS)
w - v is M2( the carrier of OAS)
K151(OAS,w,(- v)) is M2( the carrier of OAS)
b199 is M2( the carrier of X)
c199 is M2( the carrier of X)
OAS is V52() non trivial OAffinSpace-like AffinStruct
Lambda OAS is V52() non trivial strict AffinSpace-like AffinStruct
the carrier of (Lambda OAS) is V4() V5() set
c3 is M2( the carrier of (Lambda OAS))
b is M2( the carrier of (Lambda OAS))
c is M2( the carrier of (Lambda OAS))
d is M2( the carrier of (Lambda OAS))
the carrier of OAS is V4() V5() set
Line (c3,d) is M2(K11( the carrier of (Lambda OAS)))
K11( the carrier of (Lambda OAS)) is set
Line (b,c) is M2(K11( the carrier of (Lambda OAS)))
a1 is M2( the carrier of OAS)
b1 is M2( the carrier of OAS)
c1 is M2( the carrier of OAS)
d1 is M2( the carrier of OAS)
x1 is M2( the carrier of OAS)
x is M2( the carrier of (Lambda OAS))
OAS is V52() V78() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of OAS is V4() set
X is M2( the carrier of OAS)
c3 is M2( the carrier of OAS)
0. OAS is V59(OAS) M2( the carrier of OAS)
OAS is V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of OAS is V4() set
0. OAS is V59(OAS) M2( the carrier of OAS)
OASpace OAS is strict AffinStruct
c3 is M2( the carrier of OAS)
b is M2( the carrier of OAS)
X is V52() non trivial OAffinSpace-like AffinStruct
Lambda X is V52() non trivial strict AffinSpace-like AffinStruct
OAS is V52() V78() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of OAS is V4() set
X is M2( the carrier of OAS)
c3 is M2( the carrier of OAS)
0. OAS is V59(OAS) M2( the carrier of OAS)
OAS is V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of OAS is V4() set
0. OAS is V59(OAS) M2( the carrier of OAS)
OASpace OAS is strict AffinStruct
c3 is M2( the carrier of OAS)
b is M2( the carrier of OAS)
X is V52() non trivial OAffinSpace-like 2-dimensional AffinStruct
Lambda X is V52() non trivial strict AffinSpace-like 2-dimensional AffinStruct
c3 is V52() non trivial strict AffinSpace-like 2-dimensional AffinStruct
OAS is V52() V78() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of OAS is V4() set
X is M2( the carrier of OAS)
c3 is M2( the carrier of OAS)
0. OAS is V59(OAS) M2( the carrier of OAS)
OAS is V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of OAS is V4() set
0. OAS is V59(OAS) M2( the carrier of OAS)
OASpace OAS is strict AffinStruct
c3 is M2( the carrier of OAS)
b is M2( the carrier of OAS)
X is V52() non trivial OAffinSpace-like AffinStruct
Lambda X is V52() non trivial strict AffinSpace-like AffinStruct
OAS is V52() non trivial OAffinSpace-like AffinStruct
Lambda OAS is V52() non trivial strict AffinSpace-like AffinStruct
OAS is V52() non trivial OAffinSpace-like () AffinStruct
Lambda OAS is V52() non trivial strict AffinSpace-like Fanoian AffinStruct
OAS is V52() non trivial OAffinSpace-like () AffinStruct
Lambda OAS is V52() non trivial strict AffinSpace-like Fanoian AffinStruct
OAS is V52() non trivial OAffinSpace-like () AffinStruct
Lambda OAS is V52() non trivial strict AffinSpace-like Fanoian AffinStruct
OAS is V52() non trivial OAffinSpace-like () AffinStruct
Lambda OAS is V52() non trivial strict AffinSpace-like Fanoian AffinStruct