:: EUCLMETR semantic presentation

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