:: 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) -