:: PARSP_1 semantic presentation

K122() is Element of bool K118()

K118() is set

bool K118() is non empty set

K117() is set

bool K117() is non empty set

bool K122() is non empty set

{} is empty set

1 is non empty set

PS is non empty right_complementable add-associative right_zeroed addLoopStr

the carrier of PS is non empty set

a is Element of the carrier of PS

b is Element of the carrier of PS

a - b is Element of the carrier of PS

- (a - b) is Element of the carrier of PS

b - a is Element of the carrier of PS

- a is Element of the carrier of PS

b + (- a) is Element of the carrier of PS

PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of PS is non empty non trivial set

0. PS is V49(PS) Element of the carrier of PS

the ZeroF of PS is Element of the carrier of PS

a is Element of the carrier of PS

b is Element of the carrier of PS

a - b is Element of the carrier of PS

b - a is Element of the carrier of PS

c is Element of the carrier of PS

p is Element of the carrier of PS

c - p is Element of the carrier of PS

(a - b) * (c - p) is Element of the carrier of PS

p - c is Element of the carrier of PS

(b - a) * (p - c) is Element of the carrier of PS

((a - b) * (c - p)) - ((b - a) * (p - c)) is Element of the carrier of PS

- (a - b) is Element of the carrier of PS

- (c - p) is Element of the carrier of PS

((a - b) * (c - p)) - ((a - b) * (c - p)) is Element of the carrier of PS

PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of PS is non empty non trivial set

0. PS is V49(PS) Element of the carrier of PS

the ZeroF of PS is Element of the carrier of PS

a is Element of the carrier of PS

b is Element of the carrier of PS

b - b is Element of the carrier of PS

a * (b - b) is Element of the carrier of PS

c is Element of the carrier of PS

c - c is Element of the carrier of PS

p is Element of the carrier of PS

(c - c) * p is Element of the carrier of PS

(a * (b - b)) - ((c - c) * p) is Element of the carrier of PS

PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of PS is non empty non trivial set

0. PS is V49(PS) Element of the carrier of PS

the ZeroF of PS is Element of the carrier of PS

a is Element of the carrier of PS

b is Element of the carrier of PS

a * b is Element of the carrier of PS

c is Element of the carrier of PS

p is Element of the carrier of PS

c * p is Element of the carrier of PS

(a * b) - (c * p) is Element of the carrier of PS

q is Element of the carrier of PS

a * q is Element of the carrier of PS

c * q is Element of the carrier of PS

s is Element of the carrier of PS

s * p is Element of the carrier of PS

(a * q) - (s * p) is Element of the carrier of PS

s * b is Element of the carrier of PS

(c * q) - (s * b) is Element of the carrier of PS

a " is Element of the carrier of PS

(s * p) * (a ") is Element of the carrier of PS

p * (a ") is Element of the carrier of PS

s * (p * (a ")) is Element of the carrier of PS

c * s is Element of the carrier of PS

(c * s) * (p * (a ")) is Element of the carrier of PS

(c * p) * (a ") is Element of the carrier of PS

c * (p * (a ")) is Element of the carrier of PS

s * c is Element of the carrier of PS

(s * c) * (p * (a ")) is Element of the carrier of PS

PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of PS is non empty non trivial set

0. PS is V49(PS) Element of the carrier of PS

the ZeroF of PS is Element of the carrier of PS

a is Element of the carrier of PS

b is Element of the carrier of PS

a * b is Element of the carrier of PS

b * a is Element of the carrier of PS

c is Element of the carrier of PS

p is Element of the carrier of PS

c * p is Element of the carrier of PS

(a * b) - (c * p) is Element of the carrier of PS

p * c is Element of the carrier of PS

(p * c) - (b * a) is Element of the carrier of PS

- ((a * b) - (c * p)) is Element of the carrier of PS

- (b * a) is Element of the carrier of PS

(p * c) + (- (b * a)) is Element of the carrier of PS

PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of PS is non empty non trivial set

0. PS is V49(PS) Element of the carrier of PS

the ZeroF of PS is Element of the carrier of PS

a is Element of the carrier of PS

b is Element of the carrier of PS

c is Element of the carrier of PS

b * c is Element of the carrier of PS

p is Element of the carrier of PS

p * a is Element of the carrier of PS

(b * c) - (p * a) is Element of the carrier of PS

q is Element of the carrier of PS

b * q is Element of the carrier of PS

p * q is Element of the carrier of PS

s is Element of the carrier of PS

s * a is Element of the carrier of PS

(b * q) - (s * a) is Element of the carrier of PS

s * c is Element of the carrier of PS

(p * q) - (s * c) is Element of the carrier of PS

a * p is Element of the carrier of PS

c * b is Element of the carrier of PS

(a * p) - (c * b) is Element of the carrier of PS

a * s is Element of the carrier of PS

q * b is Element of the carrier of PS

(a * s) - (q * b) is Element of the carrier of PS

c * s is Element of the carrier of PS

q * p is Element of the carrier of PS

(c * s) - (q * p) is Element of the carrier of PS

PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of PS is non empty non trivial set

a is Element of the carrier of PS

b is Element of the carrier of PS

a * b is Element of the carrier of PS

c is Element of the carrier of PS

c * a is Element of the carrier of PS

(c * a) * b is Element of the carrier of PS

p is Element of the carrier of PS

c * p is Element of the carrier of PS

(a * b) * (c * p) is Element of the carrier of PS

((c * a) * b) * p is Element of the carrier of PS

c * (a * b) is Element of the carrier of PS

(c * (a * b)) * p is Element of the carrier of PS

PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of PS is non empty non trivial set

0. PS is V49(PS) Element of the carrier of PS

the ZeroF of PS is Element of the carrier of PS

a is Element of the carrier of PS

b is Element of the carrier of PS

a * b is Element of the carrier of PS

c is Element of the carrier of PS

p is Element of the carrier of PS

c * p is Element of the carrier of PS

(a * b) - (c * p) is Element of the carrier of PS

q is Element of the carrier of PS

a * q is Element of the carrier of PS

c * q is Element of the carrier of PS

s is Element of the carrier of PS

(a * q) * s is Element of the carrier of PS

((a * q) * s) * b is Element of the carrier of PS

(c * q) * s is Element of the carrier of PS

((c * q) * s) * p is Element of the carrier of PS

(((a * q) * s) * b) - (((c * q) * s) * p) is Element of the carrier of PS

q * s is Element of the carrier of PS

(q * s) * (a * b) is Element of the carrier of PS

(q * s) * (c * p) is Element of the carrier of PS

(q * s) * ((a * b) - (c * p)) is Element of the carrier of PS

PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of PS is non empty non trivial set

a is Element of the carrier of PS

b is Element of the carrier of PS

a - b is Element of the carrier of PS

c is Element of the carrier of PS

a * c is Element of the carrier of PS

p is Element of the carrier of PS

c - p is Element of the carrier of PS

(a - b) * (c - p) is Element of the carrier of PS

a * p is Element of the carrier of PS

- (a * p) is Element of the carrier of PS

b * (c - p) is Element of the carrier of PS

- (b * (c - p)) is Element of the carrier of PS

(- (a * p)) + (- (b * (c - p))) is Element of the carrier of PS

(a * c) + ((- (a * p)) + (- (b * (c - p)))) is Element of the carrier of PS

- b is Element of the carrier of PS

a + (- b) is Element of the carrier of PS

(a + (- b)) * (c - p) is Element of the carrier of PS

a * (c - p) is Element of the carrier of PS

(- b) * (c - p) is Element of the carrier of PS

(a * (c - p)) + ((- b) * (c - p)) is Element of the carrier of PS

(a * (c - p)) + (- (b * (c - p))) is Element of the carrier of PS

(a * c) - (a * p) is Element of the carrier of PS

((a * c) - (a * p)) + (- (b * (c - p))) is Element of the carrier of PS

(a * c) + (- (a * p)) is Element of the carrier of PS

((a * c) + (- (a * p))) + (- (b * (c - p))) is Element of the carrier of PS

PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of PS is non empty non trivial set

a is Element of the carrier of PS

b is Element of the carrier of PS

a + b is Element of the carrier of PS

c is Element of the carrier of PS

b + c is Element of the carrier of PS

a + (b + c) is Element of the carrier of PS

p is Element of the carrier of PS

c + p is Element of the carrier of PS

(a + b) + (c + p) is Element of the carrier of PS

(a + (b + c)) + p is Element of the carrier of PS

(a + b) + c is Element of the carrier of PS

((a + b) + c) + p is Element of the carrier of PS

PS is non empty right_complementable add-associative right_zeroed addLoopStr

the carrier of PS is non empty set

b is Element of the carrier of PS

a is Element of the carrier of PS

b + a is Element of the carrier of PS

c is Element of the carrier of PS

c + a is Element of the carrier of PS

(b + a) - (c + a) is Element of the carrier of PS

b - c is Element of the carrier of PS

- (c + a) is Element of the carrier of PS

(b + a) + (- (c + a)) is Element of the carrier of PS

- a is Element of the carrier of PS

- c is Element of the carrier of PS

(- a) + (- c) is Element of the carrier of PS

(b + a) + ((- a) + (- c)) is Element of the carrier of PS

(b + a) + (- a) is Element of the carrier of PS

((b + a) + (- a)) + (- c) is Element of the carrier of PS

a + (- a) is Element of the carrier of PS

b + (a + (- a)) is Element of the carrier of PS

(b + (a + (- a))) + (- c) is Element of the carrier of PS

0. PS is V49(PS) Element of the carrier of PS

the ZeroF of PS is Element of the carrier of PS

b + (0. PS) is Element of the carrier of PS

(b + (0. PS)) + (- c) is Element of the carrier of PS

b + (- c) is Element of the carrier of PS

PS is non empty right_complementable add-associative right_zeroed addLoopStr

the carrier of PS is non empty set

a is Element of the carrier of PS

b is Element of the carrier of PS

a + b is Element of the carrier of PS

- b is Element of the carrier of PS

- a is Element of the carrier of PS

(- b) + (- a) is Element of the carrier of PS

- ((- b) + (- a)) is Element of the carrier of PS

- (a + b) is Element of the carrier of PS

- (- (a + b)) is Element of the carrier of PS

PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of PS is non empty non trivial set

0. PS is V49(PS) Element of the carrier of PS

the ZeroF of PS is Element of the carrier of PS

a is Element of the carrier of PS

b is Element of the carrier of PS

a - b is Element of the carrier of PS

b - a is Element of the carrier of PS

c is Element of the carrier of PS

p is Element of the carrier of PS

c - p is Element of the carrier of PS

(a - b) * (c - p) is Element of the carrier of PS

q is Element of the carrier of PS

a - q is Element of the carrier of PS

b - q is Element of the carrier of PS

s is Element of the carrier of PS

c - s is Element of the carrier of PS

(a - q) * (c - s) is Element of the carrier of PS

((a - b) * (c - p)) - ((a - q) * (c - s)) is Element of the carrier of PS

s - p is Element of the carrier of PS

(b - a) * (s - p) is Element of the carrier of PS

s - c is Element of the carrier of PS

(b - q) * (s - c) is Element of the carrier of PS

((b - a) * (s - p)) - ((b - q) * (s - c)) is Element of the carrier of PS

a * c is Element of the carrier of PS

a * p is Element of the carrier of PS

- (a * p) is Element of the carrier of PS

b * (c - p) is Element of the carrier of PS

- (b * (c - p)) is Element of the carrier of PS

(- (a * p)) + (- (b * (c - p))) is Element of the carrier of PS

(a * c) + ((- (a * p)) + (- (b * (c - p)))) is Element of the carrier of PS

a * s is Element of the carrier of PS

- (a * s) is Element of the carrier of PS

q * (c - s) is Element of the carrier of PS

- (q * (c - s)) is Element of the carrier of PS

(- (a * s)) + (- (q * (c - s))) is Element of the carrier of PS

(a * c) + ((- (a * s)) + (- (q * (c - s)))) is Element of the carrier of PS

b * s is Element of the carrier of PS

b * p is Element of the carrier of PS

- (b * p) is Element of the carrier of PS

a * (s - p) is Element of the carrier of PS

- (a * (s - p)) is Element of the carrier of PS

(- (b * p)) + (- (a * (s - p))) is Element of the carrier of PS

(b * s) + ((- (b * p)) + (- (a * (s - p)))) is Element of the carrier of PS

b * c is Element of the carrier of PS

- (b * c) is Element of the carrier of PS

q * (s - c) is Element of the carrier of PS

- (q * (s - c)) is Element of the carrier of PS

(- (b * c)) + (- (q * (s - c))) is Element of the carrier of PS

(b * s) + ((- (b * c)) + (- (q * (s - c)))) is Element of the carrier of PS

((- (b * p)) + (- (a * (s - p)))) - ((- (b * c)) + (- (q * (s - c)))) is Element of the carrier of PS

(a * s) - (a * p) is Element of the carrier of PS

- ((a * s) - (a * p)) is Element of the carrier of PS

(- (b * p)) + (- ((a * s) - (a * p))) is Element of the carrier of PS

((- (b * p)) + (- ((a * s) - (a * p)))) - ((- (b * c)) + (- (q * (s - c)))) is Element of the carrier of PS

(- (a * s)) + (a * p) is Element of the carrier of PS

(- (b * p)) + ((- (a * s)) + (a * p)) is Element of the carrier of PS

((- (b * p)) + ((- (a * s)) + (a * p))) - ((- (b * c)) + (- (q * (s - c)))) is Element of the carrier of PS

(- (b * p)) + (a * p) is Element of the carrier of PS

((- (b * p)) + (a * p)) + (- (a * s)) is Element of the carrier of PS

(((- (b * p)) + (a * p)) + (- (a * s))) - ((- (b * c)) + (- (q * (s - c)))) is Element of the carrier of PS

(a * p) + (- (b * p)) is Element of the carrier of PS

((a * p) + (- (b * p))) + (- (a * s)) is Element of the carrier of PS

- ((- (b * c)) + (- (q * (s - c)))) is Element of the carrier of PS

(((a * p) + (- (b * p))) + (- (a * s))) + (- ((- (b * c)) + (- (q * (s - c))))) is Element of the carrier of PS

- (- (b * c)) is Element of the carrier of PS

- (- (q * (s - c))) is Element of the carrier of PS

(- (- (b * c))) + (- (- (q * (s - c)))) is Element of the carrier of PS

(((a * p) + (- (b * p))) + (- (a * s))) + ((- (- (b * c))) + (- (- (q * (s - c))))) is Element of the carrier of PS

(b * c) + (- (- (q * (s - c)))) is Element of the carrier of PS

(((a * p) + (- (b * p))) + (- (a * s))) + ((b * c) + (- (- (q * (s - c))))) is Element of the carrier of PS

(b * c) + (q * (s - c)) is Element of the carrier of PS

(((a * p) + (- (b * p))) + (- (a * s))) + ((b * c) + (q * (s - c))) is Element of the carrier of PS

(- (a * s)) + (b * c) is Element of the carrier of PS

((a * p) + (- (b * p))) + ((- (a * s)) + (b * c)) is Element of the carrier of PS

(((a * p) + (- (b * p))) + ((- (a * s)) + (b * c))) + (q * (s - c)) is Element of the carrier of PS

((a * p) + (- (b * p))) + (b * c) is Element of the carrier of PS

(- (a * s)) + (q * (s - c)) is Element of the carrier of PS

(((a * p) + (- (b * p))) + (b * c)) + ((- (a * s)) + (q * (s - c))) is Element of the carrier of PS

(- (b * p)) + (b * c) is Element of the carrier of PS

(a * p) + ((- (b * p)) + (b * c)) is Element of the carrier of PS

((a * p) + ((- (b * p)) + (b * c))) + ((- (a * s)) + (q * (s - c))) is Element of the carrier of PS

(b * c) - (b * p) is Element of the carrier of PS

(a * p) + ((b * c) - (b * p)) is Element of the carrier of PS

((a * p) + ((b * c) - (b * p))) + ((- (a * s)) + (q * (s - c))) is Element of the carrier of PS

(a * p) + (b * (c - p)) is Element of the carrier of PS

((a * p) + (b * (c - p))) + ((- (a * s)) + (q * (s - c))) is Element of the carrier of PS

- ((- (a * p)) + (- (b * (c - p)))) is Element of the carrier of PS

(- ((- (a * p)) + (- (b * (c - p))))) + ((- (a * s)) + (q * (s - c))) is Element of the carrier of PS

- (- (a * s)) is Element of the carrier of PS

(- (- (a * s))) + (- (q * (s - c))) is Element of the carrier of PS

- ((- (- (a * s))) + (- (q * (s - c)))) is Element of the carrier of PS

(- ((- (a * p)) + (- (b * (c - p))))) + (- ((- (- (a * s))) + (- (q * (s - c))))) is Element of the carrier of PS

(a * s) + (- (q * (s - c))) is Element of the carrier of PS

- ((a * s) + (- (q * (s - c)))) is Element of the carrier of PS

(- ((- (a * p)) + (- (b * (c - p))))) + (- ((a * s) + (- (q * (s - c))))) is Element of the carrier of PS

((- (a * p)) + (- (b * (c - p)))) + ((a * s) + (- (q * (s - c)))) is Element of the carrier of PS

- (((- (a * p)) + (- (b * (c - p)))) + ((a * s) + (- (q * (s - c))))) is Element of the carrier of PS

(- (a * s)) + (- (- (q * (s - c)))) is Element of the carrier of PS

- ((- (a * s)) + (- (- (q * (s - c))))) is Element of the carrier of PS

((- (a * p)) + (- (b * (c - p)))) + (- ((- (a * s)) + (- (- (q * (s - c)))))) is Element of the carrier of PS

- (((- (a * p)) + (- (b * (c - p)))) + (- ((- (a * s)) + (- (- (q * (s - c))))))) is Element of the carrier of PS

((- (a * p)) + (- (b * (c - p)))) - ((- (a * s)) + (- (- (q * (s - c))))) is Element of the carrier of PS

- (((- (a * p)) + (- (b * (c - p)))) - ((- (a * s)) + (- (- (q * (s - c)))))) is Element of the carrier of PS

- (s - c) is Element of the carrier of PS

(- (s - c)) * q is Element of the carrier of PS

- ((- (s - c)) * q) is Element of the carrier of PS

(- (a * s)) + (- ((- (s - c)) * q)) is Element of the carrier of PS

((- (a * p)) + (- (b * (c - p)))) - ((- (a * s)) + (- ((- (s - c)) * q))) is Element of the carrier of PS

- (((- (a * p)) + (- (b * (c - p)))) - ((- (a * s)) + (- ((- (s - c)) * q)))) is Element of the carrier of PS

((- (a * p)) + (- (b * (c - p)))) - ((- (a * s)) + (- (q * (c - s)))) is Element of the carrier of PS

- (((- (a * p)) + (- (b * (c - p)))) - ((- (a * s)) + (- (q * (c - s))))) is Element of the carrier of PS

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

PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of PS is non empty non trivial set

a is Element of the carrier of PS

b is Element of the carrier of PS

a + b is Element of the carrier of PS

c is Element of the carrier of PS

- c is Element of the carrier of PS

(a + b) + (- c) is Element of the carrier of PS

a - ((a + b) + (- c)) is Element of the carrier of PS

c - b is Element of the carrier of PS

b + (- c) is Element of the carrier of PS

a + (b + (- c)) is Element of the carrier of PS

a - (a + (b + (- c))) is Element of the carrier of PS

b - c is Element of the carrier of PS

a + (b - c) is Element of the carrier of PS

a - (a + (b - c)) is Element of the carrier of PS

- (a + (b - c)) is Element of the carrier of PS

a + (- (a + (b - c))) is Element of the carrier of PS

- a is Element of the carrier of PS

- (b - c) is Element of the carrier of PS

(- a) + (- (b - c)) is Element of the carrier of PS

a + ((- a) + (- (b - c))) is Element of the carrier of PS

a + (- a) is Element of the carrier of PS

(a + (- a)) + (- (b - c)) is Element of the carrier of PS

0. PS is V49(PS) Element of the carrier of PS

the ZeroF of PS is Element of the carrier of PS

(0. PS) + (- (b - c)) is Element of the carrier of PS

PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of PS is non empty non trivial set

0. PS is V49(PS) Element of the carrier of PS

the ZeroF of PS is Element of the carrier of PS

a is Element of the carrier of PS

- a is Element of the carrier of PS

b is Element of the carrier of PS

a - b is Element of the carrier of PS

c is Element of the carrier of PS

p is Element of the carrier of PS

c + p is Element of the carrier of PS

q is Element of the carrier of PS

- q is Element of the carrier of PS

(c + p) + (- q) is Element of the carrier of PS

c - ((c + p) + (- q)) is Element of the carrier of PS

(a - b) * (c - ((c + p) + (- q))) is Element of the carrier of PS

q - p is Element of the carrier of PS

s is Element of the carrier of PS

s + b is Element of the carrier of PS

(s + b) + (- a) is Element of the carrier of PS

s - ((s + b) + (- a)) is Element of the carrier of PS

(s - ((s + b) + (- a))) * (q - p) is Element of the carrier of PS

((a - b) * (c - ((c + p) + (- q)))) - ((s - ((s + b) + (- a))) * (q - p)) is Element of the carrier of PS

PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of PS is non empty non trivial set

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

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

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

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

[:H

[:[:H

bool [:[:H

a is V6() V18([:H

b is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

c is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

a . (b,c) is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

b `1_3 is Element of the carrier of PS

c `1_3 is Element of the carrier of PS

(b `1_3) + (c `1_3) is Element of the carrier of PS

b `2_3 is Element of the carrier of PS

c `2_3 is Element of the carrier of PS

(b `2_3) + (c `2_3) is Element of the carrier of PS

b `3_3 is Element of the carrier of PS

c `3_3 is Element of the carrier of PS

(b `3_3) + (c `3_3) is Element of the carrier of PS

[((b `1_3) + (c `1_3)),((b `2_3) + (c `2_3)),((b `3_3) + (c `3_3))] is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

[:H

[:[:H

bool [:[:H

a is V6() V18([:H

b is V6() V18([:H

c is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

p is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

a . (c,p) is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

b . (c,p) is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

c `1_3 is Element of the carrier of PS

p `1_3 is Element of the carrier of PS

(c `1_3) + (p `1_3) is Element of the carrier of PS

c `2_3 is Element of the carrier of PS

p `2_3 is Element of the carrier of PS

(c `2_3) + (p `2_3) is Element of the carrier of PS

c `3_3 is Element of the carrier of PS

p `3_3 is Element of the carrier of PS

(c `3_3) + (p `3_3) is Element of the carrier of PS

[((c `1_3) + (p `1_3)),((c `2_3) + (p `2_3)),((c `3_3) + (p `3_3))] is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of PS is non empty non trivial set

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

(PS) is V6() V18([:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:],[: the carrier of PS, the carrier of PS, the carrier of PS:]) Element of bool [:[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:]

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

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

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

a is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

b is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

(PS) . (a,b) is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of PS is non empty non trivial set

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

a is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

b is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

(PS,a,b) is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

(PS) is V6() V18([:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:],[: the carrier of PS, the carrier of PS, the carrier of PS:]) Element of bool [:[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:]

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

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

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

(PS) . (a,b) is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

a `1_3 is Element of the carrier of PS

b `1_3 is Element of the carrier of PS

(a `1_3) + (b `1_3) is Element of the carrier of PS

a `2_3 is Element of the carrier of PS

b `2_3 is Element of the carrier of PS

(a `2_3) + (b `2_3) is Element of the carrier of PS

a `3_3 is Element of the carrier of PS

b `3_3 is Element of the carrier of PS

(a `3_3) + (b `3_3) is Element of the carrier of PS

[((a `1_3) + (b `1_3)),((a `2_3) + (b `2_3)),((a `3_3) + (b `3_3))] is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of PS is non empty non trivial set

a is Element of the carrier of PS

b is Element of the carrier of PS

c is Element of the carrier of PS

[a,b,c] is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

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

p is Element of the carrier of PS

a + p is Element of the carrier of PS

q is Element of the carrier of PS

b + q is Element of the carrier of PS

s is Element of the carrier of PS

[p,q,s] is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

(PS,[a,b,c],[p,q,s]) is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

(PS) is V6() V18([:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:],[: the carrier of PS, the carrier of PS, the carrier of PS:]) Element of bool [:[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:]

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

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

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

(PS) . ([a,b,c],[p,q,s]) is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

c + s is Element of the carrier of PS

[(a + p),(b + q),(c + s)] is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

[a,b,c] `3_3 is Element of the carrier of PS

[p,q,s] `1_3 is Element of the carrier of PS

[p,q,s] `2_3 is Element of the carrier of PS

[p,q,s] `3_3 is Element of the carrier of PS

[a,b,c] `1_3 is Element of the carrier of PS

[a,b,c] `2_3 is Element of the carrier of PS

PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of PS is non empty non trivial set

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

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

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

[:H

bool [:H

a is V6() V18(H

b is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

a . b is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

b `1_3 is Element of the carrier of PS

- (b `1_3) is Element of the carrier of PS

b `2_3 is Element of the carrier of PS

- (b `2_3) is Element of the carrier of PS

b `3_3 is Element of the carrier of PS

- (b `3_3) is Element of the carrier of PS

[(- (b `1_3)),(- (b `2_3)),(- (b `3_3))] is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

[:H

bool [:H

a is V6() V18(H

b is V6() V18(H

c is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

a . c is Element of H

b . c is Element of H

c `1_3 is Element of the carrier of PS

- (c `1_3) is Element of the carrier of PS

c `2_3 is Element of the carrier of PS

- (c `2_3) is Element of the carrier of PS

c `3_3 is Element of the carrier of PS

- (c `3_3) is Element of the carrier of PS

[(- (c `1_3)),(- (c `2_3)),(- (c `3_3))] is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of PS is non empty non trivial set

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

(PS) is V6() V18([: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]) Element of bool [:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:]

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

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

a is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

(PS) . a is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of PS is non empty non trivial set

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

a is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

(PS,a) is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

(PS) is V6() V18([: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]) Element of bool [:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:]

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

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

(PS) . a is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

a `1_3 is Element of the carrier of PS

- (a `1_3) is Element of the carrier of PS

a `2_3 is Element of the carrier of PS

- (a `2_3) is Element of the carrier of PS

a `3_3 is Element of the carrier of PS

- (a `3_3) is Element of the carrier of PS

[(- (a `1_3)),(- (a `2_3)),(- (a `3_3))] is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

PS is set

[:PS,PS,PS,PS:] is set

the non empty set is non empty set

the ( the non empty set ) is ( the non empty set )

( the non empty set , the ( the non empty set )) is () ()

the carrier of ( the non empty set , the ( the non empty set )) is set

PS is non empty ()

the carrier of PS is non empty set

PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of PS is non empty non trivial set

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

PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

(PS) is set

the carrier of PS is non empty non trivial set

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

PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

(PS) is non empty set

the carrier of PS is non empty non trivial set

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

[:(PS),(PS),(PS),(PS):] is non empty set

PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

(PS) is set

(PS) is non empty set

the carrier of PS is non empty non trivial set

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

[:(PS),(PS),(PS),(PS):] is non empty set

PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

(PS) is non empty set

(PS) is non empty set

the carrier of PS is non empty non trivial set

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

[:(PS),(PS),(PS),(PS):] is non empty set

0. PS is V49(PS) Element of the carrier of PS

the ZeroF of PS is Element of the carrier of PS

a is set

b is set

c is set

p is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

q is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

s is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

s is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

[p,q,s,s] is Element of [:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:]

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

p `1_3 is Element of the carrier of PS

q `1_3 is Element of the carrier of PS

(p `1_3) - (q `1_3) is Element of the carrier of PS

s `2_3 is Element of the carrier of PS

s `2_3 is Element of the carrier of PS

(s `2_3) - (s `2_3) is Element of the carrier of PS

((p `1_3) - (q `1_3)) * ((s `2_3) - (s `2_3)) is Element of the carrier of PS

s `1_3 is Element of the carrier of PS

s `1_3 is Element of the carrier of PS

(s `1_3) - (s `1_3) is Element of the carrier of PS

p `2_3 is Element of the carrier of PS

q `2_3 is Element of the carrier of PS

(p `2_3) - (q `2_3) is Element of the carrier of PS

((s `1_3) - (s `1_3)) * ((p `2_3) - (q `2_3)) is Element of the carrier of PS

(((p `1_3) - (q `1_3)) * ((s `2_3) - (s `2_3))) - (((s `1_3) - (s `1_3)) * ((p `2_3) - (q `2_3))) is Element of the carrier of PS

s `3_3 is Element of the carrier of PS

s `3_3 is Element of the carrier of PS

(s `3_3) - (s `3_3) is Element of the carrier of PS

((p `1_3) - (q `1_3)) * ((s `3_3) - (s `3_3)) is Element of the carrier of PS

p `3_3 is Element of the carrier of PS

q `3_3 is Element of the carrier of PS

(p `3_3) - (q `3_3) is Element of the carrier of PS

((s `1_3) - (s `1_3)) * ((p `3_3) - (q `3_3)) is Element of the carrier of PS

(((p `1_3) - (q `1_3)) * ((s `3_3) - (s `3_3))) - (((s `1_3) - (s `1_3)) * ((p `3_3) - (q `3_3))) is Element of the carrier of PS

((p `2_3) - (q `2_3)) * ((s `3_3) - (s `3_3)) is Element of the carrier of PS

((s `2_3) - (s `2_3)) * ((p `3_3) - (q `3_3)) is Element of the carrier of PS

(((p `2_3) - (q `2_3)) * ((s `3_3) - (s `3_3))) - (((s `2_3) - (s `2_3)) * ((p `3_3) - (q `3_3))) is Element of the carrier of PS

p is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

q is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

s is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

s is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

[p,q,s,s] is Element of [:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:]

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

p `1_3 is Element of the carrier of PS

q `1_3 is Element of the carrier of PS

(p `1_3) - (q `1_3) is Element of the carrier of PS

s `2_3 is Element of the carrier of PS

s `2_3 is Element of the carrier of PS

(s `2_3) - (s `2_3) is Element of the carrier of PS

((p `1_3) - (q `1_3)) * ((s `2_3) - (s `2_3)) is Element of the carrier of PS

s `1_3 is Element of the carrier of PS

s `1_3 is Element of the carrier of PS

(s `1_3) - (s `1_3) is Element of the carrier of PS

p `2_3 is Element of the carrier of PS

q `2_3 is Element of the carrier of PS

(p `2_3) - (q `2_3) is Element of the carrier of PS

((s `1_3) - (s `1_3)) * ((p `2_3) - (q `2_3)) is Element of the carrier of PS

(((p `1_3) - (q `1_3)) * ((s `2_3) - (s `2_3))) - (((s `1_3) - (s `1_3)) * ((p `2_3) - (q `2_3))) is Element of the carrier of PS

s `3_3 is Element of the carrier of PS

s `3_3 is Element of the carrier of PS

(s `3_3) - (s `3_3) is Element of the carrier of PS

((p `1_3) - (q `1_3)) * ((s `3_3) - (s `3_3)) is Element of the carrier of PS

p `3_3 is Element of the carrier of PS

q `3_3 is Element of the carrier of PS

(p `3_3) - (q `3_3) is Element of the carrier of PS

((s `1_3) - (s `1_3)) * ((p `3_3) - (q `3_3)) is Element of the carrier of PS

(((p `1_3) - (q `1_3)) * ((s `3_3) - (s `3_3))) - (((s `1_3) - (s `1_3)) * ((p `3_3) - (q `3_3))) is Element of the carrier of PS

((p `2_3) - (q `2_3)) * ((s `3_3) - (s `3_3)) is Element of the carrier of PS

((s `2_3) - (s `2_3)) * ((p `3_3) - (q `3_3)) is Element of the carrier of PS

(((p `2_3) - (q `2_3)) * ((s `3_3) - (s `3_3))) - (((s `2_3) - (s `2_3)) * ((p `3_3) - (q `3_3))) is Element of the carrier of PS

PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

(PS) is set

(PS) is non empty set

the carrier of PS is non empty non trivial set

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

[:(PS),(PS),(PS),(PS):] is non empty set

a is set

(PS) is non empty set

PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

(PS) is set

(PS) is non empty set

the carrier of PS is non empty non trivial set

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

[:(PS),(PS),(PS),(PS):] is non empty set

PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

(PS) is non empty set

the carrier of PS is non empty non trivial set

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

(PS) is ((PS))

(PS) is set

((PS),(PS)) is () ()

PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

(PS) is ()

(PS) is non empty set

the carrier of PS is non empty non trivial set

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

(PS) is ((PS))

(PS) is set

((PS),(PS)) is () ()

PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

(PS) is non empty () ()

(PS) is non empty set

the carrier of PS is non empty non trivial set

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

(PS) is ((PS))

(PS) is set

((PS),(PS)) is () ()

the carrier of (PS) is non empty set

PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

(PS) is non empty () ()

(PS) is non empty set

the carrier of PS is non empty non trivial set

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

(PS) is ((PS))

(PS) is set

((PS),(PS)) is () ()

the of (PS) is ( the carrier of (PS))

the carrier of (PS) is non empty set

PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

(PS) is non empty () ()

(PS) is non empty set

the carrier of PS is non empty non trivial set

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

(PS) is ((PS))

(PS) is set

((PS),(PS)) is () ()

the carrier of (PS) is non empty set

q is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

(q) is non empty () ()

(q) is non empty set

the carrier of q is non empty non trivial set

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

(q) is ((q))

(q) is set

((q),(q)) is () ()

the carrier of (q) is non empty set

a is Element of the carrier of (PS)

b is Element of the carrier of (PS)

c is Element of the carrier of (PS)

p is Element of the carrier of (PS)

[a,b,c,p] is Element of [: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):]

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

s is Element of the carrier of (q)

s is Element of the carrier of (q)

s is Element of the carrier of (q)

c

[s,s,s,c

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

PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

(PS) is non empty () ()

(PS) is non empty set

the carrier of PS is non empty non trivial set

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

(PS) is ((PS))

(PS) is set

((PS),(PS)) is () ()

the carrier of (PS) is non empty set

q is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

(q) is non empty () ()

(q) is non empty set

the carrier of q is non empty non trivial set

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

(q) is ((q))

(q) is set

((q),(q)) is () ()

the carrier of (q) is non empty set

a is Element of the carrier of (PS)

b is Element of the carrier of (PS)

c is Element of the carrier of (PS)

p is Element of the carrier of (PS)

[a,b,c,p] is Element of [: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):]

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

(PS) is non empty set

[:(PS),(PS),(PS),(PS):] is non empty set

0. PS is V49(PS) Element of the carrier of PS

the ZeroF of PS is Element of the carrier of PS

s is Element of the carrier of (q)

s is Element of the carrier of (q)

s is Element of the carrier of (q)

c

[s,s,s,c

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

(q) is non empty set

[:(q),(q),(q),(q):] is non empty set

h is Element of [: the carrier of q, the carrier of q, the carrier of q:]

i is Element of [: the carrier of q, the carrier of q, the carrier of q:]

j is Element of [: the carrier of q, the carrier of q, the carrier of q:]

k is Element of [: the carrier of q, the carrier of q, the carrier of q:]

[h,i,j,k] is Element of [:[: the carrier of q, the carrier of q, the carrier of q:],[: the carrier of q, the carrier of q, the carrier of q:],[: the carrier of q, the carrier of q, the carrier of q:],[: the carrier of q, the carrier of q, the carrier of q:]:]

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

h `1_3 is Element of the carrier of q

i `1_3 is Element of the carrier of q

(h `1_3) - (i `1_3) is Element of the carrier of q

j `2_3 is Element of the carrier of q

k `2_3 is Element of the carrier of q

(j `2_3) - (k `2_3) is Element of the carrier of q

((h `1_3) - (i `1_3)) * ((j `2_3) - (k `2_3)) is Element of the carrier of q

j `1_3 is Element of the carrier of q

k `1_3 is Element of the carrier of q

(j `1_3) - (k `1_3) is Element of the carrier of q

h `2_3 is Element of the carrier of q

i `2_3 is Element of the carrier of q

(h `2_3) - (i `2_3) is Element of the carrier of q

((j `1_3) - (k `1_3)) * ((h `2_3) - (i `2_3)) is Element of the carrier of q

(((h `1_3) - (i `1_3)) * ((j `2_3) - (k `2_3))) - (((j `1_3) - (k `1_3)) * ((h `2_3) - (i `2_3))) is Element of the carrier of q

0. q is V49(q) Element of the carrier of q

the ZeroF of q is Element of the carrier of q

j `3_3 is Element of the carrier of q

k `3_3 is Element of the carrier of q

(j `3_3) - (k `3_3) is Element of the carrier of q

((h `1_3) - (i `1_3)) * ((j `3_3) - (k `3_3)) is Element of the carrier of q

h `3_3 is Element of the carrier of q

i `3_3 is Element of the carrier of q

(h `3_3) - (i `3_3) is Element of the carrier of q

((j `1_3) - (k `1_3)) * ((h `3_3) - (i `3_3)) is Element of the carrier of q

(((h `1_3) - (i `1_3)) * ((j `3_3) - (k `3_3))) - (((j `1_3) - (k `1_3)) * ((h `3_3) - (i `3_3))) is Element of the carrier of q

((h `2_3) - (i `2_3)) * ((j `3_3) - (k `3_3)) is Element of the carrier of q

((j `2_3) - (k `2_3)) * ((h `3_3) - (i `3_3)) is Element of the carrier of q

(((h `2_3) - (i `2_3)) * ((j `3_3) - (k `3_3))) - (((j `2_3) - (k `2_3)) * ((h `3_3) - (i `3_3))) is Element of the carrier of q

PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

(PS) is non empty () ()

(PS) is non empty set

the carrier of PS is non empty non trivial set

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

(PS) is ((PS))

(PS) is set

((PS),(PS)) is () ()

the carrier of (PS) is non empty set

(PS) is non empty set

[:(PS),(PS),(PS),(PS):] is non empty set

0. PS is V49(PS) Element of the carrier of PS

the ZeroF of PS is Element of the carrier of PS

a is Element of the carrier of (PS)

b is Element of the carrier of (PS)

c is Element of the carrier of (PS)

p is Element of the carrier of (PS)

[a,b,c,p] is Element of [: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):]

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

q is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

s is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

s is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

s is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

[q,s,s,s] is Element of [:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:]

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

q `1_3 is Element of the carrier of PS

s `1_3 is Element of the carrier of PS

(q `1_3) - (s `1_3) is Element of the carrier of PS

s `2_3 is Element of the carrier of PS

s `2_3 is Element of the carrier of PS

(s `2_3) - (s `2_3) is Element of the carrier of PS

((q `1_3) - (s `1_3)) * ((s `2_3) - (s `2_3)) is Element of the carrier of PS

s `1_3 is Element of the carrier of PS

s `1_3 is Element of the carrier of PS

(s `1_3) - (s `1_3) is Element of the carrier of PS

q `2_3 is Element of the carrier of PS

s `2_3 is Element of the carrier of PS

(q `2_3) - (s `2_3) is Element of the carrier of PS

((s `1_3) - (s `1_3)) * ((q `2_3) - (s `2_3)) is Element of the carrier of PS

(((q `1_3) - (s `1_3)) * ((s `2_3) - (s `2_3))) - (((s `1_3) - (s `1_3)) * ((q `2_3) - (s `2_3))) is Element of the carrier of PS

s `3_3 is Element of the carrier of PS

s `3_3 is Element of the carrier of PS

(s `3_3) - (s `3_3) is Element of the carrier of PS

((q `1_3) - (s `1_3)) * ((s `3_3) - (s `3_3)) is Element of the carrier of PS

q `3_3 is Element of the carrier of PS

s `3_3 is Element of the carrier of PS

(q `3_3) - (s `3_3) is Element of the carrier of PS

((s `1_3) - (s `1_3)) * ((q `3_3) - (s `3_3)) is Element of the carrier of PS

(((q `1_3) - (s `1_3)) * ((s `3_3) - (s `3_3))) - (((s `1_3) - (s `1_3)) * ((q `3_3) - (s `3_3))) is Element of the carrier of PS

((q `2_3) - (s `2_3)) * ((s `3_3) - (s `3_3)) is Element of the carrier of PS

((s `2_3) - (s `2_3)) * ((q `3_3) - (s `3_3)) is Element of the carrier of PS

(((q `2_3) - (s `2_3)) * ((s `3_3) - (s `3_3))) - (((s `2_3) - (s `2_3)) * ((q `3_3) - (s `3_3))) is Element of the carrier of PS

PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

(PS) is non empty () ()

(PS) is non empty set

the carrier of PS is non empty non trivial set

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

(PS) is ((PS))

(PS) is set

((PS),(PS)) is () ()

the carrier of (PS) is non empty set

PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

(PS) is non empty () ()

(PS) is non empty set

the carrier of PS is non empty non trivial set

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

(PS) is ((PS))

(PS) is set

((PS),(PS)) is () ()

the carrier of (PS) is non empty set

a is Element of the carrier of (PS)

b is Element of the carrier of (PS)

c is Element of the carrier of (PS)

p is Element of the carrier of (PS)

[a,b,c,p] is Element of [: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):]

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

(PS) is non empty set

[:(PS),(PS),(PS),(PS):] is non empty set

PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

(PS) is non empty () ()

(PS) is non empty set

the carrier of PS is non empty non trivial set

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

(PS) is ((PS))

(PS) is set

((PS),(PS)) is () ()

the carrier of (PS) is non empty set

0. PS is V49(PS) Element of the carrier of PS

the ZeroF of PS is Element of the carrier of PS

a is Element of the carrier of (PS)

b is Element of the carrier of (PS)

c is Element of the carrier of (PS)

p is Element of the carrier of (PS)

[a,b,c,p] is Element of [: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):]

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

(PS) is non empty set

[:(PS),(PS),(PS),(PS):] is non empty set

q is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

s is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

s is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

s is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

[q,s,s,s] is Element of [:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:]

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

q `1_3 is Element of the carrier of PS

s `1_3 is Element of the carrier of PS

(q `1_3) - (s `1_3) is Element of the carrier of PS

s `2_3 is Element of the carrier of PS

s `2_3 is Element of the carrier of PS

(s `2_3) - (s `2_3) is Element of the carrier of PS

((q `1_3) - (s `1_3)) * ((s `2_3) - (s `2_3)) is Element of the carrier of PS

s `1_3 is Element of the carrier of PS

s `1_3 is Element of the carrier of PS

(s `1_3) - (s `1_3) is Element of the carrier of PS

q `2_3 is Element of the carrier of PS

s `2_3 is Element of the carrier of PS

(q `2_3) - (s `2_3) is Element of the carrier of PS

((s `1_3) - (s `1_3)) * ((q `2_3) - (s `2_3)) is Element of the carrier of PS

(((q `1_3) - (s `1_3)) * ((s `2_3) - (s `2_3))) - (((s `1_3) - (s `1_3)) * ((q `2_3) - (s `2_3))) is Element of the carrier of PS

s `3_3 is Element of the carrier of PS

s `3_3 is Element of the carrier of PS

(s `3_3) - (s `3_3) is Element of the carrier of PS

((q `1_3) - (s `1_3)) * ((s `3_3) - (s `3_3)) is Element of the carrier of PS

q `3_3 is Element of the carrier of PS

s `3_3 is Element of the carrier of PS

(q `3_3) - (s `3_3) is Element of the carrier of PS

((s `1_3) - (s `1_3)) * ((q `3_3) - (s `3_3)) is Element of the carrier of PS

(((q `1_3) - (s `1_3)) * ((s `3_3) - (s `3_3))) - (((s `1_3) - (s `1_3)) * ((q `3_3) - (s `3_3))) is Element of the carrier of PS

((q `2_3) - (s `2_3)) * ((s `3_3) - (s `3_3)) is Element of the carrier of PS

((s `2_3) - (s `2_3)) * ((q `3_3) - (s `3_3)) is Element of the carrier of PS

(((q `2_3) - (s `2_3)) * ((s `3_3) - (s `3_3))) - (((s `2_3) - (s `2_3)) * ((q `3_3) - (s `3_3))) is Element of the carrier of PS

PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

(PS) is non empty () ()

(PS) is non empty set

the carrier of PS is non empty non trivial set

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

(PS) is ((PS))

(PS) is set

((PS),(PS)) is () ()

the carrier of (PS) is non empty set

a is Element of the carrier of (PS)

b is Element of the carrier of (PS)

[a,b,b,a] is Element of [: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):]

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

c is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

p is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

[c,p,p,c] is Element of [:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:]

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

c `2_3 is Element of the carrier of PS

p `2_3 is Element of the carrier of PS

(c `2_3) - (p `2_3) is Element of the carrier of PS

p `3_3 is Element of the carrier of PS

c `3_3 is Element of the carrier of PS

(p `3_3) - (c `3_3) is Element of the carrier of PS

((c `2_3) - (p `2_3)) * ((p `3_3) - (c `3_3)) is Element of the carrier of PS

(p `2_3) - (c `2_3) is Element of the carrier of PS

(c `3_3) - (p `3_3) is Element of the carrier of PS

((p `2_3) - (c `2_3)) * ((c `3_3) - (p `3_3)) is Element of the carrier of PS

(((c `2_3) - (p `2_3)) * ((p `3_3) - (c `3_3))) - (((p `2_3) - (c `2_3)) * ((c `3_3) - (p `3_3))) is Element of the carrier of PS

0. PS is V49(PS) Element of the carrier of PS

the ZeroF of PS is Element of the carrier of PS

c `1_3 is Element of the carrier of PS

p `1_3 is Element of the carrier of PS

(c `1_3) - (p `1_3) is Element of the carrier of PS

((c `1_3) - (p `1_3)) * ((p `2_3) - (c `2_3)) is Element of the carrier of PS

(p `1_3) - (c `1_3) is Element of the carrier of PS

((p `1_3) - (c `1_3)) * ((c `2_3) - (p `2_3)) is Element of the carrier of PS

(((c `1_3) - (p `1_3)) * ((p `2_3) - (c `2_3))) - (((p `1_3) - (c `1_3)) * ((c `2_3) - (p `2_3))) is Element of the carrier of PS

((c `1_3) - (p `1_3)) * ((p `3_3) - (c `3_3)) is Element of the carrier of PS

((p `1_3) - (c `1_3)) * ((c `3_3) - (p `3_3)) is Element of the carrier of PS

(((c `1_3) - (p `1_3)) * ((p `3_3) - (c `3_3))) - (((p `1_3) - (c `1_3)) * ((c `3_3) - (p `3_3))) is Element of the carrier of PS

PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

(PS) is non empty () ()

(PS) is non empty set

the carrier of PS is non empty non trivial set

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

(PS) is ((PS))

(PS) is set

((PS),(PS)) is () ()

the carrier of (PS) is non empty set

a is Element of the carrier of (PS)

b is Element of the carrier of (PS)

c is Element of the carrier of (PS)

[a,b,c,c] is Element of [: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):]

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

p is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

q is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

s is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

[p,q,s,s] is Element of [:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:]

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

p `2_3 is Element of the carrier of PS

q `2_3 is Element of the carrier of PS

(p `2_3) - (q `2_3) is Element of the carrier of PS

s `3_3 is Element of the carrier of PS

(s `3_3) - (s `3_3) is Element of the carrier of PS

((p `2_3) - (q `2_3))