:: PAPDESAF semantic presentation

REAL is V16() V17() V18() V22() set

NAT is V16() V17() V18() V19() V20() V21() V22() M2(K11(REAL))

K11(REAL) is set

NAT is V16() V17() V18() V19() V20() V21() V22() set

K11(NAT) is set

K11(NAT) is set

0 is set

1 is V1() V2() V4() V13() V14() V15() V16() V17() V18() V19() V20() V21() M3( REAL , NAT )

0 is V1() V13() V14() V15() V16() V17() V18() V19() V20() V21() M3( REAL , NAT )

K44(0) is V14() set

OAS is V52() non trivial OAffinSpace-like AffinStruct

Lambda OAS is V52() strict AffinStruct

OAS is V52() non trivial OAffinSpace-like 2-dimensional AffinStruct

Lambda OAS is V52() non trivial strict AffinSpace-like AffinStruct

OAS is V52() non trivial OAffinSpace-like AffinStruct

the carrier of OAS is V4() V5() set

Lambda OAS is V52() non trivial strict AffinSpace-like AffinStruct

the carrier of (Lambda OAS) is V4() V5() set

K11( the carrier of OAS) is set

K11( the carrier of (Lambda OAS)) is set

the CONGR of OAS is M2(K11(K12(K12( the carrier of OAS, the carrier of OAS),K12( the carrier of OAS, the carrier of OAS))))

K12( the carrier of OAS, the carrier of OAS) is set

K12(K12( the carrier of OAS, the carrier of OAS),K12( the carrier of OAS, the carrier of OAS)) is set

K11(K12(K12( the carrier of OAS, the carrier of OAS),K12( the carrier of OAS, the carrier of OAS))) is set

lambda the CONGR of OAS is M2(K11(K12(K12( the carrier of OAS, the carrier of OAS),K12( the carrier of OAS, the carrier of OAS))))

AffinStruct(# the carrier of OAS,(lambda the CONGR of OAS) #) is strict AffinStruct

X is set

c

b is set

c is set

OAS is V52() non trivial OAffinSpace-like AffinStruct

the carrier of OAS is V4() V5() set

Lambda OAS is V52() non trivial strict AffinSpace-like AffinStruct

the carrier of (Lambda OAS) is V4() V5() set

X is M2( the carrier of OAS)

c

b is M2( the carrier of OAS)

c is M2( the carrier of (Lambda OAS))

d is M2( the carrier of (Lambda OAS))

a1 is M2( the carrier of (Lambda OAS))

OAS is V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

OASpace OAS is strict AffinStruct

the carrier of (OASpace OAS) is set

the carrier of OAS is V4() set

X is set

DirPar OAS is M2(K11(K12(K12( the carrier of OAS, the carrier of OAS),K12( the carrier of OAS, the carrier of OAS))))

K12( the carrier of OAS, the carrier of OAS) is set

K12(K12( the carrier of OAS, the carrier of OAS),K12( the carrier of OAS, the carrier of OAS)) is set

K11(K12(K12( the carrier of OAS, the carrier of OAS),K12( the carrier of OAS, the carrier of OAS))) is set

AffinStruct(# the carrier of OAS,(DirPar OAS) #) is strict AffinStruct

OAS is V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

OASpace OAS is strict AffinStruct

the carrier of OAS is V4() set

X is V52() non trivial OAffinSpace-like AffinStruct

the carrier of X is V4() V5() set

c

b is M2( the carrier of X)

c is M2( the carrier of X)

d is M2( the carrier of X)

a1 is M2( the carrier of OAS)

b1 is M2( the carrier of OAS)

c1 is M2( the carrier of OAS)

d1 is M2( the carrier of OAS)

OAS is V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

OASpace OAS is strict AffinStruct

the carrier of OAS is V4() set

0. OAS is V59(OAS) M2( the carrier of OAS)

X is V52() non trivial OAffinSpace-like AffinStruct

the carrier of X is V4() V5() set

c

b is M2( the carrier of X)

c is M2( the carrier of X)

d is M2( the carrier of X)

b1 is M2( the carrier of OAS)

a1 is M2( the carrier of OAS)

b1 - a1 is M2( the carrier of OAS)

- a1 is M2( the carrier of OAS)

K151(OAS,b1,(- a1)) is M2( the carrier of OAS)

P is M2( the carrier of OAS)

d1 is M2( the carrier of OAS)

c1 is M2( the carrier of OAS)

d1 - c1 is M2( the carrier of OAS)

- c1 is M2( the carrier of OAS)

K151(OAS,d1,(- c1)) is M2( the carrier of OAS)

Q is M2( the carrier of OAS)

x1 is V1() V14() V15() M2( REAL )

x1 * P is M2( the carrier of OAS)

x is V1() V14() V15() M2( REAL )

x * Q is M2( the carrier of OAS)

(x1 * P) + (x * Q) is M2( the carrier of OAS)

- (x * Q) is M2( the carrier of OAS)

- Q is M2( the carrier of OAS)

x * (- Q) is M2( the carrier of OAS)

- x is V1() V14() V15() M2( REAL )

(- x) * Q is M2( the carrier of OAS)

x1 is V1() V14() V15() M2( REAL )

x1 * P is M2( the carrier of OAS)

x is V1() V14() V15() M2( REAL )

x * Q is M2( the carrier of OAS)

(x1 * P) + (x * Q) is M2( the carrier of OAS)

OAS is V52() non trivial AffinSpace-like AffinStruct

the carrier of OAS is V4() V5() set

X is M2( the carrier of OAS)

c

b is M2( the carrier of OAS)

c is M2( the carrier of OAS)

X is M2( the carrier of OAS)

c

b is M2( the carrier of OAS)

c is M2( the carrier of OAS)

OAS is V52() non trivial OAffinSpace-like AffinStruct

the carrier of OAS is V4() V5() set

X is M2( the carrier of OAS)

c

d is M2( the carrier of OAS)

b is M2( the carrier of OAS)

a1 is M2( the carrier of OAS)

c is M2( the carrier of OAS)

b1 is M2( the carrier of OAS)

c1 is M2( the carrier of OAS)

d1 is M2( the carrier of OAS)

P is M2( the carrier of OAS)

OAS is V52() non trivial OAffinSpace-like AffinStruct

the carrier of OAS is V4() V5() set

X is M2( the carrier of OAS)

c

b is M2( the carrier of OAS)

c is M2( the carrier of OAS)

d is M2( the carrier of OAS)

OAS is V52() non trivial OAffinSpace-like AffinStruct

the carrier of OAS is V4() V5() set

X is M2( the carrier of OAS)

c

b is M2( the carrier of OAS)

c is M2( the carrier of OAS)

d is M2( the carrier of OAS)

a1 is M2( the carrier of OAS)

b1 is M2( the carrier of OAS)

OAS is V52() non trivial OAffinSpace-like AffinStruct

Lambda OAS is V52() non trivial strict AffinSpace-like AffinStruct

the carrier of (Lambda OAS) is V4() V5() set

K11( the carrier of (Lambda OAS)) is set

c

b is M2(K11( the carrier of (Lambda OAS)))

c is M2(K11( the carrier of (Lambda OAS)))

d is M2( the carrier of (Lambda OAS))

a1 is M2( the carrier of (Lambda OAS))

b1 is M2( the carrier of (Lambda OAS))

c1 is M2( the carrier of (Lambda OAS))

d1 is M2( the carrier of (Lambda OAS))

P is M2( the carrier of (Lambda OAS))

Q is M2( the carrier of (Lambda OAS))

the carrier of OAS is V4() V5() set

x1 is M2( the carrier of OAS)

c1 is M2( the carrier of OAS)

c19 is M2( the carrier of OAS)

x is M2( the carrier of OAS)

a19 is M2( the carrier of OAS)

v is M2(K11( the carrier of (Lambda OAS)))

v is M2(K11( the carrier of (Lambda OAS)))

u is M2( the carrier of OAS)

b19 is M2( the carrier of OAS)

OAS is V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of OAS is V4() set

X is M2( the carrier of OAS)

c

X - c

- c

K151(OAS,X,(- c

c is M2( the carrier of OAS)

c - X is M2( the carrier of OAS)

- X is M2( the carrier of OAS)

K151(OAS,c,(- X)) is M2( the carrier of OAS)

b is M2( the carrier of OAS)

d is M2( the carrier of OAS)

b - c

K151(OAS,b,(- c

b - X is M2( the carrier of OAS)

K151(OAS,b,(- X)) is M2( the carrier of OAS)

d - c is M2( the carrier of OAS)

- c is M2( the carrier of OAS)

K151(OAS,d,(- c)) is M2( the carrier of OAS)

a1 is V1() V14() V15() M2( REAL )

a1 * (c - X) is M2( the carrier of OAS)

- a1 is V1() V14() V15() M2( REAL )

(- a1) " is V1() V14() V15() M2( REAL )

((- a1) ") * (b - c

c + (((- a1) ") * (b - c

((- a1) ") * (b - X) is M2( the carrier of OAS)

X + (((- a1) ") * (b - X)) is M2( the carrier of OAS)

(- a1) * (d - c) is M2( the carrier of OAS)

c

K151(OAS,c

0. OAS is V59(OAS) M2( the carrier of OAS)

b1 is V1() V14() V15() M2( REAL )

b1 * (c

c1 is V1() V14() V15() M2( REAL )

c1 * (b - X) is M2( the carrier of OAS)

(b1 * (c

- (c1 * (b - X)) is M2( the carrier of OAS)

- (b - X) is M2( the carrier of OAS)

c1 * (- (b - X)) is M2( the carrier of OAS)

- c1 is V1() V14() V15() M2( REAL )

(- c1) * (b - X) is M2( the carrier of OAS)

OASpace OAS is strict AffinStruct

b1 is V52() non trivial OAffinSpace-like AffinStruct

the carrier of b1 is V4() V5() set

P is M2( the carrier of b1)

x1 is M2( the carrier of b1)

Q is M2( the carrier of b1)

x is M2( the carrier of b1)

d1 is M2( the carrier of b1)

(c + (((- a1) ") * (b - c

K151(OAS,(c + (((- a1) ") * (b - c

(- a1) * ((c + (((- a1) ") * (b - c

(- a1) * (((- a1) ") * (b - c

(- a1) * ((- a1) ") is V1() V14() V15() M2( REAL )

((- a1) * ((- a1) ")) * (b - c

1 * (b - c

c1 is M2( the carrier of b1)

X - (c + (((- a1) ") * (b - c

- (c + (((- a1) ") * (b - c

K151(OAS,X,(- (c + (((- a1) ") * (b - c

(- a1) * (X - (c + (((- a1) ") * (b - c

(- a1) * X is M2( the carrier of OAS)

(- a1) * (c + (((- a1) ") * (b - c

((- a1) * X) - ((- a1) * (c + (((- a1) ") * (b - c

- ((- a1) * (c + (((- a1) ") * (b - c

K151(OAS,((- a1) * X),(- ((- a1) * (c + (((- a1) ") * (b - c

(- a1) * c is M2( the carrier of OAS)

((- a1) * c) + ((- a1) * (((- a1) ") * (b - c

((- a1) * X) - (((- a1) * c) + ((- a1) * (((- a1) ") * (b - c

- (((- a1) * c) + ((- a1) * (((- a1) ") * (b - c

K151(OAS,((- a1) * X),(- (((- a1) * c) + ((- a1) * (((- a1) ") * (b - c

((- a1) * c) + (((- a1) * ((- a1) ")) * (b - c

((- a1) * X) - (((- a1) * c) + (((- a1) * ((- a1) ")) * (b - c

- (((- a1) * c) + (((- a1) * ((- a1) ")) * (b - c

K151(OAS,((- a1) * X),(- (((- a1) * c) + (((- a1) * ((- a1) ")) * (b - c

((- a1) * c) + (1 * (b - c

((- a1) * X) - (((- a1) * c) + (1 * (b - c

- (((- a1) * c) + (1 * (b - c

K151(OAS,((- a1) * X),(- (((- a1) * c) + (1 * (b - c

((- a1) * c) + (b - c

((- a1) * X) - (((- a1) * c) + (b - c

- (((- a1) * c) + (b - c

K151(OAS,((- a1) * X),(- (((- a1) * c) + (b - c

((- a1) * X) - ((- a1) * c) is M2( the carrier of OAS)

- ((- a1) * c) is M2( the carrier of OAS)

K151(OAS,((- a1) * X),(- ((- a1) * c))) is M2( the carrier of OAS)

(((- a1) * X) - ((- a1) * c)) - (b - c

- (b - c

K151(OAS,(((- a1) * X) - ((- a1) * c)),(- (b - c

X - c is M2( the carrier of OAS)

K151(OAS,X,(- c)) is M2( the carrier of OAS)

(- a1) * (X - c) is M2( the carrier of OAS)

((- a1) * (X - c)) - (b - c

K151(OAS,((- a1) * (X - c)),(- (b - c

- (X - c) is M2( the carrier of OAS)

a1 * (- (X - c)) is M2( the carrier of OAS)

(a1 * (- (X - c))) - (b - c

K151(OAS,(a1 * (- (X - c))),(- (b - c

(X - c

K151(OAS,(X - c

(b - c

X - ((b - c

- ((b - c

K151(OAS,X,(- ((b - c

X - b is M2( the carrier of OAS)

- b is M2( the carrier of OAS)

K151(OAS,X,(- b)) is M2( the carrier of OAS)

1 * (X - b) is M2( the carrier of OAS)

1 * (c

- (c

- 1 is V1() V14() V15() M2( REAL )

(- 1) * (- (c

(- 1) * (a1 * (c - X)) is M2( the carrier of OAS)

(- 1) * a1 is V1() V14() V15() M2( REAL )

((- 1) * a1) * (c - X) is M2( the carrier of OAS)

(- a1) * (c - X) is M2( the carrier of OAS)

(c + (((- a1) ") * (b - c

K151(OAS,(c + (((- a1) ") * (b - c

(- a1) * ((c + (((- a1) ") * (b - c

- ((c + (((- a1) ") * (b - c

a1 * (- ((c + (((- a1) ") * (b - c

a1 * (X - (c + (((- a1) ") * (b - c

- (a1 * (X - (c + (((- a1) ") * (b - c

- (- (a1 * (X - (c + (((- a1) ") * (b - c

- (X - (c + (((- a1) ") * (b - c

a1 * (- (X - (c + (((- a1) ") * (b - c

- (a1 * (- (X - (c + (((- a1) ") * (b - c

- (1 * (X - b)) is M2( the carrier of OAS)

- (X - b) is M2( the carrier of OAS)

X + ((c + (((- a1) ") * (b - c

OAS is V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of OAS is V4() set

X is M2( the carrier of OAS)

c

b is M2( the carrier of OAS)

c

- X is M2( the carrier of OAS)

K151(OAS,c

b - c

- c

K151(OAS,b,(- c

c is V1() V14() V15() M2( REAL )

c * (c

d is V1() V14() V15() M2( REAL )

d * (b - c

c " is V1() V14() V15() M2( REAL )

(c ") * d is V1() V14() V15() M2( REAL )

a1 is V1() V14() V15() M2( REAL )

a1 * (b - c

0 * d is V1() V14() V15() M2( REAL )

1 * (c

(c ") * c is V1() V14() V15() M2( REAL )

((c ") * c) * (c

(c ") * (d * (b - c

OAS is V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

OASpace OAS is strict AffinStruct

X is V52() non trivial OAffinSpace-like AffinStruct

the carrier of X is V4() V5() set

b is M2( the carrier of X)

c

a1 is M2( the carrier of X)

c is M2( the carrier of X)

b1 is M2( the carrier of X)

d is M2( the carrier of X)

c1 is M2( the carrier of X)

the carrier of OAS is V4() set

d1 is M2( the carrier of OAS)

P is M2( the carrier of OAS)

Q is M2( the carrier of OAS)

x1 is M2( the carrier of OAS)

a19 is M2( the carrier of OAS)

c1 is M2( the carrier of OAS)

x is M2( the carrier of OAS)

d1 - P is M2( the carrier of OAS)

- P is M2( the carrier of OAS)

K151(OAS,d1,(- P)) is M2( the carrier of OAS)

x - d1 is M2( the carrier of OAS)

- d1 is M2( the carrier of OAS)

K151(OAS,x,(- d1)) is M2( the carrier of OAS)

b19 is V1() V14() V15() M2( REAL )

b19 * (x - d1) is M2( the carrier of OAS)

x1 - P is M2( the carrier of OAS)

K151(OAS,x1,(- P)) is M2( the carrier of OAS)

- b19 is V1() V14() V15() M2( REAL )

(- b19) " is V1() V14() V15() M2( REAL )

((- b19) ") * (x1 - P) is M2( the carrier of OAS)

x + (((- b19) ") * (x1 - P)) is M2( the carrier of OAS)

Q - P is M2( the carrier of OAS)

K151(OAS,Q,(- P)) is M2( the carrier of OAS)

((- b19) ") * (Q - P) is M2( the carrier of OAS)

x + (((- b19) ") * (Q - P)) is M2( the carrier of OAS)

a19 - c1 is M2( the carrier of OAS)

- c1 is M2( the carrier of OAS)

K151(OAS,a19,(- c1)) is M2( the carrier of OAS)

1 * (a19 - c1) is M2( the carrier of OAS)

(x + (((- b19) ") * (x1 - P))) - (x + (((- b19) ") * (Q - P))) is M2( the carrier of OAS)

- (x + (((- b19) ") * (Q - P))) is M2( the carrier of OAS)

K151(OAS,(x + (((- b19) ") * (x1 - P))),(- (x + (((- b19) ") * (Q - P))))) is M2( the carrier of OAS)

(((- b19) ") * (x1 - P)) + x is M2( the carrier of OAS)

((((- b19) ") * (x1 - P)) + x) - x is M2( the carrier of OAS)

- x is M2( the carrier of OAS)

K151(OAS,((((- b19) ") * (x1 - P)) + x),(- x)) is M2( the carrier of OAS)

(((((- b19) ") * (x1 - P)) + x) - x) - (((- b19) ") * (Q - P)) is M2( the carrier of OAS)

- (((- b19) ") * (Q - P)) is M2( the carrier of OAS)

K151(OAS,(((((- b19) ") * (x1 - P)) + x) - x),(- (((- b19) ") * (Q - P)))) is M2( the carrier of OAS)

(((- b19) ") * (x1 - P)) - (((- b19) ") * (Q - P)) is M2( the carrier of OAS)

K151(OAS,(((- b19) ") * (x1 - P)),(- (((- b19) ") * (Q - P)))) is M2( the carrier of OAS)

(x1 - P) - (Q - P) is M2( the carrier of OAS)

- (Q - P) is M2( the carrier of OAS)

K151(OAS,(x1 - P),(- (Q - P))) is M2( the carrier of OAS)

((- b19) ") * ((x1 - P) - (Q - P)) is M2( the carrier of OAS)

(Q - P) + P is M2( the carrier of OAS)

x1 - ((Q - P) + P) is M2( the carrier of OAS)

- ((Q - P) + P) is M2( the carrier of OAS)

K151(OAS,x1,(- ((Q - P) + P))) is M2( the carrier of OAS)

((- b19) ") * (x1 - ((Q - P) + P)) is M2( the carrier of OAS)

x1 - Q is M2( the carrier of OAS)

- Q is M2( the carrier of OAS)

K151(OAS,x1,(- Q)) is M2( the carrier of OAS)

((- b19) ") * (x1 - Q) is M2( the carrier of OAS)

b19 " is V1() V14() V15() M2( REAL )

- (b19 ") is V1() V14() V15() M2( REAL )

(- (b19 ")) * (x1 - Q) is M2( the carrier of OAS)

- (x1 - Q) is M2( the carrier of OAS)

(b19 ") * (- (x1 - Q)) is M2( the carrier of OAS)

Q - x1 is M2( the carrier of OAS)

- x1 is M2( the carrier of OAS)

K151(OAS,Q,(- x1)) is M2( the carrier of OAS)

(b19 ") * (Q - x1) is M2( the carrier of OAS)

X is V52() non trivial OAffinSpace-like AffinStruct

OAS is V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

OASpace OAS is strict AffinStruct

OAS is V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of OAS is V4() set

X is M2( the carrier of OAS)

c

b is M2( the carrier of OAS)

c

- X is M2( the carrier of OAS)

K151(OAS,c

b - X is M2( the carrier of OAS)

K151(OAS,b,(- X)) is M2( the carrier of OAS)

c is V1() V14() V15() M2( REAL )

c * (c

d is V1() V14() V15() M2( REAL )

d * (b - X) is M2( the carrier of OAS)

0. OAS is V59(OAS) M2( the carrier of OAS)

c " is V1() V14() V15() M2( REAL )

(c ") * d is V1() V14() V15() M2( REAL )

a1 is V1() V14() V15() M2( REAL )

a1 * (b - X) is M2( the carrier of OAS)

(c ") * (c * (c

(c ") * c is V1() V14() V15() M2( REAL )

((c ") * c) * (c

1 * (c

OAS is V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of OAS is V4() set

X is M2( the carrier of OAS)

b is M2( the carrier of OAS)

X - b is M2( the carrier of OAS)

- b is M2( the carrier of OAS)

K151(OAS,X,(- b)) is M2( the carrier of OAS)

c

c

K151(OAS,c

(X - b) - (c

- (c

K151(OAS,(X - b),(- (c

X - c

- c

K151(OAS,X,(- c

(c

X - ((c

- ((c

K151(OAS,X,(- ((c

OAS is V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

OASpace OAS is strict AffinStruct

X is V52() non trivial OAffinSpace-like AffinStruct

Lambda X is V52() non trivial strict AffinSpace-like AffinStruct

the carrier of (Lambda X) is V4() V5() set

K11( the carrier of (Lambda X)) is set

b is M2(K11( the carrier of (Lambda X)))

c is M2(K11( the carrier of (Lambda X)))

d is M2( the carrier of (Lambda X))

a1 is M2( the carrier of (Lambda X))

d1 is M2( the carrier of (Lambda X))

b1 is M2( the carrier of (Lambda X))

P is M2( the carrier of (Lambda X))

c1 is M2( the carrier of (Lambda X))

Q is M2( the carrier of (Lambda X))

the carrier of X is V4() V5() set

the carrier of OAS is V4() set

x1 is M2( the carrier of X)

x is M2( the carrier of X)

c1 is M2( the carrier of X)

a19 is M2( the carrier of X)

b19 is M2( the carrier of X)

c19 is M2( the carrier of X)

u is M2( the carrier of X)

u9 is M2( the carrier of OAS)

c199 is M2( the carrier of OAS)

v99 is M2( the carrier of OAS)

b199 is M2( the carrier of OAS)

v is M2( the carrier of OAS)

w99 is M2( the carrier of OAS)

v99 - v is M2( the carrier of OAS)

- v is M2( the carrier of OAS)

K151(OAS,v99,(- v)) is M2( the carrier of OAS)

u9 - v is M2( the carrier of OAS)

K151(OAS,u9,(- v)) is M2( the carrier of OAS)

r2 is V1() V14() V15() M2( REAL )

r2 * (u9 - v) is M2( the carrier of OAS)

- r2 is V1() V14() V15() M2( REAL )

w is M2( the carrier of OAS)

w - v is M2( the carrier of OAS)

K151(OAS,w,(- v)) is M2( the carrier of OAS)

r1 is V1() V14() V15() M2( REAL )

r1 * (u9 - v) is M2( the carrier of OAS)

v - u9 is M2( the carrier of OAS)

- u9 is M2( the carrier of OAS)

K151(OAS,v,(- u9)) is M2( the carrier of OAS)

- r1 is V1() V14() V15() M2( REAL )

(- r1) * (v - u9) is M2( the carrier of OAS)

- (v - u9) is M2( the carrier of OAS)

r1 * (- (v - u9)) is M2( the carrier of OAS)

(- r2) * (v - u9) is M2( the carrier of OAS)

r2 * (- (v - u9)) is M2( the carrier of OAS)

(- r2) " is V1() V14() V15() M2( REAL )

((- r2) ") * (v99 - v) is M2( the carrier of OAS)

c199 - v is M2( the carrier of OAS)

K151(OAS,c199,(- v)) is M2( the carrier of OAS)

- ((- r2) ") is V1() V14() V15() M2( REAL )

(- ((- r2) ")) " is V1() V14() V15() M2( REAL )

((- ((- r2) ")) ") * (c199 - v) is M2( the carrier of OAS)

v + (((- ((- r2) ")) ") * (c199 - v)) is M2( the carrier of OAS)

r2 " is V1() V14() V15() M2( REAL )

- (r2 ") is V1() V14() V15() M2( REAL )

- (- (r2 ")) is V1() V14() V15() M2( REAL )

(- (- (r2 "))) " is V1() V14() V15() M2( REAL )

((- (- (r2 "))) ") * (c199 - v) is M2( the carrier of OAS)

v + (((- (- (r2 "))) ") * (c199 - v)) is M2( the carrier of OAS)

r2 * (c199 - v) is M2( the carrier of OAS)

v + (r2 * (c199 - v)) is M2( the carrier of OAS)

b199 - v is M2( the carrier of OAS)

K151(OAS,b199,(- v)) is M2( the carrier of OAS)

r1 " is V1() V14() V15() M2( REAL )

(r1 ") * r2 is V1() V14() V15() M2( REAL )

r1 * (r2 ") is V1() V14() V15() M2( REAL )

(r2 ") * (v99 - v) is M2( the carrier of OAS)

r1 * ((r2 ") * (v99 - v)) is M2( the carrier of OAS)

(r1 * (r2 ")) * (v99 - v) is M2( the carrier of OAS)

(- r1) " is V1() V14() V15() M2( REAL )

((- r1) ") * (w - v) is M2( the carrier of OAS)

w99 - v is M2( the carrier of OAS)

K151(OAS,w99,(- v)) is M2( the carrier of OAS)

- ((- r1) ") is V1() V14() V15() M2( REAL )

(- ((- r1) ")) " is V1() V14() V15() M2( REAL )

((- ((- r1) ")) ") * (w99 - v) is M2( the carrier of OAS)

v + (((- ((- r1) ")) ") * (w99 - v)) is M2( the carrier of OAS)

- (r1 ") is V1() V14() V15() M2( REAL )

- (- (r1 ")) is V1() V14() V15() M2( REAL )

(- (- (r1 "))) " is V1() V14() V15() M2( REAL )

((- (- (r1 "))) ") * (w99 - v) is M2( the carrier of OAS)

v + (((- (- (r1 "))) ") * (w99 - v)) is M2( the carrier of OAS)

r1 * (w99 - v) is M2( the carrier of OAS)

v + (r1 * (w99 - v)) is M2( the carrier of OAS)

(r1 ") * (r2 * (c199 - v)) is M2( the carrier of OAS)

((r1 ") * r2) * (c199 - v) is M2( the carrier of OAS)

((r1 ") * r2) " is V1() V14() V15() M2( REAL )

(((r1 ") * r2) ") * (w99 - v) is M2( the carrier of OAS)

(r1 ") " is V1() V14() V15() M2( REAL )

((r1 ") ") * (r2 ") is V1() V14() V15() M2( REAL )

(((r1 ") ") * (r2 ")) * (w99 - v) is M2( the carrier of OAS)

(r1 * (r2 ")) * (w99 - v) is M2( the carrier of OAS)

c199 - w is M2( the carrier of OAS)

- w is M2( the carrier of OAS)

K151(OAS,c199,(- w)) is M2( the carrier of OAS)

1 * (c199 - w) is M2( the carrier of OAS)

((r1 * (r2 ")) * (w99 - v)) - ((r1 * (r2 ")) * (v99 - v)) is M2( the carrier of OAS)

- ((r1 * (r2 ")) * (v99 - v)) is M2( the carrier of OAS)

K151(OAS,((r1 * (r2 ")) * (w99 - v)),(- ((r1 * (r2 ")) * (v99 - v)))) is M2( the carrier of OAS)

(w99 - v) - (v99 - v) is M2( the carrier of OAS)

- (v99 - v) is M2( the carrier of OAS)

K151(OAS,(w99 - v),(- (v99 - v))) is M2( the carrier of OAS)

(r1 * (r2 ")) * ((w99 - v) - (v99 - v)) is M2( the carrier of OAS)

w99 - v99 is M2( the carrier of OAS)

- v99 is M2( the carrier of OAS)

K151(OAS,w99,(- v99)) is M2( the carrier of OAS)

(r1 * (r2 ")) * (w99 - v99) is M2( the carrier of OAS)

X is V52() non trivial OAffinSpace-like AffinStruct

OAS is V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

OASpace OAS is strict AffinStruct

Lambda X is V52() non trivial strict AffinSpace-like AffinStruct

OAS is V52() non trivial AffinSpace-like AffinStruct

the carrier of OAS is V4() V5() set

K11( the carrier of OAS) is set

X is M2(K11( the carrier of OAS))

c

d is M2( the carrier of OAS)

c1 is M2( the carrier of OAS)

b is M2( the carrier of OAS)

c is M2( the carrier of OAS)

a1 is M2( the carrier of OAS)

b1 is M2( the carrier of OAS)

Line (c

Line (c

OAS is V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

OASpace OAS is strict AffinStruct

X is V52() non trivial OAffinSpace-like AffinStruct

Lambda X is V52() non trivial strict AffinSpace-like AffinStruct

OAS is V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

OASpace OAS is strict AffinStruct

X is V52() non trivial OAffinSpace-like AffinStruct

Lambda X is V52() non trivial strict AffinSpace-like AffinStruct

the carrier of (Lambda X) is V4() V5() set

K11( the carrier of (Lambda X)) is set

b is M2(K11( the carrier of (Lambda X)))

c is M2(K11( the carrier of (Lambda X)))

d is M2(K11( the carrier of (Lambda X)))

a1 is M2( the carrier of (Lambda X))

d1 is M2( the carrier of (Lambda X))

b1 is M2( the carrier of (Lambda X))

P is M2( the carrier of (Lambda X))

c1 is M2( the carrier of (Lambda X))

Q is M2( the carrier of (Lambda X))

the carrier of X is V4() V5() set

the carrier of OAS is V4() set

x1 is M2( the carrier of X)

x is M2( the carrier of X)

c1 is M2( the carrier of X)

a19 is M2( the carrier of X)

c19 is M2( the carrier of X)

b19 is M2( the carrier of X)

u9 is M2( the carrier of OAS)

v is M2( the carrier of OAS)

u9 + v is M2( the carrier of OAS)

u is M2( the carrier of OAS)

(u9 + v) - u is M2( the carrier of OAS)

- u is M2( the carrier of OAS)

K151(OAS,(u9 + v),(- u)) is M2( the carrier of OAS)

w is M2( the carrier of OAS)

u9 + w is M2( the carrier of OAS)

(u9 + w) - u is M2( the carrier of OAS)

K151(OAS,(u9 + w),(- u)) is M2( the carrier of OAS)

((u9 + w) - u) - ((u9 + v) - u) is M2( the carrier of OAS)

- ((u9 + v) - u) is M2( the carrier of OAS)

K151(OAS,((u9 + w) - u),(- ((u9 + v) - u))) is M2( the carrier of OAS)

((u9 + v) - u) + u is M2( the carrier of OAS)

(u9 + w) - (((u9 + v) - u) + u) is M2( the carrier of OAS)

- (((u9 + v) - u) + u) is M2( the carrier of OAS)

K151(OAS,(u9 + w),(- (((u9 + v) - u) + u))) is M2( the carrier of OAS)

(u9 + w) - (u9 + v) is M2( the carrier of OAS)

- (u9 + v) is M2( the carrier of OAS)

K151(OAS,(u9 + w),(- (u9 + v))) is M2( the carrier of OAS)

w + u9 is M2( the carrier of OAS)

(w + u9) - u9 is M2( the carrier of OAS)

- u9 is M2( the carrier of OAS)

K151(OAS,(w + u9),(- u9)) is M2( the carrier of OAS)

((w + u9) - u9) - v is M2( the carrier of OAS)

- v is M2( the carrier of OAS)

K151(OAS,((w + u9) - u9),(- v)) is M2( the carrier of OAS)

w - v is M2( the carrier of OAS)

K151(OAS,w,(- v)) is M2( the carrier of OAS)

b199 is M2( the carrier of X)

c199 is M2( the carrier of X)

OAS is V52() non trivial OAffinSpace-like AffinStruct

Lambda OAS is V52() non trivial strict AffinSpace-like AffinStruct

the carrier of (Lambda OAS) is V4() V5() set

c

b is M2( the carrier of (Lambda OAS))

c is M2( the carrier of (Lambda OAS))

d is M2( the carrier of (Lambda OAS))

the carrier of OAS is V4() V5() set

Line (c

K11( the carrier of (Lambda OAS)) is set

Line (b,c) is M2(K11( the carrier of (Lambda OAS)))

a1 is M2( the carrier of OAS)

b1 is M2( the carrier of OAS)

c1 is M2( the carrier of OAS)

d1 is M2( the carrier of OAS)

x1 is M2( the carrier of OAS)

x is M2( the carrier of (Lambda OAS))

OAS is V52() V78() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of OAS is V4() set

X is M2( the carrier of OAS)

c

0. OAS is V59(OAS) M2( the carrier of OAS)

OAS is V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of OAS is V4() set

0. OAS is V59(OAS) M2( the carrier of OAS)

OASpace OAS is strict AffinStruct

c

b is M2( the carrier of OAS)

X is V52() non trivial OAffinSpace-like AffinStruct

Lambda X is V52() non trivial strict AffinSpace-like AffinStruct

OAS is V52() V78() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of OAS is V4() set

X is M2( the carrier of OAS)

c

0. OAS is V59(OAS) M2( the carrier of OAS)

OAS is V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of OAS is V4() set

0. OAS is V59(OAS) M2( the carrier of OAS)

OASpace OAS is strict AffinStruct

c

b is M2( the carrier of OAS)

X is V52() non trivial OAffinSpace-like 2-dimensional AffinStruct

Lambda X is V52() non trivial strict AffinSpace-like 2-dimensional AffinStruct

c

OAS is V52() V78() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of OAS is V4() set

X is M2( the carrier of OAS)

c

0. OAS is V59(OAS) M2( the carrier of OAS)

OAS is V52() V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of OAS is V4() set

0. OAS is V59(OAS) M2( the carrier of OAS)

OASpace OAS is strict AffinStruct

c

b is M2( the carrier of OAS)

X is V52() non trivial OAffinSpace-like AffinStruct

Lambda X is V52() non trivial strict AffinSpace-like AffinStruct

OAS is V52() non trivial OAffinSpace-like AffinStruct

Lambda OAS is V52() non trivial strict AffinSpace-like AffinStruct

OAS is V52() non trivial OAffinSpace-like () AffinStruct

Lambda OAS is V52() non trivial strict AffinSpace-like Fanoian AffinStruct

OAS is V52() non trivial OAffinSpace-like () AffinStruct

Lambda OAS is V52() non trivial strict AffinSpace-like Fanoian AffinStruct

OAS is V52() non trivial OAffinSpace-like () AffinStruct

Lambda OAS is V52() non trivial strict AffinSpace-like Fanoian AffinStruct

OAS is V52() non trivial OAffinSpace-like () AffinStruct

Lambda OAS is V52() non trivial strict AffinSpace-like Fanoian AffinStruct