:: GEOMTRAP semantic presentation

REAL is V36() V37() V38() V42() set

NAT is V36() V37() V38() V39() V40() V41() V42() Element of bool REAL

bool REAL is non empty set

NAT is V36() V37() V38() V39() V40() V41() V42() set

bool NAT is non empty set

bool NAT is non empty set

{} is set

1 is non empty V24() V25() V33() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

- 1 is V24() V34() V35() Element of REAL

0 is V24() V33() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

MOS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of MOS is non empty set

MOS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of MOS is non empty set

OASpace MOS is non empty strict AffinStruct

X is Element of the carrier of MOS

MOS is Element of the carrier of MOS

0. MOS is V59(MOS) Element of the carrier of MOS

the ZeroF of MOS is Element of the carrier of MOS

X is V24() V34() V35() Element of REAL

X * X is Element of the carrier of MOS

the Mult of MOS is V1() V4([:REAL, the carrier of MOS:]) V5( the carrier of MOS) V6() V18([:REAL, the carrier of MOS:], the carrier of MOS) Element of bool [:[:REAL, the carrier of MOS:], the carrier of MOS:]

[:REAL, the carrier of MOS:] is set

[:[:REAL, the carrier of MOS:], the carrier of MOS:] is set

bool [:[:REAL, the carrier of MOS:], the carrier of MOS:] is non empty set

the Mult of MOS . (X,X) is set

p is V24() V34() V35() Element of REAL

p * MOS is Element of the carrier of MOS

the Mult of MOS . (p,MOS) is set

(X * X) + (p * MOS) is Element of the carrier of MOS

MOS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of MOS is non empty set

OASpace MOS is non empty strict AffinStruct

the carrier of (OASpace MOS) is non empty set

X is Element of the carrier of MOS

MOS is Element of the carrier of MOS

X is Element of the carrier of MOS

p is Element of the carrier of MOS

DirPar MOS is V1() V4([: the carrier of MOS, the carrier of MOS:]) V5([: the carrier of MOS, the carrier of MOS:]) Element of bool [:[: the carrier of MOS, the carrier of MOS:],[: the carrier of MOS, the carrier of MOS:]:]

[: the carrier of MOS, the carrier of MOS:] is non empty set

[:[: the carrier of MOS, the carrier of MOS:],[: the carrier of MOS, the carrier of MOS:]:] is non empty set

bool [:[: the carrier of MOS, the carrier of MOS:],[: the carrier of MOS, the carrier of MOS:]:] is non empty set

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

q is Element of the carrier of (OASpace MOS)

a is Element of the carrier of (OASpace MOS)

a1 is Element of the carrier of (OASpace MOS)

b is Element of the carrier of (OASpace MOS)

[: the carrier of (OASpace MOS), the carrier of (OASpace MOS):] is non empty set

[q,a] is Element of [: the carrier of (OASpace MOS), the carrier of (OASpace MOS):]

[a1,b] is Element of [: the carrier of (OASpace MOS), the carrier of (OASpace MOS):]

[[q,a],[a1,b]] is Element of [:[: the carrier of (OASpace MOS), the carrier of (OASpace MOS):],[: the carrier of (OASpace MOS), the carrier of (OASpace MOS):]:]

[:[: the carrier of (OASpace MOS), the carrier of (OASpace MOS):],[: the carrier of (OASpace MOS), the carrier of (OASpace MOS):]:] is non empty set

the CONGR of (OASpace MOS) is V1() V4([: the carrier of (OASpace MOS), the carrier of (OASpace MOS):]) V5([: the carrier of (OASpace MOS), the carrier of (OASpace MOS):]) Element of bool [:[: the carrier of (OASpace MOS), the carrier of (OASpace MOS):],[: the carrier of (OASpace MOS), the carrier of (OASpace MOS):]:]

bool [:[: the carrier of (OASpace MOS), the carrier of (OASpace MOS):],[: the carrier of (OASpace MOS), the carrier of (OASpace MOS):]:] is non empty set

[X,MOS] is Element of [: the carrier of MOS, the carrier of MOS:]

[X,p] is Element of [: the carrier of MOS, the carrier of MOS:]

[[X,MOS],[X,p]] is Element of [:[: the carrier of MOS, the carrier of MOS:],[: the carrier of MOS, the carrier of MOS:]:]

MOS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of MOS is non empty set

OASpace MOS is non empty strict AffinStruct

Lambda (OASpace MOS) is non empty strict AffinStruct

the carrier of (Lambda (OASpace MOS)) is non empty set

X is Element of the carrier of MOS

MOS is Element of the carrier of MOS

X is Element of the carrier of MOS

p is Element of the carrier of MOS

q is Element of the carrier of MOS

a is Element of the carrier of MOS

b is Element of the carrier of (Lambda (OASpace MOS))

b1 is Element of the carrier of (Lambda (OASpace MOS))

c is Element of the carrier of (Lambda (OASpace MOS))

c1 is Element of the carrier of (Lambda (OASpace MOS))

the carrier of (OASpace MOS) is non empty set

the CONGR of (OASpace MOS) is V1() V4([: the carrier of (OASpace MOS), the carrier of (OASpace MOS):]) V5([: the carrier of (OASpace MOS), the carrier of (OASpace MOS):]) Element of bool [:[: the carrier of (OASpace MOS), the carrier of (OASpace MOS):],[: the carrier of (OASpace MOS), the carrier of (OASpace MOS):]:]

[: the carrier of (OASpace MOS), the carrier of (OASpace MOS):] is non empty set

[:[: the carrier of (OASpace MOS), the carrier of (OASpace MOS):],[: the carrier of (OASpace MOS), the carrier of (OASpace MOS):]:] is non empty set

bool [:[: the carrier of (OASpace MOS), the carrier of (OASpace MOS):],[: the carrier of (OASpace MOS), the carrier of (OASpace MOS):]:] is non empty set

lambda the CONGR of (OASpace MOS) is V1() V4([: the carrier of (OASpace MOS), the carrier of (OASpace MOS):]) V5([: the carrier of (OASpace MOS), the carrier of (OASpace MOS):]) Element of bool [:[: the carrier of (OASpace MOS), the carrier of (OASpace MOS):],[: the carrier of (OASpace MOS), the carrier of (OASpace MOS):]:]

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

a1 is non empty non trivial OAffinSpace-like AffinStruct

the carrier of a1 is non empty non trivial set

d is Element of the carrier of a1

d1 is Element of the carrier of a1

a9 is Element of the carrier of a1

b9 is Element of the carrier of a1

MOS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of MOS is non empty set

X is Element of the carrier of MOS

MOS is Element of the carrier of MOS

AMSpace (MOS,X,MOS) is non empty strict ParOrtStr

the carrier of (AMSpace (MOS,X,MOS)) is non empty set

X is Element of the carrier of MOS

p is Element of the carrier of MOS

q is Element of the carrier of MOS

a is Element of the carrier of MOS

a1 is Element of the carrier of (AMSpace (MOS,X,MOS))

b is Element of the carrier of (AMSpace (MOS,X,MOS))

b1 is Element of the carrier of (AMSpace (MOS,X,MOS))

c is Element of the carrier of (AMSpace (MOS,X,MOS))

p - X is Element of the carrier of MOS

- X is Element of the carrier of MOS

K163(MOS,p,(- X)) is Element of the carrier of MOS

a - q is Element of the carrier of MOS

- q is Element of the carrier of MOS

K163(MOS,a,(- q)) is Element of the carrier of MOS

c1 is V24() V34() V35() Element of REAL

c1 * (p - X) is Element of the carrier of MOS

the Mult of MOS is V1() V4([:REAL, the carrier of MOS:]) V5( the carrier of MOS) V6() V18([:REAL, the carrier of MOS:], the carrier of MOS) Element of bool [:[:REAL, the carrier of MOS:], the carrier of MOS:]

[:REAL, the carrier of MOS:] is set

[:[:REAL, the carrier of MOS:], the carrier of MOS:] is set

bool [:[:REAL, the carrier of MOS:], the carrier of MOS:] is non empty set

the Mult of MOS . (c1,(p - X)) is set

d is V24() V34() V35() Element of REAL

d * (a - q) is Element of the carrier of MOS

the Mult of MOS . (d,(a - q)) is set

c1 is V24() V34() V35() Element of REAL

c1 * (p - X) is Element of the carrier of MOS

the Mult of MOS is V1() V4([:REAL, the carrier of MOS:]) V5( the carrier of MOS) V6() V18([:REAL, the carrier of MOS:], the carrier of MOS) Element of bool [:[:REAL, the carrier of MOS:], the carrier of MOS:]

[:REAL, the carrier of MOS:] is set

[:[:REAL, the carrier of MOS:], the carrier of MOS:] is set

bool [:[:REAL, the carrier of MOS:], the carrier of MOS:] is non empty set

the Mult of MOS . (c1,(p - X)) is set

d is V24() V34() V35() Element of REAL

d * (a - q) is Element of the carrier of MOS

the Mult of MOS . (d,(a - q)) is set

MOS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of MOS is non empty set

X is Element of the carrier of MOS

MOS is Element of the carrier of MOS

X + MOS is Element of the carrier of MOS

2 is non empty V24() V25() V33() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

2 " is V24() V34() V35() Element of REAL

(2 ") * (X + MOS) is Element of the carrier of MOS

the Mult of MOS is V1() V4([:REAL, the carrier of MOS:]) V5( the carrier of MOS) V6() V18([:REAL, the carrier of MOS:], the carrier of MOS) Element of bool [:[:REAL, the carrier of MOS:], the carrier of MOS:]

[:REAL, the carrier of MOS:] is set

[:[:REAL, the carrier of MOS:], the carrier of MOS:] is set

bool [:[:REAL, the carrier of MOS:], the carrier of MOS:] is non empty set

the Mult of MOS . ((2 "),(X + MOS)) is set

(2 ") + (2 ") is V24() V34() V35() Element of REAL

((2 ") * (X + MOS)) + ((2 ") * (X + MOS)) is Element of the carrier of MOS

1 * (X + MOS) is Element of the carrier of MOS

the Mult of MOS . (1,(X + MOS)) is set

X is Element of the carrier of MOS

X + X is Element of the carrier of MOS

p is Element of the carrier of MOS

p + p is Element of the carrier of MOS

0. MOS is V59(MOS) Element of the carrier of MOS

the ZeroF of MOS is Element of the carrier of MOS

(X + X) - (p + p) is Element of the carrier of MOS

- (p + p) is Element of the carrier of MOS

K163(MOS,(X + X),(- (p + p))) is Element of the carrier of MOS

X - (p + p) is Element of the carrier of MOS

K163(MOS,X,(- (p + p))) is Element of the carrier of MOS

X + (X - (p + p)) is Element of the carrier of MOS

X - p is Element of the carrier of MOS

- p is Element of the carrier of MOS

K163(MOS,X,(- p)) is Element of the carrier of MOS

(X - p) - p is Element of the carrier of MOS

K163(MOS,(X - p),(- p)) is Element of the carrier of MOS

X + ((X - p) - p) is Element of the carrier of MOS

X + (X - p) is Element of the carrier of MOS

(X + (X - p)) - p is Element of the carrier of MOS

K163(MOS,(X + (X - p)),(- p)) is Element of the carrier of MOS

(X - p) + (X - p) is Element of the carrier of MOS

X is Element of the carrier of MOS

X + X is Element of the carrier of MOS

p is Element of the carrier of MOS

q is Element of the carrier of MOS

p + q is Element of the carrier of MOS

q + p is Element of the carrier of MOS

X is Element of the carrier of MOS

X + X is Element of the carrier of MOS

MOS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of MOS is non empty set

X is Element of the carrier of MOS

MOS is Element of the carrier of MOS

- X is Element of the carrier of MOS

MOS + MOS is Element of the carrier of MOS

(- X) + (MOS + MOS) is Element of the carrier of MOS

X is Element of the carrier of MOS

(MOS,X,X) is Element of the carrier of MOS

X + X is Element of the carrier of MOS

X + (- X) is Element of the carrier of MOS

(X + (- X)) + (MOS + MOS) is Element of the carrier of MOS

0. MOS is V59(MOS) Element of the carrier of MOS

the ZeroF of MOS is Element of the carrier of MOS

(0. MOS) + (MOS + MOS) is Element of the carrier of MOS

MOS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of MOS is non empty set

X is Element of the carrier of MOS

MOS is Element of the carrier of MOS

(MOS,X,MOS) is Element of the carrier of MOS

X is Element of the carrier of MOS

(MOS,X,X) is Element of the carrier of MOS

p is Element of the carrier of MOS

(MOS,X,p) is Element of the carrier of MOS

(MOS,(MOS,X,MOS),(MOS,X,p)) is Element of the carrier of MOS

(MOS,MOS,p) is Element of the carrier of MOS

(MOS,(MOS,X,X),(MOS,MOS,p)) is Element of the carrier of MOS

c1 is Element of the carrier of MOS

1 * c1 is Element of the carrier of MOS

the Mult of MOS is V1() V4([:REAL, the carrier of MOS:]) V5( the carrier of MOS) V6() V18([:REAL, the carrier of MOS:], the carrier of MOS) Element of bool [:[:REAL, the carrier of MOS:], the carrier of MOS:]

[:REAL, the carrier of MOS:] is set

[:[:REAL, the carrier of MOS:], the carrier of MOS:] is set

bool [:[:REAL, the carrier of MOS:], the carrier of MOS:] is non empty set

the Mult of MOS . (1,c1) is set

c1 + c1 is Element of the carrier of MOS

(c1 + c1) + (c1 + c1) is Element of the carrier of MOS

1 + 1 is V24() V34() V35() Element of REAL

(1 + 1) * c1 is Element of the carrier of MOS

the Mult of MOS . ((1 + 1),c1) is set

(1 * c1) + (1 * c1) is Element of the carrier of MOS

((1 + 1) * c1) + ((1 * c1) + (1 * c1)) is Element of the carrier of MOS

((1 + 1) * c1) + ((1 + 1) * c1) is Element of the carrier of MOS

(1 + 1) + (1 + 1) is V24() V34() V35() Element of REAL

((1 + 1) + (1 + 1)) * c1 is Element of the carrier of MOS

the Mult of MOS . (((1 + 1) + (1 + 1)),c1) is set

4 is non empty V24() V25() V33() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

4 * c1 is Element of the carrier of MOS

the Mult of MOS . (4,c1) is set

(MOS,(MOS,X,MOS),(MOS,X,p)) + (MOS,(MOS,X,MOS),(MOS,X,p)) is Element of the carrier of MOS

((MOS,(MOS,X,MOS),(MOS,X,p)) + (MOS,(MOS,X,MOS),(MOS,X,p))) + ((MOS,(MOS,X,MOS),(MOS,X,p)) + (MOS,(MOS,X,MOS),(MOS,X,p))) is Element of the carrier of MOS

(MOS,X,MOS) + (MOS,X,p) is Element of the carrier of MOS

((MOS,(MOS,X,MOS),(MOS,X,p)) + (MOS,(MOS,X,MOS),(MOS,X,p))) + ((MOS,X,MOS) + (MOS,X,p)) is Element of the carrier of MOS

((MOS,X,MOS) + (MOS,X,p)) + ((MOS,X,MOS) + (MOS,X,p)) is Element of the carrier of MOS

(MOS,X,p) + ((MOS,X,MOS) + (MOS,X,p)) is Element of the carrier of MOS

(MOS,X,MOS) + ((MOS,X,p) + ((MOS,X,MOS) + (MOS,X,p))) is Element of the carrier of MOS

(MOS,X,p) + (MOS,X,p) is Element of the carrier of MOS

(MOS,X,MOS) + ((MOS,X,p) + (MOS,X,p)) is Element of the carrier of MOS

(MOS,X,MOS) + ((MOS,X,MOS) + ((MOS,X,p) + (MOS,X,p))) is Element of the carrier of MOS

(MOS,X,MOS) + (MOS,X,MOS) is Element of the carrier of MOS

((MOS,X,MOS) + (MOS,X,MOS)) + ((MOS,X,p) + (MOS,X,p)) is Element of the carrier of MOS

X + p is Element of the carrier of MOS

((MOS,X,MOS) + (MOS,X,MOS)) + (X + p) is Element of the carrier of MOS

X + MOS is Element of the carrier of MOS

(X + MOS) + (X + p) is Element of the carrier of MOS

MOS + (X + p) is Element of the carrier of MOS

X + (MOS + (X + p)) is Element of the carrier of MOS

p + MOS is Element of the carrier of MOS

X + (p + MOS) is Element of the carrier of MOS

X + (X + (p + MOS)) is Element of the carrier of MOS

X + X is Element of the carrier of MOS

(X + X) + (p + MOS) is Element of the carrier of MOS

(MOS,MOS,p) + (MOS,MOS,p) is Element of the carrier of MOS

(X + X) + ((MOS,MOS,p) + (MOS,MOS,p)) is Element of the carrier of MOS

(MOS,X,X) + (MOS,X,X) is Element of the carrier of MOS

((MOS,X,X) + (MOS,X,X)) + ((MOS,MOS,p) + (MOS,MOS,p)) is Element of the carrier of MOS

(MOS,X,X) + ((MOS,MOS,p) + (MOS,MOS,p)) is Element of the carrier of MOS

(MOS,X,X) + ((MOS,X,X) + ((MOS,MOS,p) + (MOS,MOS,p))) is Element of the carrier of MOS

(MOS,MOS,p) + (MOS,X,X) is Element of the carrier of MOS

(MOS,MOS,p) + ((MOS,MOS,p) + (MOS,X,X)) is Element of the carrier of MOS

(MOS,X,X) + ((MOS,MOS,p) + ((MOS,MOS,p) + (MOS,X,X))) is Element of the carrier of MOS

(MOS,X,X) + (MOS,MOS,p) is Element of the carrier of MOS

((MOS,X,X) + (MOS,MOS,p)) + ((MOS,MOS,p) + (MOS,X,X)) is Element of the carrier of MOS

(MOS,(MOS,X,X),(MOS,MOS,p)) + (MOS,(MOS,X,X),(MOS,MOS,p)) is Element of the carrier of MOS

((MOS,(MOS,X,X),(MOS,MOS,p)) + (MOS,(MOS,X,X),(MOS,MOS,p))) + ((MOS,X,X) + (MOS,MOS,p)) is Element of the carrier of MOS

((MOS,(MOS,X,X),(MOS,MOS,p)) + (MOS,(MOS,X,X),(MOS,MOS,p))) + ((MOS,(MOS,X,X),(MOS,MOS,p)) + (MOS,(MOS,X,X),(MOS,MOS,p))) is Element of the carrier of MOS

4 * (MOS,(MOS,X,MOS),(MOS,X,p)) is Element of the carrier of MOS

the Mult of MOS . (4,(MOS,(MOS,X,MOS),(MOS,X,p))) is set

4 * (MOS,(MOS,X,X),(MOS,MOS,p)) is Element of the carrier of MOS

the Mult of MOS . (4,(MOS,(MOS,X,X),(MOS,MOS,p))) is set

MOS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of MOS is non empty set

X is Element of the carrier of MOS

MOS is Element of the carrier of MOS

(MOS,X,MOS) is Element of the carrier of MOS

X is Element of the carrier of MOS

(MOS,X,X) is Element of the carrier of MOS

X + MOS is Element of the carrier of MOS

(MOS,X,MOS) + (MOS,X,MOS) is Element of the carrier of MOS

X + X is Element of the carrier of MOS

MOS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of MOS is non empty set

X is Element of the carrier of MOS

MOS is Element of the carrier of MOS

X is Element of the carrier of MOS

(MOS,X,X) is Element of the carrier of MOS

(MOS,X,MOS) is Element of the carrier of MOS

X + X is Element of the carrier of MOS

(MOS,X,X) + (MOS,X,X) is Element of the carrier of MOS

X + MOS is Element of the carrier of MOS

(MOS,X,MOS) + (MOS,X,MOS) is Element of the carrier of MOS

(MOS,X,MOS) - (MOS,X,X) is Element of the carrier of MOS

- (MOS,X,X) is Element of the carrier of MOS

K163(MOS,(MOS,X,MOS),(- (MOS,X,X))) is Element of the carrier of MOS

2 is non empty V24() V25() V33() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

2 * ((MOS,X,MOS) - (MOS,X,X)) is Element of the carrier of MOS

the Mult of MOS is V1() V4([:REAL, the carrier of MOS:]) V5( the carrier of MOS) V6() V18([:REAL, the carrier of MOS:], the carrier of MOS) Element of bool [:[:REAL, the carrier of MOS:], the carrier of MOS:]

[:REAL, the carrier of MOS:] is set

[:[:REAL, the carrier of MOS:], the carrier of MOS:] is set

bool [:[:REAL, the carrier of MOS:], the carrier of MOS:] is non empty set

the Mult of MOS . (2,((MOS,X,MOS) - (MOS,X,X))) is set

1 + 1 is V24() V34() V35() Element of REAL

(1 + 1) * (MOS,X,MOS) is Element of the carrier of MOS

the Mult of MOS . ((1 + 1),(MOS,X,MOS)) is set

(1 + 1) * (MOS,X,X) is Element of the carrier of MOS

the Mult of MOS . ((1 + 1),(MOS,X,X)) is set

((1 + 1) * (MOS,X,MOS)) - ((1 + 1) * (MOS,X,X)) is Element of the carrier of MOS

- ((1 + 1) * (MOS,X,X)) is Element of the carrier of MOS

K163(MOS,((1 + 1) * (MOS,X,MOS)),(- ((1 + 1) * (MOS,X,X)))) is Element of the carrier of MOS

1 * (MOS,X,MOS) is Element of the carrier of MOS

the Mult of MOS . (1,(MOS,X,MOS)) is set

(1 * (MOS,X,MOS)) + (1 * (MOS,X,MOS)) is Element of the carrier of MOS

((1 * (MOS,X,MOS)) + (1 * (MOS,X,MOS))) - ((1 + 1) * (MOS,X,X)) is Element of the carrier of MOS

K163(MOS,((1 * (MOS,X,MOS)) + (1 * (MOS,X,MOS))),(- ((1 + 1) * (MOS,X,X)))) is Element of the carrier of MOS

1 * (MOS,X,X) is Element of the carrier of MOS

the Mult of MOS . (1,(MOS,X,X)) is set

(1 * (MOS,X,X)) + (1 * (MOS,X,X)) is Element of the carrier of MOS

((1 * (MOS,X,MOS)) + (1 * (MOS,X,MOS))) - ((1 * (MOS,X,X)) + (1 * (MOS,X,X))) is Element of the carrier of MOS

- ((1 * (MOS,X,X)) + (1 * (MOS,X,X))) is Element of the carrier of MOS

K163(MOS,((1 * (MOS,X,MOS)) + (1 * (MOS,X,MOS))),(- ((1 * (MOS,X,X)) + (1 * (MOS,X,X))))) is Element of the carrier of MOS

(MOS,X,MOS) + (1 * (MOS,X,MOS)) is Element of the carrier of MOS

((MOS,X,MOS) + (1 * (MOS,X,MOS))) - ((1 * (MOS,X,X)) + (1 * (MOS,X,X))) is Element of the carrier of MOS

K163(MOS,((MOS,X,MOS) + (1 * (MOS,X,MOS))),(- ((1 * (MOS,X,X)) + (1 * (MOS,X,X))))) is Element of the carrier of MOS

((MOS,X,MOS) + (MOS,X,MOS)) - ((1 * (MOS,X,X)) + (1 * (MOS,X,X))) is Element of the carrier of MOS

K163(MOS,((MOS,X,MOS) + (MOS,X,MOS)),(- ((1 * (MOS,X,X)) + (1 * (MOS,X,X))))) is Element of the carrier of MOS

(MOS,X,X) + (1 * (MOS,X,X)) is Element of the carrier of MOS

((MOS,X,MOS) + (MOS,X,MOS)) - ((MOS,X,X) + (1 * (MOS,X,X))) is Element of the carrier of MOS

- ((MOS,X,X) + (1 * (MOS,X,X))) is Element of the carrier of MOS

K163(MOS,((MOS,X,MOS) + (MOS,X,MOS)),(- ((MOS,X,X) + (1 * (MOS,X,X))))) is Element of the carrier of MOS

(X + MOS) - (X + X) is Element of the carrier of MOS

- (X + X) is Element of the carrier of MOS

K163(MOS,(X + MOS),(- (X + X))) is Element of the carrier of MOS

X - (X + X) is Element of the carrier of MOS

K163(MOS,X,(- (X + X))) is Element of the carrier of MOS

MOS + (X - (X + X)) is Element of the carrier of MOS

X - X is Element of the carrier of MOS

- X is Element of the carrier of MOS

K163(MOS,X,(- X)) is Element of the carrier of MOS

(X - X) - X is Element of the carrier of MOS

- X is Element of the carrier of MOS

K163(MOS,(X - X),(- X)) is Element of the carrier of MOS

MOS + ((X - X) - X) is Element of the carrier of MOS

0. MOS is V59(MOS) Element of the carrier of MOS

the ZeroF of MOS is Element of the carrier of MOS

(0. MOS) - X is Element of the carrier of MOS

K163(MOS,(0. MOS),(- X)) is Element of the carrier of MOS

MOS + ((0. MOS) - X) is Element of the carrier of MOS

MOS - X is Element of the carrier of MOS

K163(MOS,MOS,(- X)) is Element of the carrier of MOS

1 * (MOS - X) is Element of the carrier of MOS

the Mult of MOS . (1,(MOS - X)) is set

MOS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of MOS is non empty set

X is Element of the carrier of MOS

MOS is Element of the carrier of MOS

X is Element of the carrier of MOS

(MOS,X,X) is Element of the carrier of MOS

(MOS,X,MOS) is Element of the carrier of MOS

2 is non empty V24() V25() V33() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT

MOS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of MOS is non empty set

X is Element of the carrier of MOS

MOS is Element of the carrier of MOS

(MOS,X,MOS) is Element of the carrier of MOS

(MOS,X,MOS) - X is Element of the carrier of MOS

- X is Element of the carrier of MOS

K163(MOS,(MOS,X,MOS),(- X)) is Element of the carrier of MOS

2 * ((MOS,X,MOS) - X) is Element of the carrier of MOS

the Mult of MOS is V1() V4([:REAL, the carrier of MOS:]) V5( the carrier of MOS) V6() V18([:REAL, the carrier of MOS:], the carrier of MOS) Element of bool [:[:REAL, the carrier of MOS:], the carrier of MOS:]

[:REAL, the carrier of MOS:] is set

[:[:REAL, the carrier of MOS:], the carrier of MOS:] is set

bool [:[:REAL, the carrier of MOS:], the carrier of MOS:] is non empty set

the Mult of MOS . (2,((MOS,X,MOS) - X)) is set

MOS - X is Element of the carrier of MOS

K163(MOS,MOS,(- X)) is Element of the carrier of MOS

MOS - (MOS,X,MOS) is Element of the carrier of MOS

- (MOS,X,MOS) is Element of the carrier of MOS

K163(MOS,MOS,(- (MOS,X,MOS))) is Element of the carrier of MOS

2 * (MOS - (MOS,X,MOS)) is Element of the carrier of MOS

the Mult of MOS . (2,(MOS - (MOS,X,MOS))) is set

2 - 1 is V24() V34() V35() Element of REAL

2 * MOS is Element of the carrier of MOS

the Mult of MOS . (2,MOS) is set

1 + 1 is V24() V34() V35() Element of REAL

(1 + 1) * (MOS,X,MOS) is Element of the carrier of MOS

the Mult of MOS . ((1 + 1),(MOS,X,MOS)) is set

(2 * MOS) - ((1 + 1) * (MOS,X,MOS)) is Element of the carrier of MOS

- ((1 + 1) * (MOS,X,MOS)) is Element of the carrier of MOS

K163(MOS,(2 * MOS),(- ((1 + 1) * (MOS,X,MOS)))) is Element of the carrier of MOS

1 * (MOS,X,MOS) is Element of the carrier of MOS

the Mult of MOS . (1,(MOS,X,MOS)) is set

(1 * (MOS,X,MOS)) + (1 * (MOS,X,MOS)) is Element of the carrier of MOS

(2 * MOS) - ((1 * (MOS,X,MOS)) + (1 * (MOS,X,MOS))) is Element of the carrier of MOS

- ((1 * (MOS,X,MOS)) + (1 * (MOS,X,MOS))) is Element of the carrier of MOS

K163(MOS,(2 * MOS),(- ((1 * (MOS,X,MOS)) + (1 * (MOS,X,MOS))))) is Element of the carrier of MOS

(1 * (MOS,X,MOS)) + (MOS,X,MOS) is Element of the carrier of MOS

(2 * MOS) - ((1 * (MOS,X,MOS)) + (MOS,X,MOS)) is Element of the carrier of MOS

- ((1 * (MOS,X,MOS)) + (MOS,X,MOS)) is Element of the carrier of MOS

K163(MOS,(2 * MOS),(- ((1 * (MOS,X,MOS)) + (MOS,X,MOS)))) is Element of the carrier of MOS

(MOS,X,MOS) + (MOS,X,MOS) is Element of the carrier of MOS

(2 * MOS) - ((MOS,X,MOS) + (MOS,X,MOS)) is Element of the carrier of MOS

- ((MOS,X,MOS) + (MOS,X,MOS)) is Element of the carrier of MOS

K163(MOS,(2 * MOS),(- ((MOS,X,MOS) + (MOS,X,MOS)))) is Element of the carrier of MOS

X + MOS is Element of the carrier of MOS

(2 * MOS) - (X + MOS) is Element of the carrier of MOS

- (X + MOS) is Element of the carrier of MOS

K163(MOS,(2 * MOS),(- (X + MOS))) is Element of the carrier of MOS

(2 * MOS) - MOS is Element of the carrier of MOS

- MOS is Element of the carrier of MOS

K163(MOS,(2 * MOS),(- MOS)) is Element of the carrier of MOS

((2 * MOS) - MOS) - X is Element of the carrier of MOS

K163(MOS,((2 * MOS) - MOS),(- X)) is Element of the carrier of MOS

1 * MOS is Element of the carrier of MOS

the Mult of MOS . (1,MOS) is set

(2 * MOS) - (1 * MOS) is Element of the carrier of MOS

- (1 * MOS) is Element of the carrier of MOS

K163(MOS,(2 * MOS),(- (1 * MOS))) is Element of the carrier of MOS

((2 * MOS) - (1 * MOS)) - X is Element of the carrier of MOS

K163(MOS,((2 * MOS) - (1 * MOS)),(- X)) is Element of the carrier of MOS

(1 * MOS) - X is Element of the carrier of MOS

K163(MOS,(1 * MOS),(- X)) is Element of the carrier of MOS

1 - 2 is V24() V34() V35() Element of REAL

2 * X is Element of the carrier of MOS

the Mult of MOS . (2,X) is set

((1 + 1) * (MOS,X,MOS)) - (2 * X) is Element of the carrier of MOS

- (2 * X) is Element of the carrier of MOS

K163(MOS,((1 + 1) * (MOS,X,MOS)),(- (2 * X))) is Element of the carrier of MOS

((1 * (MOS,X,MOS)) + (1 * (MOS,X,MOS))) - (2 * X) is Element of the carrier of MOS

K163(MOS,((1 * (MOS,X,MOS)) + (1 * (MOS,X,MOS))),(- (2 * X))) is Element of the carrier of MOS

(MOS,X,MOS) + (1 * (MOS,X,MOS)) is Element of the carrier of MOS

((MOS,X,MOS) + (1 * (MOS,X,MOS))) - (2 * X) is Element of the carrier of MOS

K163(MOS,((MOS,X,MOS) + (1 * (MOS,X,MOS))),(- (2 * X))) is Element of the carrier of MOS

((MOS,X,MOS) + (MOS,X,MOS)) - (2 * X) is Element of the carrier of MOS

K163(MOS,((MOS,X,MOS) + (MOS,X,MOS)),(- (2 * X))) is Element of the carrier of MOS

(X + MOS) - (2 * X) is Element of the carrier of MOS

K163(MOS,(X + MOS),(- (2 * X))) is Element of the carrier of MOS

X - (2 * X) is Element of the carrier of MOS

K163(MOS,X,(- (2 * X))) is Element of the carrier of MOS

MOS + (X - (2 * X)) is Element of the carrier of MOS

1 * X is Element of the carrier of MOS

the Mult of MOS . (1,X) is set

(1 * X) - (2 * X) is Element of the carrier of MOS

K163(MOS,(1 * X),(- (2 * X))) is Element of the carrier of MOS

MOS + ((1 * X) - (2 * X)) is Element of the carrier of MOS

(- 1) * X is Element of the carrier of MOS

the Mult of MOS . ((- 1),X) is set

MOS + ((- 1) * X) is Element of the carrier of MOS

MOS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of MOS is non empty set

X is Element of the carrier of MOS

MOS is Element of the carrier of MOS

(MOS,X,MOS) is Element of the carrier of MOS

(MOS,X,MOS) - X is Element of the carrier of MOS

- X is Element of the carrier of MOS

K163(MOS,(MOS,X,MOS),(- X)) is Element of the carrier of MOS

2 * ((MOS,X,MOS) - X) is Element of the carrier of MOS

the Mult of MOS is V1() V4([:REAL, the carrier of MOS:]) V5( the carrier of MOS) V6() V18([:REAL, the carrier of MOS:], the carrier of MOS) Element of bool [:[:REAL, the carrier of MOS:], the carrier of MOS:]

[:REAL, the carrier of MOS:] is set

[:[:REAL, the carrier of MOS:], the carrier of MOS:] is set

bool [:[:REAL, the carrier of MOS:], the carrier of MOS:] is non empty set

the Mult of MOS . (2,((MOS,X,MOS) - X)) is set

MOS - X is Element of the carrier of MOS

K163(MOS,MOS,(- X)) is Element of the carrier of MOS

MOS - (MOS,X,MOS) is Element of the carrier of MOS

- (MOS,X,MOS) is Element of the carrier of MOS

K163(MOS,MOS,(- (MOS,X,MOS))) is Element of the carrier of MOS

2 * (MOS - (MOS,X,MOS)) is Element of the carrier of MOS

the Mult of MOS . (2,(MOS - (MOS,X,MOS))) is set

MOS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of MOS is non empty set

X is Element of the carrier of MOS

MOS is Element of the carrier of MOS

(MOS,X,MOS) is Element of the carrier of MOS

MOS - X is Element of the carrier of MOS

- X is Element of the carrier of MOS

K163(MOS,MOS,(- X)) is Element of the carrier of MOS

1 * (MOS - X) is Element of the carrier of MOS

the Mult of MOS is V1() V4([:REAL, the carrier of MOS:]) V5( the carrier of MOS) V6() V18([:REAL, the carrier of MOS:], the carrier of MOS) Element of bool [:[:REAL, the carrier of MOS:], the carrier of MOS:]

[:REAL, the carrier of MOS:] is set

[:[:REAL, the carrier of MOS:], the carrier of MOS:] is set

bool [:[:REAL, the carrier of MOS:], the carrier of MOS:] is non empty set

the Mult of MOS . (1,(MOS - X)) is set

(MOS,X,MOS) - X is Element of the carrier of MOS

K163(MOS,(MOS,X,MOS),(- X)) is Element of the carrier of MOS

2 * ((MOS,X,MOS) - X) is Element of the carrier of MOS

the Mult of MOS . (2,((MOS,X,MOS) - X)) is set

MOS - (MOS,X,MOS) is Element of the carrier of MOS

- (MOS,X,MOS) is Element of the carrier of MOS

K163(MOS,MOS,(- (MOS,X,MOS))) is Element of the carrier of MOS

2 * (MOS - (MOS,X,MOS)) is Element of the carrier of MOS

the Mult of MOS . (2,(MOS - (MOS,X,MOS))) is set

MOS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of MOS is non empty set

X is Element of the carrier of MOS

MOS is Element of the carrier of MOS

X is Element of the carrier of MOS

MOS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of MOS is non empty set

X is Element of the carrier of MOS

MOS is Element of the carrier of MOS

(MOS,X,MOS) is Element of the carrier of MOS

X is Element of the carrier of MOS

(MOS,MOS,X) is Element of the carrier of MOS

MOS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of MOS is non empty set

X is Element of the carrier of MOS

MOS is Element of the carrier of MOS

X is Element of the carrier of MOS

(MOS,X,X) is Element of the carrier of MOS

p is Element of the carrier of MOS

(MOS,MOS,p) is Element of the carrier of MOS

MOS - X is Element of the carrier of MOS

- X is Element of the carrier of MOS

K163(MOS,MOS,(- X)) is Element of the carrier of MOS

p - X is Element of the carrier of MOS

- X is Element of the carrier of MOS

K163(MOS,p,(- X)) is Element of the carrier of MOS

a1 is V24() V34() V35() Element of REAL

b is V24() V34() V35() Element of REAL

a1 * (MOS - X) is Element of the carrier of MOS

the Mult of MOS is V1() V4([:REAL, the carrier of MOS:]) V5( the carrier of MOS) V6() V18([:REAL, the carrier of MOS:], the carrier of MOS) Element of bool [:[:REAL, the carrier of MOS:], the carrier of MOS:]

[:REAL, the carrier of MOS:] is set

[:[:REAL, the carrier of MOS:], the carrier of MOS:] is set

bool [:[:REAL, the carrier of MOS:], the carrier of MOS:] is non empty set

the Mult of MOS . (a1,(MOS - X)) is set

b * (p - X) is Element of the carrier of MOS

the Mult of MOS . (b,(p - X)) is set

a1 + b is V24() V34() V35() Element of REAL

b * 2 is V24() V34() V35() Element of REAL

(MOS,MOS,p) - (MOS,X,X) is Element of the carrier of MOS

- (MOS,X,X) is Element of the carrier of MOS

K163(MOS,(MOS,MOS,p),(- (MOS,X,X))) is Element of the carrier of MOS

(b * 2) * ((MOS,MOS,p) - (MOS,X,X)) is Element of the carrier of MOS

the Mult of MOS . ((b * 2),((MOS,MOS,p) - (MOS,X,X))) is set

2 * ((MOS,MOS,p) - (MOS,X,X)) is Element of the carrier of MOS

the Mult of MOS . (2,((MOS,MOS,p) - (MOS,X,X))) is set

b * (2 * ((MOS,MOS,p) - (MOS,X,X))) is Element of the carrier of MOS

the Mult of MOS . (b,(2 * ((MOS,MOS,p) - (MOS,X,X)))) is set

1 + 1 is V24() V34() V35() Element of REAL

(1 + 1) * (MOS,MOS,p) is Element of the carrier of MOS

the Mult of MOS . ((1 + 1),(MOS,MOS,p)) is set

2 * (MOS,X,X) is Element of the carrier of MOS

the Mult of MOS . (2,(MOS,X,X)) is set

((1 + 1) * (MOS,MOS,p)) - (2 * (MOS,X,X)) is Element of the carrier of MOS

- (2 * (MOS,X,X)) is Element of the carrier of MOS

K163(MOS,((1 + 1) * (MOS,MOS,p)),(- (2 * (MOS,X,X)))) is Element of the carrier of MOS

b * (((1 + 1) * (MOS,MOS,p)) - (2 * (MOS,X,X))) is Element of the carrier of MOS

the Mult of MOS . (b,(((1 + 1) * (MOS,MOS,p)) - (2 * (MOS,X,X)))) is set

1 * (MOS,MOS,p) is Element of the carrier of MOS

the Mult of MOS . (1,(MOS,MOS,p)) is set

(1 * (MOS,MOS,p)) + (1 * (MOS,MOS,p)) is Element of the carrier of MOS

((1 * (MOS,MOS,p)) + (1 * (MOS,MOS,p))) - (2 * (MOS,X,X)) is Element of the carrier of MOS

K163(MOS,((1 * (MOS,MOS,p)) + (1 * (MOS,MOS,p))),(- (2 * (MOS,X,X)))) is Element of the carrier of MOS

b * (((1 * (MOS,MOS,p)) + (1 * (MOS,MOS,p))) - (2 * (MOS,X,X))) is Element of the carrier of MOS

the Mult of MOS . (b,(((1 * (MOS,MOS,p)) + (1 * (MOS,MOS,p))) - (2 * (MOS,X,X)))) is set

(MOS,MOS,p) + (1 * (MOS,MOS,p)) is Element of the carrier of MOS

((MOS,MOS,p) + (1 * (MOS,MOS,p))) - (2 * (MOS,X,X)) is Element of the carrier of MOS

K163(MOS,((MOS,MOS,p) + (1 * (MOS,MOS,p))),(- (2 * (MOS,X,X)))) is Element of the carrier of MOS

b * (((MOS,MOS,p) + (1 * (MOS,MOS,p))) - (2 * (MOS,X,X))) is Element of the carrier of MOS

the Mult of MOS . (b,(((MOS,MOS,p) + (1 * (MOS,MOS,p))) - (2 * (MOS,X,X)))) is set

(MOS,MOS,p) + (MOS,MOS,p) is Element of the carrier of MOS

((MOS,MOS,p) + (MOS,MOS,p)) - (2 * (MOS,X,X)) is Element of the carrier of MOS

K163(MOS,((MOS,MOS,p) + (MOS,MOS,p)),(- (2 * (MOS,X,X)))) is Element of the carrier of MOS

b * (((MOS,MOS,p) + (MOS,MOS,p)) - (2 * (MOS,X,X))) is Element of the carrier of MOS

the Mult of MOS . (b,(((MOS,MOS,p) + (MOS,MOS,p)) - (2 * (MOS,X,X)))) is set

MOS + p is Element of the carrier of MOS

(MOS + p) - (2 * (MOS,X,X)) is Element of the carrier of MOS

K163(MOS,(MOS + p),(- (2 * (MOS,X,X)))) is Element of the carrier of MOS

b * ((MOS + p) - (2 * (MOS,X,X))) is Element of the carrier of MOS

the Mult of MOS . (b,((MOS + p) - (2 * (MOS,X,X)))) is set

(1 + 1) * (MOS,X,X) is Element of the carrier of MOS

the Mult of MOS . ((1 + 1),(MOS,X,X)) is set

p - ((1 + 1) * (MOS,X,X)) is Element of the carrier of MOS

- ((1 + 1) * (MOS,X,X)) is Element of the carrier of MOS

K163(MOS,p,(- ((1 + 1) * (MOS,X,X)))) is Element of the carrier of MOS

MOS + (p - ((1 + 1) * (MOS,X,X))) is Element of the carrier of MOS

b * (MOS + (p - ((1 + 1) * (MOS,X,X)))) is Element of the carrier of MOS

the Mult of MOS . (b,(MOS + (p - ((1 + 1) * (MOS,X,X))))) is set

1 * (MOS,X,X) is Element of the carrier of MOS

the Mult of MOS . (1,(MOS,X,X)) is set

(1 * (MOS,X,X)) + (1 * (MOS,X,X)) is Element of the carrier of MOS

p - ((1 * (MOS,X,X)) + (1 * (MOS,X,X))) is Element of the carrier of MOS

- ((1 * (MOS,X,X)) + (1 * (MOS,X,X))) is Element of the carrier of MOS

K163(MOS,p,(- ((1 * (MOS,X,X)) + (1 * (MOS,X,X))))) is Element of the carrier of MOS

MOS + (p - ((1 * (MOS,X,X)) + (1 * (MOS,X,X)))) is Element of the carrier of MOS

b * (MOS + (p - ((1 * (MOS,X,X)) + (1 * (MOS,X,X))))) is Element of the carrier of MOS

the Mult of MOS . (b,(MOS + (p - ((1 * (MOS,X,X)) + (1 * (MOS,X,X)))))) is set

(MOS,X,X) + (1 * (MOS,X,X)) is Element of the carrier of MOS

p - ((MOS,X,X) + (1 * (MOS,X,X))) is Element of the carrier of MOS

- ((MOS,X,X) + (1 * (MOS,X,X))) is Element of the carrier of MOS

K163(MOS,p,(- ((MOS,X,X) + (1 * (MOS,X,X))))) is Element of the carrier of MOS

MOS + (p - ((MOS,X,X) + (1 * (MOS,X,X)))) is Element of the carrier of MOS

b * (MOS + (p - ((MOS,X,X) + (1 * (MOS,X,X))))) is Element of the carrier of MOS

the Mult of MOS . (b,(MOS + (p - ((MOS,X,X) + (1 * (MOS,X,X)))))) is set

(MOS,X,X) + (MOS,X,X) is Element of the carrier of MOS

p - ((MOS,X,X) + (MOS,X,X)) is Element of the carrier of MOS

- ((MOS,X,X) + (MOS,X,X)) is Element of the carrier of MOS

K163(MOS,p,(- ((MOS,X,X) + (MOS,X,X)))) is Element of the carrier of MOS

MOS + (p - ((MOS,X,X) + (MOS,X,X))) is Element of the carrier of MOS

b * (MOS + (p - ((MOS,X,X) + (MOS,X,X)))) is Element of the carrier of MOS

the Mult of MOS . (b,(MOS + (p - ((MOS,X,X) + (MOS,X,X))))) is set

X + X is Element of the carrier of MOS

p - (X + X) is Element of the carrier of MOS

- (X + X) is Element of the carrier of MOS

K163(MOS,p,(- (X + X))) is Element of the carrier of MOS

MOS + (p - (X + X)) is Element of the carrier of MOS

b * (MOS + (p - (X + X))) is Element of the carrier of MOS

the Mult of MOS . (b,(MOS + (p - (X + X)))) is set

(p - X) - X is Element of the carrier of MOS

K163(MOS,(p - X),(- X)) is Element of the carrier of MOS

MOS + ((p - X) - X) is Element of the carrier of MOS

b * (MOS + ((p - X) - X)) is Element of the carrier of MOS

the Mult of MOS . (b,(MOS + ((p - X) - X))) is set

MOS + (p - X) is Element of the carrier of MOS

(MOS + (p - X)) - X is Element of the carrier of MOS

K163(MOS,(MOS + (p - X)),(- X)) is Element of the carrier of MOS

b * ((MOS + (p - X)) - X) is Element of the carrier of MOS

the Mult of MOS . (b,((MOS + (p - X)) - X)) is set

(p - X) + (MOS - X) is Element of the carrier of MOS

b * ((p - X) + (MOS - X)) is Element of the carrier of MOS

the Mult of MOS . (b,((p - X) + (MOS - X))) is set

b * (MOS - X) is Element of the carrier of MOS

the Mult of MOS . (b,(MOS - X)) is set

(a1 * (MOS - X)) + (b * (MOS - X)) is Element of the carrier of MOS

(a1 + b) * (MOS - X) is Element of the carrier of MOS

the Mult of MOS . ((a1 + b),(MOS - X)) is set

MOS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of MOS is non empty set

X is Element of the carrier of MOS

MOS is Element of the carrier of MOS

X is Element of the carrier of MOS

(MOS,MOS,X) is Element of the carrier of MOS

p is Element of the carrier of MOS

(MOS,X,p) is Element of the carrier of MOS

MOS - X is Element of the carrier of MOS

- X is Element of the carrier of MOS

K163(MOS,MOS,(- X)) is Element of the carrier of MOS

p - X is Element of the carrier of MOS

- X is Element of the carrier of MOS

K163(MOS,p,(- X)) is Element of the carrier of MOS

q is V24() V34() V35() Element of REAL

a is V24() V34() V35() Element of REAL

q * (MOS - X) is Element of the carrier of MOS

the Mult of MOS is V1() V4([:REAL, the carrier of MOS:]) V5( the carrier of MOS) V6() V18([:REAL, the carrier of MOS:], the carrier of MOS) Element of bool [:[:REAL, the carrier of MOS:], the carrier of MOS:]

[:REAL, the carrier of MOS:] is set

[:[:REAL, the carrier of MOS:], the carrier of MOS:] is set

bool [:[:REAL, the carrier of MOS:], the carrier of MOS:] is non empty set

the Mult of MOS . (q,(MOS - X)) is set

a * (p - X) is Element of the carrier of MOS

the Mult of MOS . (a,(p - X)) is set

X - p is Element of the carrier of MOS

- p is Element of the carrier of MOS

K163(MOS,X,(- p)) is Element of the carrier of MOS

a * (X - p) is Element of the carrier of MOS

the Mult of MOS . (a,(X - p)) is set

- (p - X) is Element of the carrier of MOS

a * (- (p - X)) is Element of the carrier of MOS

the Mult of MOS . (a,(- (p - X))) is set

- (q * (MOS - X)) is Element of the carrier of MOS

- (MOS - X) is Element of the carrier of MOS

q * (- (MOS - X)) is Element of the carrier of MOS

the Mult of MOS . (q,(- (MOS - X))) is set

- q is V24() V34() V35() Element of REAL

(- q) * (MOS - X) is Element of the carrier of MOS

the Mult of MOS . ((- q),(MOS - X)) is set

a * 2 is V24() V34() V35() Element of REAL

a - q is V24() V34() V35() Element of REAL

(MOS,MOS,X) - (MOS,X,p) is Element of the carrier of MOS

- (MOS,X,p) is Element of the carrier of MOS

K163(MOS,(MOS,MOS,X),(- (MOS,X,p))) is Element of the carrier of MOS

(a * 2) * ((MOS,MOS,X) - (MOS,X,p)) is Element of the carrier of MOS

the Mult of MOS . ((a * 2),((MOS,MOS,X) - (MOS,X,p))) is set

2 * ((MOS,MOS,X) - (MOS,X,p)) is Element of the carrier of MOS

the Mult of MOS . (2,((MOS,MOS,X) - (MOS,X,p))) is set

a * (2 * ((MOS,MOS,X) - (MOS,X,p))) is Element of the carrier of MOS

the Mult of MOS . (a,(2 * ((MOS,MOS,X) - (MOS,X,p)))) is set

1 + 1 is V24() V34() V35() Element of REAL

(1 + 1) * (MOS,MOS,X) is Element of the carrier of MOS

the Mult of MOS . ((1 + 1),(MOS,MOS,X)) is set

2 * (MOS,X,p) is Element of the carrier of MOS

the Mult of MOS . (2,(MOS,X,p)) is set

((1 + 1) * (MOS,MOS,X)) - (2 * (MOS,X,p)) is Element of the carrier of MOS

- (2 * (MOS,X,p)) is Element of the carrier of MOS

K163(MOS,((1 + 1) * (MOS,MOS,X)),(- (2 * (MOS,X,p)))) is Element of the carrier of MOS

a * (((1 + 1) * (MOS,MOS,X)) - (2 * (MOS,X,p))) is Element of the carrier of MOS

the Mult of MOS . (a,(((1 + 1) * (MOS,MOS,X)) - (2 * (MOS,X,p)))) is set

1 * (MOS,MOS,X) is Element of the carrier of MOS

the Mult of MOS . (1,(MOS,MOS,X)) is set

(1 * (MOS,MOS,X)) + (1 * (MOS,MOS,X)) is Element of the carrier of MOS

((1 * (MOS,MOS,X)) + (1 * (MOS,MOS,X))) - (2 * (MOS,X,p)) is Element of the carrier of MOS

K163(MOS,((1 * (MOS,MOS,X)) + (1 * (MOS,MOS,X))),(- (2 * (MOS,X,p)))) is Element of the carrier of MOS

a * (((1 * (MOS,MOS,X)) + (1 * (MOS,MOS,X))) - (2 * (MOS,X,p))) is Element of the carrier of MOS

the Mult of MOS . (a,(((1 * (MOS,MOS,X)) + (1 * (MOS,MOS,X))) - (2 * (MOS,X,p)))) is set

(MOS,MOS,X) + (1 * (MOS,MOS,X)) is Element of the carrier of MOS

((MOS,MOS,X) + (1 * (MOS,MOS,X))) - (2 * (MOS,X,p)) is Element of the carrier of MOS

K163(MOS,((MOS,MOS,X) + (1 * (MOS,MOS,X))),(- (2 * (MOS,X,p)))) is Element of the carrier of MOS

a * (((MOS,MOS,X) + (1 * (MOS,MOS,X))) - (2 * (MOS,X,p))) is Element of the carrier of MOS

the Mult of MOS . (a,(((MOS,MOS,X) + (1 * (MOS,MOS,X))) - (2 * (MOS,X,p)))) is set

(MOS,MOS,X) + (MOS,MOS,X) is Element of the carrier of MOS

((MOS,MOS,X) + (MOS,MOS,X)) - (2 * (MOS,X,p)) is Element of the carrier of MOS

K163(MOS,((MOS,MOS,X) + (MOS,MOS,X)),(- (2 * (MOS,X,p)))) is Element of the carrier of MOS

a * (((MOS,MOS,X) + (MOS,MOS,X)) - (2 * (MOS,X,p))) is Element of the carrier of MOS

the Mult of MOS . (a,(((MOS,MOS,X) + (MOS,MOS,X)) - (2 * (MOS,X,p)))) is set

MOS + X is Element of the carrier of MOS

(MOS + X) - (2 * (MOS,X,p)) is Element of the carrier of MOS

K163(MOS,(MOS + X),(- (2 * (MOS,X,p)))) is Element of the carrier of MOS

a * ((MOS + X) - (2 * (MOS,X,p))) is Element of the carrier of MOS

the Mult of MOS . (a,((MOS + X) - (2 * (MOS,X,p)))) is set

(1 + 1) * (MOS,X,p) is Element of the carrier of MOS

the Mult of MOS . ((1 + 1),(MOS,X,p)) is set

X - ((1 + 1) * (MOS,X,p)) is Element of the carrier of MOS

- ((1 + 1) * (MOS,X,p)) is Element of the carrier of MOS

K163(MOS,X,(- ((1 + 1) * (MOS,X,p)))) is Element of the carrier of MOS

MOS + (X - ((1 + 1) * (MOS,X,p))) is Element of the carrier of MOS

a * (MOS + (X - ((1 + 1) * (MOS,X,p)))) is Element of the carrier of MOS

the Mult of MOS . (a,(MOS + (X - ((1 + 1) * (MOS,X,p))))) is set

1 * (MOS,X,p) is Element of the carrier of MOS

the Mult of MOS . (1,(MOS,X,p)) is set

(1 * (MOS,X,p)) + (1 * (MOS,X,p)) is Element of the carrier of MOS

X - ((1 * (MOS,X,p)) + (1 * (MOS,X,p))) is Element of the carrier of MOS

- ((1 * (MOS,X,p)) + (1 * (MOS,X,p))) is Element of the carrier of MOS

K163(MOS,X,(- ((1 * (MOS,X,p)) + (1 * (MOS,X,p))))) is Element of the carrier of MOS

MOS + (X - ((1 * (MOS,X,p)) + (1 * (MOS,X,p)))) is Element of the carrier of MOS

a * (MOS + (X - ((1 * (MOS,X,p)) + (1 * (MOS,X,p))))) is Element of the carrier of MOS

the Mult of MOS . (a,(MOS + (X - ((1 * (MOS,X,p)) + (1 * (MOS,X,p)))))) is set

(MOS,X,p) + (1 * (MOS,X,p)) is Element of the carrier of MOS

X - ((MOS,X,p) + (1 * (MOS,X,p))) is Element of the carrier of MOS

- ((MOS,X,p) + (1 * (MOS,X,p))) is Element of the carrier of MOS

K163(MOS,X,(- ((MOS,X,p) + (1 * (MOS,X,p))))) is Element of the carrier of MOS

MOS + (X - ((MOS,X,p) + (1 * (MOS,X,p)))) is Element of the carrier of MOS

a * (MOS + (X - ((MOS,X,p) + (1 * (MOS,X,p))))) is Element of the carrier of MOS

the Mult of MOS . (a,(MOS + (X - ((MOS,X,p) + (1 * (MOS,X,p)))))) is set

(MOS,X,p) + (MOS,X,p) is Element of the carrier of MOS

X - ((MOS,X,p) + (MOS,X,p)) is Element of the carrier of MOS

- ((MOS,X,p) + (MOS,X,p)) is Element of the carrier of MOS

K163(MOS,X,(- ((MOS,X,p) + (MOS,X,p)))) is Element of the carrier of MOS

MOS + (X - ((MOS,X,p) + (MOS,X,p))) is Element of the carrier of MOS

a * (MOS + (X - ((MOS,X,p) + (MOS,X,p)))) is Element of the carrier of MOS

the Mult of MOS . (a,(MOS + (X - ((MOS,X,p) + (MOS,X,p))))) is set

X + p is Element of the carrier of MOS

X - (X + p) is Element of the carrier of MOS

- (X + p) is Element of the carrier of MOS

K163(MOS,X,(- (X + p))) is Element of the carrier of MOS

MOS + (X - (X + p)) is Element of the carrier of MOS

a * (MOS + (X - (X + p))) is Element of the carrier of MOS

the Mult of MOS . (a,(MOS + (X - (X + p)))) is set

(X - p) - X is Element of the carrier of MOS

K163(MOS,(X - p),(- X)) is Element of the carrier of MOS

MOS + ((X - p) - X) is Element of the carrier of MOS

a * (MOS + ((X - p) - X)) is Element of the carrier of MOS

the Mult of MOS . (a,(MOS + ((X - p) - X))) is set

MOS + (X - p) is Element of the carrier of MOS

(MOS + (X - p)) - X is Element of the carrier of MOS

K163(MOS,(MOS + (X - p)),(- X)) is Element of the carrier of MOS

a * ((MOS + (X - p)) - X) is Element of the carrier of MOS

the Mult of MOS . (a,((MOS + (X - p)) - X)) is set

(X - p) + (MOS - X) is Element of the carrier of MOS

a * ((X - p) + (MOS - X)) is Element of the carrier of MOS

the Mult of MOS . (a,((X - p) + (MOS - X))) is set

a * (MOS - X) is Element of the carrier of MOS

the Mult of MOS . (a,(MOS - X)) is set

((- q) * (MOS - X)) + (a * (MOS - X)) is Element of the carrier of MOS

a + (- q) is V24() V34() V35() Element of REAL

(a + (- q)) * (MOS - X) is Element of the carrier of MOS

the Mult of MOS . ((a + (- q)),(MOS - X)) is set

(a - q) * (MOS - X) is Element of the carrier of MOS

the Mult of MOS . ((a - q),(MOS - X)) is set

MOS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of MOS is non empty set

X is Element of the carrier of MOS

MOS is Element of the carrier of MOS

(MOS,X,MOS) is Element of the carrier of MOS

X is Element of the carrier of MOS

X - X is Element of the carrier of MOS

- X is Element of the carrier of MOS

K163(MOS,X,(- X)) is Element of the carrier of MOS

p is Element of the carrier of MOS

(MOS,X,p) is Element of the carrier of MOS

p - MOS is Element of the carrier of MOS

- MOS is Element of the carrier of MOS

K163(MOS,p,(- MOS)) is Element of the carrier of MOS

- (p - MOS) is Element of the carrier of MOS

(MOS,X,MOS) + (MOS,X,MOS) is Element of the carrier of MOS

X + MOS is Element of the carrier of MOS

X + p is Element of the carrier of MOS

(X - X) + p is Element of the carrier of MOS

p + X is Element of the carrier of MOS

(p + X) - X is Element of the carrier of MOS

K163(MOS,(p + X),(- X)) is Element of the carrier of MOS

(X - X) + (p - MOS) is Element of the carrier of MOS

MOS - MOS is Element of the carrier of MOS

K163(MOS,MOS,(- MOS)) is Element of the carrier of MOS

0. MOS is V59(MOS) Element of the carrier of MOS

the ZeroF of MOS is Element of the carrier of MOS

MOS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of MOS is non empty set

X is Element of the carrier of MOS

MOS is Element of the carrier of MOS

X is Element of the carrier of MOS

p is Element of the carrier of MOS

q is Element of the carrier of MOS

a is Element of the carrier of MOS

MOS - X is Element of the carrier of MOS

- X is Element of the carrier of MOS

K163(MOS,MOS,(- X)) is Element of the carrier of MOS

p - X is Element of the carrier of MOS

- X is Element of the carrier of MOS

K163(MOS,p,(- X)) is Element of the carrier of MOS

(- 1) * (p - X) is Element of the carrier of MOS

the Mult of MOS is V1() V4([:REAL, the carrier of MOS:]) V5( the carrier of MOS) V6() V18([:REAL, the carrier of MOS:], the carrier of MOS) Element of bool [:[:REAL, the carrier of MOS:], the carrier of MOS:]

[:REAL, the carrier of MOS:] is set

[:[:REAL, the carrier of MOS:], the carrier of MOS:] is set

bool [:[:REAL, the carrier of MOS:], the carrier of MOS:] is non empty set

the Mult of MOS . ((- 1),(p - X)) is set

- (p - X) is Element of the carrier of MOS

X - p is Element of the carrier of MOS

- p is Element of the carrier of MOS

K163(MOS,X,(- p)) is Element of the carrier of MOS

MOS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of MOS is non empty set

X is Element of the carrier of MOS

MOS is Element of the carrier of MOS

X is Element of the carrier of MOS

p is Element of the carrier of MOS

q is Element of the carrier of MOS

a is Element of the carrier of MOS

MOS - X is Element of the carrier of MOS

- X is Element of the carrier of MOS

K163(MOS,MOS,(- X)) is Element of the carrier of MOS

p - X is Element of the carrier of MOS

- X is Element of the carrier of MOS

K163(MOS,p,(- X)) is Element of the carrier of MOS

MOS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of MOS is non empty set

X is Element of the carrier of MOS

MOS is Element of the carrier of MOS

X is Element of the carrier of MOS

p is Element of the carrier of MOS

q is Element of the carrier of MOS

q - q is Element of the carrier of MOS

- q is Element of the carrier of MOS

K163(MOS,q,(- q)) is Element of the carrier of MOS

0. MOS is V59(MOS) Element of the carrier of MOS

the ZeroF of MOS is Element of the carrier of MOS

p - X is Element of the carrier of MOS

- X is Element of the carrier of MOS

K163(MOS,p,(- X)) is Element of the carrier of MOS

MOS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of MOS is non empty set

X is Element of the carrier of MOS

MOS is Element of the carrier of MOS

X is Element of the carrier of MOS

p is Element of the carrier of MOS

q is Element of the carrier of MOS

a is Element of the carrier of MOS

a1 is Element of the carrier of MOS

p - X is Element of the carrier of MOS

- X is Element of the carrier of MOS

K163(MOS,p,(- X)) is Element of the carrier of MOS

a - q is Element of the carrier of MOS

- q is Element of the carrier of MOS

K163(MOS,a,(- q)) is Element of the carrier of MOS

a1 - q is Element of the carrier of MOS

K163(MOS,a1,(- q)) is Element of the carrier of MOS

(a1 - q) - (a - q) is Element of the carrier of MOS

- (a - q) is Element of the carrier of MOS

K163(MOS,(a1 - q),(- (a - q))) is Element of the carrier of MOS

q + (a - q) is Element of the carrier of MOS

a1 - (q + (a - q)) is Element of the carrier of MOS

- (q + (a - q)) is Element of the carrier of MOS

K163(MOS,a1,(- (q + (a - q)))) is Element of the carrier of MOS

q - q is Element of the carrier of MOS

K163(MOS,q,(- q)) is Element of the carrier of MOS

a - (q - q) is Element of the carrier of MOS

- (q - q) is Element of the carrier of MOS

K163(MOS,a,(- (q - q))) is Element of the carrier of MOS

a1 - (a - (q - q)) is Element of the carrier of MOS

- (a - (q - q)) is Element of the carrier of MOS

K163(MOS,a1,(- (a - (q - q)))) is Element of the carrier of MOS

0. MOS is V59(MOS) Element of the carrier of MOS

the ZeroF of MOS is Element of the carrier of MOS

a - (0. MOS) is Element of the carrier of MOS

- (0. MOS) is Element of the carrier of MOS

K163(MOS,a,(- (0. MOS))) is Element of the carrier of MOS

a1 - (a - (0. MOS)) is Element of the carrier of MOS

- (a - (0. MOS)) is Element of the carrier of MOS

K163(MOS,a1,(- (a - (0. MOS)))) is Element of the carrier of MOS

a1 - a is Element of the carrier of MOS

- a is Element of the carrier of MOS

K163(MOS,a1,(- a)) is Element of the carrier of MOS

MOS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of MOS is non empty set

X is Element of the carrier of MOS

MOS is Element of the carrier of MOS

X is Element of the carrier of MOS

p is Element of the carrier of MOS

p - X is Element of the carrier of MOS

- X is Element of the carrier of MOS

K163(MOS,p,(- X)) is Element of the carrier of MOS

0. MOS is V59(MOS) Element of the carrier of MOS

the ZeroF of MOS is Element of the carrier of MOS

MOS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of MOS is non empty set

X is Element of the carrier of MOS

MOS is Element of the carrier of MOS

X is Element of the carrier of MOS

p is Element of the carrier of MOS

q is Element of the carrier of MOS

q - q is Element of the carrier of MOS

- q is Element of the carrier of MOS

K163(MOS,q,(- q)) is Element of the carrier of MOS

0. MOS is V59(MOS) Element of the carrier of MOS

the ZeroF of MOS is Element of the carrier of MOS

p - X is Element of the carrier of MOS

- X is Element of the carrier of MOS

K163(MOS,p,(- X)) is Element of the carrier of MOS

MOS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of MOS is non empty set

X is Element of the carrier of MOS

MOS is Element of the carrier of MOS

X is Element of the carrier of MOS

p is Element of the carrier of MOS

q is Element of the carrier of MOS

a is Element of the carrier of MOS

a1 is Element of the carrier of MOS

b is Element of the carrier of MOS

AMSpace (MOS,X,MOS) is non empty strict ParOrtStr

the carrier of (AMSpace (MOS,X,MOS)) is non empty set

b9 is non empty OrtAfSp-like ParOrtStr

the carrier of b9 is non empty set

b1 is Element of the carrier of (AMSpace (MOS,X,MOS))

c is Element of the carrier of (AMSpace (MOS,X,MOS))

c1 is Element of the carrier of (AMSpace (MOS,X,MOS))

d is Element of the carrier of (AMSpace (MOS,X,MOS))

d1 is Element of the carrier of (AMSpace (MOS,X,MOS))

a9 is Element of the carrier of (AMSpace (MOS,X,MOS))

c19 is Element of the carrier of b9

d19 is Element of the carrier of b9

c9 is Element of the carrier of b9

d9 is Element of the carrier of b9

a19 is Element of the carrier of b9

b19 is Element of the carrier of b9

MOS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of MOS is non empty set

MOS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of MOS is non empty set

X is Element of the carrier of MOS

MOS is Element of the carrier of MOS

X is Element of the carrier of MOS

p is Element of the carrier of MOS

(MOS,X,X) is Element of the carrier of MOS

(MOS,p,p) is Element of the carrier of MOS

MOS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of MOS is non empty set

X is Element of the carrier of MOS

MOS is Element of the carrier of MOS

X is Element of the carrier of MOS

p is Element of the carrier of MOS

(MOS,X,p) is Element of the carrier of MOS

MOS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of MOS is non empty set

X is Element of the carrier of MOS

MOS is Element of the carrier of MOS

X is Element of the carrier of MOS

p is Element of the carrier of MOS

MOS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of MOS is non empty set

X is Element of the carrier of MOS

MOS is Element of the carrier of MOS

X is Element of the carrier of MOS

p is Element of the carrier of MOS

q is Element of the carrier of MOS

(MOS,X,p) is Element of the carrier of MOS

(MOS,p,q) is Element of the carrier of MOS

(MOS,p,p) is Element of the carrier of MOS

(MOS,p,p) is Element of the carrier of MOS

MOS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of MOS is non empty set

X is Element of the carrier of MOS

MOS is Element of the carrier of MOS

X is Element of the carrier of MOS

p is Element of the carrier of MOS

q is Element of the carrier of MOS

a is Element of the carrier of MOS

a1 is Element of the carrier of MOS

b is Element of the carrier of MOS

(MOS,q,a) is Element of the carrier of MOS

(MOS,a1,b) is Element of the carrier of MOS

(MOS,X,p) is Element of the carrier of MOS

MOS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of MOS is non empty set

X is Element of the carrier of MOS

MOS is Element of the carrier of MOS

X is Element of the carrier of MOS

p is Element of the carrier of MOS

q is Element of the carrier of MOS

(MOS,X,p) is Element of the carrier of MOS

(MOS,X,X) is Element of the carrier of MOS

(MOS,q,q) is Element of the carrier of MOS

(MOS,X,X) is Element of the carrier of MOS

X - (MOS,X,p) is Element of the carrier of MOS

- (MOS,X,p) is Element of the carrier of MOS

K163(MOS,X,(- (MOS,X,p))) is Element of the carrier of MOS

0. MOS is V59(MOS) Element of the carrier of MOS

the ZeroF of MOS is Element of the carrier of MOS

q - (MOS,X,p) is Element of the carrier of MOS

K163(MOS,q,(- (MOS,X,p))) is Element of the carrier of MOS

a1 is V24() V34() V35() Element of REAL

a1 * (X - (MOS,X,p)) is Element of the carrier of MOS

the Mult of MOS is V1() V4([:REAL, the carrier of MOS:]) V5( the carrier of MOS) V6() V18([:REAL, the carrier of MOS:], the carrier of MOS) Element of bool [:[:REAL, the carrier of MOS:], the carrier of MOS:]

[:REAL, the carrier of MOS:] is set

[:[:REAL, the carrier of MOS:], the carrier of MOS:] is set

bool [:[:REAL, the carrier of MOS:], the carrier of MOS:] is non empty set

the Mult of MOS . (a1,(X - (MOS,X,p))) is set

(q - (MOS,X,p)) - (a1 * (X - (MOS,X,p))) is Element of the carrier of MOS

- (a1 * (X - (MOS,X,p))) is Element of the carrier of MOS

K163(MOS,(q - (MOS,X,p)),(- (a1 * (X - (MOS,X,p))))) is Element of the carrier of MOS

q - (a1 * (X - (MOS,X,p))) is Element of the carrier of MOS

K163(MOS,q,(- (a1 * (X - (MOS,X,p))))) is Element of the carrier of MOS

2 * (q - (a1 * (X - (MOS,X,p)))) is Element of the carrier of MOS

the Mult of MOS . (2,(q - (a1 * (X - (MOS,X,p))))) is set

(2 * (q - (a1 * (X - (MOS,X,p))))) - q is Element of the carrier of MOS

- q is Element of the carrier of MOS

K163(MOS,(2 * (q - (a1 * (X - (MOS,X,p))))),(- q)) is Element of the carrier of MOS

q + ((2 * (q - (a1 * (X - (MOS,X,p))))) - q) is Element of the carrier of MOS

1 + 1 is V24() V34() V35() Element of REAL

(1 + 1) * (q - (a1 * (X - (MOS,X,p)))) is Element of the carrier of MOS

the Mult of MOS . ((1 + 1),(q - (a1 * (X - (MOS,X,p))))) is set

1 * (q - (a1 * (X - (MOS,X,p)))) is Element of the carrier of MOS

the Mult of MOS . (1,(q - (a1 * (X - (MOS,X,p))))) is set

(1 * (q - (a1 * (X - (MOS,X,p))))) + (1 * (q - (a1 * (X - (MOS,X,p))))) is Element of the carrier of MOS

(q - (a1 * (X - (MOS,X,p)))) + (1 * (q - (a1 * (X - (MOS,X,p))))) is Element of the carrier of MOS

(q - (a1 * (X - (MOS,X,p)))) + (q - (a1 * (X - (MOS,X,p)))) is Element of the carrier of MOS

(MOS,q,((2 * (q - (a1 * (X - (MOS,X,p))))) - q)) is Element of the carrier of MOS

q - (q - (a1 * (X - (MOS,X,p)))) is Element of the carrier of MOS

- (q - (a1 * (X - (MOS,X,p)))) is Element of the carrier of MOS

K163(MOS,q,(- (q - (a1 * (X - (MOS,X,p)))))) is Element of the carrier of MOS

q - q is Element of the carrier of MOS

K163(MOS,q,(- q)) is Element of the carrier of MOS

(q - q) + (a1 * (X - (MOS,X,p))) is Element of the carrier of MOS

(0. MOS) + (a1 * (X - (MOS,X,p))) is Element of the carrier of MOS

q - ((2 * (q - (a1 * (X - (MOS,X,p))))) - q) is Element of the carrier of MOS

- ((2 * (q - (a1 * (X - (MOS,X,p))))) - q) is Element of the carrier of MOS

K163(MOS,q,(- ((2 * (q - (a1 * (X - (MOS,X,p))))) - q))) is Element of the carrier of MOS

2 * (a1 * (X - (MOS,X,p))) is Element of the carrier of MOS

the Mult of MOS . (2,(a1 * (X - (MOS,X,p)))) is set

2 * a1 is V24() V34() V35() Element of REAL

(2 * a1) * (X - (MOS,X,p)) is Element of the carrier of MOS

the Mult of MOS . ((2 * a1),(X - (MOS,X,p))) is set

(MOS,X,p) + (a1 * (X - (MOS,X,p))) is Element of the carrier of MOS

q - ((MOS,X,p) + (a1 * (X - (MOS,X,p)))) is Element of the carrier of MOS

- ((MOS,X,p) + (a1 * (X - (MOS,X,p)))) is Element of the carrier of MOS

K163(MOS,q,(- ((MOS,X,p) + (a1 * (X - (MOS,X,p)))))) is Element of the carrier of MOS

(q - (a1 * (X - (MOS,X,p)))) - (MOS,X,p) is Element of the carrier of MOS

K163(MOS,(q - (a1 * (X - (MOS,X,p)))),(- (MOS,X,p))) is Element of the carrier of MOS

(MOS,((2 * (q - (a1 * (X - (MOS,X,p))))) - q),q) is Element of the carrier of MOS

X - p is Element of the carrier of MOS

- p is Element of the carrier of MOS

K163(MOS,X,(- p)) is Element of the carrier of MOS

2 * (X - (MOS,X,p)) is Element of the carrier of MOS

the Mult of MOS . (2,(X - (MOS,X,p))) is set

a1 * (X - p) is Element of the carrier of MOS

the Mult of MOS . (a1,(X - p)) is set

1 * (q - ((2 * (q - (a1 * (X - (MOS,X,p))))) - q)) is Element of the carrier of MOS

the Mult of MOS . (1,(q - ((2 * (q - (a1 * (X - (MOS,X,p))))) - q))) is set

MOS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of MOS is non empty set

X is Element of the carrier of MOS

MOS is Element of the carrier of MOS

X is Element of the carrier of MOS

p is Element of the carrier of MOS

q is Element of the carrier of MOS

a is Element of the carrier of MOS

(MOS,X,MOS) is Element of the carrier of MOS

(MOS,X,p) is Element of the carrier of MOS

MOS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of MOS is non empty set

X is Element of the carrier of MOS

MOS is Element of the carrier of MOS

X is Element of the carrier of MOS

p is Element of the carrier of MOS

q is Element of the carrier of MOS

a is Element of the carrier of MOS

a1 is Element of the carrier of MOS

b is Element of the carrier of MOS

b1 is Element of the carrier of MOS

c is Element of the carrier of MOS

(MOS,X,MOS) is Element of the carrier of MOS

(MOS,X,p) is Element of the carrier of MOS

(MOS,MOS,X) is Element of the carrier of MOS

(MOS,p,X) is Element of the carrier of MOS

MOS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of MOS is non empty set

X is Element of the carrier of MOS

MOS is Element of the carrier of MOS

X is Element of the carrier of MOS

p is Element of the carrier of MOS

q is Element of the carrier of MOS

a is Element of the carrier of MOS

a1 is Element of the carrier of MOS

b is Element of the carrier of MOS

OASpace MOS is non empty strict AffinStruct

Lambda (OASpace MOS) is non empty strict AffinStruct

the carrier of (Lambda (OASpace MOS)) is non empty set

b9 is non empty non trivial OAffinSpace-like AffinStruct

Lambda b9 is non empty strict AffinStruct

c9 is non empty non trivial AffinSpace-like AffinStruct

the carrier of c9 is non empty non trivial set

b1 is Element of the carrier of (Lambda (OASpace MOS))

c is Element of the carrier of (Lambda (OASpace MOS))

c1 is Element of the carrier of (Lambda (OASpace MOS))

d is Element of the carrier of (Lambda (OASpace MOS))

d1 is Element of the carrier of (Lambda (OASpace MOS))

a9 is Element of the carrier of (Lambda (OASpace MOS))

d9 is Element of the carrier of c9

a19 is Element of the carrier of c9

b19 is Element of the carrier of c9

c19 is Element of the carrier of c9

p9 is Element of the carrier of c9

d19 is Element of the carrier of c9

MOS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of MOS is non empty set

X is Element of the carrier of MOS

MOS is Element of the carrier of MOS

X is Element of the carrier of MOS

p is Element of the carrier of MOS

q is Element of the carrier of MOS

(MOS,X,p) is Element of the carrier of MOS

(MOS,X,q) is Element of the carrier of MOS

MOS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of MOS is non empty set

X is Element of the carrier of MOS

MOS is Element of the carrier of MOS

X is Element of the carrier of MOS

p is Element of the carrier of MOS

q is Element of the carrier of MOS

a is Element of the carrier of MOS

a1 is Element of the carrier of MOS

MOS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of MOS is non empty set

X is Element of the carrier of MOS

MOS is Element of the carrier of MOS

X is Element of the carrier of MOS

p is Element of the carrier of MOS

q is Element of the carrier of MOS

a is Element of the carrier of MOS

a1 is Element of the carrier of MOS

MOS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of MOS is non empty set

X is Element of the carrier of MOS

MOS is Element of the carrier of MOS

X is Element of the carrier of MOS

p is Element of the carrier of MOS

q is Element of the carrier of MOS

(MOS,X,q) is Element of the carrier of MOS

a is Element of the carrier of MOS

(MOS,p,a) is Element of the carrier of MOS

(MOS,X,p) is Element of the carrier of MOS

(MOS,q,a) is Element of the carrier of MOS

(MOS,(MOS,X,q),(MOS,p,a)) is Element of the carrier of MOS

(MOS,(MOS,X,p),(MOS,q,a)) is Element of the carrier of MOS

(MOS,q,X) is Element of the carrier of MOS

(MOS,a,p) is Element of the carrier of MOS

MOS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of MOS is non empty set

X is Element of the carrier of MOS

MOS is Element of the carrier of MOS

X is Element of the carrier of MOS

p is Element of the carrier of MOS

q is Element of the carrier of MOS

(MOS,p,q) is Element of the carrier of MOS

a is Element of the carrier of MOS

(MOS,X,a) is Element of the carrier of MOS

(MOS,X,p) is Element of the carrier of MOS

(MOS,q,a) is Element of the carrier of MOS

(MOS,(MOS,X,a),(MOS,p,q)) is Element of the carrier of MOS

(MOS,(MOS,X,p),(MOS,q,a)) is Element of the carrier of MOS

(MOS,(MOS,p,q),(MOS,X,a)) is Element of the carrier of MOS

(MOS,(MOS,p,q),(MOS,X,a)) is Element of the carrier of MOS

MOS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of MOS is non empty set

X is Element of the carrier of MOS

MOS is Element of the carrier of MOS

X is Element of the carrier of MOS

p is Element of the carrier of MOS

b is Element of the carrier of MOS

(MOS,p,b) is Element of the carrier of MOS

q is Element of the carrier of MOS

b1 is Element of the carrier of MOS

(MOS,q,b1) is Element of the carrier of MOS

a is Element of the carrier of MOS

c is Element of the carrier of MOS

(MOS,a,c) is Element of the carrier of MOS

a1 is Element of the carrier of MOS

c1 is Element of the carrier of MOS

(MOS,a1,c1) is Element of the carrier of MOS

(MOS,p,q) is Element of the carrier of MOS

(MOS,a,a1) is Element of the carrier of MOS

(MOS,b,b1) is Element of the carrier of MOS

(MOS,c,c1) is Element of the carrier of MOS

(MOS,(MOS,a,a1),(MOS,c,c1)) is Element of the carrier of MOS

(MOS,X,X) is Element of the carrier of MOS

(MOS,(MOS,p,q),(MOS,b,b1)) is Element of the carrier of MOS

(MOS,c,c1) - (MOS,b,b1) is Element of the carrier of MOS

- (MOS,b,b1) is Element of the carrier of MOS

K163(MOS,(MOS,c,c1),(- (MOS,b,b1))) is Element of the carrier of MOS

(MOS,a,a1) - (MOS,p,q) is Element of the carrier of MOS

- (MOS,p,q) is Element of the carrier of MOS

K163(MOS,(MOS,a,a1),(- (MOS,p,q))) is Element of the carrier of MOS

- ((MOS,a,a1) - (MOS,p,q)) is Element of the carrier of MOS

(- 1) * ((MOS,a,a1) - (MOS,p,q)) is Element of the carrier of MOS

the Mult of MOS is V1() V4([:REAL, the carrier of MOS:]) V5( the carrier of MOS) V6() V18([:REAL, the carrier of MOS:], the carrier of MOS) Element of bool [:[:REAL, the carrier of MOS:], the carrier of MOS:]

[:REAL, the carrier of MOS:] is set

[:[:REAL, the carrier of MOS:], the carrier of MOS:] is set

bool [:[:REAL, the carrier of MOS:], the carrier of MOS:] is non empty set

the Mult of MOS . ((