:: LMOD_7 semantic presentation

K149() is Element of bool K145()
K145() is set
bool K145() is non empty set
K144() is set
bool K144() is non empty set
bool K149() is non empty set
K118(K149()) is V27() set

the empty set is empty set
1 is non empty set
F1() is set
K is Element of F1()
V is Element of F1()
W is set
F1() is non empty set
[:F1(),F1():] is non empty set
bool [:F1(),F1():] is non empty set
K is V6() V18(F1(),F1()) Element of bool [:F1(),F1():]
V is V6() V18(F1(),F1()) Element of bool [:F1(),F1():]
W is Element of F1()
K . W is Element of F1()
F2(W) is set
V . W is Element of F1()
F1() is non empty set
[:F1(),F1(),F1():] is non empty set
[:[:F1(),F1(),F1():],F1():] is non empty set
bool [:[:F1(),F1(),F1():],F1():] is non empty set
K is V6() V18([:F1(),F1(),F1():],F1()) Element of bool [:[:F1(),F1(),F1():],F1():]
V is V6() V18([:F1(),F1(),F1():],F1()) Element of bool [:[:F1(),F1(),F1():],F1():]
W is Element of F1()
x is Element of F1()
y is Element of F1()
K . (W,x,y) is Element of F1()
F2(W,x,y) is set
V . (W,x,y) is Element of F1()
F1() is non empty set
[:F1(),F1(),F1(),F1():] is non empty set
[:[:F1(),F1(),F1(),F1():],F1():] is non empty set
bool [:[:F1(),F1(),F1(),F1():],F1():] is non empty set
K is V6() V18([:F1(),F1(),F1(),F1():],F1()) Element of bool [:[:F1(),F1(),F1(),F1():],F1():]
V is V6() V18([:F1(),F1(),F1(),F1():],F1()) Element of bool [:[:F1(),F1(),F1(),F1():],F1():]
W is Element of F1()
x is Element of F1()
y is Element of F1()
v is Element of F1()
K . (W,x,y,v) is Element of F1()
F2(W,x,y,v) is set
V . (W,x,y,v) is Element of F1()
F2() is non empty set
bool F2() is non empty set
F1() is non empty set
{ F3(b1) where b1 is Element of F1() : P1[b1] } is set
K is Element of bool F2()
F1() is non empty set
F2() is Element of F1()
{ b1 where b1 is Element of F1() : P1[b1] } is set
K is Element of F1()
F2() is non empty set
F1() is set
{ b1 where b1 is Element of F2() : P1[b1] } is set
F3() is Element of F2()
F2() is non empty set
F3() is Element of F2()
F1() is set
{ b1 where b1 is Element of F2() : P1[b1] } is set
F2() is set
F3() is non empty set
{ b1 where b1 is Element of F3() : P1[b1] } is set
F1() is set
K is Element of F3()
F1() is non empty set
F3() is set
F5(F3()) is set
{ b1 where b1 is Element of F1() : P2[b1,F3()] } is set
F4() is Element of F1()
F2() is non empty set
{ b1 where b1 is Element of F1() : S1[b1] } is set
K is Element of F2()
V is Element of F2()
K is Element of F2()

the carrier of K is non empty set
V is right_complementable Element of the carrier of K
W is right_complementable Element of the carrier of K
V - W is right_complementable Element of the carrier of K
- W is right_complementable Element of the carrier of K
V + (- W) is right_complementable Element of the carrier of K
the addF of K is V6() V18([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the addF of K . (V,(- W)) is right_complementable Element of the carrier of K
- (V - W) is right_complementable Element of the carrier of K
- V is right_complementable Element of the carrier of K
(- V) - (- W) is right_complementable Element of the carrier of K
- (- W) is right_complementable Element of the carrier of K
(- V) + (- (- W)) is right_complementable Element of the carrier of K
the addF of K . ((- V),(- (- W))) is right_complementable Element of the carrier of K
x is right_complementable Element of the carrier of K
(V - W) + x is right_complementable Element of the carrier of K
the addF of K . ((V - W),x) is right_complementable Element of the carrier of K
V + x is right_complementable Element of the carrier of K
the addF of K . (V,x) is right_complementable Element of the carrier of K
(V + x) - W is right_complementable Element of the carrier of K
(V + x) + (- W) is right_complementable Element of the carrier of K
the addF of K . ((V + x),(- W)) is right_complementable Element of the carrier of K
(- V) + W is right_complementable Element of the carrier of K
the addF of K . ((- V),W) is right_complementable Element of the carrier of K

the carrier of V is non empty set
bool the carrier of V is non empty set
0. V is V55(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
W is Element of bool the carrier of V
0. K is V55(K) right_complementable Element of the carrier of K
the carrier of K is non empty set
the ZeroF of K is right_complementable Element of the carrier of K
1_ K is right_complementable Element of the carrier of K
K184(K) is right_complementable Element of the carrier of K
the OneF of K is right_complementable Element of the carrier of K

the carrier of K is non empty set
0. K is V55(K) right_complementable Element of the carrier of K
the ZeroF of K is right_complementable Element of the carrier of K

the carrier of V is non empty set
bool the carrier of V is non empty set
W is right_complementable Element of the carrier of V
x is Element of bool the carrier of V
y is V6() V18( the carrier of V, the carrier of K) Linear_Combination of x
y . W is right_complementable Element of the carrier of K
Carrier y is V36() Element of bool the carrier of V

the carrier of K is non empty set

the carrier of V is non empty set
bool the carrier of V is non empty set
W is Element of bool the carrier of V

x is V6() V18( the carrier of V, the carrier of K) Linear_Combination of W
Carrier x is V36() Element of bool the carrier of V
the Element of Carrier x is Element of Carrier x
0. K is V55(K) right_complementable Element of the carrier of K
the ZeroF of K is right_complementable Element of the carrier of K
v is right_complementable Element of the carrier of V
x . v is right_complementable Element of the carrier of K
the carrier of (Lin W) is non empty set
x is right_complementable Element of the carrier of (Lin W)
y is V6() V18( the carrier of V, the carrier of K) Linear_Combination of W
Sum y is right_complementable Element of the carrier of V
Carrier y is V36() Element of bool the carrier of V
0. V is V55(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
0. (Lin W) is V55( Lin W) right_complementable Element of the carrier of (Lin W)
the ZeroF of (Lin W) is right_complementable Element of the carrier of (Lin W)

the carrier of V is non empty set
bool the carrier of V is non empty set
W is Element of bool the carrier of V
{} the carrier of V is empty proper Element of bool 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the ZeroF of V is right_complementable Element of the carrier of V
the lmult of V is V6() V18([: the carrier of K, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of K, the carrier of V:], the carrier of V:]
the carrier of K is non empty set
[: the carrier of K, the carrier of V:] is non empty set
[:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set
VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is non empty strict VectSpStr over K

the carrier of V is non empty set
bool the carrier of V is non empty set

W is Element of bool the carrier of V

x is Element of bool the carrier of V
W \/ x is Element of bool the carrier of V

W /\ x is Element of bool the carrier of V

the carrier of y is non empty set
the carrier of (Lin W) is non empty set
the carrier of (Lin x) is non empty set
the carrier of (Lin W) /\ the carrier of (Lin x) is set
w is set
the carrier of K is non empty set
a is V6() V18( the carrier of V, the carrier of K) Linear_Combination of W
Sum a is right_complementable Element of the carrier of V
b is V6() V18( the carrier of V, the carrier of K) Linear_Combination of x
Sum b is right_complementable Element of the carrier of V
Carrier a is V36() Element of bool the carrier of V
Carrier b is V36() Element of bool the carrier of V
() \/ () is Element of bool the carrier of V
a - b is V6() V18( the carrier of V, the carrier of K) Linear_Combination of V
Carrier (a - b) is V36() Element of bool the carrier of V
c is V6() V18( the carrier of V, the carrier of K) Linear_Combination of W \/ x
Sum c is right_complementable Element of the carrier of V
(Sum a) - (Sum b) is right_complementable Element of the carrier of V
- (Sum b) is right_complementable Element of the carrier of V
(Sum a) + (- (Sum b)) 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . ((Sum a),(- (Sum b))) is right_complementable Element of the carrier of V
0. V is V55(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
Carrier c is V36() Element of bool the carrier of V
the Element of Carrier a is Element of Carrier a
0. K is V55(K) right_complementable Element of the carrier of K
the ZeroF of K is right_complementable Element of the carrier of K
b is right_complementable Element of the carrier of V
a . b is right_complementable Element of the carrier of K
c . b is right_complementable Element of the carrier of K
b . b is right_complementable Element of the carrier of K
(a . b) - (b . b) is right_complementable Element of the carrier of K
- (b . b) is right_complementable Element of the carrier of K
(a . b) + (- (b . b)) is right_complementable Element of the carrier of K
the addF of K is V6() V18([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the addF of K . ((a . b),(- (b . b))) is right_complementable Element of the carrier of K
w is set
a is set
{(0. V)} is non empty Element of bool the carrier of V

the carrier of V is non empty set
bool the carrier of V is non empty set
W is Element of bool the carrier of V
x is Element of bool the carrier of V

y is Element of bool the carrier of V
x \/ y is Element of bool 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the ZeroF of V is right_complementable Element of the carrier of V
the lmult of V is V6() V18([: the carrier of K, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of K, the carrier of V:], the carrier of V:]
the carrier of K is non empty set
[: the carrier of K, the carrier of V:] is non empty set
[:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set
VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is non empty strict VectSpStr over K

{} is non empty set
y is set

Subspaces V is non empty set
W is set

W is non empty (K,V)
x is Element of W

W is non empty (K,V)

the carrier of V is non empty set
0. V is V55(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
W is right_complementable Element of the carrier of V

{} is non empty set
y is set

(K,V) is non empty (K,V)
{ } is set

w is set
v is non empty set

w is non empty (K,V)
a is set

a is set
b is set
W is non empty (K,V)
x is non empty (K,V)
y is set

W is non empty (K,V)
x is Element of W

the carrier of V is non empty set
0. V is V55(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
bool the carrier of V is non empty set
W is Element of bool the carrier of V
x is Element of bool the carrier of V
the Element of x is Element of x
v is right_complementable Element of the carrier of V
{v} is non empty Element of bool the carrier of V
w is Element of bool the carrier of V
x \ w is Element of bool the carrier of V

w \/ (x \ w) is Element of bool the carrier of V

c is right_complementable Element of the carrier of V

{} is non empty set
y is set

(K,V) is non empty (K,V)
{ } is set

w is set
v is non empty set

w is non empty (K,V)
a is set

a is set
b is set
W is non empty (K,V)
x is non empty (K,V)
y is set

W is non empty (K,V)
x is Element of W

Subspaces V is non empty set

SubJoin V is V6() V18([:(),():], Subspaces V) Element of bool [:[:(),():],():]
[:(),():] is non empty set
[:[:(),():],():] is non empty set
bool [:[:(),():],():] is non empty set
() \$\$ W is Element of Subspaces V
(K,V) is non empty (K,V)
SubMeet V is V6() V18([:(),():], Subspaces V) Element of bool [:[:(),():],():]
() \$\$ W is Element of Subspaces V

Subspaces V is non empty set
SubJoin V is V6() V18([:(),():], Subspaces V) Element of bool [:[:(),():],():]
[:(),():] is non empty set
[:[:(),():],():] is non empty set
bool [:[:(),():],():] is non empty set

the_unity_wrt () is Element of Subspaces V
(K,V) is non empty (K,V)
SubMeet V is V6() V18([:(),():], Subspaces V) Element of bool [:[:(),():],():]
LattStr(# (K,V),(),() #) is non empty strict LattStr

the carrier of y is non empty set
[: the carrier of y, the carrier of y:] is non empty set
the L_join of y is V6() V18([: the carrier of y, the carrier of y:], the carrier of y) commutative associative idempotent Element of bool [:[: the carrier of y, the carrier of y:], the carrier of y:]
[:[: the carrier of y, the carrier of y:], the carrier of y:] is non empty set
bool [:[: the carrier of y, the carrier of y:], the carrier of y:] is non empty set
@ ((0). V) is Element of Subspaces V
w is Element of (K,V)
a is Element of (K,V)

() . (w,a) is Element of (K,V)

() . (a,w) is Element of (K,V)

Subspaces V is non empty set
SubMeet V is V6() V18([:(),():], Subspaces V) Element of bool [:[:(),():],():]
[:(),():] is non empty set
[:[:(),():],():] is non empty set
bool [:[:(),():],():] is non empty set

the_unity_wrt () is Element of Subspaces V
(K,V) is non empty (K,V)
SubJoin V is V6() V18([:(),():], Subspaces V) Element of bool [:[:(),():],():]
LattStr(# (K,V),(),() #) is non empty strict LattStr

the carrier of y is non empty set
[: the carrier of y, the carrier of y:] is non empty set
the L_meet of y is V6() V18([: the carrier of y, the carrier of y:], the carrier of y) commutative associative idempotent Element of bool [:[: the carrier of y, the carrier of y:], the carrier of y:]
[:[: the carrier of y, the carrier of y:], the carrier of y:] is non empty set
bool [:[: the carrier of y, the carrier of y:], the carrier of y:] is non empty set
@ () is Element of Subspaces V
w is Element of (K,V)
a is Element of (K,V)

() . (w,a) is Element of (K,V)

() . (a,w) is Element of (K,V)

the carrier of V is non empty set
bool the carrier of V is non empty set
W is Element of bool the carrier of V
x is Element of bool the carrier of V
{ (b1 + b2) where b1, b2 is right_complementable Element of the carrier of V : ( b1 in W & b2 in x ) } is set
v is set
w is right_complementable Element of the carrier of V
a is right_complementable Element of the carrier of V
w + a 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . (w,a) is right_complementable Element of the carrier of V
v is set
w is right_complementable Element of the carrier of V
a is right_complementable Element of the carrier of V
w + a 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . (w,a) is right_complementable Element of the carrier of V
v is Element of bool the carrier of V
w is set
b is right_complementable Element of the carrier of V
c is right_complementable Element of the carrier of V
a is set
b + c 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . (b,c) is right_complementable Element of the carrier of V
y is Element of bool the carrier of V
v is Element of bool the carrier of V
w is set
a is right_complementable Element of the carrier of V
b is right_complementable Element of the carrier of V
a + b 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . (a,b) is right_complementable Element of the carrier of V
a is right_complementable Element of the carrier of V
b is right_complementable Element of the carrier of V
a + b 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . (a,b) is right_complementable Element of the carrier of V

the carrier of V is non empty set
bool the carrier of V is non empty set
W is Element of bool the carrier of V
x is right_complementable Element of the carrier of V

the carrier of V is non empty set
bool the carrier of V is non empty set
W is Element of bool the carrier of V
x is Element of bool the carrier of V
y is set
v is right_complementable (K,V,W)

the carrier of V is non empty set
W is right_complementable Element of the carrier of V
x is right_complementable Element of the carrier of V
x - W is right_complementable Element of the carrier of V
- W is right_complementable Element of the carrier of V
x + (- W) 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . (x,(- W)) is right_complementable Element of the carrier of V

x + y is Element of bool the carrier of V
bool the carrier of V is non empty set
x - (x - W) is right_complementable Element of the carrier of V
- (x - W) is right_complementable Element of the carrier of V
x + (- (x - W)) is right_complementable Element of the carrier of V
the addF of V . (x,(- (x - W))) is right_complementable Element of the carrier of V
x - x is right_complementable Element of the carrier of V
- x is right_complementable Element of the carrier of V
x + (- x) is right_complementable Element of the carrier of V
the addF of V . (x,(- x)) is right_complementable Element of the carrier of V
(x - x) + W is right_complementable Element of the carrier of V
the addF of V . ((x - x),W) is right_complementable Element of the carrier of V
0. V is V55(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
(0. V) + W is right_complementable Element of the carrier of V
the addF of V . ((0. V),W) is right_complementable Element of the carrier of V

the carrier of V is non empty set
W is right_complementable Element of the carrier of V
x is right_complementable Element of the carrier of V
W - x is right_complementable Element of the carrier of V
- x is right_complementable Element of the carrier of V
W + (- x) 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . (W,(- x)) is right_complementable Element of the carrier of V

W + y is Element of bool the carrier of V
bool the carrier of V is non empty set
x + y is Element of bool the carrier of V

the carrier of V is non empty set

{ (b1 + W) where b1 is right_complementable Element of the carrier of V : verum } is set
x is set
y is set
v is right_complementable Element of the carrier of V
v + W is Element of bool the carrier of V
bool the carrier of V is non empty set

(K,V,W) is set
the carrier of V is non empty set
x is right_complementable Element of the carrier of V
x + W is Element of bool the carrier of V
bool the carrier of V is non empty set

the carrier of V is non empty set
x is right_complementable Element of the carrier of V

x + W is Element of bool the carrier of V
bool the carrier of V is non empty set
(K,V,W) is non empty set

the carrier of V is non empty set

(K,V,W) is non empty set
x is Element of (K,V,W)
y is right_complementable Element of the carrier of V
y + W is Element of bool the carrier of V
bool the carrier of V is non empty set
(K,V,W,y) is Element of (K,V,W)

the carrier of V is non empty set

the carrier of w is non empty set

W is right_complementable Element of the carrier of V
(K,V,y,W) is Element of (K,V,y)
(K,V,y) is non empty set
W + y is Element of bool the carrier of V
bool the carrier of V is non empty set
x is right_complementable Element of the carrier of V
(K,V,y,x) is Element of (K,V,y)
x + y is Element of bool the carrier of V
W - x is right_complementable Element of the carrier of V
- x is right_complementable Element of the carrier of V
W + (- x) 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . (W,(- x)) is right_complementable Element of the carrier of V

a is right_complementable Element of the carrier of w
b is right_complementable Element of the carrier of w
a - b is right_complementable Element of the carrier of w
- b is right_complementable Element of the carrier of w
a + (- b) 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 non empty set
[:[: the carrier of w, the carrier of w:], the carrier of w:] is non empty set
bool [:[: the carrier of w, the carrier of w:], the carrier of w:] is non empty set
the addF of w . (a,(- b)) is right_complementable Element of the carrier of w
(v,w,c,a) is Element of (v,w,c)
(v,w,c) is non empty set
a + c is Element of bool the carrier of w
bool the carrier of w is non empty set
(v,w,c,b) is Element of (v,w,c)
b + c is Element of bool the carrier of w

(K,V,W) is non empty set
the carrier of V is non empty set
x is Element of (K,V,W)
y is right_complementable Element of the carrier of V
(K,V,W,y) is Element of (K,V,W)
y + W is Element of bool the carrier of V
bool the carrier of V is non empty set
v is right_complementable Element of the carrier of V
(K,V,W,v) is Element of (K,V,W)
v + W is Element of bool the carrier of V
y - v is right_complementable Element of the carrier of V
- v is right_complementable Element of the carrier of V
y + (- v) 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . (y,(- v)) is right_complementable Element of the carrier of V
- (y - v) is right_complementable Element of the carrier of V
- y is right_complementable Element of the carrier of V
(- y) - (- v) is right_complementable Element of the carrier of V
- (- v) is right_complementable Element of the carrier of V
(- y) + (- (- v)) is right_complementable Element of the carrier of V
the addF of V . ((- y),(- (- v))) is right_complementable Element of the carrier of V
(K,V,W,(- y)) is Element of (K,V,W)
(- y) + W is Element of bool the carrier of V
(K,V,W,(- v)) is Element of (K,V,W)
(- v) + W is Element of bool the carrier of V
v is right_complementable Element of the carrier of V
(K,V,W,v) is Element of (K,V,W)
v + W is Element of bool the carrier of V
- v is right_complementable Element of the carrier of V
(K,V,W,(- v)) is Element of (K,V,W)
(- v) + W is Element of bool the carrier of V
y is Element of (K,V,W)
v is Element of (K,V,W)
w is right_complementable Element of the carrier of V
(K,V,W,w) is Element of (K,V,W)
w + W is Element of bool the carrier of V
bool the carrier of V is non empty set
- w is right_complementable Element of the carrier of V
(K,V,W,(- w)) is Element of (K,V,W)
(- w) + W is Element of bool the carrier of V
y is Element of (K,V,W)
v is right_complementable Element of the carrier of V
(K,V,W,v) is Element of (K,V,W)
v + W is Element of bool the carrier of V
bool the carrier of V is non empty set
w is right_complementable Element of the carrier of V
(K,V,W,w) is Element of (K,V,W)
w + W is Element of bool the carrier of V
a is right_complementable Element of the carrier of V
(K,V,W,a) is Element of (K,V,W)
a + W is Element of bool the carrier of V
b is right_complementable Element of the carrier of V
(K,V,W,b) is Element of (K,V,W)
b + W is Element of bool the carrier of V
v - a is right_complementable Element of the carrier of V
- a is right_complementable Element of the carrier of V
v + (- a) 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . (v,(- a)) is right_complementable Element of the carrier of V
w - b is right_complementable Element of the carrier of V
- b is right_complementable Element of the carrier of V
w + (- b) is right_complementable Element of the carrier of V
the addF of V . (w,(- b)) is right_complementable Element of the carrier of V
(v - a) + (w - b) is right_complementable Element of the carrier of V
the addF of V . ((v - a),(w - b)) is right_complementable Element of the carrier of V
(v - a) + w is right_complementable Element of the carrier of V
the addF of V . ((v - a),w) is right_complementable Element of the carrier of V
((v - a) + w) - b is right_complementable Element of the carrier of V
((v - a) + w) + (- b) is right_complementable Element of the carrier of V
the addF of V . (((v - a) + w),(- b)) is right_complementable Element of the carrier of V
v + w is right_complementable Element of the carrier of V
the addF of V . (v,w) is right_complementable Element of the carrier of V
(v + w) - a is right_complementable Element of the carrier of V
(v + w) + (- a) is right_complementable Element of the carrier of V
the addF of V . ((v + w),(- a)) is right_complementable Element of the carrier of V
((v + w) - a) - b is right_complementable Element of the carrier of V
((v + w) - a) + (- b) is right_complementable Element of the carrier of V
the addF of V . (((v + w) - a),(- b)) is right_complementable Element of the carrier of V
a + b is right_complementable Element of the carrier of V
the addF of V . (a,b) is right_complementable Element of the carrier of V
(v + w) - (a + b) is right_complementable Element of the carrier of V
- (a + b) is right_complementable Element of the carrier of V
(v + w) + (- (a + b)) is right_complementable Element of the carrier of V
the addF of V . ((v + w),(- (a + b))) is right_complementable Element of the carrier of V
(K,V,W,(v + w)) is Element of (K,V,W)
(v + w) + W is Element of bool the carrier of V
(K,V,W,(a + b)) is Element of (K,V,W)
(a + b) + W is Element of bool the carrier of V
a is right_complementable Element of the carrier of V
(K,V,W,a) is Element of (K,V,W)
a + W is Element of bool the carrier of V
b is right_complementable Element of the carrier of V
(K,V,W,b) is Element of (K,V,W)
b + W is Element of bool the carrier of V
a + b is right_complementable Element of the carrier of V
the addF of V . (a,b) is right_complementable Element of the carrier of V
(K,V,W,(a + b)) is Element of (K,V,W)
(a + b) + W is Element of bool the carrier of V
v is Element of (K,V,W)
w is Element of (K,V,W)
a is right_complementable Element of the carrier of V
(K,V,W,a) is Element of (K,V,W)
a + W is Element of bool the carrier of V
bool the carrier of V is non empty set
b is right_complementable Element of the carrier of V
(K,V,W,b) is Element of (K,V,W)
b + W is Element of bool the carrier of V
a + b 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . (a,b) is right_complementable Element of the carrier of V
(K,V,W,(a + b)) is Element of (K,V,W)
(a + b) + W is Element of bool the carrier of V

(K,V,W) is non empty set
[:(K,V,W),(K,V,W):] is non empty set
bool [:(K,V,W),(K,V,W):] is non empty set
[:[:(K,V,W),(K,V,W):],(K,V,W):] is non empty set
bool [:[:(K,V,W),(K,V,W):],(K,V,W):] is non empty set

(K,V,W) is non empty set
(K,V,W) is V6() V18([:(K,V,W),(K,V,W):],(K,V,W)) Element of bool [:[:(K,V,W),(K,V,W):],(K,V,W):]
[:(K,V,W),(K,V,W):] is non empty set
[:[:(K,V,W),(K,V,W):],(K,V,W):] is non empty set
bool [:[:(K,V,W),(K,V,W):],(K,V,W):] is non empty set
0. V is V55(V) right_complementable Element of the carrier of V
the carrier of V is non empty set
the ZeroF of V is right_complementable Element of the carrier of V
(K,V,W,(0. V)) is Element of (K,V,W)
(0. V) + W is Element of bool the carrier of V
bool the carrier of V is non empty set

(K,V,W) is non empty set
(K,V,W) is V6() V18([:(K,V,W),(K,V,W):],(K,V,W)) Element of bool [:[:(K,V,W),(K,V,W):],(K,V,W):]
[:(K,V,W),(K,V,W):] is non empty set
[:[:(K,V,W),(K,V,W):],(K,V,W):] is non empty set
bool [:[:(K,V,W),(K,V,W):],(K,V,W):] is non empty set
0. V is V55(V) right_complementable Element of the carrier of V
the carrier of V is non empty set
the ZeroF of V is right_complementable Element of the carrier of V
(K,V,W,(0. V)) is Element of (K,V,W)
(0. V) + W is Element of bool the carrier of V
bool the carrier of V is non empty set

the carrier of V is non empty set

W is right_complementable Element of the carrier of V
(K,V,x,W) is Element of (K,V,x)
(K,V,x) is non empty set
W + x is Element of bool the carrier of V
bool the carrier of V is non empty set
(K,V,x) is non empty strict addLoopStr
(K,V,x) is V6() V18([:(K,V,x),(K,V,x):],(K,V,x)) Element of bool [:[:(K,V,x),(K,V,x):],(K,V,x):]
[:(K,V,x),(K,V,x):] is non empty set
[:[:(K,V,x),(K,V,x):],(K,V,x):] is non empty set
bool [:[:(K,V,x),(K,V,x):],(K,V,x):] is non empty set
0. V is V55(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
(K,V,x,(0. V)) is Element of (K,V,x)
(0. V) + x is Element of bool the carrier of V
the carrier of (K,V,x) is non empty set

the carrier of V is non empty set

x is right_complementable Element of the carrier of V
(K,V,W,x) is Element of (K,V,W)
(K,V,W) is non empty set
x + W is Element of bool the carrier of V
bool the carrier of V is non empty set
(K,V,W) is non empty strict addLoopStr
(K,V,W) is V6() V18([:(K,V,W),(K,V,W):],(K,V,W)) Element of bool [:[:(K,V,W),(K,V,W):],(K,V,W):]
[:(K,V,W),(K,V,W):] is non empty set
[:[:(K,V,W),(K,V,W):],(K,V,W):] is non empty set
bool [:[:(K,V,W),(K,V,W):],(K,V,W):] is non empty set
0. V is V55(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
(K,V,W,(0. V)) is Element of (K,V,W)
(0. V) + W is Element of bool the carrier of V
the carrier of (K,V,W) is non empty set

the carrier of V is non empty set

(K,V,W) is non empty strict addLoopStr
(K,V,W) is non empty set
(K,V,W) is V6() V18([:(K,V,W),(K,V,W):],(K,V,W)) Element of bool [:[:(K,V,W),(K,V,W):],(K,V,W):]
[:(K,V,W),(K,V,W):] is non empty set
[:[:(K,V,W),(K,V,W):],(K,V,W):] is non empty set
bool [:[:(K,V,W),(K,V,W):],(K,V,W):] is non empty set
0. V is V55(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
(K,V,W,(0. V)) is Element of (K,V,W)
(0. V) + W is Element of bool the carrier of V
bool the carrier of V is non empty set
the carrier of (K,V,W) is non empty set
x is Element of the carrier of (K,V,W)
y is right_complementable Element of the carrier of V
(K,V,W,y) is Element of (K,V,W)
y + W is Element of bool the carrier of V
(K,V,W,y) is Element of the carrier of (K,V,W)

the carrier of V is non empty set

the carrier of w is non empty set

W is right_complementable Element of the carrier of V
(K,V,y,W) is Element of the carrier of (K,V,y)
(K,V,y) is non empty strict addLoopStr
(K,V,y) is non empty set
(K,V,y) is V6() V18([:(K,V,y),(K,V,y):],(K,V,y)) Element of bool [:[:(K,V,y),(K,V,y):],(K,V,y):]
[:(K,V,y),(K,V,y):] is non empty set
[:[:(K,V,y),(K,V,y):],(K,V,y):] is non empty set
bool [:[:(K,V,y),(K,V,y):],(K,V,y):] is non empty set
0. V is V55(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
(K,V,y,(0. V)) is Element of (K,V,y)
(0. V) + y is Element of bool the carrier of V
bool the carrier of V is non empty set
the carrier of (K,V,y) is non empty set
(K,V,y,W) is Element of (K,V,y)
W + y is Element of bool the carrier of V
x is right_complementable Element of the carrier of V
(K,V,y,x) is Element of the carrier of (K,V,y)
(K,V,y,x) is Element of (K,V,y)
x + y is Element of bool the carrier of V
W - x is right_complementable Element of the carrier of V
- x is right_complementable Element of the carrier of V
W + (- x) 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . (W,(- x)) is right_complementable Element of the carrier of V

a is right_complementable Element of the carrier of w
b is right_complementable Element of the carrier of w
a - b is right_complementable Element of the carrier of w
- b is right_complementable Element of the carrier of w
a + (- b) 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 non empty set
[:[: the carrier of w, the carrier of w:], the carrier of w:] is non empty set
bool [:[: the carrier of w, the carrier of w:], the carrier of w:] is non empty set
the addF of w . (a,(- b)) is right_complementable Element of the carrier of w
(v,w,c,a) is Element of the carrier of (v,w,c)
(v,w,c) is non empty strict addLoopStr
(v,w,c) is non empty set
(v,w,c) is V6() V18([:(v,w,c),(v,w,c):],(v,w,c)) Element of bool [:[:(v,w,c),(v,w,c):],(v,w,c):]
[:(v,w,c),(v,w,c):] is non empty set
[:[:(v,w,c),(v,w,c):],(v,w,c):] is non empty set
bool [:[:(v,w,c),(v,w,c):],(v,w,c):] is non empty set
0. w is V55(w) right_complementable Element of the carrier of w
the ZeroF of w is right_complementable Element of the carrier of w
(v,w,c,(0. w)) is Element of (v,w,c)
(0. w) + c is Element of bool the carrier of w
bool the carrier of w is non empty set
the carrier of (v,w,c) is non empty set
(v,w,c,a) is Element of (v,w,c)
a + c is Element of bool the carrier of w
(v,w,c,b) is Element of the carrier of (v,w,c)
(v,w,c,b) is Element of (v,w,c)
b + c is Element of bool the carrier of w

the carrier of V is non empty set
0. V is V55(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
W is right_complementable Element of the carrier of V
x is right_complementable Element of the carrier of V
W + x 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . (W,x) is right_complementable Element of the carrier of V

(K,V,y) is non empty strict addLoopStr
(K,V,y) is non empty set
(K,V,y) is V6() V18([:(K,V,y),(K,V,y):],(K,V,y)) Element of bool [:[:(K,V,y),(K,V,y):],(K,V,y):]
[:(K,V,y),(K,V,y):] is non empty set
[:[:(K,V,y),(K,V,y):],(K,V,y):] is non empty set
bool [:[:(K,V,y),(K,V,y):],(K,V,y):] is non empty set
(K,V,y,(0. V)) is Element of (K,V,y)
(0. V) + y is Element of bool the carrier of V
bool the carrier of V is non empty set
(K,V,y,W) is Element of the carrier of (K,V,y)
the carrier of (K,V,y) is non empty set
(K,V,y,W) is Element of (K,V,y)
W + y is Element of bool the carrier of V
(K,V,y,x) is Element of the carrier of (K,V,y)
(K,V,y,x) is Element of (K,V,y)
x + y is Element of bool the carrier of V
(K,V,y,W) + (K,V,y,x) is Element of the carrier of (K,V,y)
the addF of (K,V,y) is V6() V18([: the carrier of (K,V,y), the carrier of (K,V,y):], the carrier of (K,V,y)) Element of bool [:[: the carrier of (K,V,y), the carrier of (K,V,y):], the carrier of (K,V,y):]
[: the carrier of (K,V,y), the carrier of (K,V,y):] is non empty set
[:[: the carrier of (K,V,y), the carrier of (K,V,y):], the carrier of (K,V,y):] is non empty set
bool [:[: the carrier of (K,V,y), the carrier of (K,V,y):], the carrier of (K,V,y):] is non empty set
the addF of (K,V,y) . ((K,V,y,W),(K,V,y,x)) is Element of the carrier of (K,V,y)
(K,V,y,(W + x)) is Element of the carrier of (K,V,y)
(K,V,y,(W + x)) is Element of (K,V,y)
(W + x) + y is Element of bool the carrier of V
0. (K,V,y) is V55((K,V,y)) Element of the carrier of (K,V,y)
the ZeroF of (K,V,y) is Element of the carrier of (K,V,y)
(K,V,y,(0. V)) is Element of the carrier of (K,V,y)
(K,V,y,(K,V,y,W),(K,V,y,x)) is Element of (K,V,y)

(K,V,W) is non empty strict addLoopStr
(K,V,W) is non empty set
(K,V,W) is V6() V18([:(K,V,W),(K,V,W):],(K,V,W)) Element of bool [:[:(K,V,W),(K,V,W):],(K,V,W):]
[:(K,V,W),(K,V,W):] is non empty set
[:[:(K,V,W),(K,V,W):],(K,V,W):] is non empty set
bool [:[:(K,V,W),(K,V,W):],(K,V,W):] is non empty set
0. V is V55(V) right_complementable Element of the carrier of V
the carrier of V is non empty set
the ZeroF of V is right_complementable Element of the carrier of V
(K,V,W,(0. V)) is Element of (K,V,W)
(0. V) + W is Element of bool the carrier of V
bool the carrier of V is non empty set
the carrier of (K,V,W) is non empty set
y is Element of the carrier of (K,V,W)
w is right_complementable Element of the carrier of V
(K,V,W,w) is Element of the carrier of (K,V,W)
(K,V,W,w) is Element of (K,V,W)
w + W is Element of bool the carrier of V
v is Element of the carrier of (K,V,W)
a is right_complementable Element of the carrier of V
(K,V,W,a) is Element of the carrier of (K,V,W)
(K,V,W,a) is Element of (K,V,W)
a + W is Element of bool the carrier of V
y + v is Element of the carrier of (K,V,W)
the addF of (K,V,W) is V6() V18([: the carrier of (K,V,W), the carrier of (K,V,W):], the carrier of (K,V,W)) Element of bool [:[: the carrier of (K,V,W), the carrier of (K,V,W):], the carrier of (K,V,W):]
[: the carrier of (K,V,W), the carrier of (K,V,W):] is non empty set
[:[: the carrier of (K,V,W), the carrier of (K,V,W):], the carrier of (K,V,W):] is non empty set
bool [:[: the carrier of (K,V,W), the carrier of (K,V,W):], the carrier of (K,V,W):] is non empty set
the addF of (K,V,W) . (y,v) is Element of the carrier of (K,V,W)
w + a 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . (w,a) is right_complementable Element of the carrier of V
(K,V,W,(w + a)) is Element of the carrier of (K,V,W)
(K,V,W,(w + a)) is Element of (K,V,W)
(w + a) + W is Element of bool the carrier of V
v + y is Element of the carrier of (K,V,W)
the addF of (K,V,W) . (v,y) is Element of the carrier of (K,V,W)
y is Element of the carrier of (K,V,W)
a is right_complementable Element of the carrier of V
(K,V,W,a) is Element of the carrier of (K,V,W)
(K,V,W,a) is Element of (K,V,W)
a + W is Element of bool the carrier of V
v is Element of the carrier of (K,V,W)
b is right_complementable Element of the carrier of V
(K,V,W,b) is Element of the carrier of (K,V,W)
(K,V,W,b) is Element of (K,V,W)
b + W is Element of bool the carrier of V
w is Element of the carrier of (K,V,W)
c is right_complementable Element of the carrier of V
(K,V,W,c) is Element of the carrier of (K,V,W)
(K,V,W,c) is Element of (K,V,W)
c + W is Element of bool the carrier of V
y + v is Element of the carrier of (K,V,W)
the addF of (K,V,W) . (y,v) is Element of the carrier of (K,V,W)
a + b is right_complementable Element of the carrier of V
the addF of V . (a,b) is right_complementable Element of the carrier of V
(K,V,W,(a + b)) is Element of the carrier of (K,V,W)
(K,V,W,(a + b)) is Element of (K,V,W)
(a + b) + W is Element of bool the carrier of V
v + w is Element of the carrier of (K,V,W)
the addF of (K,V,W) . (v,w) is Element of the carrier of (K,V,W)
b + c is right_complementable Element of the carrier of V
the addF of V . (b,c) is right_complementable Element of the carrier of V
(K,V,W,(b + c)) is Element of the carrier of (K,V,W)
(K,V,W,(b + c)) is Element of (K,V,W)
(b + c) + W is Element of bool the carrier of V
(y + v) + w is Element of the carrier of (K,V,W)
the addF of (K,V,W) . ((y + v),w) is Element of the carrier of (K,V,W)
(a + b) + c is right_complementable Element of the carrier of V
the addF of V . ((a + b),c) is right_complementable Element of the carrier of V
(K,V,W,((a + b) + c)) is Element of the carrier of (K,V,W)
(K,V,W,((a + b) + c)) is Element of (K,V,W)
((a + b) + c) + W is Element of bool the carrier of V
a + (b + c) is right_complementable Element of the carrier of V
the addF of V . (a,(b + c)) is right_complementable Element of the carrier of V
(K,V,W,(a + (b + c))) is Element of the carrier of (K,V,W)
(K,V,W,(a + (b + c))) is Element of (K,V,W)
(a + (b + c)) + W is Element of bool the carrier of V
y + (v + w) is Element of the carrier of (K,V,W)
the addF of (K,V,W) . (y,(v + w)) is Element of the carrier of (K,V,W)
y is Element of the carrier of (K,V,W)
v is right_complementable Element of the carrier of V
(K,V,W,v) is Element of the carrier of (K,V,W)
(K,V,W,v) is Element of (K,V,W)
v + W is Element of bool the carrier of V
0. (K,V,W) is V55((K,V,W)) Element of the carrier of (K,V,W)
the ZeroF of (K,V,W) is Element of the carrier of (K,V,W)
(K,V,W,(0. V)) is Element of the carrier of (K,V,W)
y + (0. (K,V,W)) is Element of the carrier of (K,V,W)
the addF of (K,V,W) . (y,(0. (K,V,W))) is Element of the carrier of (K,V,W)
v + (0. V) is right_complementable Element of the carrier of V
the addF of V . (v,(0. V)) is right_complementable Element of the carrier of V
(K,V,W,(v + (0. V))) is Element of the carrier of (K,V,W)
(K,V,W,(v + (0. V))) is Element of (K,V,W)
(v + (0. V)) + W is Element of bool the carrier of V
y is Element of the carrier of (K,V,W)
v is right_complementable Element of the carrier of V
(K,V,W,v) is Element of the carrier of (K,V,W)
(K,V,W,v) is Element of (K,V,W)
v + W is Element of bool the carrier of V
w is right_complementable Element of the carrier of V
v + w is right_complementable Element of the carrier of V
the addF of V . (v,w) is right_complementable Element of the carrier of V
(K,V,W,w) is Element of the carrier of (K,V,W)
(K,V,W,w) is Element of (K,V,W)
w + W is Element of bool the carrier of V
a is Element of the carrier of (K,V,W)
y + a is Element of the carrier of (K,V,W)
the addF of (K,V,W) . (y,a) is Element of the carrier of (K,V,W)

the carrier of K is non empty set

(K,V,W) is non empty set
(K,V,W) is V6() V18([:(K,V,W),(K,V,W):],(K,V,W)) Element of bool [:[:(K,V,W),(K,V,W):],(K,V,W):]
[:(K,V,W),(K,V,W):] is non empty set
[:[:(K,V,W),(K,V,W):],(K,V,W):] is non empty set
bool [:[:(K,V,W),(K,V,W):],(K,V,W):] is non empty set
0. V is V55(V) right_complementable Element of the carrier of V
the carrier of V is non empty set
the ZeroF of V is right_complementable Element of the carrier of V
(K,V,W,(0. V)) is Element of (K,V,W)
(0. V) + W is Element of bool the carrier of V
bool the carrier of V is non empty set
the carrier of (K,V,W) is non empty set
y is right_complementable Element of the carrier of (K,V,W)
x is right_complementable Element of the carrier of K
v is right_complementable Element of the carrier of V
(K,V,W,v) is right_complementable Element of the carrier of (K,V,W)
(K,V,W,v) is Element of (K,V,W)
v + W is Element of bool the carrier of V
w is right_complementable Element of the carrier of V
(K,V,W,w) is right_complementable Element of the carrier of (K,V,W)
(K,V,W,w) is Element of (K,V,W)
w + W is Element of bool the carrier of V
w - v is right_complementable Element of the carrier of V
- v is right_complementable Element of the carrier of V
w + (- v) 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the