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 . ((