K28() is set
K32() is V1() V4() V5() V6() Element of K6(K28())
K6(K28()) is set
K27() is V1() V4() V5() V6() set
K6(K27()) is set
K6(K32()) is set
0 is set
1 is V1() V4() V5() V6() V10() V11() V12() Element of K32()
0 is V4() V5() V6() V10() V11() V12() Element of K32()
K39(0) is V11() V12() set
MS is V42() OrtAfSp-like ParOrtStr
the carrier of MS is V1() set
V is Element of the carrier of MS
w is Element of the carrier of MS
y is Element of the carrier of MS
Af MS is V42() V47() strict AffinSpace-like AffinStruct
the carrier of (Af MS) is V1() V2() set
OAS is Element of the carrier of (Af MS)
MS9 is Element of the carrier of (Af MS)
a1 is Element of the carrier of (Af MS)
MS is V42() OrtAfSp-like OrtAfPl-like ParOrtStr
the carrier of MS is V1() set
K6( the carrier of MS) is set
V is Element of the carrier of MS
w is Element of the carrier of MS
y is Element of the carrier of MS
MS9 is Element of the carrier of MS
OAS is Element of K6( the carrier of MS)
Af MS is V42() V47() strict AffinSpace-like 2-dimensional AffinStruct
the carrier of (Af MS) is V1() V2() set
K6( the carrier of (Af MS)) is set
a1 is Element of K6( the carrier of (Af MS))
b is Element of the carrier of (Af MS)
b1 is Element of the carrier of (Af MS)
c is Element of the carrier of MS
c1 is Element of the carrier of MS
MS is V42() OrtAfSp-like OrtAfPl-like ParOrtStr
the carrier of MS is V1() set
K6( the carrier of MS) is set
V is Element of the carrier of MS
w is Element of the carrier of MS
MS9 is Element of K6( the carrier of MS)
y is Element of K6( the carrier of MS)
OAS is Element of the carrier of MS
a1 is Element of the carrier of MS
Line (OAS,a1) is Element of K6( the carrier of MS)
b is Element of the carrier of MS
b1 is Element of the carrier of MS
Line (b,b1) is Element of K6( the carrier of MS)
MS is V42() OrtAfSp-like ParOrtStr
the carrier of MS is V1() set
V is Element of the carrier of MS
w is Element of the carrier of MS
y is Element of the carrier of MS
Af MS is V42() V47() strict AffinSpace-like AffinStruct
the carrier of (Af MS) is V1() V2() set
MS9 is Element of the carrier of (Af MS)
OAS is Element of the carrier of (Af MS)
a1 is Element of the carrier of (Af MS)
MS is V42() OrtAfSp-like OrtAfPl-like ParOrtStr
the carrier of MS is V1() set
V is Element of the carrier of MS
w is Element of the carrier of MS
y is Element of the carrier of MS
Line (V,y) is Element of K6( the carrier of MS)
K6( the carrier of MS) is set
Line (w,y) is Element of K6( the carrier of MS)
Af MS is V42() V47() strict AffinSpace-like 2-dimensional AffinStruct
the carrier of (Af MS) is V1() V2() set
K6( the carrier of (Af MS)) is set
b is Element of K6( the carrier of (Af MS))
c is Element of the carrier of (Af MS)
c1 is Element of the carrier of (Af MS)
Line (c,c1) is Element of K6( the carrier of (Af MS))
q is Element of K6( the carrier of MS)
u1 is Element of K6( the carrier of MS)
u3 is Element of K6( the carrier of (Af MS))
a1 is Element of K6( the carrier of (Af MS))
b1 is Element of the carrier of (Af MS)
Line (b1,c1) is Element of K6( the carrier of (Af MS))
u2 is Element of K6( the carrier of (Af MS))
v1 is Element of the carrier of (Af MS)
r is Element of the carrier of MS
MS is V42() OrtAfSp-like OrtAfPl-like ParOrtStr
the carrier of MS is V1() set
V is Element of the carrier of MS
w is Element of the carrier of MS
y is Element of the carrier of MS
MS9 is Element of the carrier of MS
OAS is Element of the carrier of MS
Af MS is V42() V47() strict AffinSpace-like 2-dimensional AffinStruct
the carrier of (Af MS) is V1() V2() set
c is Element of the carrier of (Af MS)
a1 is Element of the carrier of (Af MS)
c1 is Element of the carrier of (Af MS)
b is Element of the carrier of (Af MS)
Line (a1,b) is Element of K6( the carrier of (Af MS))
K6( the carrier of (Af MS)) is set
K6( the carrier of MS) is set
u1 is Element of K6( the carrier of MS)
b1 is Element of the carrier of (Af MS)
MS is V42() OrtAfSp-like OrtAfPl-like ParOrtStr
the carrier of MS is V1() set
V is Element of the carrier of MS
w is Element of the carrier of MS
y is Element of the carrier of MS
MS9 is Element of the carrier of MS
Af MS is V42() V47() strict AffinSpace-like 2-dimensional AffinStruct
the carrier of (Af MS) is V1() V2() set
OAS is Element of the carrier of (Af MS)
a1 is Element of the carrier of (Af MS)
b is Element of the carrier of (Af MS)
K6( the carrier of (Af MS)) is set
c is Element of K6( the carrier of (Af MS))
K6( the carrier of MS) is set
c1 is Element of K6( the carrier of MS)
b1 is Element of the carrier of (Af MS)
MS is V42() OrtAfSp-like OrtAfPl-like ParOrtStr
the carrier of MS is V1() set
V is Element of the carrier of MS
w is Element of the carrier of MS
y is Element of the carrier of MS
MS9 is Element of the carrier of MS
OAS is Element of the carrier of MS
V is Element of the carrier of MS
w is Element of the carrier of MS
y is Element of the carrier of MS
MS9 is Element of the carrier of MS
OAS is Element of the carrier of MS
MS is V42() OrtAfSp-like OrtAfPl-like ParOrtStr
the carrier of MS is V1() set
V is Element of the carrier of MS
w is Element of the carrier of MS
y is Element of the carrier of MS
MS9 is Element of the carrier of MS
OAS is Element of the carrier of MS
a1 is Element of the carrier of MS
b is Element of the carrier of MS
V is Element of the carrier of MS
w is Element of the carrier of MS
y is Element of the carrier of MS
MS9 is Element of the carrier of MS
OAS is Element of the carrier of MS
a1 is Element of the carrier of MS
b is Element of the carrier of MS
MS is V42() OrtAfSp-like OrtAfPl-like ParOrtStr
Af MS is V42() V47() strict AffinSpace-like 2-dimensional AffinStruct
the carrier of (Af MS) is V1() V2() set
K6( the carrier of (Af MS)) is set
w is Element of K6( the carrier of (Af MS))
y is Element of K6( the carrier of (Af MS))
MS9 is Element of the carrier of (Af MS)
OAS is Element of the carrier of (Af MS)
b1 is Element of the carrier of (Af MS)
a1 is Element of the carrier of (Af MS)
c is Element of the carrier of (Af MS)
b is Element of the carrier of (Af MS)
c1 is Element of the carrier of (Af MS)
the carrier of MS is V1() set
K6( the carrier of MS) is set
u3 is Element of the carrier of MS
B2 is Element of the carrier of MS
v1 is Element of the carrier of MS
B1 is Element of the carrier of MS
u2 is Element of the carrier of MS
r is Element of the carrier of MS
q is Element of K6( the carrier of MS)
u1 is Element of K6( the carrier of MS)
c is Element of K6( the carrier of MS)
c1 is Element of K6( the carrier of MS)
w is Element of the carrier of MS
y is Element of the carrier of MS
MS9 is Element of the carrier of MS
OAS is Element of the carrier of MS
a1 is Element of the carrier of MS
b is Element of the carrier of MS
b1 is Element of the carrier of MS
v1 is Element of the carrier of (Af MS)
B2 is Element of the carrier of (Af MS)
u2 is Element of the carrier of (Af MS)
r is Element of the carrier of (Af MS)
u3 is Element of the carrier of (Af MS)
B1 is Element of the carrier of (Af MS)
q is Element of K6( the carrier of (Af MS))
u1 is Element of K6( the carrier of (Af MS))
MS is V42() OrtAfSp-like OrtAfPl-like ParOrtStr
Af MS is V42() V47() strict AffinSpace-like 2-dimensional AffinStruct
MS is V42() OrtAfSp-like OrtAfPl-like ParOrtStr
Af MS is V42() V47() strict AffinSpace-like 2-dimensional AffinStruct
the carrier of (Af MS) is V1() V2() set
K6( the carrier of (Af MS)) is set
OAS is Element of the carrier of (Af MS)
w is Element of K6( the carrier of (Af MS))
y is Element of K6( the carrier of (Af MS))
MS9 is Element of K6( the carrier of (Af MS))
a1 is Element of the carrier of (Af MS)
b is Element of the carrier of (Af MS)
b1 is Element of the carrier of (Af MS)
c is Element of the carrier of (Af MS)
c1 is Element of the carrier of (Af MS)
q is Element of the carrier of (Af MS)
the carrier of MS is V1() set
u2 is Element of the carrier of MS
u3 is Element of the carrier of MS
r is Element of the carrier of MS
B1 is Element of the carrier of MS
v1 is Element of the carrier of MS
B2 is Element of the carrier of MS
u1 is Element of the carrier of MS
w is Element of the carrier of MS
y is Element of the carrier of MS
MS9 is Element of the carrier of MS
OAS is Element of the carrier of MS
a1 is Element of the carrier of MS
b is Element of the carrier of MS
b1 is Element of the carrier of MS
c is Element of the carrier of (Af MS)
c1 is Element of the carrier of (Af MS)
u2 is Element of the carrier of (Af MS)
r is Element of K6( the carrier of (Af MS))
u1 is Element of the carrier of (Af MS)
v1 is Element of the carrier of (Af MS)
B1 is Element of K6( the carrier of (Af MS))
q is Element of the carrier of (Af MS)
u3 is Element of the carrier of (Af MS)
B2 is Element of K6( the carrier of (Af MS))
MS is V42() OrtAfSp-like OrtAfPl-like ParOrtStr
Af MS is V42() V47() strict AffinSpace-like 2-dimensional AffinStruct
MS is V42() OrtAfSp-like OrtAfPl-like ParOrtStr
Af MS is V42() V47() strict AffinSpace-like 2-dimensional AffinStruct
the carrier of (Af MS) is V1() V2() set
K6( the carrier of (Af MS)) is set
w is Element of K6( the carrier of (Af MS))
y is Element of the carrier of (Af MS)
a1 is Element of the carrier of (Af MS)
c is Element of the carrier of (Af MS)
MS9 is Element of the carrier of (Af MS)
OAS is Element of the carrier of (Af MS)
b is Element of the carrier of (Af MS)
b1 is Element of the carrier of (Af MS)
the carrier of MS is V1() set
c1 is Element of the carrier of MS
u1 is Element of the carrier of MS
q is Element of the carrier of MS
u2 is Element of the carrier of MS
u3 is Element of the carrier of MS
r is Element of the carrier of MS
Line (MS9,OAS) is Element of K6( the carrier of (Af MS))
v1 is Element of the carrier of MS
w is Element of the carrier of MS
y is Element of the carrier of MS
MS9 is Element of the carrier of MS
OAS is Element of the carrier of MS
a1 is Element of the carrier of MS
b is Element of the carrier of MS
b1 is Element of the carrier of MS
c is Element of the carrier of (Af MS)
u3 is Element of the carrier of (Af MS)
Line (c,u3) is Element of K6( the carrier of (Af MS))
c1 is Element of the carrier of (Af MS)
u1 is Element of the carrier of (Af MS)
q is Element of the carrier of (Af MS)
u2 is Element of the carrier of (Af MS)
v1 is Element of the carrier of (Af MS)
MS is V42() OrtAfSp-like OrtAfPl-like ParOrtStr
Af MS is V42() V47() strict AffinSpace-like 2-dimensional AffinStruct
the carrier of (Af MS) is V1() V2() set
K6( the carrier of (Af MS)) is set
w is Element of K6( the carrier of (Af MS))
y is Element of K6( the carrier of (Af MS))
MS9 is Element of K6( the carrier of (Af MS))
OAS is Element of the carrier of (Af MS)
b1 is Element of the carrier of (Af MS)
a1 is Element of the carrier of (Af MS)
c is Element of the carrier of (Af MS)
b is Element of the carrier of (Af MS)
c1 is Element of the carrier of (Af MS)
the carrier of MS is V1() set
q is Element of the carrier of MS
u1 is Element of the carrier of MS
u2 is Element of the carrier of MS
u3 is Element of the carrier of MS
v1 is Element of the carrier of MS
r is Element of the carrier of MS
w is Element of the carrier of MS
y is Element of the carrier of MS
MS9 is Element of the carrier of MS
a1 is Element of the carrier of MS
OAS is Element of the carrier of MS
b is Element of the carrier of MS
b1 is Element of the carrier of (Af MS)
c is Element of the carrier of (Af MS)
c1 is Element of the carrier of (Af MS)
q is Element of the carrier of (Af MS)
u1 is Element of the carrier of (Af MS)
u2 is Element of the carrier of (Af MS)
Line (b1,c) is Element of K6( the carrier of (Af MS))
v1 is Element of K6( the carrier of (Af MS))
r is Element of K6( the carrier of (Af MS))
MS is V42() OrtAfSp-like OrtAfPl-like ParOrtStr
Af MS is V42() V47() strict AffinSpace-like 2-dimensional AffinStruct
MS is V42() OrtAfSp-like OrtAfPl-like ParOrtStr
MS is V42() OrtAfSp-like OrtAfPl-like ParOrtStr
MS is V42() OrtAfSp-like OrtAfPl-like ParOrtStr
the carrier of MS is V1() set
V is Element of the carrier of MS
w is Element of the carrier of MS
MS9 is Element of the carrier of MS
y is Element of the carrier of MS
OAS is Element of the carrier of MS
a1 is Element of the carrier of MS
Af MS is V42() V47() strict AffinSpace-like 2-dimensional AffinStruct
the carrier of (Af MS) is V1() V2() set
b is Element of the carrier of (Af MS)
b1 is Element of the carrier of (Af MS)
c is Element of the carrier of (Af MS)
c1 is Element of the carrier of (Af MS)
MS is V42() OrtAfSp-like OrtAfPl-like ParOrtStr
the carrier of MS is V1() set
V is Element of the carrier of MS
w is Element of the carrier of MS
MS9 is Element of the carrier of MS
y is Element of the carrier of MS
Line (w,MS9) is Element of K6( the carrier of MS)
K6( the carrier of MS) is set
Line (V,MS9) is Element of K6( the carrier of MS)
b is Element of K6( the carrier of MS)
b1 is Element of K6( the carrier of MS)
Af MS is V42() V47() strict AffinSpace-like 2-dimensional AffinStruct
the carrier of (Af MS) is V1() V2() set
K6( the carrier of (Af MS)) is set
c1 is Element of K6( the carrier of (Af MS))
u1 is Element of the carrier of (Af MS)
u2 is Element of the carrier of (Af MS)
Line (u1,u2) is Element of K6( the carrier of (Af MS))
q is Element of the carrier of (Af MS)
Line (q,u2) is Element of K6( the carrier of (Af MS))
u3 is Element of K6( the carrier of (Af MS))
v1 is Element of K6( the carrier of (Af MS))
c is Element of K6( the carrier of (Af MS))
u3 is Element of the carrier of (Af MS)
v1 is Element of the carrier of MS
MS is V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of MS is V1() set
V is Element of the carrier of MS
y is Element of the carrier of MS
V - y is Element of the carrier of MS
- y is Element of the carrier of MS
K146(MS,V,(- y)) is Element of the carrier of MS
w is Element of the carrier of MS
w - y is Element of the carrier of MS
K146(MS,w,(- y)) is Element of the carrier of MS
(V - y) - (w - y) is Element of the carrier of MS
- (w - y) is Element of the carrier of MS
K146(MS,(V - y),(- (w - y))) is Element of the carrier of MS
V - w is Element of the carrier of MS
- w is Element of the carrier of MS
K146(MS,V,(- w)) is Element of the carrier of MS
V + y is Element of the carrier of MS
w + y is Element of the carrier of MS
(V + y) - (w + y) is Element of the carrier of MS
- (w + y) is Element of the carrier of MS
K146(MS,(V + y),(- (w + y))) is Element of the carrier of MS
y - w is Element of the carrier of MS
K146(MS,y,(- w)) is Element of the carrier of MS
(V - y) + (y - w) is Element of the carrier of MS
V - (- y) is Element of the carrier of MS
- (- y) is Element of the carrier of MS
K146(MS,V,(- (- y))) is Element of the carrier of MS
(V - (- y)) - (w + y) is Element of the carrier of MS
K146(MS,(V - (- y)),(- (w + y))) is Element of the carrier of MS
w - (- y) is Element of the carrier of MS
K146(MS,w,(- (- y))) is Element of the carrier of MS
(V - (- y)) - (w - (- y)) is Element of the carrier of MS
- (w - (- y)) is Element of the carrier of MS
K146(MS,(V - (- y)),(- (w - (- y)))) is Element of the carrier of MS
(- y) - w is Element of the carrier of MS
K146(MS,(- y),(- w)) is Element of the carrier of MS
(V - (- y)) + ((- y) - w) is Element of the carrier of MS
MS is V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of MS is V1() set
V is Element of the carrier of MS
w is Element of the carrier of MS
y is V11() V12() Element of K28()
y * V is Element of the carrier of MS
MS9 is V11() V12() Element of K28()
MS9 * w is Element of the carrier of MS
(y * V) + (MS9 * w) is Element of the carrier of MS
OAS is V11() V12() Element of K28()
OAS * MS9 is V11() V12() Element of K28()
(OAS * MS9) * V is Element of the carrier of MS
OAS * y is V11() V12() Element of K28()
- (OAS * y) is V11() V12() Element of K28()
(- (OAS * y)) * w is Element of the carrier of MS
((OAS * MS9) * V) + ((- (OAS * y)) * w) is Element of the carrier of MS
PProJ (V,w,((y * V) + (MS9 * w)),(((OAS * MS9) * V) + ((- (OAS * y)) * w))) is V11() V12() Element of K28()
pr2 (V,w,((y * V) + (MS9 * w))) is V11() V12() Element of K28()
pr2 (V,w,(((OAS * MS9) * V) + ((- (OAS * y)) * w))) is V11() V12() Element of K28()
pr1 (V,w,((y * V) + (MS9 * w))) is V11() V12() Element of K28()
pr1 (V,w,(((OAS * MS9) * V) + ((- (OAS * y)) * w))) is V11() V12() Element of K28()
MS9 * OAS is V11() V12() Element of K28()
y * (MS9 * OAS) is V11() V12() Element of K28()
MS9 * (- (OAS * y)) is V11() V12() Element of K28()
(y * (MS9 * OAS)) + (MS9 * (- (OAS * y))) is V11() V12() Element of K28()
MS is V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of MS is V1() set
0. MS is V49(MS) Element of the carrier of MS
V is Element of the carrier of MS
w is Element of the carrier of MS
y is Element of the carrier of MS
MS9 is Element of the carrier of MS
OAS is V11() V12() Element of K28()
OAS * V is Element of the carrier of MS
a1 is V11() V12() Element of K28()
a1 * w is Element of the carrier of MS
(OAS * V) + (a1 * w) is Element of the carrier of MS
a1 * V is Element of the carrier of MS
- OAS is V11() V12() Element of K28()
(- OAS) * w is Element of the carrier of MS
(a1 * V) + ((- OAS) * w) is Element of the carrier of MS
1 * a1 is V11() V12() Element of K28()
(1 * a1) * V is Element of the carrier of MS
1 * OAS is V11() V12() Element of K28()
- (1 * OAS) is V11() V12() Element of K28()
(- (1 * OAS)) * w is Element of the carrier of MS
((1 * a1) * V) + ((- (1 * OAS)) * w) is Element of the carrier of MS
b1 is V11() V12() Element of K28()
b1 * MS9 is Element of the carrier of MS
c is V11() V12() Element of K28()
c * ((a1 * V) + ((- OAS) * w)) is Element of the carrier of MS
0 * w is Element of the carrier of MS
(0. MS) + (0 * w) is Element of the carrier of MS
(0. MS) + (0. MS) is Element of the carrier of MS
b1 " is V11() V12() Element of K28()
(b1 ") * c is V11() V12() Element of K28()
c1 is V11() V12() Element of K28()
c1 * a1 is V11() V12() Element of K28()
(c1 * a1) * V is Element of the carrier of MS
c1 * OAS is V11() V12() Element of K28()
- (c1 * OAS) is V11() V12() Element of K28()
(- (c1 * OAS)) * w is Element of the carrier of MS
((c1 * a1) * V) + ((- (c1 * OAS)) * w) is Element of the carrier of MS
(b1 ") * (c * ((a1 * V) + ((- OAS) * w))) is Element of the carrier of MS
c1 * ((a1 * V) + ((- OAS) * w)) is Element of the carrier of MS
c1 * (a1 * V) is Element of the carrier of MS
c1 * ((- OAS) * w) is Element of the carrier of MS
(c1 * (a1 * V)) + (c1 * ((- OAS) * w)) is Element of the carrier of MS
((c1 * a1) * V) + (c1 * ((- OAS) * w)) is Element of the carrier of MS
c1 * (- OAS) is V11() V12() Element of K28()
(c1 * (- OAS)) * w is Element of the carrier of MS
((c1 * a1) * V) + ((c1 * (- OAS)) * w) is Element of the carrier of MS
MS is V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of MS is V1() set
0. MS is V49(MS) Element of the carrier of MS
V is Element of the carrier of MS
w is Element of the carrier of MS
y is Element of the carrier of MS
MS9 is Element of the carrier of MS
OAS is V11() V12() Element of K28()
OAS * V is Element of the carrier of MS
a1 is V11() V12() Element of K28()
a1 * w is Element of the carrier of MS
(OAS * V) + (a1 * w) is Element of the carrier of MS
b is V11() V12() Element of K28()
b * a1 is V11() V12() Element of K28()
(b * a1) * V is Element of the carrier of MS
b * OAS is V11() V12() Element of K28()
- (b * OAS) is V11() V12() Element of K28()
(- (b * OAS)) * w is Element of the carrier of MS
((b * a1) * V) + ((- (b * OAS)) * w) is Element of the carrier of MS
b1 is V11() V12() Element of K28()
b1 * V is Element of the carrier of MS
c is V11() V12() Element of K28()
c * w is Element of the carrier of MS
(b1 * V) + (c * w) is Element of the carrier of MS
b * c is V11() V12() Element of K28()
(b * c) * V is Element of the carrier of MS
b * b1 is V11() V12() Element of K28()
- (b * b1) is V11() V12() Element of K28()
(- (b * b1)) * w is Element of the carrier of MS
((b * c) * V) + ((- (b * b1)) * w) is Element of the carrier of MS
((b1 * V) + (c * w)) - y is Element of the carrier of MS
- y is Element of the carrier of MS
K146(MS,((b1 * V) + (c * w)),(- y)) is Element of the carrier of MS
(((b * c) * V) + ((- (b * b1)) * w)) - MS9 is Element of the carrier of MS
- MS9 is Element of the carrier of MS
K146(MS,(((b * c) * V) + ((- (b * b1)) * w)),(- MS9)) is Element of the carrier of MS
pr1 (V,w,((b1 * V) + (c * w))) is V11() V12() Element of K28()
pr2 (V,w,((b1 * V) + (c * w))) is V11() V12() Element of K28()
pr1 (V,w,(((b * c) * V) + ((- (b * b1)) * w))) is V11() V12() Element of K28()
pr2 (V,w,(((b * c) * V) + ((- (b * b1)) * w))) is V11() V12() Element of K28()
pr1 (V,w,y) is V11() V12() Element of K28()
pr2 (V,w,y) is V11() V12() Element of K28()
PProJ (V,w,y,(((b * c) * V) + ((- (b * b1)) * w))) is V11() V12() Element of K28()
OAS * (b * c) is V11() V12() Element of K28()
a1 * (- (b * b1)) is V11() V12() Element of K28()
(OAS * (b * c)) + (a1 * (- (b * b1))) is V11() V12() Element of K28()
pr1 (V,w,MS9) is V11() V12() Element of K28()
pr2 (V,w,MS9) is V11() V12() Element of K28()
PProJ (V,w,((b1 * V) + (c * w)),MS9) is V11() V12() Element of K28()
(b * a1) * b1 is V11() V12() Element of K28()
(- (b * OAS)) * c is V11() V12() Element of K28()
((b * a1) * b1) + ((- (b * OAS)) * c) is V11() V12() Element of K28()
PProJ (V,w,(((b1 * V) + (c * w)) - y),((((b * c) * V) + ((- (b * b1)) * w)) - MS9)) is V11() V12() Element of K28()
PProJ (V,w,(((b1 * V) + (c * w)) - y),(((b * c) * V) + ((- (b * b1)) * w))) is V11() V12() Element of K28()
PProJ (V,w,(((b1 * V) + (c * w)) - y),MS9) is V11() V12() Element of K28()
(PProJ (V,w,(((b1 * V) + (c * w)) - y),(((b * c) * V) + ((- (b * b1)) * w)))) - (PProJ (V,w,(((b1 * V) + (c * w)) - y),MS9)) is V11() V12() Element of K28()
PProJ (V,w,((b1 * V) + (c * w)),(((b * c) * V) + ((- (b * b1)) * w))) is V11() V12() Element of K28()
(PProJ (V,w,((b1 * V) + (c * w)),(((b * c) * V) + ((- (b * b1)) * w)))) - (PProJ (V,w,y,(((b * c) * V) + ((- (b * b1)) * w)))) is V11() V12() Element of K28()
((PProJ (V,w,((b1 * V) + (c * w)),(((b * c) * V) + ((- (b * b1)) * w)))) - (PProJ (V,w,y,(((b * c) * V) + ((- (b * b1)) * w))))) - (PProJ (V,w,(((b1 * V) + (c * w)) - y),MS9)) is V11() V12() Element of K28()
0 - (PProJ (V,w,y,(((b * c) * V) + ((- (b * b1)) * w)))) is V11() V12() Element of K28()
(0 - (PProJ (V,w,y,(((b * c) * V) + ((- (b * b1)) * w))))) - (PProJ (V,w,(((b1 * V) + (c * w)) - y),MS9)) is V11() V12() Element of K28()
- (PProJ (V,w,y,(((b * c) * V) + ((- (b * b1)) * w)))) is V11() V12() Element of K28()
PProJ (V,w,y,MS9) is V11() V12() Element of K28()
(PProJ (V,w,((b1 * V) + (c * w)),MS9)) - (PProJ (V,w,y,MS9)) is V11() V12() Element of K28()
(- (PProJ (V,w,y,(((b * c) * V) + ((- (b * b1)) * w))))) - ((PProJ (V,w,((b1 * V) + (c * w)),MS9)) - (PProJ (V,w,y,MS9))) is V11() V12() Element of K28()
(PProJ (V,w,((b1 * V) + (c * w)),MS9)) - 0 is V11() V12() Element of K28()
(- (PProJ (V,w,y,(((b * c) * V) + ((- (b * b1)) * w))))) - ((PProJ (V,w,((b1 * V) + (c * w)),MS9)) - 0) is V11() V12() Element of K28()
- 1 is V11() V12() Element of K28()
(PProJ (V,w,y,(((b * c) * V) + ((- (b * b1)) * w)))) + (PProJ (V,w,((b1 * V) + (c * w)),MS9)) is V11() V12() Element of K28()
(- 1) * ((PProJ (V,w,y,(((b * c) * V) + ((- (b * b1)) * w)))) + (PProJ (V,w,((b1 * V) + (c * w)),MS9))) is V11() V12() Element of K28()
MS is V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of MS is V1() set
V is Element of the carrier of MS
w is Element of the carrier of MS
y is V11() V12() Element of K28()
y * V is Element of the carrier of MS
MS9 is V11() V12() Element of K28()
MS9 * w is Element of the carrier of MS
(y * V) + (MS9 * w) is Element of the carrier of MS
OAS is V11() V12() Element of K28()
OAS * V is Element of the carrier of MS
a1 is V11() V12() Element of K28()
a1 * w is Element of the carrier of MS
(OAS * V) + (a1 * w) is Element of the carrier of MS
((y * V) + (MS9 * w)) - ((OAS * V) + (a1 * w)) is Element of the carrier of MS
- ((OAS * V) + (a1 * w)) is Element of the carrier of MS
K146(MS,((y * V) + (MS9 * w)),(- ((OAS * V) + (a1 * w)))) is Element of the carrier of MS
y - OAS is V11() V12() Element of K28()
(y - OAS) * V is Element of the carrier of MS
MS9 - a1 is V11() V12() Element of K28()
(MS9 - a1) * w is Element of the carrier of MS
((y - OAS) * V) + ((MS9 - a1) * w) is Element of the carrier of MS
(y * V) - ((OAS * V) + (a1 * w)) is Element of the carrier of MS
K146(MS,(y * V),(- ((OAS * V) + (a1 * w)))) is Element of the carrier of MS
(MS9 * w) + ((y * V) - ((OAS * V) + (a1 * w))) is Element of the carrier of MS
(y * V) - (OAS * V) is Element of the carrier of MS
- (OAS * V) is Element of the carrier of MS
K146(MS,(y * V),(- (OAS * V))) is Element of the carrier of MS
((y * V) - (OAS * V)) - (a1 * w) is Element of the carrier of MS
- (a1 * w) is Element of the carrier of MS
K146(MS,((y * V) - (OAS * V)),(- (a1 * w))) is Element of the carrier of MS
(MS9 * w) + (((y * V) - (OAS * V)) - (a1 * w)) is Element of the carrier of MS
((y - OAS) * V) - (a1 * w) is Element of the carrier of MS
K146(MS,((y - OAS) * V),(- (a1 * w))) is Element of the carrier of MS
(MS9 * w) + (((y - OAS) * V) - (a1 * w)) is Element of the carrier of MS
((y - OAS) * V) + (MS9 * w) is Element of the carrier of MS
(((y - OAS) * V) + (MS9 * w)) - (a1 * w) is Element of the carrier of MS
K146(MS,(((y - OAS) * V) + (MS9 * w)),(- (a1 * w))) is Element of the carrier of MS
(MS9 * w) - (a1 * w) is Element of the carrier of MS
K146(MS,(MS9 * w),(- (a1 * w))) is Element of the carrier of MS
((y - OAS) * V) + ((MS9 * w) - (a1 * w)) is Element of the carrier of MS
MS is V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of MS is V1() set
V is Element of the carrier of MS
w is Element of the carrier of MS
y is V11() V12() Element of K28()
y * V is Element of the carrier of MS
OAS is V11() V12() Element of K28()
OAS * w is Element of the carrier of MS
(y * V) + (OAS * w) is Element of the carrier of MS
MS9 is V11() V12() Element of K28()
MS9 * V is Element of the carrier of MS
a1 is V11() V12() Element of K28()
a1 * w is Element of the carrier of MS
(MS9 * V) + (a1 * w) is Element of the carrier of MS
0. MS is V49(MS) Element of the carrier of MS
((y * V) + (OAS * w)) - ((MS9 * V) + (a1 * w)) is Element of the carrier of MS
- ((MS9 * V) + (a1 * w)) is Element of the carrier of MS
K146(MS,((y * V) + (OAS * w)),(- ((MS9 * V) + (a1 * w)))) is Element of the carrier of MS
y - MS9 is V11() V12() Element of K28()
(y - MS9) * V is Element of the carrier of MS
OAS - a1 is V11() V12() Element of K28()
(OAS - a1) * w is Element of the carrier of MS
((y - MS9) * V) + ((OAS - a1) * w) is Element of the carrier of MS
- MS9 is V11() V12() Element of K28()
(- MS9) + y is V11() V12() Element of K28()
- a1 is V11() V12() Element of K28()
(- a1) + OAS is V11() V12() Element of K28()
MS is V42() OrtAfSp-like OrtAfPl-like ParOrtStr
V is V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is V1() set
w is Element of the carrier of V
y is Element of the carrier of V
AMSpace (V,w,y) is V42() strict ParOrtStr
the carrier of MS is V1() set
MS9 is Element of the carrier of MS
OAS is Element of the carrier of MS
a1 is Element of the carrier of MS
b is Element of the carrier of MS
b1 is Element of the carrier of MS
c is Element of the carrier of MS
c1 is Element of the carrier of MS
u1 is Element of the carrier of V
q is Element of the carrier of V
u1 - q is Element of the carrier of V
- q is Element of the carrier of V
K146(V,u1,(- q)) is Element of the carrier of V
r is V11() V12() Element of K28()
r * w is Element of the carrier of V
B1 is V11() V12() Element of K28()
B1 * y is Element of the carrier of V
(r * w) + (B1 * y) is Element of the carrier of V
Af MS is V42() V47() strict AffinSpace-like 2-dimensional AffinStruct
the carrier of (Af MS) is V1() V2() set
B2 is Element of the carrier of (Af MS)
v39 is Element of the carrier of (Af MS)
A2 is Element of the carrier of (Af MS)
A1 is Element of the carrier of (Af MS)
u3 is Element of the carrier of V
v1 is Element of the carrier of V
u3 - q is Element of the carrier of V
K146(V,u3,(- q)) is Element of the carrier of V
v1 - q is Element of the carrier of V
K146(V,v1,(- q)) is Element of the carrier of V
0. V is V49(V) Element of the carrier of V
B2 is V11() V12() Element of K28()
u2 is Element of the carrier of V
u2 - q is Element of the carrier of V
K146(V,u2,(- q)) is Element of the carrier of V
A1 is V11() V12() Element of K28()
A1 * (u1 - q) is Element of the carrier of V
A2 is V11() V12() Element of K28()
A2 * (u2 - q) is Element of the carrier of V
v39 is V11() V12() Element of K28()
v39 * w is Element of the carrier of V
v29 is V11() V12() Element of K28()
v29 * y is Element of the carrier of V
(v39 * w) + (v29 * y) is Element of the carrier of V
A2 " is V11() V12() Element of K28()
(A2 ") * A1 is V11() V12() Element of K28()
(A2 ") * (A1 * (u1 - q)) is Element of the carrier of V
((A2 ") * A1) * (u1 - q) is Element of the carrier of V
((A2 ") * A1) * (r * w) is Element of the carrier of V
((A2 ") * A1) * (B1 * y) is Element of the carrier of V
(((A2 ") * A1) * (r * w)) + (((A2 ") * A1) * (B1 * y)) is Element of the carrier of V
((A2 ") * A1) * r is V11() V12() Element of K28()
(((A2 ") * A1) * r) * w is Element of the carrier of V
((((A2 ") * A1) * r) * w) + (((A2 ") * A1) * (B1 * y)) is Element of the carrier of V
((A2 ") * A1) * B1 is V11() V12() Element of K28()
(((A2 ") * A1) * B1) * y is Element of the carrier of V
((((A2 ") * A1) * r) * w) + ((((A2 ") * A1) * B1) * y) is Element of the carrier of V
B2 * B1 is V11() V12() Element of K28()
(B2 * B1) * w is Element of the carrier of V
B2 * r is V11() V12() Element of K28()
- (B2 * r) is V11() V12() Element of K28()
(- (B2 * r)) * y is Element of the carrier of V
((B2 * B1) * w) + ((- (B2 * r)) * y) is Element of the carrier of V
(((B2 * B1) * w) + ((- (B2 * r)) * y)) + q is Element of the carrier of V
B2 * v29 is V11() V12() Element of K28()
(B2 * v29) * w is Element of the carrier of V
B2 * v39 is V11() V12() Element of K28()
- (B2 * v39) is V11() V12() Element of K28()
(- (B2 * v39)) * y is Element of the carrier of V
((B2 * v29) * w) + ((- (B2 * v39)) * y) is Element of the carrier of V
(((B2 * v29) * w) + ((- (B2 * v39)) * y)) + q is Element of the carrier of V
((((B2 * v29) * w) + ((- (B2 * v39)) * y)) + q) - q is Element of the carrier of V
K146(V,((((B2 * v29) * w) + ((- (B2 * v39)) * y)) + q),(- q)) is Element of the carrier of V
- y is Element of the carrier of V
(B2 * v39) * (- y) is Element of the carrier of V
((B2 * v29) * w) + ((B2 * v39) * (- y)) is Element of the carrier of V
B2 * (((A2 ") * A1) * B1) is V11() V12() Element of K28()
(B2 * (((A2 ") * A1) * B1)) * w is Element of the carrier of V
B2 * (((A2 ") * A1) * r) is V11() V12() Element of K28()
(B2 * (((A2 ") * A1) * r)) * y is Element of the carrier of V
((B2 * (((A2 ") * A1) * B1)) * w) - ((B2 * (((A2 ") * A1) * r)) * y) is Element of the carrier of V
- ((B2 * (((A2 ") * A1) * r)) * y) is Element of the carrier of V
K146(V,((B2 * (((A2 ") * A1) * B1)) * w),(- ((B2 * (((A2 ") * A1) * r)) * y))) is Element of the carrier of V
(((A2 ") * A1) * B1) * w is Element of the carrier of V
B2 * ((((A2 ") * A1) * B1) * w) is Element of the carrier of V
(B2 * ((((A2 ") * A1) * B1) * w)) - ((B2 * (((A2 ") * A1) * r)) * y) is Element of the carrier of V
K146(V,(B2 * ((((A2 ") * A1) * B1) * w)),(- ((B2 * (((A2 ") * A1) * r)) * y))) is Element of the carrier of V
(((A2 ") * A1) * r) * y is Element of the carrier of V
B2 * ((((A2 ") * A1) * r) * y) is Element of the carrier of V
(B2 * ((((A2 ") * A1) * B1) * w)) - (B2 * ((((A2 ") * A1) * r) * y)) is Element of the carrier of V
- (B2 * ((((A2 ") * A1) * r) * y)) is Element of the carrier of V
K146(V,(B2 * ((((A2 ") * A1) * B1) * w)),(- (B2 * ((((A2 ") * A1) * r) * y)))) is Element of the carrier of V
((((A2 ") * A1) * B1) * w) - ((((A2 ") * A1) * r) * y) is Element of the carrier of V
- ((((A2 ") * A1) * r) * y) is Element of the carrier of V
K146(V,((((A2 ") * A1) * B1) * w),(- ((((A2 ") * A1) * r) * y))) is Element of the carrier of V
B2 * (((((A2 ") * A1) * B1) * w) - ((((A2 ") * A1) * r) * y)) is Element of the carrier of V
B1 * w is Element of the carrier of V
((A2 ") * A1) * (B1 * w) is Element of the carrier of V
(((A2 ") * A1) * (B1 * w)) - ((((A2 ") * A1) * r) * y) is Element of the carrier of V
K146(V,(((A2 ") * A1) * (B1 * w)),(- ((((A2 ") * A1) * r) * y))) is Element of the carrier of V
B2 * ((((A2 ") * A1) * (B1 * w)) - ((((A2 ") * A1) * r) * y)) is Element of the carrier of V
r * y is Element of the carrier of V
((A2 ") * A1) * (r * y) is Element of the carrier of V
(((A2 ") * A1) * (B1 * w)) - (((A2 ") * A1) * (r * y)) is Element of the carrier of V
- (((A2 ") * A1) * (r * y)) is Element of the carrier of V
K146(V,(((A2 ") * A1) * (B1 * w)),(- (((A2 ") * A1) * (r * y)))) is Element of the carrier of V
B2 * ((((A2 ") * A1) * (B1 * w)) - (((A2 ") * A1) * (r * y))) is Element of the carrier of V
(B1 * w) - (r * y) is Element of the carrier of V
- (r * y) is Element of the carrier of V
K146(V,(B1 * w),(- (r * y))) is Element of the carrier of V
((A2 ") * A1) * ((B1 * w) - (r * y)) is Element of the carrier of V
B2 * (((A2 ") * A1) * ((B1 * w) - (r * y))) is Element of the carrier of V
((A2 ") * A1) * B2 is V11() V12() Element of K28()
(((A2 ") * A1) * B2) * ((B1 * w) - (r * y)) is Element of the carrier of V
B2 * ((B1 * w) - (r * y)) is Element of the carrier of V
((A2 ") * A1) * (B2 * ((B1 * w) - (r * y))) is Element of the carrier of V
B2 * (B1 * w) is Element of the carrier of V
B2 * (r * y) is Element of the carrier of V
(B2 * (B1 * w)) - (B2 * (r * y)) is Element of the carrier of V
- (B2 * (r * y)) is Element of the carrier of V
K146(V,(B2 * (B1 * w)),(- (B2 * (r * y)))) is Element of the carrier of V
((A2 ") * A1) * ((B2 * (B1 * w)) - (B2 * (r * y))) is Element of the carrier of V
((B2 * B1) * w) - (B2 * (r * y)) is Element of the carrier of V
K146(V,((B2 * B1) * w),(- (B2 * (r * y)))) is Element of the carrier of V
((A2 ") * A1) * (((B2 * B1) * w) - (B2 * (r * y))) is Element of the carrier of V
(B2 * r) * y is Element of the carrier of V
- ((B2 * r) * y) is Element of the carrier of V
((B2 * B1) * w) + (- ((B2 * r) * y)) is Element of the carrier of V
((A2 ") * A1) * (((B2 * B1) * w) + (- ((B2 * r) * y))) is Element of the carrier of V
(B2 * r) * (- y) is Element of the carrier of V
((B2 * B1) * w) + ((B2 * r) * (- y)) is Element of the carrier of V
((A2 ") * A1) * (((B2 * B1) * w) + ((B2 * r) * (- y))) is Element of the carrier of V
((A2 ") * A1) * (((B2 * B1) * w) + ((- (B2 * r)) * y)) is Element of the carrier of V
((((B2 * B1) * w) + ((- (B2 * r)) * y)) + q) - q is Element of the carrier of V
K146(V,((((B2 * B1) * w) + ((- (B2 * r)) * y)) + q),(- q)) is Element of the carrier of V
((A2 ") * A1) * (((((B2 * B1) * w) + ((- (B2 * r)) * y)) + q) - q) is Element of the carrier of V
b19 is Element of the carrier of MS
u2 - ((((B2 * v29) * w) + ((- (B2 * v39)) * y)) + q) is Element of the carrier of V
- ((((B2 * v29) * w) + ((- (B2 * v39)) * y)) + q) is Element of the carrier of V
K146(V,u2,(- ((((B2 * v29) * w) + ((- (B2 * v39)) * y)) + q))) is Element of the carrier of V
1 * (u2 - ((((B2 * v29) * w) + ((- (B2 * v39)) * y)) + q)) is Element of the carrier of V
(((A2 ") * A1) * (u1 - q)) - (((A2 ") * A1) * (((((B2 * B1) * w) + ((- (B2 * r)) * y)) + q) - q)) is Element of the carrier of V
- (((A2 ") * A1) * (((((B2 * B1) * w) + ((- (B2 * r)) * y)) + q) - q)) is Element of the carrier of V
K146(V,(((A2 ") * A1) * (u1 - q)),(- (((A2 ") * A1) * (((((B2 * B1) * w) + ((- (B2 * r)) * y)) + q) - q)))) is Element of the carrier of V
(u1 - q) - (((((B2 * B1) * w) + ((- (B2 * r)) * y)) + q) - q) is Element of the carrier of V
- (((((B2 * B1) * w) + ((- (B2 * r)) * y)) + q) - q) is Element of the carrier of V
K146(V,(u1 - q),(- (((((B2 * B1) * w) + ((- (B2 * r)) * y)) + q) - q))) is Element of the carrier of V
((A2 ") * A1) * ((u1 - q) - (((((B2 * B1) * w) + ((- (B2 * r)) * y)) + q) - q)) is Element of the carrier of V
u1 - ((((B2 * B1) * w) + ((- (B2 * r)) * y)) + q) is Element of the carrier of V
- ((((B2 * B1) * w) + ((- (B2 * r)) * y)) + q) is Element of the carrier of V
K146(V,u1,(- ((((B2 * B1) * w) + ((- (B2 * r)) * y)) + q))) is Element of the carrier of V
((A2 ") * A1) * (u1 - ((((B2 * B1) * w) + ((- (B2 * r)) * y)) + q)) is Element of the carrier of V
a19 is Element of the carrier of MS
(u2 - q) - (u3 - q) is Element of the carrier of V
- (u3 - q) is Element of the carrier of V
K146(V,(u2 - q),(- (u3 - q))) is Element of the carrier of V
u2 - u3 is Element of the carrier of V
- u3 is Element of the carrier of V
K146(V,u2,(- u3)) is Element of the carrier of V
(((((B2 * v29) * w) + ((- (B2 * v39)) * y)) + q) - q) - (v1 - q) is Element of the carrier of V
- (v1 - q) is Element of the carrier of V
K146(V,(((((B2 * v29) * w) + ((- (B2 * v39)) * y)) + q) - q),(- (v1 - q))) is Element of the carrier of V
((((B2 * v29) * w) + ((- (B2 * v39)) * y)) + q) - v1 is Element of the carrier of V
- v1 is Element of the carrier of V
K146(V,((((B2 * v29) * w) + ((- (B2 * v39)) * y)) + q),(- v1)) is Element of the carrier of V
(u1 - q) - (u3 - q) is Element of the carrier of V
K146(V,(u1 - q),(- (u3 - q))) is Element of the carrier of V
u1 - u3 is Element of the carrier of V
K146(V,u1,(- u3)) is Element of the carrier of V
(((((B2 * B1) * w) + ((- (B2 * r)) * y)) + q) - q) - (v1 - q) is Element of the carrier of V
K146(V,(((((B2 * B1) * w) + ((- (B2 * r)) * y)) + q) - q),(- (v1 - q))) is Element of the carrier of V
((((B2 * B1) * w) + ((- (B2 * r)) * y)) + q) - v1 is Element of the carrier of V
K146(V,((((B2 * B1) * w) + ((- (B2 * r)) * y)) + q),(- v1)) is Element of the carrier of V
MS is V42() OrtAfSp-like OrtAfPl-like ParOrtStr
the carrier of MS is V1() set
V is Element of the carrier of MS
MS9 is Element of the carrier of MS
OAS is Element of the carrier of MS
a1 is Element of the carrier of MS
b is Element of the carrier of MS
w is Element of the carrier of MS
y is Element of the carrier of MS
MS is V42() OrtAfSp-like OrtAfPl-like ParOrtStr
V is V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is V1() set
w is Element of the carrier of V
y is Element of the carrier of V
AMSpace (V,w,y) is V42() strict ParOrtStr
the carrier of MS is V1() set
MS9 is Element of the carrier of MS
OAS is Element of the carrier of MS
a1 is Element of the carrier of MS
b is Element of the carrier of MS
b1 is Element of the carrier of MS
c is Element of the carrier of MS
c1 is Element of the carrier of MS
q is Element of the carrier of V
u1 is Element of the carrier of V
v1 is Element of the carrier of V
u1 - q is Element of the carrier of V
- q is Element of the carrier of V
K146(V,u1,(- q)) is Element of the carrier of V
v1 - q is Element of the carrier of V
K146(V,v1,(- q)) is Element of the carrier of V
0. V is V49(V) Element of the carrier of V
r is V11() V12() Element of K28()
u2 is Element of the carrier of V
u2 - q is Element of the carrier of V
K146(V,u2,(- q)) is Element of the carrier of V
B1 is V11() V12() Element of K28()
B1 * w is Element of the carrier of V
B2 is V11() V12() Element of K28()
B2 * y is Element of the carrier of V
(B1 * w) + (B2 * y) is Element of the carrier of V
u3 is Element of the carrier of V
u3 - q is Element of the carrier of V
K146(V,u3,(- q)) is Element of the carrier of V
A1 is V11() V12() Element of K28()
A1 * w is Element of the carrier of V
A2 is V11() V12() Element of K28()
A2 * y is Element of the carrier of V
(A1 * w) + (A2 * y) is Element of the carrier of V
r * A2 is V11() V12() Element of K28()
(r * A2) * w is Element of the carrier of V
r * A1 is V11() V12() Element of K28()
- (r * A1) is V11() V12() Element of K28()
(- (r * A1)) * y is Element of the carrier of V
((r * A2) * w) + ((- (r * A1)) * y) is Element of the carrier of V
(((r * A2) * w) + ((- (r * A1)) * y)) + q is Element of the carrier of V
r * B2 is V11() V12() Element of K28()
(r * B2) * w is Element of the carrier of V
r * B1 is V11() V12() Element of K28()
- (r * B1) is V11() V12() Element of K28()
(- (r * B1)) * y is Element of the carrier of V
((r * B2) * w) + ((- (r * B1)) * y) is Element of the carrier of V
(((r * B2) * w) + ((- (r * B1)) * y)) + q is Element of the carrier of V
((((r * B2) * w) + ((- (r * B1)) * y)) + q) - q is Element of the carrier of V
K146(V,((((r * B2) * w) + ((- (r * B1)) * y)) + q),(- q)) is Element of the carrier of V
(u2 - q) - (u1 - q) is Element of the carrier of V
- (u1 - q) is Element of the carrier of V
K146(V,(u2 - q),(- (u1 - q))) is Element of the carrier of V
u2 - u1 is Element of the carrier of V
- u1 is Element of the carrier of V
K146(V,u2,(- u1)) is Element of the carrier of V
(((((r * B2) * w) + ((- (r * B1)) * y)) + q) - q) - (v1 - q) is Element of the carrier of V
- (v1 - q) is Element of the carrier of V
K146(V,(((((r * B2) * w) + ((- (r * B1)) * y)) + q) - q),(- (v1 - q))) is Element of the carrier of V
((((r * B2) * w) + ((- (r * B1)) * y)) + q) - v1 is Element of the carrier of V
- v1 is Element of the carrier of V
K146(V,((((r * B2) * w) + ((- (r * B1)) * y)) + q),(- v1)) is Element of the carrier of V
b19 is Element of the carrier of MS
((((r * A2) * w) + ((- (r * A1)) * y)) + q) - q is Element of the carrier of V
K146(V,((((r * A2) * w) + ((- (r * A1)) * y)) + q),(- q)) is Element of the carrier of V
u3 - u2 is Element of the carrier of V
- u2 is Element of the carrier of V
K146(V,u3,(- u2)) is Element of the carrier of V
((A1 * w) + (A2 * y)) - ((B1 * w) + (B2 * y)) is Element of the carrier of V
- ((B1 * w) + (B2 * y)) is Element of the carrier of V
K146(V,((A1 * w) + (A2 * y)),(- ((B1 * w) + (B2 * y)))) is Element of the carrier of V
A1 - B1 is V11() V12() Element of K28()
(A1 - B1) * w is Element of the carrier of V
A2 - B2 is V11() V12() Element of K28()
(A2 - B2) * y is Element of the carrier of V
((A1 - B1) * w) + ((A2 - B2) * y) is Element of the carrier of V
pr1 (w,y,(u3 - u2)) is V11() V12() Element of K28()
pr2 (w,y,(u3 - u2)) is V11() V12() Element of K28()
((((r * A2) * w) + ((- (r * A1)) * y)) + q) - ((((r * B2) * w) + ((- (r * B1)) * y)) + q) is Element of the carrier of V
- ((((r * B2) * w) + ((- (r * B1)) * y)) + q) is Element of the carrier of V
K146(V,((((r * A2) * w) + ((- (r * A1)) * y)) + q),(- ((((r * B2) * w) + ((- (r * B1)) * y)) + q))) is Element of the carrier of V
- A1 is V11() V12() Element of K28()
r * (- A1) is V11() V12() Element of K28()
(r * (- A1)) * y is Element of the carrier of V
((r * A2) * w) + ((r * (- A1)) * y) is Element of the carrier of V
(((r * A2) * w) + ((r * (- A1)) * y)) - (((r * B2) * w) + ((- (r * B1)) * y)) is Element of the carrier of V
- (((r * B2) * w) + ((- (r * B1)) * y)) is Element of the carrier of V
K146(V,(((r * A2) * w) + ((r * (- A1)) * y)),(- (((r * B2) * w) + ((- (r * B1)) * y)))) is Element of the carrier of V
(r * A2) - (r * B2) is V11() V12() Element of K28()
((r * A2) - (r * B2)) * w is Element of the carrier of V
- B1 is V11() V12() Element of K28()
r * (- B1) is V11() V12() Element of K28()
(r * (- A1)) - (r * (- B1)) is V11() V12() Element of K28()
((r * (- A1)) - (r * (- B1))) * y is Element of the carrier of V
(((r * A2) - (r * B2)) * w) + (((r * (- A1)) - (r * (- B1))) * y) is Element of the carrier of V
r * (A2 - B2) is V11() V12() Element of K28()
(r * (A2 - B2)) * w is Element of the carrier of V
B1 - A1 is V11() V12() Element of K28()
r * (B1 - A1) is V11() V12() Element of K28()
(r * (B1 - A1)) * y is Element of the carrier of V
((r * (A2 - B2)) * w) + ((r * (B1 - A1)) * y) is Element of the carrier of V
pr1 (w,y,(((((r * A2) * w) + ((- (r * A1)) * y)) + q) - ((((r * B2) * w) + ((- (r * B1)) * y)) + q))) is V11() V12() Element of K28()
pr2 (w,y,(((((r * A2) * w) + ((- (r * A1)) * y)) + q) - ((((r * B2) * w) + ((- (r * B1)) * y)) + q))) is V11() V12() Element of K28()
PProJ (w,y,(u3 - u2),(((((r * A2) * w) + ((- (r * A1)) * y)) + q) - ((((r * B2) * w) + ((- (r * B1)) * y)) + q))) is V11() V12() Element of K28()
(A1 - B1) * (r * (A2 - B2)) is V11() V12() Element of K28()
(A2 - B2) * (r * (B1 - A1)) is V11() V12() Element of K28()
((A1 - B1) * (r * (A2 - B2))) + ((A2 - B2) * (r * (B1 - A1))) is V11() V12() Element of K28()
(u3 - q) - (u1 - q) is Element of the carrier of V
K146(V,(u3 - q),(- (u1 - q))) is Element of the carrier of V
u3 - u1 is Element of the carrier of V
K146(V,u3,(- u1)) is Element of the carrier of V
(((((r * A2) * w) + ((- (r * A1)) * y)) + q) - q) - (v1 - q) is Element of the carrier of V
K146(V,(((((r * A2) * w) + ((- (r * A1)) * y)) + q) - q),(- (v1 - q))) is Element of the carrier of V
((((r * A2) * w) + ((- (r * A1)) * y)) + q) - v1 is Element of the carrier of V
K146(V,((((r * A2) * w) + ((- (r * A1)) * y)) + q),(- v1)) is Element of the carrier of V
c19 is Element of the carrier of MS
MS is V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of MS is V1() set
V is Element of the carrier of MS
w is Element of the carrier of MS
MS is V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of MS is V1() set
V is Element of the carrier of MS
w is Element of the carrier of MS
V is Element of the carrier of MS
w is Element of the carrier of MS
AMSpace (MS,V,w) is V42() strict ParOrtStr
y is V42() OrtAfSp-like OrtAfPl-like ParOrtStr
0. MS is V49(MS) Element of the carrier of MS
MS9 is V11() V12() Element of K28()
MS9 * V is Element of the carrier of MS
OAS is V11() V12() Element of K28()
OAS * w is Element of the carrier of MS
(MS9 * V) + (OAS * w) is Element of the carrier of MS
OASpace MS is strict AffinStruct
Af y is V42() V47() strict AffinSpace-like 2-dimensional AffinStruct
MS9 is V42() V47() OAffinSpace-like AffinStruct
Lambda MS9 is V42() V47() strict AffinSpace-like Fanoian AffinStruct
the V42() OrtAfSp-like OrtAfPl-like () () () () () () () ParOrtStr is V42() OrtAfSp-like OrtAfPl-like () () () () () () () ParOrtStr
MS is V42() OrtAfSp-like OrtAfPl-like ParOrtStr
V is V42() V68() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is V1() set
w is Element of the carrier of V
y is Element of the carrier of V
AMSpace (V,w,y) is V42() strict ParOrtStr
MS9 is V42() OrtAfSp-like OrtAfPl-like ParOrtStr
0. V is V49(V) Element of the carrier of V
OAS is V11() V12() Element of K28()
OAS * w is Element of the carrier of V
a1 is V11() V12() Element of K28()
a1 * y is Element of the carrier of V
(OAS * w) + (a1 * y) is Element of the carrier of V
OASpace V is strict AffinStruct
Af MS9 is V42() V47() strict AffinSpace-like 2-dimensional AffinStruct
OAS is V42() V47() OAffinSpace-like AffinStruct
Lambda OAS is V42() V47() strict AffinSpace-like Fanoian AffinStruct
MS is V42() OrtAfSp-like OrtAfPl-like () ParOrtStr
Af MS is V42() V47() strict AffinSpace-like 2-dimensional AffinStruct
MS is V42() OrtAfSp-like OrtAfPl-like () ParOrtStr
Af MS is V42() V47() strict AffinSpace-like 2-dimensional AffinStruct
MS is V42() OrtAfSp-like OrtAfPl-like () ParOrtStr
Af MS is V42() V47() strict AffinSpace-like 2-dimensional AffinStruct
MS is V42() OrtAfSp-like OrtAfPl-like () ParOrtStr
Af MS is V42() V47() strict AffinSpace-like 2-dimensional AffinStruct
MS is V42() OrtAfSp-like OrtAfPl-like () ParOrtStr
Af MS is V42() V47() strict AffinSpace-like 2-dimensional AffinStruct
MS is V42() OrtAfSp-like OrtAfPl-like () ParOrtStr
Af MS is V42() V47() strict AffinSpace-like 2-dimensional AffinStruct
MS is V42() OrtAfSp-like OrtAfPl-like () () ParOrtStr
Af MS is V42() V47() strict AffinSpace-like 2-dimensional Desarguesian AffinStruct
MS is V42() OrtAfSp-like () ParOrtStr
Af MS is V42() V47() strict AffinSpace-like AffinStruct
MS is V42() OrtAfSp-like () ParOrtStr
Af MS is V42() V47() strict AffinSpace-like AffinStruct
MS is V42() OrtAfSp-like () ParOrtStr
Af MS is V42() V47() strict AffinSpace-like AffinStruct
MS is V42() OrtAfSp-like () ParOrtStr
Af MS is V42() V47() strict AffinSpace-like AffinStruct
MS is V42() OrtAfSp-like () ParOrtStr
Af MS is V42() V47() strict AffinSpace-like AffinStruct