:: VECTSP_2 semantic presentation

K108() is Element of bool K104()
K104() is set
bool K104() is set

1 is non empty set
K81({},1) is non empty set
K103() is set
bool K103() is set
bool K108() is set
[:1,1:] is set
bool [:1,1:] is set
[:[:1,1:],1:] is set
bool [:[:1,1:],1:] is set
K80({}) is non empty set
F is non empty multLoopStr
1. F is Element of the carrier of F
the carrier of F is non empty set
the OneF of F is Element of the carrier of F
1_ F is Element of the carrier of F
x is Element of the carrier of F
x * (1. F) is Element of the carrier of F
the multF of F is V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
the multF of F . (x,(1. F)) is Element of the carrier of F
V is Element of the carrier of F
(1. F) * V is Element of the carrier of F
the multF of F . ((1. F),V) is Element of the carrier of F

the multF of the non empty non degenerated non trivial right_complementable almost_left_invertible strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr is V6() V18([::], the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr ) Element of bool [:[::], the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr :]
[::] is set
[:[::], the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr :] is set
bool [:[::], the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr :] is set

the carrier of F is non empty non trivial set
0. F is V46(F) right_complementable Element of the carrier of F
the ZeroF of F is right_complementable Element of the carrier of F
x is right_complementable Element of the carrier of F
V is right_complementable Element of the carrier of F
x * V is right_complementable Element of the carrier of F
the multF of F is V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
the multF of F . (x,V) is right_complementable Element of the carrier of F
F is non empty multLoopStr
the carrier of F is non empty set
x is Element of the carrier of F
1. F is Element of the carrier of F
the OneF of F is Element of the carrier of F
x * (1. F) is Element of the carrier of F
the multF of F is V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
the multF of F . (x,(1. F)) is Element of the carrier of F
(1. F) * x is Element of the carrier of F
the multF of F . ((1. F),x) is Element of the carrier of F
V is non empty commutative multMagma
the carrier of V is non empty set
v is Element of the carrier of V
w is Element of the carrier of V
v * w is Element of the carrier of V
the multF of V is V6() V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is set
the multF of V . (v,w) is Element of the carrier of V
w * v is Element of the carrier of V
the multF of V . (w,v) is Element of the carrier of V
F is non empty multLoopStr
the carrier of F is non empty set
x is Element of the carrier of F
1. F is Element of the carrier of F
the OneF of F is Element of the carrier of F
x * (1. F) is Element of the carrier of F
the multF of F is V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
the multF of F . (x,(1. F)) is Element of the carrier of F
(1. F) * x is Element of the carrier of F
the multF of F . ((1. F),x) is Element of the carrier of F
V is non empty commutative multMagma
the carrier of V is non empty set
v is Element of the carrier of V
w is Element of the carrier of V
v * w is Element of the carrier of V
the multF of V is V6() V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is set
the multF of V . (v,w) is Element of the carrier of V
w * v is Element of the carrier of V
the multF of V . (w,v) is Element of the carrier of V

the carrier of F is non empty set
x is right_complementable Element of the carrier of F
V is right_complementable Element of the carrier of F
x + V is right_complementable Element of the carrier of F
the addF of F is V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
the addF of F . (x,V) is right_complementable Element of the carrier of F
v is right_complementable Element of the carrier of F
v - V is right_complementable Element of the carrier of F
- V is right_complementable Element of the carrier of F
v + (- V) is right_complementable Element of the carrier of F
the addF of F . (v,(- V)) is right_complementable Element of the carrier of F
0. F is V46(F) right_complementable Element of the carrier of F
the ZeroF of F is right_complementable Element of the carrier of F
x + (0. F) is right_complementable Element of the carrier of F
the addF of F . (x,(0. F)) is right_complementable Element of the carrier of F
V + (- V) is right_complementable Element of the carrier of F
the addF of F . (V,(- V)) is right_complementable Element of the carrier of F
x + (V + (- V)) is right_complementable Element of the carrier of F
the addF of F . (x,(V + (- V))) is right_complementable Element of the carrier of F

the carrier of F is non empty set
x is right_complementable Element of the carrier of F
V is right_complementable Element of the carrier of F
v is right_complementable Element of the carrier of F
V - v is right_complementable Element of the carrier of F
- v is right_complementable Element of the carrier of F
V + (- v) is right_complementable Element of the carrier of F
the addF of F is V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
the addF of F . (V,(- v)) is right_complementable Element of the carrier of F
x + v is right_complementable Element of the carrier of F
the addF of F . (x,v) is right_complementable Element of the carrier of F
v + (- v) is right_complementable Element of the carrier of F
the addF of F . (v,(- v)) is right_complementable Element of the carrier of F
V + (v + (- v)) is right_complementable Element of the carrier of F
the addF of F . (V,(v + (- v))) is right_complementable Element of the carrier of F
0. F is V46(F) right_complementable Element of the carrier of F
the ZeroF of F is right_complementable Element of the carrier of F
V + (0. F) is right_complementable Element of the carrier of F
the addF of F . (V,(0. F)) is right_complementable Element of the carrier of F

the carrier of F is non empty set

the carrier of w is non empty set

the carrier of v is non empty set

the carrier of c13 is non empty set
x is right_complementable Element of the carrier of F
V is right_complementable Element of the carrier of F
x + V is right_complementable Element of the carrier of F
the addF of F is V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
the addF of F . (x,V) is right_complementable Element of the carrier of F
v is right_complementable Element of the carrier of F
v - V is right_complementable Element of the carrier of F
- V is right_complementable Element of the carrier of F
v + (- V) is right_complementable Element of the carrier of F
the addF of F . (v,(- V)) is right_complementable Element of the carrier of F
y is right_complementable Element of the carrier of w
q is right_complementable Element of the carrier of w
p is right_complementable Element of the carrier of w
q - p is right_complementable Element of the carrier of w
- p is right_complementable Element of the carrier of w
q + (- p) is right_complementable Element of the carrier of w
the addF of w is V6() V18([: the carrier of w, the carrier of w:], the carrier of w) Element of bool [:[: the carrier of w, the carrier of w:], the carrier of w:]
[: the carrier of w, the carrier of w:] is set
[:[: the carrier of w, the carrier of w:], the carrier of w:] is set
bool [:[: the carrier of w, the carrier of w:], the carrier of w:] is set
the addF of w . (q,(- p)) is right_complementable Element of the carrier of w
y + p is right_complementable Element of the carrier of w
the addF of w . (y,p) is right_complementable Element of the carrier of w
w is right_complementable Element of the carrier of v
c11 is right_complementable Element of the carrier of v
w + c11 is right_complementable Element of the carrier of v
the addF of v is V6() V18([: the carrier of v, the carrier of v:], the carrier of v) Element of bool [:[: the carrier of v, the carrier of v:], the carrier of v:]
[: the carrier of v, the carrier of v:] is set
[:[: the carrier of v, the carrier of v:], the carrier of v:] is set
bool [:[: the carrier of v, the carrier of v:], the carrier of v:] is set
the addF of v . (w,c11) is right_complementable Element of the carrier of v
c12 is right_complementable Element of the carrier of v
c12 - w is right_complementable Element of the carrier of v
- w is right_complementable Element of the carrier of v
c12 + (- w) is right_complementable Element of the carrier of v
the addF of v . (c12,(- w)) is right_complementable Element of the carrier of v
c15 is right_complementable Element of the carrier of c13
c16 is right_complementable Element of the carrier of c13
c14 is right_complementable Element of the carrier of c13
c16 - c14 is right_complementable Element of the carrier of c13
- c14 is right_complementable Element of the carrier of c13
c16 + (- c14) is right_complementable Element of the carrier of c13
the addF of c13 is V6() V18([: the carrier of c13, the carrier of c13:], the carrier of c13) Element of bool [:[: the carrier of c13, the carrier of c13:], the carrier of c13:]
[: the carrier of c13, the carrier of c13:] is set
[:[: the carrier of c13, the carrier of c13:], the carrier of c13:] is set
bool [:[: the carrier of c13, the carrier of c13:], the carrier of c13:] is set
the addF of c13 . (c16,(- c14)) is right_complementable Element of the carrier of c13
c14 + c15 is right_complementable Element of the carrier of c13
the addF of c13 . (c14,c15) is right_complementable Element of the carrier of c13

the carrier of F is non empty set
0. F is V46(F) right_complementable Element of the carrier of F
the ZeroF of F is right_complementable Element of the carrier of F
x is right_complementable Element of the carrier of F
- x is right_complementable Element of the carrier of F
- (- x) is right_complementable Element of the carrier of F

the carrier of F is non empty set
x is right_complementable Element of the carrier of F
V is right_complementable Element of the carrier of F
- V is right_complementable Element of the carrier of F
(- V) + x is right_complementable Element of the carrier of F
the addF of F is V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
the addF of F . ((- V),x) is right_complementable Element of the carrier of F
v is right_complementable Element of the carrier of F
V + v is right_complementable Element of the carrier of F
the addF of F . (V,v) is right_complementable Element of the carrier of F
v + V is right_complementable Element of the carrier of F
the addF of F . (v,V) is right_complementable Element of the carrier of F
(- V) + V is right_complementable Element of the carrier of F
the addF of F . ((- V),V) is right_complementable Element of the carrier of F
x + ((- V) + V) is right_complementable Element of the carrier of F
the addF of F . (x,((- V) + V)) is right_complementable Element of the carrier of F
0. F is V46(F) right_complementable Element of the carrier of F
the ZeroF of F is right_complementable Element of the carrier of F
x + (0. F) is right_complementable Element of the carrier of F
the addF of F . (x,(0. F)) is right_complementable Element of the carrier of F

the carrier of F is non empty non trivial set
x is right_complementable Element of the carrier of F
V is right_complementable Element of the carrier of F
x * V is right_complementable Element of the carrier of F
the multF of F is V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
the multF of F . (x,V) is right_complementable Element of the carrier of F
1. F is V46(F) right_complementable Element of the carrier of F
the OneF of F is right_complementable Element of the carrier of F
0. F is V46(F) right_complementable Element of the carrier of F
the ZeroF of F is right_complementable Element of the carrier of F

the carrier of F is non empty non trivial set
0. F is V46(F) right_complementable Element of the carrier of F
the ZeroF of F is right_complementable Element of the carrier of F
1. F is V46(F) right_complementable Element of the carrier of F
the OneF of F is right_complementable Element of the carrier of F
x is right_complementable Element of the carrier of F
V is right_complementable Element of the carrier of F
V * x is right_complementable Element of the carrier of F
the multF of F is V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
the multF of F . (V,x) is right_complementable Element of the carrier of F
x * V is right_complementable Element of the carrier of F
the multF of F . (x,V) is right_complementable Element of the carrier of F
v is right_complementable Element of the carrier of F
v * V is right_complementable Element of the carrier of F
the multF of F . (v,V) is right_complementable Element of the carrier of F
v * (V * x) is right_complementable Element of the carrier of F
the multF of F . (v,(V * x)) is right_complementable Element of the carrier of F
(1. F) * x is right_complementable Element of the carrier of F
the multF of F . ((1. F),x) is right_complementable Element of the carrier of F

the carrier of F is non empty non trivial set
1. F is V46(F) right_complementable Element of the carrier of F
the OneF of F is right_complementable Element of the carrier of F
V is right_complementable Element of the carrier of F
x is right_complementable Element of the carrier of F
V * x is right_complementable Element of the carrier of F
the multF of F is V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
the multF of F . (V,x) is right_complementable Element of the carrier of F
x * V is right_complementable Element of the carrier of F
the multF of F . (x,V) is right_complementable Element of the carrier of F
0. F is V46(F) right_complementable Element of the carrier of F
the ZeroF of F is right_complementable Element of the carrier of F
1_ F is right_complementable Element of the carrier of F
v is right_complementable Element of the carrier of F
x * v is right_complementable Element of the carrier of F
the multF of F . (x,v) is right_complementable Element of the carrier of F
V * (x * v) is right_complementable Element of the carrier of F
the multF of F . (V,(x * v)) is right_complementable Element of the carrier of F
(1_ F) * v is right_complementable Element of the carrier of F
the multF of F . ((1_ F),v) is right_complementable Element of the carrier of F

the carrier of F is non empty non trivial set
0. F is V46(F) right_complementable Element of the carrier of F
the ZeroF of F is right_complementable Element of the carrier of F
x is right_complementable Element of the carrier of F
V is right_complementable Element of the carrier of F
x * V is right_complementable Element of the carrier of F
the multF of F is V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
the multF of F . (x,V) is right_complementable Element of the carrier of F
v is right_complementable Element of the carrier of F
x * v is right_complementable Element of the carrier of F
the multF of F . (x,v) is right_complementable Element of the carrier of F
1_ F is right_complementable Element of the carrier of F
1. F is V46(F) right_complementable Element of the carrier of F
the OneF of F is right_complementable Element of the carrier of F
w is right_complementable Element of the carrier of F
x * w is right_complementable Element of the carrier of F
the multF of F . (x,w) is right_complementable Element of the carrier of F
w * x is right_complementable Element of the carrier of F
the multF of F . (w,x) is right_complementable Element of the carrier of F
(w * x) * V is right_complementable Element of the carrier of F
the multF of F . ((w * x),V) is right_complementable Element of the carrier of F
w * (x * v) is right_complementable Element of the carrier of F
the multF of F . (w,(x * v)) is right_complementable Element of the carrier of F
(1_ F) * v is right_complementable Element of the carrier of F
the multF of F . ((1_ F),v) is right_complementable Element of the carrier of F

the carrier of F is non empty non trivial set
x is right_complementable Element of the carrier of F
0. F is V46(F) right_complementable Element of the carrier of F
the ZeroF of F is right_complementable Element of the carrier of F
x " is right_complementable Element of the carrier of F
1. F is V46(F) right_complementable Element of the carrier of F
the OneF of F is right_complementable Element of the carrier of F
V is right_complementable Element of the carrier of F
V * x is right_complementable Element of the carrier of F
the multF of F is V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
the multF of F . (V,x) is right_complementable Element of the carrier of F
v is right_complementable Element of the carrier of F
v * x is right_complementable Element of the carrier of F
the multF of F . (v,x) is right_complementable Element of the carrier of F
x * v is right_complementable Element of the carrier of F
the multF of F . (x,v) is right_complementable Element of the carrier of F
w is right_complementable Element of the carrier of F
x * w is right_complementable Element of the carrier of F
the multF of F . (x,w) is right_complementable Element of the carrier of F
y is right_complementable Element of the carrier of F
y * x is right_complementable Element of the carrier of F
the multF of F . (y,x) is right_complementable Element of the carrier of F
p is right_complementable Element of the carrier of F
p * x is right_complementable Element of the carrier of F
the multF of F . (p,x) is right_complementable Element of the carrier of F
y * (1. F) is right_complementable Element of the carrier of F
the multF of F . (y,(1. F)) is right_complementable Element of the carrier of F
(p * x) * w is right_complementable Element of the carrier of F
the multF of F . ((p * x),w) is right_complementable Element of the carrier of F
p * (1. F) is right_complementable Element of the carrier of F
the multF of F . (p,(1. F)) is right_complementable Element of the carrier of F

the carrier of F is non empty non trivial set
x is right_complementable Element of the carrier of F
V is right_complementable Element of the carrier of F
V " is right_complementable Element of the carrier of F
x * (V ") is right_complementable Element of the carrier of F
the multF of F is V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
the multF of F . (x,(V ")) is right_complementable Element of the carrier of F

the carrier of F is non empty non trivial set
0. F is V46(F) right_complementable Element of the carrier of F
the ZeroF of F is right_complementable Element of the carrier of F
1. F is V46(F) right_complementable Element of the carrier of F
the OneF of F is right_complementable Element of the carrier of F
x is right_complementable Element of the carrier of F
x " is right_complementable Element of the carrier of F
x * (x ") is right_complementable Element of the carrier of F
the multF of F is V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
the multF of F . (x,(x ")) is right_complementable Element of the carrier of F
(x ") * x is right_complementable Element of the carrier of F
the multF of F . ((x "),x) is right_complementable Element of the carrier of F
1_ F is right_complementable Element of the carrier of F

the carrier of F is non empty non trivial set
1_ F is right_complementable Element of the carrier of F
1. F is V46(F) right_complementable Element of the carrier of F
the OneF of F is right_complementable Element of the carrier of F
x is right_complementable Element of the carrier of F
x " is right_complementable Element of the carrier of F
V is right_complementable Element of the carrier of F
x * V is right_complementable Element of the carrier of F
the multF of F is V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
the multF of F . (x,V) is right_complementable Element of the carrier of F
V " is right_complementable Element of the carrier of F
0. F is V46(F) right_complementable Element of the carrier of F
the ZeroF of F is right_complementable Element of the carrier of F
0. F is V46(F) right_complementable Element of the carrier of F
the ZeroF of F is right_complementable Element of the carrier of F
V * x is right_complementable Element of the carrier of F
the multF of F . (V,x) is right_complementable Element of the carrier of F

the carrier of F is non empty non trivial set
0. F is V46(F) right_complementable Element of the carrier of F
the ZeroF of F is right_complementable Element of the carrier of F
x is right_complementable Element of the carrier of F
x " is right_complementable Element of the carrier of F
V is right_complementable Element of the carrier of F
V " is right_complementable Element of the carrier of F
(x ") * (V ") is right_complementable Element of the carrier of F
the multF of F is V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
the multF of F . ((x "),(V ")) is right_complementable Element of the carrier of F
V * x is right_complementable Element of the carrier of F
the multF of F . (V,x) is right_complementable Element of the carrier of F
(V * x) " is right_complementable Element of the carrier of F
((x ") * (V ")) * (V * x) is right_complementable Element of the carrier of F
the multF of F . (((x ") * (V ")),(V * x)) is right_complementable Element of the carrier of F
(V ") * (V * x) is right_complementable Element of the carrier of F
the multF of F . ((V "),(V * x)) is right_complementable Element of the carrier of F
(x ") * ((V ") * (V * x)) is right_complementable Element of the carrier of F
the multF of F . ((x "),((V ") * (V * x))) is right_complementable Element of the carrier of F
(V ") * V is right_complementable Element of the carrier of F
the multF of F . ((V "),V) is right_complementable Element of the carrier of F
((V ") * V) * x is right_complementable Element of the carrier of F
the multF of F . (((V ") * V),x) is right_complementable Element of the carrier of F
(x ") * (((V ") * V) * x) is right_complementable Element of the carrier of F
the multF of F . ((x "),(((V ") * V) * x)) is right_complementable Element of the carrier of F
1_ F is right_complementable Element of the carrier of F
1. F is V46(F) right_complementable Element of the carrier of F
the OneF of F is right_complementable Element of the carrier of F
(1_ F) * x is right_complementable Element of the carrier of F
the multF of F . ((1_ F),x) is right_complementable Element of the carrier of F
(x ") * ((1_ F) * x) is right_complementable Element of the carrier of F
the multF of F . ((x "),((1_ F) * x)) is right_complementable Element of the carrier of F
(x ") * x is right_complementable Element of the carrier of F
the multF of F . ((x "),x) is right_complementable Element of the carrier of F

the carrier of F is non empty non trivial set
0. F is V46(F) right_complementable Element of the carrier of F
the ZeroF of F is right_complementable Element of the carrier of F
x is right_complementable Element of the carrier of F
V is right_complementable Element of the carrier of F
x * V is right_complementable Element of the carrier of F
the multF of F is V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
the multF of F . (x,V) is right_complementable Element of the carrier of F
x * (0. F) is right_complementable Element of the carrier of F
the multF of F . (x,(0. F)) is right_complementable Element of the carrier of F

the carrier of F is non empty non trivial set
0. F is V46(F) right_complementable Element of the carrier of F
the ZeroF of F is right_complementable Element of the carrier of F
x is right_complementable Element of the carrier of F
x " is right_complementable Element of the carrier of F
x * (x ") is right_complementable Element of the carrier of F
the multF of F is V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
the multF of F . (x,(x ")) is right_complementable Element of the carrier of F
1. F is V46(F) right_complementable Element of the carrier of F
the OneF of F is right_complementable Element of the carrier of F

the carrier of F is non empty non trivial set
0. F is V46(F) right_complementable Element of the carrier of F
the ZeroF of F is right_complementable Element of the carrier of F
x is right_complementable Element of the carrier of F
x " is right_complementable Element of the carrier of F
(x ") " is right_complementable Element of the carrier of F
1_ F is right_complementable Element of the carrier of F
1. F is V46(F) right_complementable Element of the carrier of F
the OneF of F is right_complementable Element of the carrier of F
((x ") ") * (1_ F) is right_complementable Element of the carrier of F
the multF of F is V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
the multF of F . (((x ") "),(1_ F)) is right_complementable Element of the carrier of F
(x ") * x is right_complementable Element of the carrier of F
the multF of F . ((x "),x) is right_complementable Element of the carrier of F
((x ") ") * ((x ") * x) is right_complementable Element of the carrier of F
the multF of F . (((x ") "),((x ") * x)) is right_complementable Element of the carrier of F
((x ") ") * (x ") is right_complementable Element of the carrier of F
the multF of F . (((x ") "),(x ")) is right_complementable Element of the carrier of F
(((x ") ") * (x ")) * x is right_complementable Element of the carrier of F
the multF of F . ((((x ") ") * (x ")),x) is right_complementable Element of the carrier of F
(1_ F) * x is right_complementable Element of the carrier of F
the multF of F . ((1_ F),x) is right_complementable Element of the carrier of F

the carrier of F is non empty non trivial set
0. F is V46(F) right_complementable Element of the carrier of F
the ZeroF of F is right_complementable Element of the carrier of F
1_ F is right_complementable Element of the carrier of F
1. F is V46(F) right_complementable Element of the carrier of F
the OneF of F is right_complementable Element of the carrier of F
x is right_complementable Element of the carrier of F
(F,(1_ F),x) is right_complementable Element of the carrier of F
x " is right_complementable Element of the carrier of F
(1_ F) * (x ") is right_complementable Element of the carrier of F
the multF of F is V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
the multF of F . ((1_ F),(x ")) is right_complementable Element of the carrier of F
(F,(1_ F),(x ")) is right_complementable Element of the carrier of F
(x ") " is right_complementable Element of the carrier of F
(1_ F) * ((x ") ") is right_complementable Element of the carrier of F
the multF of F . ((1_ F),((x ") ")) is right_complementable Element of the carrier of F

the carrier of F is non empty non trivial set
0. F is V46(F) right_complementable Element of the carrier of F
the ZeroF of F is right_complementable Element of the carrier of F
1_ F is right_complementable Element of the carrier of F
1. F is V46(F) right_complementable Element of the carrier of F
the OneF of F is right_complementable Element of the carrier of F
x is right_complementable Element of the carrier of F
(F,(1_ F),x) is right_complementable Element of the carrier of F
x " is right_complementable Element of the carrier of F
(1_ F) * (x ") is right_complementable Element of the carrier of F
the multF of F is V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
the multF of F . ((1_ F),(x ")) is right_complementable Element of the carrier of F
x * (F,(1_ F),x) is right_complementable Element of the carrier of F
the multF of F . (x,(F,(1_ F),x)) is right_complementable Element of the carrier of F
(F,(1_ F),x) * x is right_complementable Element of the carrier of F
the multF of F . ((F,(1_ F),x),x) is right_complementable Element of the carrier of F
x * (x ") is right_complementable Element of the carrier of F
the multF of F . (x,(x ")) is right_complementable Element of the carrier of F
(x ") * x is right_complementable Element of the carrier of F
the multF of F . ((x "),x) is right_complementable Element of the carrier of F

the carrier of F is non empty non trivial set
x is right_complementable Element of the carrier of F
0. F is V46(F) right_complementable Element of the carrier of F
the ZeroF of F is right_complementable Element of the carrier of F
(F,x,x) is right_complementable Element of the carrier of F
x " is right_complementable Element of the carrier of F
x * (x ") is right_complementable Element of the carrier of F
the multF of F is V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
the multF of F . (x,(x ")) is right_complementable Element of the carrier of F
1_ F is right_complementable Element of the carrier of F
1. F is V46(F) right_complementable Element of the carrier of F
the OneF of F is right_complementable Element of the carrier of F

the carrier of F is non empty non trivial set
0. F is V46(F) right_complementable Element of the carrier of F
the ZeroF of F is right_complementable Element of the carrier of F
x is right_complementable Element of the carrier of F
V is right_complementable Element of the carrier of F
x * V is right_complementable Element of the carrier of F
the multF of F is V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
the multF of F . (x,V) is right_complementable Element of the carrier of F
v is right_complementable Element of the carrier of F
(F,v,x) is right_complementable Element of the carrier of F
x " is right_complementable Element of the carrier of F
v * (x ") is right_complementable Element of the carrier of F
the multF of F . (v,(x ")) is right_complementable Element of the carrier of F
v * V is right_complementable Element of the carrier of F
the multF of F . (v,V) is right_complementable Element of the carrier of F
(F,(v * V),(x * V)) is right_complementable Element of the carrier of F
(x * V) " is right_complementable Element of the carrier of F
(v * V) * ((x * V) ") is right_complementable Element of the carrier of F
the multF of F . ((v * V),((x * V) ")) is right_complementable Element of the carrier of F
1_ F is right_complementable Element of the carrier of F
1. F is V46(F) right_complementable Element of the carrier of F
the OneF of F is right_complementable Element of the carrier of F
v * (1_ F) is right_complementable Element of the carrier of F
the multF of F . (v,(1_ F)) is right_complementable Element of the carrier of F
(v * (1_ F)) * (x ") is right_complementable Element of the carrier of F
the multF of F . ((v * (1_ F)),(x ")) is right_complementable Element of the carrier of F
V " is right_complementable Element of the carrier of F
V * (V ") is right_complementable Element of the carrier of F
the multF of F . (V,(V ")) is right_complementable Element of the carrier of F
v * (V * (V ")) is right_complementable Element of the carrier of F
the multF of F . (v,(V * (V "))) is right_complementable Element of the carrier of F
(v * (V * (V "))) * (x ") is right_complementable Element of the carrier of F
the multF of F . ((v * (V * (V "))),(x ")) is right_complementable Element of the carrier of F
(v * V) * (V ") is right_complementable Element of the carrier of F
the multF of F . ((v * V),(V ")) is right_complementable Element of the carrier of F
((v * V) * (V ")) * (x ") is right_complementable Element of the carrier of F
the multF of F . (((v * V) * (V ")),(x ")) is right_complementable Element of the carrier of F
(V ") * (x ") is right_complementable Element of the carrier of F
the multF of F . ((V "),(x ")) is right_complementable Element of the carrier of F
(v * V) * ((V ") * (x ")) is right_complementable Element of the carrier of F
the multF of F . ((v * V),((V ") * (x "))) is right_complementable Element of the carrier of F

the carrier of F is non empty non trivial set
0. F is V46(F) right_complementable Element of the carrier of F
the ZeroF of F is right_complementable Element of the carrier of F
x is right_complementable Element of the carrier of F
- x is right_complementable Element of the carrier of F
V is right_complementable Element of the carrier of F
(F,V,x) is right_complementable Element of the carrier of F
x " is right_complementable Element of the carrier of F
V * (x ") is right_complementable Element of the carrier of F
the multF of F is V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
the multF of F . (V,(x ")) is right_complementable Element of the carrier of F
- (F,V,x) is right_complementable Element of the carrier of F
- V is right_complementable Element of the carrier of F
(F,(- V),x) is right_complementable Element of the carrier of F
(- V) * (x ") is right_complementable Element of the carrier of F
the multF of F . ((- V),(x ")) is right_complementable Element of the carrier of F
(F,V,(- x)) is right_complementable Element of the carrier of F
(- x) " is right_complementable Element of the carrier of F
V * ((- x) ") is right_complementable Element of the carrier of F
the multF of F . (V,((- x) ")) is right_complementable Element of the carrier of F
1. F is V46(F) right_complementable Element of the carrier of F
the OneF of F is right_complementable Element of the carrier of F
- (1. F) is right_complementable Element of the carrier of F
1_ F is right_complementable Element of the carrier of F
- (1_ F) is right_complementable Element of the carrier of F
V * (- (1_ F)) is right_complementable Element of the carrier of F
the multF of F . (V,(- (1_ F))) is right_complementable Element of the carrier of F
(- x) * (- (1_ F)) is right_complementable Element of the carrier of F
the multF of F . ((- x),(- (1_ F))) is right_complementable Element of the carrier of F
(F,(V * (- (1_ F))),((- x) * (- (1_ F)))) is right_complementable Element of the carrier of F
((- x) * (- (1_ F))) " is right_complementable Element of the carrier of F
(V * (- (1_ F))) * (((- x) * (- (1_ F))) ") is right_complementable Element of the carrier of F
the multF of F . ((V * (- (1_ F))),(((- x) * (- (1_ F))) ")) is right_complementable Element of the carrier of F
V * (1_ F) is right_complementable Element of the carrier of F
the multF of F . (V,(1_ F)) is right_complementable Element of the carrier of F
- (V * (1_ F)) is right_complementable Element of the carrier of F
(F,(- (V * (1_ F))),((- x) * (- (1_ F)))) is right_complementable Element of the carrier of F
(- (V * (1_ F))) * (((- x) * (- (1_ F))) ") is right_complementable Element of the carrier of F
the multF of F . ((- (V * (1_ F))),(((- x) * (- (1_ F))) ")) is right_complementable Element of the carrier of F
(F,(- V),((- x) * (- (1_ F)))) is right_complementable Element of the carrier of F
(- V) * (((- x) * (- (1_ F))) ") is right_complementable Element of the carrier of F
the multF of F . ((- V),(((- x) * (- (1_ F))) ")) is right_complementable Element of the carrier of F
(- x) * (1_ F) is right_complementable Element of the carrier of F
the multF of F . ((- x),(1_ F)) is right_complementable Element of the carrier of F
- ((- x) * (1_ F)) is right_complementable Element of the carrier of F
(F,(- V),(- ((- x) * (1_ F)))) is right_complementable Element of the carrier of F
(- ((- x) * (1_ F))) " is right_complementable Element of the carrier of F
(- V) * ((- ((- x) * (1_ F))) ") is right_complementable Element of the carrier of F
the multF of F . ((- V),((- ((- x) * (1_ F))) ")) is right_complementable Element of the carrier of F
- (- x) is right_complementable Element of the carrier of F
(- (- x)) * (1_ F) is right_complementable Element of the carrier of F
the multF of F . ((- (- x)),(1_ F)) is right_complementable Element of the carrier of F
(F,(- V),((- (- x)) * (1_ F))) is right_complementable Element of the carrier of F
((- (- x)) * (1_ F)) " is right_complementable Element of the carrier of F
(- V) * (((- (- x)) * (1_ F)) ") is right_complementable Element of the carrier of F
the multF of F . ((- V),(((- (- x)) * (1_ F)) ")) is right_complementable Element of the carrier of F
x * (1_ F) is right_complementable Element of the carrier of F
the multF of F . (x,(1_ F)) is right_complementable Element of the carrier of F
(F,(- V),(x * (1_ F))) is right_complementable Element of the carrier of F
(x * (1_ F)) " is right_complementable Element of the carrier of F
(- V) * ((x * (1_ F)) ") is right_complementable Element of the carrier of F
the multF of F . ((- V),((x * (1_ F)) ")) is right_complementable Element of the carrier of F

the carrier of F is non empty non trivial set
0. F is V46(F) right_complementable Element of the carrier of F
the ZeroF of F is right_complementable Element of the carrier of F
x is right_complementable Element of the carrier of F
V is right_complementable Element of the carrier of F
(F,V,x) is right_complementable Element of the carrier of F
x " is right_complementable Element of the carrier of F
V * (x ") is right_complementable Element of the carrier of F
the multF of F is V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
the multF of F . (V,(x ")) is right_complementable Element of the carrier of F
v is right_complementable Element of the carrier of F
(F,v,x) is right_complementable Element of the carrier of F
v * (x ") is right_complementable Element of the carrier of F
the multF of F . (v,(x ")) is right_complementable Element of the carrier of F
(F,V,x) + (F,v,x) is right_complementable Element of the carrier of F
the addF of F is V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
the addF of F . ((F,V,x),(F,v,x)) is right_complementable Element of the carrier of F
V + v is right_complementable Element of the carrier of F
the addF of F . (V,v) is right_complementable Element of the carrier of F
(F,(V + v),x) is right_complementable Element of the carrier of F
(V + v) * (x ") is right_complementable Element of the carrier of F
the multF of F . ((V + v),(x ")) is right_complementable Element of the carrier of F
(F,V,x) - (F,v,x) is right_complementable Element of the carrier of F
- (F,v,x) is right_complementable Element of the carrier of F
(F,V,x) + (- (F,v,x)) is right_complementable Element of the carrier of F
the addF of F . ((F,V,x),(- (F,v,x))) is right_complementable Element of the carrier of F
V - v is right_complementable Element of the carrier of F
- v is right_complementable Element of the carrier of F
V + (- v) is right_complementable Element of the carrier of F
the addF of F . (V,(- v)) is right_complementable Element of the carrier of F
(F,(V - v),x) is right_complementable Element of the carrier of F
(V - v) * (x ") is right_complementable Element of the carrier of F
the multF of F . ((V - v),(x ")) is right_complementable Element of the carrier of F
(F,(- v),x) is right_complementable Element of the carrier of F
(- v) * (x ") is right_complementable Element of the carrier of F
the multF of F . ((- v),(x ")) is right_complementable Element of the carrier of F
(F,V,x) + (F,(- v),x) is right_complementable Element of the carrier of F
the addF of F . ((F,V,x),(F,(- v),x)) is right_complementable Element of the carrier of F

the carrier of F is non empty non trivial set
0. F is V46(F) right_complementable Element of the carrier of F
the ZeroF of F is right_complementable Element of the carrier of F
x is right_complementable Element of the carrier of F
V is right_complementable Element of the carrier of F
(F,x,V) is right_complementable Element of the carrier of F
V " is right_complementable Element of the carrier of F
x * (V ") is right_complementable Element of the carrier of F
the multF of F is V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
the multF of F . (x,(V ")) is right_complementable Element of the carrier of F
v is right_complementable Element of the carrier of F
(F,v,(F,x,V)) is right_complementable Element of the carrier of F
(F,x,V) " is right_complementable Element of the carrier of F
v * ((F,x,V) ") is right_complementable Element of the carrier of F
the multF of F . (v,((F,x,V) ")) is right_complementable Element of the carrier of F
v * V is right_complementable Element of the carrier of F
the multF of F . (v,V) is right_complementable Element of the carrier of F
(F,(v * V),x) is right_complementable Element of the carrier of F
x " is right_complementable Element of the carrier of F
(v * V) * (x ") is right_complementable Element of the carrier of F
the multF of F . ((v * V),(x ")) is right_complementable Element of the carrier of F
(V ") " is right_complementable Element of the carrier of F
((V ") ") * (x ") is right_complementable Element of the carrier of F
the multF of F . (((V ") "),(x ")) is right_complementable Element of the carrier of F
v * (((V ") ") * (x ")) is right_complementable Element of the carrier of F
the multF of F . (v,(((V ") ") * (x "))) is right_complementable Element of the carrier of F
V * (x ") is right_complementable Element of the carrier of F
the multF of F . (V,(x ")) is right_complementable Element of the carrier of F
v * (V * (x ")) is right_complementable Element of the carrier of F
the multF of F . (v,(V * (x "))) is right_complementable Element of the carrier of F

the carrier of F is non empty non trivial set
0. F is V46(F) right_complementable Element of the carrier of F
the ZeroF of F is right_complementable Element of the carrier of F
x is right_complementable Element of the carrier of F
V is right_complementable Element of the carrier of F
(F,V,x) is right_complementable Element of the carrier of F
x " is right_complementable Element of the carrier of F
V * (x ") is right_complementable Element of the carrier of F
the multF of F is V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
the multF of F . (V,(x ")) is right_complementable Element of the carrier of F
(F,V,x) * x is right_complementable Element of the carrier of F
the multF of F . ((F,V,x),x) is right_complementable Element of the carrier of F
(x ") * x is right_complementable Element of the carrier of F
the multF of F . ((x "),x) is right_complementable Element of the carrier of F
V * ((x ") * x) is right_complementable Element of the carrier of F
the multF of F . (V,((x ") * x)) is right_complementable Element of the carrier of F
1_ F is right_complementable Element of the carrier of F
1. F is V46(F) right_complementable Element of the carrier of F
the OneF of F is right_complementable Element of the carrier of F
V * (1_ F) is right_complementable Element of the carrier of F
the multF of F . (V,(1_ F)) is right_complementable Element of the carrier of F
F is 1-sorted
the non empty set is non empty set
[: the non empty set , the non empty set :] is set
[:[: the non empty set , the non empty set :], the non empty set :] is set
bool [:[: the non empty set , the non empty set :], the non empty set :] is set
the V6() V18([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :] is V6() V18([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :]
the Element of the non empty set is Element of the non empty set
the carrier of F is set
[: the non empty set , the carrier of F:] is set
[:[: the non empty set , the carrier of F:], the non empty set :] is set
bool [:[: the non empty set , the carrier of F:], the non empty set :] is set
the V6() V18([: the non empty set , the carrier of F:], the non empty set ) Element of bool [:[: the non empty set , the carrier of F:], the non empty set :] is V6() V18([: the non empty set , the carrier of F:], the non empty set ) Element of bool [:[: the non empty set , the carrier of F:], the non empty set :]
(F, the non empty set , the V6() V18([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the Element of the non empty set , the V6() V18([: the non empty set , the carrier of F:], the non empty set ) Element of bool [:[: the non empty set , the carrier of F:], the non empty set :]) is (F) (F)
the carrier of (F, the non empty set , the V6() V18([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the Element of the non empty set , the V6() V18([: the non empty set , the carrier of F:], the non empty set ) Element of bool [:[: the non empty set , the carrier of F:], the non empty set :]) is set
x is non empty set
[:x,x:] is set
[:[:x,x:],x:] is set
bool [:[:x,x:],x:] is set
F is 1-sorted
the carrier of F is set
[:x, the carrier of F:] is set
[:[:x, the carrier of F:],x:] is set
bool [:[:x, the carrier of F:],x:] is set
V is V6() V18([:x,x:],x) Element of bool [:[:x,x:],x:]
v is Element of x
w is V6() V18([:x, the carrier of F:],x) Element of bool [:[:x, the carrier of F:],x:]
(F,x,V,v,w) is (F) (F)
F is non empty doubleLoopStr
F is 1-sorted
x is 1-sorted
the non empty set is non empty set
[: the non empty set , the non empty set :] is set
[:[: the non empty set , the non empty set :], the non empty set :] is set
bool [:[: the non empty set , the non empty set :], the non empty set :] is set
the V6() V18([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :] is V6() V18([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :]
the Element of the non empty set is Element of the non empty set
the carrier of F is set
[: the carrier of F, the non empty set :] is set
[:[: the carrier of F, the non empty set :], the non empty set :] is set
bool [:[: the carrier of F, the non empty set :], the non empty set :] is set
the V6() V18([: the carrier of F, the non empty set :], the non empty set ) Element of bool [:[: the carrier of F, the non empty set :], the non empty set :] is V6() V18([: the carrier of F, the non empty set :], the non empty set ) Element of bool [:[: the carrier of F, the non empty set :], the non empty set :]
the carrier of x is set
[: the non empty set , the carrier of x:] is set
[:[: the non empty set , the carrier of x:], the non empty set :] is set
bool [:[: the non empty set , the carrier of x:], the non empty set :] is set
the V6() V18([: the non empty set , the carrier of x:], the non empty set ) Element of bool [:[: the non empty set , the carrier of x:], the non empty set :] is V6() V18([: the non empty set , the carrier of x:], the non empty set ) Element of bool [:[: the non empty set , the carrier of x:], the non empty set :]
(F,x, the non empty set , the V6() V18([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the Element of the non empty set , the V6() V18([: the carrier of F, the non empty set :], the non empty set ) Element of bool [:[: the carrier of F, the non empty set :], the non empty set :], the V6() V18([: the non empty set , the carrier of x:], the non empty set ) Element of bool [:[: the non empty set , the carrier of x:], the non empty set :]) is (F,x) (F,x)
the carrier of (F,x, the non empty set , the V6() V18([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the Element of the non empty set , the V6() V18([: the carrier of F, the non empty set :], the non empty set ) Element of bool [:[: the carrier of F, the non empty set :], the non empty set :], the V6() V18([: the non empty set , the carrier of x:], the non empty set ) Element of bool [:[: the non empty set , the carrier of x:], the non empty set :]) is set
V is non empty set
[:V,V:] is set
[:[:V,V:],V:] is set
bool [:[:V,V:],V:] is set
F is 1-sorted
the carrier of F is set
[: the carrier of F,V:] is set
[:[: the carrier of F,V:],V:] is set
bool [:[: the carrier of F,V:],V:] is set
x is 1-sorted
the carrier of x is set
[:V, the carrier of x:] is set
[:[:V, the carrier of x:],V:] is set
bool [:[:V, the carrier of x:],V:] is set
v is V6() V18([:V,V:],V) Element of bool [:[:V,V:],V:]
w is Element of V
y is V6() V18([: the carrier of F,V:],V) Element of bool [:[: the carrier of F,V:],V:]
p is V6() V18([:V, the carrier of x:],V) Element of bool [:[:V, the carrier of x:],V:]
(F,x,V,v,w,y,p) is (F,x) (F,x)

the carrier of F is non empty set
the addF of F is V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
0. F is V46(F) right_complementable Element of the carrier of F
the ZeroF of F is right_complementable Element of the carrier of F
the carrier of x is non empty set
0. x is V46(x) Element of the carrier of x
the ZeroF of x is Element of the carrier of x
V is Element of the carrier of x
v is Element of the carrier of x
V + v is Element of the carrier of x
the addF of x is V6() V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is set
the addF of x . (V,v) is Element of the carrier of x
v + V is Element of the carrier of x
the addF of x . (v,V) is Element of the carrier of x
w is Element of the carrier of x
(V + v) + w is Element of the carrier of x
the addF of x . ((V + v),w) is Element of the carrier of x
v + w is Element of the carrier of x
the addF of x . (v,w) is Element of the carrier of x
V + (v + w) is Element of the carrier of x
the addF of x . (V,(v + w)) is Element of the carrier of x
V + (0. x) is Element of the carrier of x
the addF of x . (V,(0. x)) is Element of the carrier of x
p is right_complementable Element of the carrier of F
y is right_complementable Element of the carrier of F
p + y is right_complementable Element of the carrier of F
the addF of F . (p,y) is right_complementable Element of the carrier of F
y + p is right_complementable Element of the carrier of F
the addF of F . (y,p) is right_complementable Element of the carrier of F
q is right_complementable Element of the carrier of F
(y + p) + q is right_complementable Element of the carrier of F
the addF of F . ((y + p),q) is right_complementable Element of the carrier of F
p + q is right_complementable Element of the carrier of F
the addF of F . (p,q) is right_complementable Element of the carrier of F
y + (p + q) is right_complementable Element of the carrier of F
the addF of F . (y,(p + q)) is right_complementable Element of the carrier of F
y + (0. F) is right_complementable Element of the carrier of F
the addF of F . (y,(0. F)) is right_complementable Element of the carrier of F
v is right_complementable Element of the carrier of F
y + v is right_complementable Element of the carrier of F
the addF of F . (y,v) is right_complementable Element of the carrier of F
w is Element of the carrier of x
V + w is Element of the carrier of x
the addF of x . (V,w) is Element of the carrier of x
V is Element of the carrier of x
v is right_complementable Element of the carrier of F
w is right_complementable Element of the carrier of F
v + w is right_complementable Element of the carrier of F
the addF of F . (v,w) is right_complementable Element of the carrier of F
y is Element of the carrier of x
V + y is Element of the carrier of x
the addF of x is V6() V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is set
the addF of x . (V,y) is Element of the carrier of x

the carrier of F is non empty set
the addF of F is V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
0. F is V46(F) right_complementable Element of the carrier of F
the ZeroF of F is right_complementable Element of the carrier of F
the multF of F is V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
VectSpStr(# the carrier of F, the addF of F,(0. F), the multF of F #) is non empty strict VectSpStr over F
the carrier of H1(F) is non empty set
x is right_complementable Element of the carrier of F
w is Element of the carrier of H1(F)
V is right_complementable Element of the carrier of F
y is Element of the carrier of H1(F)
v is right_complementable Element of the carrier of F
p is Element of the carrier of H1(F)
x + V is right_complementable Element of the carrier of F
the addF of F . (x,V) is right_complementable Element of the carrier of F
w + y is Element of the carrier of VectSpStr(# the carrier of F, the addF of F,(0. F), the multF of F #)
the carrier of VectSpStr(# the carrier of F, the addF of F,(0. F), the multF of F #) is non empty set
the addF of VectSpStr(# the carrier of F, the addF of F,(0. F), the multF of F #) is V6() V18([: the carrier of VectSpStr(# the carrier of F, the addF of F,(0. F), the multF of F #), the carrier of VectSpStr(# the carrier of F, the addF of F,(0. F), the multF of F #):], the carrier of VectSpStr(# the carrier of F, the addF of F,(0. F), the multF of F #)) Element of bool [:[: the carrier of VectSpStr(# the carrier of F, the addF of F,(0. F), the multF of F #), the carrier of VectSpStr(# the carrier of F, the addF of F,(0. F), the multF of F #):], the carrier of VectSpStr(# the carrier of F, the addF of F,(0. F), the multF of F #):]
[: the carrier of VectSpStr(# the carrier of F, the addF of F,(0. F), the multF of F #), the carrier of VectSpStr(# the carrier of F, the addF of F,(0. F), the multF of F #):] is set
[:[: the carrier of VectSpStr(# the carrier of F, the addF of F,(0. F), the multF of F #), the carrier of VectSpStr(# the carrier of F, the addF of F,(0. F), the multF of F #):], the carrier of VectSpStr(# the carrier of F, the addF of F,(0. F), the multF of F #):] is set
bool [:[: the carrier of VectSpStr(# the carrier of F, the addF of F,(0. F), the multF of F #), the carrier of VectSpStr(# the carrier of F, the addF of F,(0. F), the multF of F #):], the carrier of VectSpStr(# the carrier of F, the addF of F,(0. F), the multF of F #):] is set
the addF of VectSpStr(# the carrier of F, the addF of F,(0. F), the multF of F #) . (w,y) is Element of the carrier of VectSpStr(# the carrier of F, the addF of F,(0. F), the multF of F #)
x is Element of the carrier of H1(F)
V is Element of the carrier of H1(F)
x + V is Element of the carrier of H1(F)
the carrier of