:: PARSP_2 semantic presentation

K117() is Element of bool K113()
K113() is set
bool K113() is set
K112() is set
bool K112() is set
bool K117() is set
K27() is V4() set
1 is set
FdSp is non empty right_complementable add-associative right_zeroed addLoopStr
the carrier of FdSp is V4() set
0. FdSp is V46(FdSp) Element of the carrier of FdSp
a is Element of the carrier of FdSp
b is Element of the carrier of FdSp
a - b is Element of the carrier of FdSp
- b is Element of the carrier of FdSp
a + (- b) is Element of the carrier of FdSp
- (- b) is Element of the carrier of FdSp
FdSp is non empty right_complementable add-associative right_zeroed addLoopStr
the carrier of FdSp is V4() set
0. FdSp is V46(FdSp) Element of the carrier of FdSp
a is Element of the carrier of FdSp
b is Element of the carrier of FdSp
- b is Element of the carrier of FdSp
a + (- b) is Element of the carrier of FdSp
a - b is Element of the carrier of FdSp
(- b) + b is Element of the carrier of FdSp
a + ((- b) + b) is Element of the carrier of FdSp
(0. FdSp) + b is Element of the carrier of FdSp
a + (0. FdSp) is Element of the carrier of FdSp
(a + (- b)) + b is Element of the carrier of FdSp
(0. FdSp) + b is Element of the carrier of FdSp
(- b) + b is Element of the carrier of FdSp
a + ((- b) + b) is Element of the carrier of FdSp
a + (0. FdSp) is Element of the carrier of FdSp
b + (- b) is Element of the carrier of FdSp
FdSp is non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed doubleLoopStr
MPS FdSp is non empty strict ParStr
the carrier of (MPS FdSp) is V4() set
a is Element of the carrier of (MPS FdSp)
b is Element of the carrier of (MPS FdSp)
c is Element of the carrier of (MPS FdSp)
d is Element of the carrier of (MPS FdSp)
p is Element of the carrier of (MPS FdSp)
q is Element of the carrier of (MPS FdSp)
p is Element of the carrier of (MPS FdSp)
q is Element of the carrier of (MPS FdSp)
x is Element of the carrier of (MPS FdSp)
y is Element of the carrier of (MPS FdSp)
e is Element of the carrier of (MPS FdSp)
f is Element of the carrier of (MPS FdSp)
g is Element of the carrier of (MPS FdSp)
h is Element of the carrier of (MPS FdSp)
k is Element of the carrier of (MPS FdSp)
l is Element of the carrier of (MPS FdSp)
K is Element of the carrier of (MPS FdSp)
FdSp is non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of FdSp is V4() non trivial set
[: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:] is set
0. FdSp is V46(FdSp) Element of the carrier of FdSp
a is Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
a `1_3 is Element of the carrier of FdSp
a `1 is set
(a `1) `1 is set
a `2_3 is Element of the carrier of FdSp
(a `1) `2 is set
a `3_3 is Element of the carrier of FdSp
b is Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
b `1_3 is Element of the carrier of FdSp
b `1 is set
(b `1) `1 is set
(a `1_3) - (b `1_3) is Element of the carrier of FdSp
b `2_3 is Element of the carrier of FdSp
(b `1) `2 is set
(a `2_3) - (b `2_3) is Element of the carrier of FdSp
b `3_3 is Element of the carrier of FdSp
(a `3_3) - (b `3_3) is Element of the carrier of FdSp
c is Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
c `2_3 is Element of the carrier of FdSp
c `1 is set
(c `1) `2 is set
c `1_3 is Element of the carrier of FdSp
(c `1) `1 is set
c `3_3 is Element of the carrier of FdSp
d is Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
d `2_3 is Element of the carrier of FdSp
d `1 is set
(d `1) `2 is set
(c `2_3) - (d `2_3) is Element of the carrier of FdSp
((a `1_3) - (b `1_3)) * ((c `2_3) - (d `2_3)) is Element of the carrier of FdSp
d `1_3 is Element of the carrier of FdSp
(d `1) `1 is set
(c `1_3) - (d `1_3) is Element of the carrier of FdSp
((c `1_3) - (d `1_3)) * ((a `2_3) - (b `2_3)) is Element of the carrier of FdSp
(((a `1_3) - (b `1_3)) * ((c `2_3) - (d `2_3))) - (((c `1_3) - (d `1_3)) * ((a `2_3) - (b `2_3))) is Element of the carrier of FdSp
d `3_3 is Element of the carrier of FdSp
(c `3_3) - (d `3_3) is Element of the carrier of FdSp
((a `1_3) - (b `1_3)) * ((c `3_3) - (d `3_3)) is Element of the carrier of FdSp
((c `1_3) - (d `1_3)) * ((a `3_3) - (b `3_3)) is Element of the carrier of FdSp
(((a `1_3) - (b `1_3)) * ((c `3_3) - (d `3_3))) - (((c `1_3) - (d `1_3)) * ((a `3_3) - (b `3_3))) is Element of the carrier of FdSp
((a `2_3) - (b `2_3)) * ((c `3_3) - (d `3_3)) is Element of the carrier of FdSp
((c `2_3) - (d `2_3)) * ((a `3_3) - (b `3_3)) is Element of the carrier of FdSp
(((a `2_3) - (b `2_3)) * ((c `3_3) - (d `3_3))) - (((c `2_3) - (d `2_3)) * ((a `3_3) - (b `3_3))) is Element of the carrier of FdSp
((a `3_3) - (b `3_3)) " is Element of the carrier of FdSp
((c `3_3) - (d `3_3)) * (((a `3_3) - (b `3_3)) ") is Element of the carrier of FdSp
(((c `3_3) - (d `3_3)) * (((a `3_3) - (b `3_3)) ")) * ((a `3_3) - (b `3_3)) is Element of the carrier of FdSp
(((a `3_3) - (b `3_3)) ") * ((a `3_3) - (b `3_3)) is Element of the carrier of FdSp
((c `3_3) - (d `3_3)) * ((((a `3_3) - (b `3_3)) ") * ((a `3_3) - (b `3_3))) is Element of the carrier of FdSp
1_ FdSp is Element of the carrier of FdSp
1. FdSp is V46(FdSp) Element of the carrier of FdSp
((c `3_3) - (d `3_3)) * (1_ FdSp) is Element of the carrier of FdSp
(((c `3_3) - (d `3_3)) * (((a `3_3) - (b `3_3)) ")) * ((a `2_3) - (b `2_3)) is Element of the carrier of FdSp
(((a `2_3) - (b `2_3)) * ((c `3_3) - (d `3_3))) * (((a `3_3) - (b `3_3)) ") is Element of the carrier of FdSp
(((c `2_3) - (d `2_3)) * ((a `3_3) - (b `3_3))) * (((a `3_3) - (b `3_3)) ") is Element of the carrier of FdSp
((a `3_3) - (b `3_3)) * (((a `3_3) - (b `3_3)) ") is Element of the carrier of FdSp
((c `2_3) - (d `2_3)) * (((a `3_3) - (b `3_3)) * (((a `3_3) - (b `3_3)) ")) is Element of the carrier of FdSp
((c `2_3) - (d `2_3)) * (1_ FdSp) is Element of the carrier of FdSp
(((c `3_3) - (d `3_3)) * (((a `3_3) - (b `3_3)) ")) * ((a `1_3) - (b `1_3)) is Element of the carrier of FdSp
(((a `1_3) - (b `1_3)) * ((c `3_3) - (d `3_3))) * (((a `3_3) - (b `3_3)) ") is Element of the carrier of FdSp
(((c `1_3) - (d `1_3)) * ((a `3_3) - (b `3_3))) * (((a `3_3) - (b `3_3)) ") is Element of the carrier of FdSp
((c `1_3) - (d `1_3)) * (((a `3_3) - (b `3_3)) * (((a `3_3) - (b `3_3)) ")) is Element of the carrier of FdSp
((c `1_3) - (d `1_3)) * (1_ FdSp) is Element of the carrier of FdSp
((a `2_3) - (b `2_3)) " is Element of the carrier of FdSp
((c `2_3) - (d `2_3)) * (((a `2_3) - (b `2_3)) ") is Element of the carrier of FdSp
(((c `2_3) - (d `2_3)) * (((a `2_3) - (b `2_3)) ")) * ((a `2_3) - (b `2_3)) is Element of the carrier of FdSp
(((a `2_3) - (b `2_3)) ") * ((a `2_3) - (b `2_3)) is Element of the carrier of FdSp
((c `2_3) - (d `2_3)) * ((((a `2_3) - (b `2_3)) ") * ((a `2_3) - (b `2_3))) is Element of the carrier of FdSp
(((c `2_3) - (d `2_3)) * (((a `2_3) - (b `2_3)) ")) * ((a `3_3) - (b `3_3)) is Element of the carrier of FdSp
(((a `2_3) - (b `2_3)) ") * (((c `2_3) - (d `2_3)) * ((a `3_3) - (b `3_3))) is Element of the carrier of FdSp
(((a `2_3) - (b `2_3)) ") * (((a `2_3) - (b `2_3)) * ((c `3_3) - (d `3_3))) is Element of the carrier of FdSp
((((a `2_3) - (b `2_3)) ") * ((a `2_3) - (b `2_3))) * ((c `3_3) - (d `3_3)) is Element of the carrier of FdSp
(((c `2_3) - (d `2_3)) * (((a `2_3) - (b `2_3)) ")) * ((a `1_3) - (b `1_3)) is Element of the carrier of FdSp
(((a `1_3) - (b `1_3)) * ((c `2_3) - (d `2_3))) * (((a `2_3) - (b `2_3)) ") is Element of the carrier of FdSp
(((c `1_3) - (d `1_3)) * ((a `2_3) - (b `2_3))) * (((a `2_3) - (b `2_3)) ") is Element of the carrier of FdSp
((a `2_3) - (b `2_3)) * (((a `2_3) - (b `2_3)) ") is Element of the carrier of FdSp
((c `1_3) - (d `1_3)) * (((a `2_3) - (b `2_3)) * (((a `2_3) - (b `2_3)) ")) is Element of the carrier of FdSp
((a `1_3) - (b `1_3)) " is Element of the carrier of FdSp
((c `1_3) - (d `1_3)) * (((a `1_3) - (b `1_3)) ") is Element of the carrier of FdSp
(((c `1_3) - (d `1_3)) * (((a `1_3) - (b `1_3)) ")) * ((a `1_3) - (b `1_3)) is Element of the carrier of FdSp
(((a `1_3) - (b `1_3)) ") * ((a `1_3) - (b `1_3)) is Element of the carrier of FdSp
((c `1_3) - (d `1_3)) * ((((a `1_3) - (b `1_3)) ") * ((a `1_3) - (b `1_3))) is Element of the carrier of FdSp
(((c `1_3) - (d `1_3)) * (((a `1_3) - (b `1_3)) ")) * ((a `3_3) - (b `3_3)) is Element of the carrier of FdSp
(((a `1_3) - (b `1_3)) ") * (((c `1_3) - (d `1_3)) * ((a `3_3) - (b `3_3))) is Element of the carrier of FdSp
(((a `1_3) - (b `1_3)) ") * (((a `1_3) - (b `1_3)) * ((c `3_3) - (d `3_3))) is Element of the carrier of FdSp
((((a `1_3) - (b `1_3)) ") * ((a `1_3) - (b `1_3))) * ((c `3_3) - (d `3_3)) is Element of the carrier of FdSp
(((c `1_3) - (d `1_3)) * (((a `1_3) - (b `1_3)) ")) * ((a `2_3) - (b `2_3)) is Element of the carrier of FdSp
(((a `1_3) - (b `1_3)) ") * (((c `1_3) - (d `1_3)) * ((a `2_3) - (b `2_3))) is Element of the carrier of FdSp
(((a `1_3) - (b `1_3)) ") * (((a `1_3) - (b `1_3)) * ((c `2_3) - (d `2_3))) is Element of the carrier of FdSp
((((a `1_3) - (b `1_3)) ") * ((a `1_3) - (b `1_3))) * ((c `2_3) - (d `2_3)) is Element of the carrier of FdSp
p is Element of the carrier of FdSp
p * ((a `1_3) - (b `1_3)) is Element of the carrier of FdSp
p * ((a `2_3) - (b `2_3)) is Element of the carrier of FdSp
p * ((a `3_3) - (b `3_3)) is Element of the carrier of FdSp
q is Element of the carrier of FdSp
q * ((a `1_3) - (b `1_3)) is Element of the carrier of FdSp
q * ((a `2_3) - (b `2_3)) is Element of the carrier of FdSp
q * ((a `3_3) - (b `3_3)) is Element of the carrier of FdSp
p is Element of the carrier of FdSp
p * ((a `1_3) - (b `1_3)) is Element of the carrier of FdSp
p * ((a `2_3) - (b `2_3)) is Element of the carrier of FdSp
p * ((a `3_3) - (b `3_3)) is Element of the carrier of FdSp
p is Element of the carrier of FdSp
p * ((a `1_3) - (b `1_3)) is Element of the carrier of FdSp
p * ((a `2_3) - (b `2_3)) is Element of the carrier of FdSp
p * ((a `3_3) - (b `3_3)) is Element of the carrier of FdSp
p is Element of the carrier of FdSp
p * ((a `1_3) - (b `1_3)) is Element of the carrier of FdSp
p * ((a `2_3) - (b `2_3)) is Element of the carrier of FdSp
p * ((a `3_3) - (b `3_3)) is Element of the carrier of FdSp
(p * ((a `2_3) - (b `2_3))) * ((a `3_3) - (b `3_3)) is Element of the carrier of FdSp
((p * ((a `2_3) - (b `2_3))) * ((a `3_3) - (b `3_3))) - ((p * ((a `2_3) - (b `2_3))) * ((a `3_3) - (b `3_3))) is Element of the carrier of FdSp
(p * ((a `1_3) - (b `1_3))) * ((a `2_3) - (b `2_3)) is Element of the carrier of FdSp
((p * ((a `1_3) - (b `1_3))) * ((a `2_3) - (b `2_3))) - ((p * ((a `1_3) - (b `1_3))) * ((a `2_3) - (b `2_3))) is Element of the carrier of FdSp
(p * ((a `1_3) - (b `1_3))) * ((a `3_3) - (b `3_3)) is Element of the carrier of FdSp
((p * ((a `1_3) - (b `1_3))) * ((a `3_3) - (b `3_3))) - ((p * ((a `1_3) - (b `1_3))) * ((a `3_3) - (b `3_3))) is Element of the carrier of FdSp
q is Element of the carrier of FdSp
q * ((a `1_3) - (b `1_3)) is Element of the carrier of FdSp
q * ((a `2_3) - (b `2_3)) is Element of the carrier of FdSp
q * ((a `3_3) - (b `3_3)) is Element of the carrier of FdSp
p is Element of the carrier of FdSp
p * ((a `1_3) - (b `1_3)) is Element of the carrier of FdSp
p * ((a `2_3) - (b `2_3)) is Element of the carrier of FdSp
p * ((a `3_3) - (b `3_3)) is Element of the carrier of FdSp
p is Element of the carrier of FdSp
p * ((a `1_3) - (b `1_3)) is Element of the carrier of FdSp
p * ((a `2_3) - (b `2_3)) is Element of the carrier of FdSp
p * ((a `3_3) - (b `3_3)) is Element of the carrier of FdSp
p is Element of the carrier of FdSp
p * ((a `1_3) - (b `1_3)) is Element of the carrier of FdSp
p * ((a `2_3) - (b `2_3)) is Element of the carrier of FdSp
p * ((a `3_3) - (b `3_3)) is Element of the carrier of FdSp
q is Element of the carrier of FdSp
q * ((a `1_3) - (b `1_3)) is Element of the carrier of FdSp
q * ((a `2_3) - (b `2_3)) is Element of the carrier of FdSp
q * ((a `3_3) - (b `3_3)) is Element of the carrier of FdSp
FdSp is non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed doubleLoopStr
MPS FdSp is non empty strict ParStr
the carrier of (MPS FdSp) is V4() set
the carrier of FdSp is V4() non trivial set
[: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:] is set
0. FdSp is V46(FdSp) Element of the carrier of FdSp
a is Element of the carrier of (MPS FdSp)
b is Element of the carrier of (MPS FdSp)
c is Element of the carrier of (MPS FdSp)
d is Element of the carrier of (MPS FdSp)
[a,b,c,d] is V1() V2() V3() Element of [: the carrier of (MPS FdSp), the carrier of (MPS FdSp), the carrier of (MPS FdSp), the carrier of (MPS FdSp):]
[: the carrier of (MPS FdSp), the carrier of (MPS FdSp), the carrier of (MPS FdSp), the carrier of (MPS FdSp):] is set
[a,b,c] is V1() V2() set
K4(a,b) is V1() set
K4(K4(a,b),c) is V1() set
K4([a,b,c],d) is V1() set
p is Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
q is Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
p is Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
q is Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
[p,q,p,q] is V1() V2() V3() set
[p,q,p] is V1() V2() set
K4(p,q) is V1() set
K4(K4(p,q),p) is V1() set
K4([p,q,p],q) is V1() set
p `1_3 is Element of the carrier of FdSp
p `1 is set
(p `1) `1 is set
q `1_3 is Element of the carrier of FdSp
q `1 is set
(q `1) `1 is set
(p `1_3) - (q `1_3) is Element of the carrier of FdSp
p `2_3 is Element of the carrier of FdSp
p `1 is set
(p `1) `2 is set
q `2_3 is Element of the carrier of FdSp
q `1 is set
(q `1) `2 is set
(p `2_3) - (q `2_3) is Element of the carrier of FdSp
((p `1_3) - (q `1_3)) * ((p `2_3) - (q `2_3)) is Element of the carrier of FdSp
p `1_3 is Element of the carrier of FdSp
(p `1) `1 is set
q `1_3 is Element of the carrier of FdSp
(q `1) `1 is set
(p `1_3) - (q `1_3) is Element of the carrier of FdSp
p `2_3 is Element of the carrier of FdSp
(p `1) `2 is set
q `2_3 is Element of the carrier of FdSp
(q `1) `2 is set
(p `2_3) - (q `2_3) is Element of the carrier of FdSp
((p `1_3) - (q `1_3)) * ((p `2_3) - (q `2_3)) is Element of the carrier of FdSp
(((p `1_3) - (q `1_3)) * ((p `2_3) - (q `2_3))) - (((p `1_3) - (q `1_3)) * ((p `2_3) - (q `2_3))) is Element of the carrier of FdSp
p `3_3 is Element of the carrier of FdSp
q `3_3 is Element of the carrier of FdSp
(p `3_3) - (q `3_3) is Element of the carrier of FdSp
((p `1_3) - (q `1_3)) * ((p `3_3) - (q `3_3)) is Element of the carrier of FdSp
p `3_3 is Element of the carrier of FdSp
q `3_3 is Element of the carrier of FdSp
(p `3_3) - (q `3_3) is Element of the carrier of FdSp
((p `1_3) - (q `1_3)) * ((p `3_3) - (q `3_3)) is Element of the carrier of FdSp
(((p `1_3) - (q `1_3)) * ((p `3_3) - (q `3_3))) - (((p `1_3) - (q `1_3)) * ((p `3_3) - (q `3_3))) is Element of the carrier of FdSp
((p `2_3) - (q `2_3)) * ((p `3_3) - (q `3_3)) is Element of the carrier of FdSp
((p `2_3) - (q `2_3)) * ((p `3_3) - (q `3_3)) is Element of the carrier of FdSp
(((p `2_3) - (q `2_3)) * ((p `3_3) - (q `3_3))) - (((p `2_3) - (q `2_3)) * ((p `3_3) - (q `3_3))) is Element of the carrier of FdSp
x is Element of the carrier of FdSp
x * ((p `1_3) - (q `1_3)) is Element of the carrier of FdSp
x * ((p `2_3) - (q `2_3)) is Element of the carrier of FdSp
x * ((p `3_3) - (q `3_3)) is Element of the carrier of FdSp
p is Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
q is Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
p is Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
q is Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
[p,q,p,q] is V1() V2() V3() set
[p,q,p] is V1() V2() set
K4(p,q) is V1() set
K4(K4(p,q),p) is V1() set
K4([p,q,p],q) is V1() set
p `1_3 is Element of the carrier of FdSp
p `1 is set
(p `1) `1 is set
q `1_3 is Element of the carrier of FdSp
q `1 is set
(q `1) `1 is set
(p `1_3) - (q `1_3) is Element of the carrier of FdSp
p `1_3 is Element of the carrier of FdSp
p `1 is set
(p `1) `1 is set
q `1_3 is Element of the carrier of FdSp
q `1 is set
(q `1) `1 is set
(p `1_3) - (q `1_3) is Element of the carrier of FdSp
p `2_3 is Element of the carrier of FdSp
(p `1) `2 is set
q `2_3 is Element of the carrier of FdSp
(q `1) `2 is set
(p `2_3) - (q `2_3) is Element of the carrier of FdSp
p `2_3 is Element of the carrier of FdSp
(p `1) `2 is set
q `2_3 is Element of the carrier of FdSp
(q `1) `2 is set
(p `2_3) - (q `2_3) is Element of the carrier of FdSp
p `3_3 is Element of the carrier of FdSp
q `3_3 is Element of the carrier of FdSp
(p `3_3) - (q `3_3) is Element of the carrier of FdSp
p `3_3 is Element of the carrier of FdSp
q `3_3 is Element of the carrier of FdSp
(p `3_3) - (q `3_3) is Element of the carrier of FdSp
((p `2_3) - (q `2_3)) * ((p `3_3) - (q `3_3)) is Element of the carrier of FdSp
((p `2_3) - (q `2_3)) * ((p `3_3) - (q `3_3)) is Element of the carrier of FdSp
(((p `2_3) - (q `2_3)) * ((p `3_3) - (q `3_3))) - (((p `2_3) - (q `2_3)) * ((p `3_3) - (q `3_3))) is Element of the carrier of FdSp
x is Element of the carrier of FdSp
x * ((p `1_3) - (q `1_3)) is Element of the carrier of FdSp
x * ((p `2_3) - (q `2_3)) is Element of the carrier of FdSp
x * ((p `3_3) - (q `3_3)) is Element of the carrier of FdSp
((p `1_3) - (q `1_3)) * ((p `2_3) - (q `2_3)) is Element of the carrier of FdSp
((p `1_3) - (q `1_3)) * ((p `2_3) - (q `2_3)) is Element of the carrier of FdSp
(((p `1_3) - (q `1_3)) * ((p `2_3) - (q `2_3))) - (((p `1_3) - (q `1_3)) * ((p `2_3) - (q `2_3))) is Element of the carrier of FdSp
((p `1_3) - (q `1_3)) * ((p `3_3) - (q `3_3)) is Element of the carrier of FdSp
((p `1_3) - (q `1_3)) * ((p `3_3) - (q `3_3)) is Element of the carrier of FdSp
(((p `1_3) - (q `1_3)) * ((p `3_3) - (q `3_3))) - (((p `1_3) - (q `1_3)) * ((p `3_3) - (q `3_3))) is Element of the carrier of FdSp
x is Element of the carrier of FdSp
x * ((p `1_3) - (q `1_3)) is Element of the carrier of FdSp
x * ((p `2_3) - (q `2_3)) is Element of the carrier of FdSp
x * ((p `3_3) - (q `3_3)) is Element of the carrier of FdSp
p is Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
q is Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
p is Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
q is Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
[p,q,p,q] is V1() V2() V3() set
[p,q,p] is V1() V2() set
K4(p,q) is V1() set
K4(K4(p,q),p) is V1() set
K4([p,q,p],q) is V1() set
x is Element of the carrier of FdSp
p `1_3 is Element of the carrier of FdSp
p `1 is set
(p `1) `1 is set
q `1_3 is Element of the carrier of FdSp
q `1 is set
(q `1) `1 is set
(p `1_3) - (q `1_3) is Element of the carrier of FdSp
x * ((p `1_3) - (q `1_3)) is Element of the carrier of FdSp
p `1_3 is Element of the carrier of FdSp
p `1 is set
(p `1) `1 is set
q `1_3 is Element of the carrier of FdSp
q `1 is set
(q `1) `1 is set
(p `1_3) - (q `1_3) is Element of the carrier of FdSp
p `2_3 is Element of the carrier of FdSp
(p `1) `2 is set
q `2_3 is Element of the carrier of FdSp
(q `1) `2 is set
(p `2_3) - (q `2_3) is Element of the carrier of FdSp
x * ((p `2_3) - (q `2_3)) is Element of the carrier of FdSp
p `2_3 is Element of the carrier of FdSp
(p `1) `2 is set
q `2_3 is Element of the carrier of FdSp
(q `1) `2 is set
(p `2_3) - (q `2_3) is Element of the carrier of FdSp
p `3_3 is Element of the carrier of FdSp
q `3_3 is Element of the carrier of FdSp
(p `3_3) - (q `3_3) is Element of the carrier of FdSp
x * ((p `3_3) - (q `3_3)) is Element of the carrier of FdSp
p `3_3 is Element of the carrier of FdSp
q `3_3 is Element of the carrier of FdSp
(p `3_3) - (q `3_3) is Element of the carrier of FdSp
y is Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
e is Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
f is Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
g is Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
[y,e,f,g] is V1() V2() V3() set
[y,e,f] is V1() V2() set
K4(y,e) is V1() set
K4(K4(y,e),f) is V1() set
K4([y,e,f],g) is V1() set
h is Element of the carrier of FdSp
y `1_3 is Element of the carrier of FdSp
y `1 is set
(y `1) `1 is set
e `1_3 is Element of the carrier of FdSp
e `1 is set
(e `1) `1 is set
(y `1_3) - (e `1_3) is Element of the carrier of FdSp
h * ((y `1_3) - (e `1_3)) is Element of the carrier of FdSp
f `1_3 is Element of the carrier of FdSp
f `1 is set
(f `1) `1 is set
g `1_3 is Element of the carrier of FdSp
g `1 is set
(g `1) `1 is set
(f `1_3) - (g `1_3) is Element of the carrier of FdSp
y `2_3 is Element of the carrier of FdSp
(y `1) `2 is set
e `2_3 is Element of the carrier of FdSp
(e `1) `2 is set
(y `2_3) - (e `2_3) is Element of the carrier of FdSp
h * ((y `2_3) - (e `2_3)) is Element of the carrier of FdSp
f `2_3 is Element of the carrier of FdSp
(f `1) `2 is set
g `2_3 is Element of the carrier of FdSp
(g `1) `2 is set
(f `2_3) - (g `2_3) is Element of the carrier of FdSp
y `3_3 is Element of the carrier of FdSp
e `3_3 is Element of the carrier of FdSp
(y `3_3) - (e `3_3) is Element of the carrier of FdSp
h * ((y `3_3) - (e `3_3)) is Element of the carrier of FdSp
f `3_3 is Element of the carrier of FdSp
g `3_3 is Element of the carrier of FdSp
(f `3_3) - (g `3_3) is Element of the carrier of FdSp
FdSp is non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed doubleLoopStr
MPS FdSp is non empty strict ParStr
the carrier of (MPS FdSp) is V4() set
the carrier of FdSp is V4() non trivial set
[: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:] is set
a is Element of the carrier of (MPS FdSp)
b is Element of the carrier of (MPS FdSp)
c is Element of the carrier of (MPS FdSp)
[a,b,a,c] is V1() V2() V3() Element of [: the carrier of (MPS FdSp), the carrier of (MPS FdSp), the carrier of (MPS FdSp), the carrier of (MPS FdSp):]
[: the carrier of (MPS FdSp), the carrier of (MPS FdSp), the carrier of (MPS FdSp), the carrier of (MPS FdSp):] is set
[a,b,a] is V1() V2() set
K4(a,b) is V1() set
K4(K4(a,b),a) is V1() set
K4([a,b,a],c) is V1() set
d is Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
p is Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
q is Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
[d,p,d,q] is V1() V2() V3() set
[d,p,d] is V1() V2() set
K4(d,p) is V1() set
K4(K4(d,p),d) is V1() set
K4([d,p,d],q) is V1() set
0. FdSp is V46(FdSp) Element of the carrier of FdSp
d `1_3 is Element of the carrier of FdSp
d `1 is set
(d `1) `1 is set
p `1_3 is Element of the carrier of FdSp
p `1 is set
(p `1) `1 is set
(d `1_3) - (p `1_3) is Element of the carrier of FdSp
(0. FdSp) * ((d `1_3) - (p `1_3)) is Element of the carrier of FdSp
q `1_3 is Element of the carrier of FdSp
q `1 is set
(q `1) `1 is set
(d `1_3) - (q `1_3) is Element of the carrier of FdSp
d `2_3 is Element of the carrier of FdSp
(d `1) `2 is set
p `2_3 is Element of the carrier of FdSp
(p `1) `2 is set
(d `2_3) - (p `2_3) is Element of the carrier of FdSp
(0. FdSp) * ((d `2_3) - (p `2_3)) is Element of the carrier of FdSp
q `2_3 is Element of the carrier of FdSp
(q `1) `2 is set
(d `2_3) - (q `2_3) is Element of the carrier of FdSp
d `3_3 is Element of the carrier of FdSp
p `3_3 is Element of the carrier of FdSp
(d `3_3) - (p `3_3) is Element of the carrier of FdSp
(0. FdSp) * ((d `3_3) - (p `3_3)) is Element of the carrier of FdSp
q `3_3 is Element of the carrier of FdSp
(d `3_3) - (q `3_3) is Element of the carrier of FdSp
1_ FdSp is Element of the carrier of FdSp
1. FdSp is V46(FdSp) Element of the carrier of FdSp
((d `1_3) - (p `1_3)) * (1_ FdSp) is Element of the carrier of FdSp
((d `2_3) - (p `2_3)) * (1_ FdSp) is Element of the carrier of FdSp
((d `3_3) - (p `3_3)) * (1_ FdSp) is Element of the carrier of FdSp
FdSp is non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed doubleLoopStr
MPS FdSp is non empty strict ParStr
the carrier of (MPS FdSp) is V4() set
the carrier of FdSp is V4() non trivial set
[: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:] is set
0. FdSp is V46(FdSp) Element of the carrier of FdSp
a is Element of the carrier of (MPS FdSp)
b is Element of the carrier of (MPS FdSp)
c is Element of the carrier of (MPS FdSp)
[a,b,a,c] is V1() V2() V3() Element of [: the carrier of (MPS FdSp), the carrier of (MPS FdSp), the carrier of (MPS FdSp), the carrier of (MPS FdSp):]
[: the carrier of (MPS FdSp), the carrier of (MPS FdSp), the carrier of (MPS FdSp), the carrier of (MPS FdSp):] is set
[a,b,a] is V1() V2() set
K4(a,b) is V1() set
K4(K4(a,b),a) is V1() set
K4([a,b,a],c) is V1() set
d is Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
d `1_3 is Element of the carrier of FdSp
d `1 is set
(d `1) `1 is set
d `2_3 is Element of the carrier of FdSp
(d `1) `2 is set
d `3_3 is Element of the carrier of FdSp
p is Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
p `1_3 is Element of the carrier of FdSp
p `1 is set
(p `1) `1 is set
(d `1_3) - (p `1_3) is Element of the carrier of FdSp
p `2_3 is Element of the carrier of FdSp
(p `1) `2 is set
(d `2_3) - (p `2_3) is Element of the carrier of FdSp
p `3_3 is Element of the carrier of FdSp
(d `3_3) - (p `3_3) is Element of the carrier of FdSp
q is Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
[d,p,d,q] is V1() V2() V3() set
[d,p,d] is V1() V2() set
K4(d,p) is V1() set
K4(K4(d,p),d) is V1() set
K4([d,p,d],q) is V1() set
q `1_3 is Element of the carrier of FdSp
q `1 is set
(q `1) `1 is set
(d `1_3) - (q `1_3) is Element of the carrier of FdSp
q `2_3 is Element of the carrier of FdSp
(q `1) `2 is set
(d `2_3) - (q `2_3) is Element of the carrier of FdSp
q `3_3 is Element of the carrier of FdSp
(d `3_3) - (q `3_3) is Element of the carrier of FdSp
p is Element of the carrier of FdSp
p * ((d `1_3) - (p `1_3)) is Element of the carrier of FdSp
p * ((d `2_3) - (p `2_3)) is Element of the carrier of FdSp
p * ((d `3_3) - (p `3_3)) is Element of the carrier of FdSp
q is Element of the carrier of FdSp
q * ((d `1_3) - (q `1_3)) is Element of the carrier of FdSp
q * ((d `2_3) - (q `2_3)) is Element of the carrier of FdSp
q * ((d `3_3) - (q `3_3)) is Element of the carrier of FdSp
[(d `1_3),(d `2_3),(d `3_3)] is V1() V2() Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
K4((d `1_3),(d `2_3)) is V1() set
K4(K4((d `1_3),(d `2_3)),(d `3_3)) is V1() set
[(q `1_3),(q `2_3),(q `3_3)] is V1() V2() Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
K4((q `1_3),(q `2_3)) is V1() set
K4(K4((q `1_3),(q `2_3)),(q `3_3)) is V1() set
(p * ((d `1_3) - (p `1_3))) * ((d `2_3) - (q `2_3)) is Element of the carrier of FdSp
((d `1_3) - (q `1_3)) * ((d `2_3) - (q `2_3)) is Element of the carrier of FdSp
q * (((d `1_3) - (q `1_3)) * ((d `2_3) - (q `2_3))) is Element of the carrier of FdSp
(p * ((d `2_3) - (p `2_3))) * ((d `1_3) - (q `1_3)) is Element of the carrier of FdSp
((d `2_3) - (q `2_3)) * ((d `1_3) - (q `1_3)) is Element of the carrier of FdSp
q * (((d `2_3) - (q `2_3)) * ((d `1_3) - (q `1_3))) is Element of the carrier of FdSp
((p * ((d `1_3) - (p `1_3))) * ((d `2_3) - (q `2_3))) - ((p * ((d `2_3) - (p `2_3))) * ((d `1_3) - (q `1_3))) is Element of the carrier of FdSp
((d `1_3) - (p `1_3)) * ((d `2_3) - (q `2_3)) is Element of the carrier of FdSp
p * (((d `1_3) - (p `1_3)) * ((d `2_3) - (q `2_3))) is Element of the carrier of FdSp
(p * (((d `1_3) - (p `1_3)) * ((d `2_3) - (q `2_3)))) - ((p * ((d `2_3) - (p `2_3))) * ((d `1_3) - (q `1_3))) is Element of the carrier of FdSp
((d `2_3) - (p `2_3)) * ((d `1_3) - (q `1_3)) is Element of the carrier of FdSp
p * (((d `2_3) - (p `2_3)) * ((d `1_3) - (q `1_3))) is Element of the carrier of FdSp
(p * (((d `1_3) - (p `1_3)) * ((d `2_3) - (q `2_3)))) - (p * (((d `2_3) - (p `2_3)) * ((d `1_3) - (q `1_3)))) is Element of the carrier of FdSp
((d `1_3) - (q `1_3)) * ((d `2_3) - (p `2_3)) is Element of the carrier of FdSp
(((d `1_3) - (p `1_3)) * ((d `2_3) - (q `2_3))) - (((d `1_3) - (q `1_3)) * ((d `2_3) - (p `2_3))) is Element of the carrier of FdSp
p * ((((d `1_3) - (p `1_3)) * ((d `2_3) - (q `2_3))) - (((d `1_3) - (q `1_3)) * ((d `2_3) - (p `2_3)))) is Element of the carrier of FdSp
(p * ((d `1_3) - (p `1_3))) * ((d `3_3) - (q `3_3)) is Element of the carrier of FdSp
((d `1_3) - (q `1_3)) * ((d `3_3) - (q `3_3)) is Element of the carrier of FdSp
q * (((d `1_3) - (q `1_3)) * ((d `3_3) - (q `3_3))) is Element of the carrier of FdSp
(p * ((d `3_3) - (p `3_3))) * ((d `1_3) - (q `1_3)) is Element of the carrier of FdSp
((d `3_3) - (q `3_3)) * ((d `1_3) - (q `1_3)) is Element of the carrier of FdSp
q * (((d `3_3) - (q `3_3)) * ((d `1_3) - (q `1_3))) is Element of the carrier of FdSp
((p * ((d `1_3) - (p `1_3))) * ((d `3_3) - (q `3_3))) - ((p * ((d `3_3) - (p `3_3))) * ((d `1_3) - (q `1_3))) is Element of the carrier of FdSp
((d `1_3) - (p `1_3)) * ((d `3_3) - (q `3_3)) is Element of the carrier of FdSp
p * (((d `1_3) - (p `1_3)) * ((d `3_3) - (q `3_3))) is Element of the carrier of FdSp
(p * (((d `1_3) - (p `1_3)) * ((d `3_3) - (q `3_3)))) - ((p * ((d `3_3) - (p `3_3))) * ((d `1_3) - (q `1_3))) is Element of the carrier of FdSp
((d `3_3) - (p `3_3)) * ((d `1_3) - (q `1_3)) is Element of the carrier of FdSp
p * (((d `3_3) - (p `3_3)) * ((d `1_3) - (q `1_3))) is Element of the carrier of FdSp
(p * (((d `1_3) - (p `1_3)) * ((d `3_3) - (q `3_3)))) - (p * (((d `3_3) - (p `3_3)) * ((d `1_3) - (q `1_3)))) is Element of the carrier of FdSp
((d `1_3) - (q `1_3)) * ((d `3_3) - (p `3_3)) is Element of the carrier of FdSp
(((d `1_3) - (p `1_3)) * ((d `3_3) - (q `3_3))) - (((d `1_3) - (q `1_3)) * ((d `3_3) - (p `3_3))) is Element of the carrier of FdSp
p * ((((d `1_3) - (p `1_3)) * ((d `3_3) - (q `3_3))) - (((d `1_3) - (q `1_3)) * ((d `3_3) - (p `3_3)))) is Element of the carrier of FdSp
(p * ((d `2_3) - (p `2_3))) * ((d `3_3) - (q `3_3)) is Element of the carrier of FdSp
((d `2_3) - (q `2_3)) * ((d `3_3) - (q `3_3)) is Element of the carrier of FdSp
q * (((d `2_3) - (q `2_3)) * ((d `3_3) - (q `3_3))) is Element of the carrier of FdSp
(p * ((d `3_3) - (p `3_3))) * ((d `2_3) - (q `2_3)) is Element of the carrier of FdSp
((d `3_3) - (q `3_3)) * ((d `2_3) - (q `2_3)) is Element of the carrier of FdSp
q * (((d `3_3) - (q `3_3)) * ((d `2_3) - (q `2_3))) is Element of the carrier of FdSp
((p * ((d `2_3) - (p `2_3))) * ((d `3_3) - (q `3_3))) - ((p * ((d `3_3) - (p `3_3))) * ((d `2_3) - (q `2_3))) is Element of the carrier of FdSp
((d `2_3) - (p `2_3)) * ((d `3_3) - (q `3_3)) is Element of the carrier of FdSp
p * (((d `2_3) - (p `2_3)) * ((d `3_3) - (q `3_3))) is Element of the carrier of FdSp
(p * (((d `2_3) - (p `2_3)) * ((d `3_3) - (q `3_3)))) - ((p * ((d `3_3) - (p `3_3))) * ((d `2_3) - (q `2_3))) is Element of the carrier of FdSp
((d `3_3) - (p `3_3)) * ((d `2_3) - (q `2_3)) is Element of the carrier of FdSp
p * (((d `3_3) - (p `3_3)) * ((d `2_3) - (q `2_3))) is Element of the carrier of FdSp
(p * (((d `2_3) - (p `2_3)) * ((d `3_3) - (q `3_3)))) - (p * (((d `3_3) - (p `3_3)) * ((d `2_3) - (q `2_3)))) is Element of the carrier of FdSp
((d `2_3) - (q `2_3)) * ((d `3_3) - (p `3_3)) is Element of the carrier of FdSp
(((d `2_3) - (p `2_3)) * ((d `3_3) - (q `3_3))) - (((d `2_3) - (q `2_3)) * ((d `3_3) - (p `3_3))) is Element of the carrier of FdSp
p * ((((d `2_3) - (p `2_3)) * ((d `3_3) - (q `3_3))) - (((d `2_3) - (q `2_3)) * ((d `3_3) - (p `3_3)))) is Element of the carrier of FdSp
FdSp is non empty right_complementable add-associative right_zeroed addLoopStr
the carrier of FdSp is V4() set
b is Element of the carrier of FdSp
a is Element of the carrier of FdSp
b + a is Element of the carrier of FdSp
c is Element of the carrier of FdSp
c + a is Element of the carrier of FdSp
(b + a) - (c + a) is Element of the carrier of FdSp
b - c is Element of the carrier of FdSp
- (c + a) is Element of the carrier of FdSp
(b + a) + (- (c + a)) is Element of the carrier of FdSp
- a is Element of the carrier of FdSp
- c is Element of the carrier of FdSp
(- a) + (- c) is Element of the carrier of FdSp
(b + a) + ((- a) + (- c)) is Element of the carrier of FdSp
(b + a) + (- a) is Element of the carrier of FdSp
((b + a) + (- a)) + (- c) is Element of the carrier of FdSp
a + (- a) is Element of the carrier of FdSp
b + (a + (- a)) is Element of the carrier of FdSp
(b + (a + (- a))) + (- c) is Element of the carrier of FdSp
0. FdSp is V46(FdSp) Element of the carrier of FdSp
b + (0. FdSp) is Element of the carrier of FdSp
(b + (0. FdSp)) + (- c) is Element of the carrier of FdSp
b + (- c) is Element of the carrier of FdSp
FdSp is non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of FdSp is V4() non trivial set
a is Element of the carrier of FdSp
b is Element of the carrier of FdSp
a - b is Element of the carrier of FdSp
c is Element of the carrier of FdSp
c - b is Element of the carrier of FdSp
(a - b) - (c - b) is Element of the carrier of FdSp
a - c is Element of the carrier of FdSp
- b is Element of the carrier of FdSp
a + (- b) is Element of the carrier of FdSp
(a + (- b)) - (c - b) is Element of the carrier of FdSp
(- b) + a is Element of the carrier of FdSp
c + (- b) is Element of the carrier of FdSp
((- b) + a) - (c + (- b)) is Element of the carrier of FdSp
FdSp is non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of FdSp is V4() non trivial set
1_ FdSp is Element of the carrier of FdSp
1. FdSp is V46(FdSp) Element of the carrier of FdSp
- (1_ FdSp) is Element of the carrier of FdSp
a is Element of the carrier of FdSp
a + (- (1_ FdSp)) is Element of the carrier of FdSp
b is Element of the carrier of FdSp
c is Element of the carrier of FdSp
b - c is Element of the carrier of FdSp
a * (b - c) is Element of the carrier of FdSp
(a + (- (1_ FdSp))) * (b - c) is Element of the carrier of FdSp
d is Element of the carrier of FdSp
d + (- (1_ FdSp)) is Element of the carrier of FdSp
p is Element of the carrier of FdSp
b - p is Element of the carrier of FdSp
d * (b - p) is Element of the carrier of FdSp
(a * (b - c)) - (d * (b - p)) is Element of the carrier of FdSp
p - c is Element of the carrier of FdSp
(d + (- (1_ FdSp))) * (b - p) is Element of the carrier of FdSp
- c is Element of the carrier of FdSp
p + (- c) is Element of the carrier of FdSp
0. FdSp is V46(FdSp) Element of the carrier of FdSp
(p + (- c)) + (0. FdSp) is Element of the carrier of FdSp
(- c) + p is Element of the carrier of FdSp
- b is Element of the carrier of FdSp
(- b) + b is Element of the carrier of FdSp
((- c) + p) + ((- b) + b) is Element of the carrier of FdSp
((- b) + b) + (- c) is Element of the carrier of FdSp
p + (((- b) + b) + (- c)) is Element of the carrier of FdSp
b + (- c) is Element of the carrier of FdSp
(- b) + (b + (- c)) is Element of the carrier of FdSp
p + ((- b) + (b + (- c))) is Element of the carrier of FdSp
(- b) + (b - c) is Element of the carrier of FdSp
p + ((- b) + (b - c)) is Element of the carrier of FdSp
p + (- b) is Element of the carrier of FdSp
(p + (- b)) + (b - c) is Element of the carrier of FdSp
p - b is Element of the carrier of FdSp
(p - b) + (b - c) is Element of the carrier of FdSp
- (d * (b - p)) is Element of the carrier of FdSp
(a * (b - c)) + (- (d * (b - p))) is Element of the carrier of FdSp
((a * (b - c)) + (- (d * (b - p)))) + (d * (b - p)) is Element of the carrier of FdSp
((p - b) + (b - c)) + (d * (b - p)) is Element of the carrier of FdSp
(- (d * (b - p))) + (d * (b - p)) is Element of the carrier of FdSp
(a * (b - c)) + ((- (d * (b - p))) + (d * (b - p))) is Element of the carrier of FdSp
(a * (b - c)) + (0. FdSp) is Element of the carrier of FdSp
(p - b) + (d * (b - p)) is Element of the carrier of FdSp
((p - b) + (d * (b - p))) + (b - c) is Element of the carrier of FdSp
- (b - c) is Element of the carrier of FdSp
(a * (b - c)) + (- (b - c)) is Element of the carrier of FdSp
(b - c) + (- (b - c)) is Element of the carrier of FdSp
((p - b) + (d * (b - p))) + ((b - c) + (- (b - c))) is Element of the carrier of FdSp
((p - b) + (d * (b - p))) + (0. FdSp) is Element of the carrier of FdSp
(p + (- b)) + (d * (b - p)) is Element of the carrier of FdSp
- (b - p) is Element of the carrier of FdSp
(d * (b - p)) + (- (b - p)) is Element of the carrier of FdSp
(1_ FdSp) * (b - c) is Element of the carrier of FdSp
- ((1_ FdSp) * (b - c)) is Element of the carrier of FdSp
(a * (b - c)) + (- ((1_ FdSp) * (b - c))) is Element of the carrier of FdSp
(- (1_ FdSp)) * (b - c) is Element of the carrier of FdSp
(a * (b - c)) + ((- (1_ FdSp)) * (b - c)) is Element of the carrier of FdSp
(1_ FdSp) * (b - p) is Element of the carrier of FdSp
- ((1_ FdSp) * (b - p)) is Element of the carrier of FdSp
(d * (b - p)) + (- ((1_ FdSp) * (b - p))) is Element of the carrier of FdSp
(- (1_ FdSp)) * (b - p) is Element of the carrier of FdSp
(d * (b - p)) + ((- (1_ FdSp)) * (b - p)) is Element of the carrier of FdSp
FdSp is non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of FdSp is V4() non trivial set
a is Element of the carrier of FdSp
b is Element of the carrier of FdSp
a - b is Element of the carrier of FdSp
c is Element of the carrier of FdSp
b + c is Element of the carrier of FdSp
(b + c) - a is Element of the carrier of FdSp
d is Element of the carrier of FdSp
c - d is Element of the carrier of FdSp
- b is Element of the carrier of FdSp
a + (- b) is Element of the carrier of FdSp
d + (a + (- b)) is Element of the carrier of FdSp
d + (c - d) is Element of the carrier of FdSp
- d is Element of the carrier of FdSp
c + (- d) is Element of the carrier of FdSp
d + (c + (- d)) is Element of the carrier of FdSp
d + a is Element of the carrier of FdSp
(d + a) + (- b) is Element of the carrier of FdSp
d + c is Element of the carrier of FdSp
(d + c) + (- d) is Element of the carrier of FdSp
(d + a) - b is Element of the carrier of FdSp
c + d is Element of the carrier of FdSp
(c + d) + (- d) is Element of the carrier of FdSp
d + (- d) is Element of the carrier of FdSp
c + (d + (- d)) is Element of the carrier of FdSp
0. FdSp is V46(FdSp) Element of the carrier of FdSp
c + (0. FdSp) is Element of the carrier of FdSp
((d + a) - b) + b is Element of the carrier of FdSp
c + b is Element of the carrier of FdSp
((d + a) + (- b)) + b is Element of the carrier of FdSp
(- b) + b is Element of the carrier of FdSp
(d + a) + ((- b) + b) is Element of the carrier of FdSp
(d + a) + (0. FdSp) is Element of the carrier of FdSp
- a is Element of the carrier of FdSp
(d + a) + (- a) is Element of the carrier of FdSp
(b + c) + (- a) is Element of the carrier of FdSp
a + (- a) is Element of the carrier of FdSp
d + (a + (- a)) is Element of the carrier of FdSp
d + (0. FdSp) is Element of the carrier of FdSp
FdSp is non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed doubleLoopStr
MPS FdSp is non empty strict ParStr
the carrier of (MPS FdSp) is V4() set
the carrier of FdSp is V4() non trivial set
[: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:] is set
a is Element of the carrier of (MPS FdSp)
b is Element of the carrier of (MPS FdSp)
c is Element of the carrier of (MPS FdSp)
d is Element of the carrier of (MPS FdSp)
[a,b,c,d] is V1() V2() V3() Element of [: the carrier of (MPS FdSp), the carrier of (MPS FdSp), the carrier of (MPS FdSp), the carrier of (MPS FdSp):]
[: the carrier of (MPS FdSp), the carrier of (MPS FdSp), the carrier of (MPS FdSp), the carrier of (MPS FdSp):] is set
[a,b,c] is V1() V2() set
K4(a,b) is V1() set
K4(K4(a,b),c) is V1() set
K4([a,b,c],d) is V1() set
p is Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
p `1_3 is Element of the carrier of FdSp
p `1 is set
(p `1) `1 is set
p `2_3 is Element of the carrier of FdSp
(p `1) `2 is set
p `3_3 is Element of the carrier of FdSp
q is Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
q `1_3 is Element of the carrier of FdSp
q `1 is set
(q `1) `1 is set
q `2_3 is Element of the carrier of FdSp
(q `1) `2 is set
q `3_3 is Element of the carrier of FdSp
p is Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
p `1_3 is Element of the carrier of FdSp
p `1 is set
(p `1) `1 is set
(q `1_3) + (p `1_3) is Element of the carrier of FdSp
((q `1_3) + (p `1_3)) - (p `1_3) is Element of the carrier of FdSp
p `2_3 is Element of the carrier of FdSp
(p `1) `2 is set
(q `2_3) + (p `2_3) is Element of the carrier of FdSp
((q `2_3) + (p `2_3)) - (p `2_3) is Element of the carrier of FdSp
p `3_3 is Element of the carrier of FdSp
(q `3_3) + (p `3_3) is Element of the carrier of FdSp
((q `3_3) + (p `3_3)) - (p `3_3) is Element of the carrier of FdSp
q is Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
[p,q,p,q] is V1() V2() V3() set
[p,q,p] is V1() V2() set
K4(p,q) is V1() set
K4(K4(p,q),p) is V1() set
K4([p,q,p],q) is V1() set
q `1_3 is Element of the carrier of FdSp
q `1 is set
(q `1) `1 is set
q `2_3 is Element of the carrier of FdSp
(q `1) `2 is set
q `3_3 is Element of the carrier of FdSp
[(p `1_3),(p `2_3),(p `3_3)] is V1() V2() Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
K4((p `1_3),(p `2_3)) is V1() set
K4(K4((p `1_3),(p `2_3)),(p `3_3)) is V1() set
[a,c,b,d] is V1() V2() V3() Element of [: the carrier of (MPS FdSp), the carrier of (MPS FdSp), the carrier of (MPS FdSp), the carrier of (MPS FdSp):]
[a,c,b] is V1() V2() set
K4(a,c) is V1() set
K4(K4(a,c),b) is V1() set
K4([a,c,b],d) is V1() set
0. FdSp is V46(FdSp) Element of the carrier of FdSp
x is Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
y is Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
e is Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
f is Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
[x,y,e,f] is V1() V2() V3() set
[x,y,e] is V1() V2() set
K4(x,y) is V1() set
K4(K4(x,y),e) is V1() set
K4([x,y,e],f) is V1() set
x `1_3 is Element of the carrier of FdSp
x `1 is set
(x `1) `1 is set
y `1_3 is Element of the carrier of FdSp
y `1 is set
(y `1) `1 is set
(x `1_3) - (y `1_3) is Element of the carrier of FdSp
e `1_3 is Element of the carrier of FdSp
e `1 is set
(e `1) `1 is set
f `1_3 is Element of the carrier of FdSp
f `1 is set
(f `1) `1 is set
(e `1_3) - (f `1_3) is Element of the carrier of FdSp
x `2_3 is Element of the carrier of FdSp
(x `1) `2 is set
y `2_3 is Element of the carrier of FdSp
(y `1) `2 is set
(x `2_3) - (y `2_3) is Element of the carrier of FdSp
e `2_3 is Element of the carrier of FdSp
(e `1) `2 is set
f `2_3 is Element of the carrier of FdSp
(f `1) `2 is set
(e `2_3) - (f `2_3) is Element of the carrier of FdSp
x `3_3 is Element of the carrier of FdSp
y `3_3 is Element of the carrier of FdSp
(x `3_3) - (y `3_3) is Element of the carrier of FdSp
e `3_3 is Element of the carrier of FdSp
f `3_3 is Element of the carrier of FdSp
(e `3_3) - (f `3_3) is Element of the carrier of FdSp
[a,b,a,c] is V1() V2() V3() Element of [: the carrier of (MPS FdSp), the carrier of (MPS FdSp), the carrier of (MPS FdSp), the carrier of (MPS FdSp):]
[a,b,a] is V1() V2() set
K4(K4(a,b),a) is V1() set
K4([a,b,a],c) is V1() set
[p,q,p,p] is V1() V2() V3() set
[p,q,p] is V1() V2() set
K4(K4(p,q),p) is V1() set
K4([p,q,p],p) is V1() set
g is Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
h is Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
k is Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
l is Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
[g,h,k,l] is V1() V2() V3() set
[g,h,k] is V1() V2() set
K4(g,h) is V1() set
K4(K4(g,h),k) is V1() set
K4([g,h,k],l) is V1() set
g `1_3 is Element of the carrier of FdSp
g `1 is set
(g `1) `1 is set
h `1_3 is Element of the carrier of FdSp
h `1 is set
(h `1) `1 is set
(g `1_3) - (h `1_3) is Element of the carrier of FdSp
k `1_3 is Element of the carrier of FdSp
k `1 is set
(k `1) `1 is set
l `1_3 is Element of the carrier of FdSp
l `1 is set
(l `1) `1 is set
(k `1_3) - (l `1_3) is Element of the carrier of FdSp
g `2_3 is Element of the carrier of FdSp
(g `1) `2 is set
h `2_3 is Element of the carrier of FdSp
(h `1) `2 is set
(g `2_3) - (h `2_3) is Element of the carrier of FdSp
k `2_3 is Element of the carrier of FdSp
(k `1) `2 is set
l `2_3 is Element of the carrier of FdSp
(l `1) `2 is set
(k `2_3) - (l `2_3) is Element of the carrier of FdSp
g `3_3 is Element of the carrier of FdSp
h `3_3 is Element of the carrier of FdSp
(g `3_3) - (h `3_3) is Element of the carrier of FdSp
k `3_3 is Element of the carrier of FdSp
l `3_3 is Element of the carrier of FdSp
(k `3_3) - (l `3_3) is Element of the carrier of FdSp
[(q `1_3),(q `2_3),(q `3_3)] is V1() V2() Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
K4((q `1_3),(q `2_3)) is V1() set
K4(K4((q `1_3),(q `2_3)),(q `3_3)) is V1() set
(p `1_3) - (q `1_3) is Element of the carrier of FdSp
(p `1_3) - (q `1_3) is Element of the carrier of FdSp
(p `2_3) - (q `2_3) is Element of the carrier of FdSp
(p `2_3) - (q `2_3) is Element of the carrier of FdSp
(p `3_3) - (q `3_3) is Element of the carrier of FdSp
(p `3_3) - (q `3_3) is Element of the carrier of FdSp
K is Element of the carrier of FdSp
K * ((g `1_3) - (h `1_3)) is Element of the carrier of FdSp
K * ((g `2_3) - (h `2_3)) is Element of the carrier of FdSp
K * ((g `3_3) - (h `3_3)) is Element of the carrier of FdSp
K is Element of the carrier of FdSp
K * ((p `1_3) - (q `1_3)) is Element of the carrier of FdSp
K * ((p `2_3) - (q `2_3)) is Element of the carrier of FdSp
K * ((p `3_3) - (q `3_3)) is Element of the carrier of FdSp
[(p `1_3),(p `2_3),(p `3_3)] is V1() V2() Element of [: the carrier of FdSp, the carrier of FdSp, the carrier of FdSp:]
K4((p `1_3),(p `2_3)) is V1() set
K4(K4((p `1_3),(p `2_3)),(p `3_3)) is V1() set
(p `1_3) - (p `1_3) is Element of the carrier of FdSp
(q `1_3) - (q `1_3) is Element of the carrier of FdSp
(p `2_3) - (p `2_3) is Element of the carrier of FdSp
(q `2_3) - (q `2_3) is Element of the carrier of FdSp
(p `3_3) - (p `3_3) is Element of the carrier of FdSp
(q `3_3) - (q `3_3) is Element of the carrier of FdSp
L is Element of the carrier of FdSp
L * ((x `1_3) - (y `1_3)) is Element of the carrier of FdSp
L * ((x `2_3) - (y `2_3)) is Element of the carrier of FdSp
L * ((x `3_3) - (y `3_3)) is Element of the carrier of FdSp
L is Element of the carrier of FdSp
L * ((p `1_3) - (p `1_3)) is Element of the carrier of FdSp
L * ((p `2_3) - (p `2_3)) is Element of the carrier of FdSp
L * ((p `3_3) - (p `3_3)) is Element of the carrier of FdSp
(K * ((p `2_3) - (q `2_3))) - (L * ((p `2_3) - (p `2_3))) is Element of the carrier of FdSp
(p `2_3) - (q `2_3) is Element of the carrier of FdSp
1_ FdSp is Element of the carrier of FdSp
1. FdSp is V46(FdSp) Element of the carrier of FdSp
- (1_ FdSp) is Element of the carrier of FdSp
K + (- (1_ FdSp)) is Element of the carrier of FdSp
(K + (- (1_ FdSp))) * ((p `2_3) - (q `2_3)) is Element of the carrier of FdSp
L + (- (1_ FdSp)) is Element of the carrier of FdSp
(L + (- (1_ FdSp))) * ((p `2_3) - (p `2_3)) is Element of the carrier of FdSp
(K * ((p `3_3) - (q `3_3))) - (L * ((p `3_3) - (p `3_3))) is Element of the carrier of FdSp
(p `3_3) - (q `3_3) is Element of the carrier of FdSp
(K + (- (1_ FdSp))) * ((p `3_3) - (q `3_3)) is Element of the carrier of FdSp
(L + (- (1_ FdSp))) * ((p `3_3) - (p `3_3)) is Element of the carrier of FdSp
(K * ((p `1_3) - (q `1_3))) - (L * ((p `1_3) - (p `1_3))) is Element of the carrier of FdSp
(p `1_3) - (q `1_3) is Element of the carrier of FdSp
(K + (- (1_ FdSp))) * ((p `1_3) - (q `1_3)) is Element of the carrier of FdSp
(L + (- (1_ FdSp))) * ((p `1_3) - (p `1_3)) is Element of the carrier of FdSp
((p `2_3) - (q `2_3)) * (1_ FdSp) is Element of the carrier of FdSp
((p `3_3) - (q `3_3)) * (1_ FdSp) is Element of the carrier of FdSp
((p `1_3) - (q `1_3)) * (1_ FdSp) is Element of the carrier of FdSp
FdSp is non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of FdSp is V4() non trivial set
1_ FdSp is Element of the carrier of FdSp
1. FdSp is V46(FdSp) Element of the carrier of FdSp
a is Element of the carrier of FdSp
a - (1_ FdSp) is Element of the carrier of FdSp
a + (1_ FdSp) is Element of the carrier of FdSp
b is Element of the carrier of FdSp
a * b is Element of the carrier of FdSp
(a - (1_ FdSp)) * b is Element of the carrier of FdSp
c is Element of the carrier of FdSp
a * c is Element of the carrier of FdSp
(a * b) - (a * c) is Element of the carrier of FdSp
c + b is Element of the carrier of FdSp
(a + (1_ FdSp)) * c is Element of the carrier of FdSp
- (a * c) is Element of the carrier of FdSp
(a * b) + (- (a * c)) is Element of the carrier of FdSp
- b is Element of the carrier of FdSp
((a * b) + (- (a * c))) + (- b) is Element of the carrier of FdSp
(c + b) + (- b) is Element of the carrier of FdSp
b + (- b) is Element of the carrier of FdSp
c + (b + (- b)) is Element of the carrier of FdSp
0. FdSp is V46(FdSp) Element of the carrier of FdSp
c + (0. FdSp) is Element of the carrier of FdSp
(a * b) + (- b) is Element of the carrier of FdSp
((a * b) + (- b)) + (- (a * c)) is Element of the carrier of FdSp
(1_ FdSp) * b is Element of the carrier of FdSp
- ((1_ FdSp) * b) is Element of the carrier of FdSp
(a * b) + (- ((1_ FdSp) * b)) is Element of the carrier of FdSp
((a * b) + (- ((1_ FdSp) * b))) + (- (a * c)) is Element of the carrier of FdSp
- (1_ FdSp) is Element of the carrier of FdSp
(- (1_ FdSp)) * b is Element of the carrier of FdSp
(a * b) + ((- (1_ FdSp)) * b) is Element of the carrier of FdSp
((a * b) + ((- (1_ FdSp)) * b)) + (- (a * c)) is Element of the carrier of FdSp
a + (- (1_ FdSp)) is Element of the carrier of FdSp
(a + (- (1_ FdSp))) * b is Element of the carrier of FdSp
((a + (- (1_ FdSp))) * b) + (- (a * c)) is Element of the carrier of FdSp
((a - (1_ FdSp)) * b) + (- (a * c)) is Element of the carrier of FdSp
(((a - (1_ FdSp)) * b) + (- (a * c))) + (a * c) is Element of the carrier of FdSp
c + (a * c) is Element of the carrier of FdSp
(- (a * c)) + (a * c) is Element of the carrier of FdSp
((a - (1_ FdSp)) * b) + ((- (a * c)) + (a * c)) is Element of the carrier of FdSp
((a - (1_ FdSp)) * b) + (0. FdSp) is Element of the carrier of FdSp
(a * c) + c is Element of the carrier of FdSp
(1_ FdSp) * c is Element of the carrier of FdSp
(a * c) + ((1_ FdSp) * c) is Element of the carrier of FdSp
FdSp is non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of FdSp is V4() non trivial set
1_ FdSp is Element of the carrier of FdSp
1. FdSp is V46(FdSp) Element of the carrier of FdSp
a is Element of the carrier of FdSp
a - (1_ FdSp) is Element of the carrier of FdSp
a + (1_ FdSp) is Element of the carrier of FdSp
b is Element of the carrier of FdSp
c is Element of the carrier of FdSp
b - c is Element of the carrier of FdSp
a * (b - c) is Element of the carrier of FdSp
b + c is Element of the carrier of FdSp
d is Element of the carrier of FdSp
(b + c) - d is Element of the carrier of FdSp
d - c is Element of the carrier of FdSp
(a - (1_ FdSp)) * (d - c) is Element of the carrier of FdSp
d - b is Element of the carrier of FdSp
(a + (1_ FdSp)) * (d - b) is Element of the carrier of FdSp
p is Element of the carrier of FdSp
d - p is Element of the carrier of FdSp
- ((b + c) - d) is Element of the carrier of FdSp
d + (- ((b + c) - d)) is Element of the carrier of FdSp
- (b + c) is Element of the carrier of FdSp
d + (- (b + c)) is Element of the carrier of FdSp
d + (d + (- (b + c))) is Element of the carrier of FdSp
- b is Element of the carrier of FdSp
- c is Element of the carrier of FdSp
(- b) + (- c) is Element of the carrier of FdSp
d + ((- b) + (- c)) is Element of the carrier of FdSp
d + (d + ((- b) + (- c))) is Element of the carrier of FdSp
d + (- b) is Element of the carrier of FdSp
(- c) + (d + (- b)) is Element of the carrier of FdSp
d + ((- c) + (d + (- b))) is Element of the carrier of FdSp
d + (- c) is Element of the carrier of FdSp
(d + (- c)) + (d + (- b)) is Element of the carrier of FdSp
(d - c) + (d + (- b)) is Element of the carrier of FdSp
(d - b) + (d - c) is Element of the carrier of FdSp
a * (d - c) is Element of the carrier of FdSp
a * (d - b) is Element of the carrier of FdSp
(a * (d - c)) - (a * (d - b)) is Element of the carrier of FdSp
a * (d + (- c)) is Element of the carrier of FdSp
(a * (d + (- c))) - (a * (d - b)) is Element of the carrier of FdSp
a * (d + (- b)) is Element of the carrier of FdSp
(a * (d + (- c))) - (a * (d + (- b))) is Element of the carrier of FdSp
- (a * (d + (- b))) is Element of the carrier of FdSp
(a * (d + (- c))) + (- (a * (d + (- b)))) is Element of the carrier of FdSp
a * d is Element of the carrier of FdSp
a * (- c) is Element of the carrier of FdSp
(a * d) + (a * (- c)) is Element of the carrier of FdSp
((a * d) + (a * (- c))) + (- (a * (d + (- b)))) is Element of the carrier of FdSp
- a is Element of the carrier of FdSp
(- a) * (d + (- b)) is Element of the carrier of FdSp
((a * d) + (a * (- c))) + ((- a) * (d + (- b))) is Element of the carrier of FdSp
(- a) * d is Element of the carrier of FdSp
(- a) * (- b) is Element of the carrier of FdSp
((- a) * d) + ((- a) * (- b)) is Element of the carrier of FdSp
((a * d) + (a * (- c))) + (((- a) * d) + ((- a) * (- b))) is Element of the carrier of FdSp
a * b is Element of the carrier of FdSp
((- a) * d) + (a * b) is Element of the carrier of FdSp
((a * d) + (a * (- c))) + (((- a) * d) + (a * b)) is Element of the carrier of FdSp
(a * (- c)) + (a * d) is Element of the carrier of FdSp
- (a * d) is Element of the carrier of FdSp
(- (a * d)) + (a * b) is Element of the carrier of FdSp
((a * (- c)) + (a * d)) + ((- (a * d)) + (a * b)) is Element of the carrier of FdSp
((a * (- c)) + (a * d)) + (- (a * d)) is Element of the carrier of FdSp
(((a * (- c)) + (a * d)) + (- (a * d))) + (a * b) is Element of the carrier of FdSp
(a * d) + (- (a * d)) is Element of the carrier of FdSp
(a * (- c)) + ((a * d) + (- (a * d))) is Element of the carrier of FdSp
((a * (- c)) + ((a * d) + (- (a * d)))) + (a * b) is Element of the carrier of FdSp
0. FdSp is V46(FdSp) Element of the carrier of FdSp
(a * (- c)) + (0. FdSp) is Element of the carrier of FdSp
((a * (- c)) + (0. FdSp)) + (a * b) is Element of the carrier of FdSp
(a * b) + (a * (- c)) is Element of the carrier of FdSp
b + (- c) is Element of the carrier of FdSp
a * (b + (- c)) is Element of the carrier of FdSp
FdSp is non empty non degenerated non trivial right_complementable almost_left_invertible unital V91() V93() right-distributive left-distributive right_unital well-unital V99() left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of FdSp is V4() non trivial set
1_ FdSp is Element of the carrier of FdSp
1. FdSp is V46(FdSp) Element of the carrier of FdSp
a is Element of the carrier of FdSp
b is Element of the carrier of FdSp
c is Element of the carrier of FdSp
b + c is Element of the carrier of FdSp
d is Element of the carrier of FdSp
(b + c) -