:: VECTSP10 semantic presentation

K92() is Element of bool K88()
K88() is set
bool K88() is non empty set

the carrier of K242() is set
K87() is set
bool K87() is non empty set
bool K92() is non empty set
2 is non empty set
[:2,2:] is V1() non empty set
[:[:2,2:],2:] is V1() non empty set
bool [:[:2,2:],2:] is non empty set
K89() is set
{} is set

1 is non empty set
{{},1} is V29() set

the carrier of K is set
the addF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like quasi_total Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is V1() set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is V1() set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
0. K is V48(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
the multF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like quasi_total Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
VectSpStr(# the carrier of K, the addF of K,(0. K), the multF of K #) is strict VectSpStr over K
K is non empty doubleLoopStr
(K) is strict VectSpStr over K
the carrier of K is non empty set
the addF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like non empty V14([: the carrier of K, the carrier of K:]) quasi_total Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is V1() non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is V1() non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
0. K is V48(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
the multF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like non empty V14([: the carrier of K, the carrier of K:]) quasi_total Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
VectSpStr(# the carrier of K, the addF of K,(0. K), the multF of K #) is non empty strict VectSpStr over K
K is non empty Abelian doubleLoopStr
(K) is non empty strict VectSpStr over K
the carrier of K is non empty set
the addF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like non empty V14([: the carrier of K, the carrier of K:]) quasi_total Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is V1() non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is V1() non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
0. K is V48(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
the multF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like non empty V14([: the carrier of K, the carrier of K:]) quasi_total Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
VectSpStr(# the carrier of K, the addF of K,(0. K), the multF of K #) is non empty strict VectSpStr over K
the carrier of (K) is non empty set
f is Element of the carrier of (K)
qf is Element of the carrier of (K)
f + qf is Element of the carrier of (K)
the addF of (K) is V1() V4([: the carrier of (K), the carrier of (K):]) V5( the carrier of (K)) Function-like non empty V14([: the carrier of (K), the carrier of (K):]) quasi_total Element of bool [:[: the carrier of (K), the carrier of (K):], the carrier of (K):]
[: the carrier of (K), the carrier of (K):] is V1() non empty set
[:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is V1() non empty set
bool [:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
the addF of (K) . (f,qf) is Element of the carrier of (K)
qV is Element of the carrier of K
W is Element of the carrier of K
qV + W is Element of the carrier of K
the addF of K . (qV,W) is Element of the carrier of K
qf + f is Element of the carrier of (K)
the addF of (K) . (qf,f) is Element of the carrier of (K)
K is non empty add-associative doubleLoopStr
(K) is non empty strict VectSpStr over K
the carrier of K is non empty set
the addF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like non empty V14([: the carrier of K, the carrier of K:]) quasi_total Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is V1() non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is V1() non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
0. K is V48(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
the multF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like non empty V14([: the carrier of K, the carrier of K:]) quasi_total Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
VectSpStr(# the carrier of K, the addF of K,(0. K), the multF of K #) is non empty strict VectSpStr over K
the carrier of (K) is non empty set
f is Element of the carrier of (K)
qf is Element of the carrier of (K)
W is Element of the carrier of (K)
f + qf is Element of the carrier of (K)
the addF of (K) is V1() V4([: the carrier of (K), the carrier of (K):]) V5( the carrier of (K)) Function-like non empty V14([: the carrier of (K), the carrier of (K):]) quasi_total Element of bool [:[: the carrier of (K), the carrier of (K):], the carrier of (K):]
[: the carrier of (K), the carrier of (K):] is V1() non empty set
[:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is V1() non empty set
bool [:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
the addF of (K) . (f,qf) is Element of the carrier of (K)
(f + qf) + W is Element of the carrier of (K)
the addF of (K) . ((f + qf),W) is Element of the carrier of (K)
qV is Element of the carrier of K
x is Element of the carrier of K
qV + x is Element of the carrier of K
the addF of K . (qV,x) is Element of the carrier of K
w is Element of the carrier of K
(qV + x) + w is Element of the carrier of K
the addF of K . ((qV + x),w) is Element of the carrier of K
x + w is Element of the carrier of K
the addF of K . (x,w) is Element of the carrier of K
qV + (x + w) is Element of the carrier of K
the addF of K . (qV,(x + w)) is Element of the carrier of K
qf + W is Element of the carrier of (K)
the addF of (K) . (qf,W) is Element of the carrier of (K)
f + (qf + W) is Element of the carrier of (K)
the addF of (K) . (f,(qf + W)) is Element of the carrier of (K)
K is non empty right_zeroed doubleLoopStr
(K) is non empty strict VectSpStr over K
the carrier of K is non empty set
the addF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like non empty V14([: the carrier of K, the carrier of K:]) quasi_total Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is V1() non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is V1() non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
0. K is V48(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
the multF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like non empty V14([: the carrier of K, the carrier of K:]) quasi_total Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
VectSpStr(# the carrier of K, the addF of K,(0. K), the multF of K #) is non empty strict VectSpStr over K
the carrier of (K) is non empty set
f is Element of the carrier of (K)
0. (K) is V48((K)) Element of the carrier of (K)
the ZeroF of (K) is Element of the carrier of (K)
f + (0. (K)) is Element of the carrier of (K)
the addF of (K) is V1() V4([: the carrier of (K), the carrier of (K):]) V5( the carrier of (K)) Function-like non empty V14([: the carrier of (K), the carrier of (K):]) quasi_total Element of bool [:[: the carrier of (K), the carrier of (K):], the carrier of (K):]
[: the carrier of (K), the carrier of (K):] is V1() non empty set
[:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is V1() non empty set
bool [:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
the addF of (K) . (f,(0. (K))) is Element of the carrier of (K)
qf is Element of the carrier of K
qf + (0. K) is Element of the carrier of K
the addF of K . (qf,(0. K)) is Element of the carrier of K

(K) is non empty strict VectSpStr over K
the carrier of K is non empty set
the addF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like non empty V14([: the carrier of K, the carrier of K:]) quasi_total Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is V1() non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is V1() non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
0. K is V48(K) right_complementable Element of the carrier of K
the ZeroF of K is right_complementable Element of the carrier of K
the multF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like non empty V14([: the carrier of K, the carrier of K:]) quasi_total Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
VectSpStr(# the carrier of K, the addF of K,(0. K), the multF of K #) is non empty strict VectSpStr over K
the carrier of (K) is non empty set
f is Element of the carrier of (K)
qf is right_complementable Element of the carrier of K
W is right_complementable Element of the carrier of K
qf + W is right_complementable Element of the carrier of K
the addF of K . (qf,W) is right_complementable Element of the carrier of K
qV is Element of the carrier of (K)
f + qV is Element of the carrier of (K)
the addF of (K) is V1() V4([: the carrier of (K), the carrier of (K):]) V5( the carrier of (K)) Function-like non empty V14([: the carrier of (K), the carrier of (K):]) quasi_total Element of bool [:[: the carrier of (K), the carrier of (K):], the carrier of (K):]
[: the carrier of (K), the carrier of (K):] is V1() non empty set
[:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is V1() non empty set
bool [:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
the addF of (K) . (f,qV) is Element of the carrier of (K)
0. (K) is V48((K)) Element of the carrier of (K)
the ZeroF of (K) is Element of the carrier of (K)

(K) is non empty strict VectSpStr over K
the carrier of K is non empty set
the addF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like non empty V14([: the carrier of K, the carrier of K:]) quasi_total Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is V1() non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is V1() non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
0. K is V48(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
the multF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like non empty V14([: the carrier of K, the carrier of K:]) quasi_total Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
VectSpStr(# the carrier of K, the addF of K,(0. K), the multF of K #) is non empty strict VectSpStr over K
the carrier of (K) is non empty set
W is Element of the carrier of (K)
qV is Element of the carrier of (K)
f is Element of the carrier of K
W + qV is Element of the carrier of (K)
the addF of (K) is V1() V4([: the carrier of (K), the carrier of (K):]) V5( the carrier of (K)) Function-like non empty V14([: the carrier of (K), the carrier of (K):]) quasi_total Element of bool [:[: the carrier of (K), the carrier of (K):], the carrier of (K):]
[: the carrier of (K), the carrier of (K):] is V1() non empty set
[:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is V1() non empty set
bool [:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
the addF of (K) . (W,qV) is Element of the carrier of (K)
f * (W + qV) is Element of the carrier of (K)
the lmult of (K) is V1() V4([: the carrier of K, the carrier of (K):]) V5( the carrier of (K)) Function-like non empty V14([: the carrier of K, the carrier of (K):]) quasi_total Element of bool [:[: the carrier of K, the carrier of (K):], the carrier of (K):]
[: the carrier of K, the carrier of (K):] is V1() non empty set
[:[: the carrier of K, the carrier of (K):], the carrier of (K):] is V1() non empty set
bool [:[: the carrier of K, the carrier of (K):], the carrier of (K):] is non empty set
the lmult of (K) . (f,(W + qV)) is Element of the carrier of (K)
x is Element of the carrier of K
w is Element of the carrier of K
x + w is Element of the carrier of K
the addF of K . (x,w) is Element of the carrier of K
f * (x + w) is Element of the carrier of K
the multF of K . (f,(x + w)) is Element of the carrier of K
f * x is Element of the carrier of K
the multF of K . (f,x) is Element of the carrier of K
f * w is Element of the carrier of K
the multF of K . (f,w) is Element of the carrier of K
(f * x) + (f * w) is Element of the carrier of K
the addF of K . ((f * x),(f * w)) is Element of the carrier of K
f * W is Element of the carrier of (K)
the lmult of (K) . (f,W) is Element of the carrier of (K)
f * qV is Element of the carrier of (K)
the lmult of (K) . (f,qV) is Element of the carrier of (K)
(f * W) + (f * qV) is Element of the carrier of (K)
the addF of (K) . ((f * W),(f * qV)) is Element of the carrier of (K)
qf is Element of the carrier of K
f + qf is Element of the carrier of K
the addF of K . (f,qf) is Element of the carrier of K
(f + qf) * W is Element of the carrier of (K)
the lmult of (K) . ((f + qf),W) is Element of the carrier of (K)
(f + qf) * x is Element of the carrier of K
the multF of K . ((f + qf),x) is Element of the carrier of K
qf * x is Element of the carrier of K
the multF of K . (qf,x) is Element of the carrier of K
(f * x) + (qf * x) is Element of the carrier of K
the addF of K . ((f * x),(qf * x)) is Element of the carrier of K
qf * W is Element of the carrier of (K)
the lmult of (K) . (qf,W) is Element of the carrier of (K)
(f * W) + (qf * W) is Element of the carrier of (K)
the addF of (K) . ((f * W),(qf * W)) is Element of the carrier of (K)
f * qf is Element of the carrier of K
the multF of K . (f,qf) is Element of the carrier of K
(f * qf) * W is Element of the carrier of (K)
the lmult of (K) . ((f * qf),W) is Element of the carrier of (K)
(f * qf) * x is Element of the carrier of K
the multF of K . ((f * qf),x) is Element of the carrier of K
f * (qf * x) is Element of the carrier of K
the multF of K . (f,(qf * x)) is Element of the carrier of K
the lmult of (K) . (f,(qf * W)) is Element of the carrier of (K)
f * (qf * W) is Element of the carrier of (K)
1. K is Element of the carrier of K
the OneF of K is Element of the carrier of K
(1. K) * W is Element of the carrier of (K)
the lmult of (K) . ((1. K),W) is Element of the carrier of (K)
(1. K) * x is Element of the carrier of K
the multF of K . ((1. K),x) is Element of the carrier of K
K is non empty non degenerated non trivial doubleLoopStr
(K) is non empty strict VectSpStr over K
the carrier of K is non empty non trivial set
the addF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like non empty V14([: the carrier of K, the carrier of K:]) quasi_total Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is V1() non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is V1() non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
0. K is V48(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
the multF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like non empty V14([: the carrier of K, the carrier of K:]) quasi_total Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
VectSpStr(# the carrier of K, the addF of K,(0. K), the multF of K #) is non empty strict VectSpStr over K
K is non empty non degenerated non trivial doubleLoopStr
(K) is non empty non trivial strict VectSpStr over K
the carrier of K is non empty non trivial set
the addF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like non empty V14([: the carrier of K, the carrier of K:]) quasi_total Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is V1() non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is V1() non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
0. K is V48(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
the multF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like non empty V14([: the carrier of K, the carrier of K:]) quasi_total Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
VectSpStr(# the carrier of K, the addF of K,(0. K), the multF of K #) is non empty strict VectSpStr over K

(K) is non empty right_complementable add-associative right_zeroed strict VectSpStr over K
the carrier of K is non empty set
the addF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like non empty V14([: the carrier of K, the carrier of K:]) quasi_total Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is V1() non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is V1() non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
0. K is V48(K) right_complementable Element of the carrier of K
the ZeroF of K is right_complementable Element of the carrier of K
the multF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like non empty V14([: the carrier of K, the carrier of K:]) quasi_total Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
VectSpStr(# the carrier of K, the addF of K,(0. K), the multF of K #) is non empty strict VectSpStr over K

the carrier of K is non empty set
the addF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like non empty V14([: the carrier of K, the carrier of K:]) quasi_total Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is V1() non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is V1() non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
0. K is V48(K) right_complementable Element of the carrier of K
the ZeroF of K is right_complementable Element of the carrier of K
the multF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like non empty V14([: the carrier of K, the carrier of K:]) quasi_total Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
VectSpStr(# the carrier of K, the addF of K,(0. K), the multF of K #) is non empty strict VectSpStr over K

the carrier of K is non empty non trivial set
the addF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like non empty V14([: the carrier of K, the carrier of K:]) quasi_total Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is V1() non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is V1() non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
0. K is V48(K) right_complementable Element of the carrier of K
the ZeroF of K is right_complementable Element of the carrier of K
the multF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like non empty V14([: the carrier of K, the carrier of K:]) quasi_total Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
VectSpStr(# the carrier of K, the addF of K,(0. K), the multF of K #) is non empty strict VectSpStr over K

the carrier of K is non empty set
0. K is V48(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 K

the carrier of f is non empty set
0. f is V48(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 lmult of f is V1() V4([: the carrier of K, the carrier of f:]) V5( the carrier of f) Function-like non empty V14([: the carrier of K, the carrier of f:]) quasi_total Element of bool [:[: the carrier of K, the carrier of f:], the carrier of f:]
[: the carrier of K, the carrier of f:] is V1() non empty set
[:[: the carrier of K, the carrier of f:], the carrier of f:] is V1() non empty set
bool [:[: the carrier of K, the carrier of f:], the carrier of f:] is non empty set
the lmult of f . (V,(0. f)) is right_complementable Element of the carrier of f
qf is right_complementable Element of the carrier of f
(0. K) * qf is right_complementable Element of the carrier of f
the lmult of f . ((0. K),qf) is right_complementable Element of the carrier of f
qf + ((0. K) * qf) is right_complementable Element of the carrier of f
the addF of f is V1() V4([: the carrier of f, the carrier of f:]) V5( the carrier of f) Function-like non empty V14([: the carrier of f, the carrier of f:]) quasi_total Element of bool [:[: the carrier of f, the carrier of f:], the carrier of f:]
[: the carrier of f, the carrier of f:] is V1() non empty set
[:[: the carrier of f, the carrier of f:], the carrier of f:] is V1() non empty set
bool [:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
the addF of f . (qf,((0. K) * qf)) is right_complementable Element of the carrier of f
1. K is right_complementable Element of the carrier of K
the OneF of K is right_complementable Element of the carrier of K
(1. K) * qf is right_complementable Element of the carrier of f
the lmult of f . ((1. K),qf) is right_complementable Element of the carrier of f
((1. K) * qf) + ((0. K) * qf) is right_complementable Element of the carrier of f
the addF of f . (((1. K) * qf),((0. K) * qf)) is right_complementable Element of the carrier of f
(1. K) + (0. K) is right_complementable Element of the carrier of K
the addF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like non empty V14([: the carrier of K, the carrier of K:]) quasi_total Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is V1() non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is V1() non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the addF of K . ((1. K),(0. K)) is right_complementable Element of the carrier of K
((1. K) + (0. K)) * qf is right_complementable Element of the carrier of f
the lmult of f . (((1. K) + (0. K)),qf) is right_complementable Element of the carrier of f
qf + (0. f) is right_complementable Element of the carrier of f
the addF of f . (qf,(0. f)) is right_complementable Element of the carrier of f
V * (0. K) is right_complementable Element of the carrier of K
the multF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like non empty V14([: the carrier of K, the carrier of K:]) quasi_total Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
the multF of K . (V,(0. K)) is right_complementable Element of the carrier of K
(V * (0. K)) * qf is right_complementable Element of the carrier of f
the lmult of f . ((V * (0. K)),qf) is right_complementable Element of the carrier of f

the carrier of V is non empty set

0. V is V48(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
the carrier of f is non empty set
the carrier of qf is non empty set
the carrier of f /\ the carrier of qf is set
the carrier of (f /\ qf) is non empty set
{(0. V)} is trivial V29() Element of bool the carrier of V
bool the carrier of V is non empty set

the carrier of K is non empty non trivial set

the carrier of V is non empty set
f is set
qf is right_complementable Element of the carrier of V
{qf} is trivial V29() Element of bool the carrier of V
bool the carrier of V is non empty set

W is V1() V4( the carrier of V) V5( the carrier of K) Function-like V14( the carrier of V) quasi_total Linear_Combination of {qf}
Sum W is right_complementable Element of the carrier of V
W . qf is right_complementable Element of the carrier of K
(W . qf) * qf is right_complementable Element of the carrier of V
the lmult of V is V1() V4([: the carrier of K, the carrier of V:]) V5( the carrier of V) Function-like non empty V14([: the carrier of K, the carrier of V:]) quasi_total Element of bool [:[: the carrier of K, the carrier of V:], the carrier of V:]
[: the carrier of K, the carrier of V:] is V1() non empty set
[:[: the carrier of K, the carrier of V:], the carrier of V:] is V1() non empty set
bool [:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set
the lmult of V . ((W . qf),qf) is right_complementable Element of the carrier of V
W is right_complementable Element of the carrier of K
W * qf is right_complementable Element of the carrier of V
the lmult of V is V1() V4([: the carrier of K, the carrier of V:]) V5( the carrier of V) Function-like non empty V14([: the carrier of K, the carrier of V:]) quasi_total Element of bool [:[: the carrier of K, the carrier of V:], the carrier of V:]
[: the carrier of K, the carrier of V:] is V1() non empty set
[:[: the carrier of K, the carrier of V:], the carrier of V:] is V1() non empty set
bool [:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set
the lmult of V . (W,qf) is right_complementable Element of the carrier of V
0. K is V48(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, the carrier of K:] is V1() non empty set
bool [: the carrier of V, the carrier of K:] is non empty set
qV is V1() V4( the carrier of V) V5( the carrier of K) Function-like non empty V14( the carrier of V) quasi_total Element of bool [: the carrier of V, the carrier of K:]
qV . qf is right_complementable Element of the carrier of K
Funcs ( the carrier of V, the carrier of K) is functional non empty FUNCTION_DOMAIN of the carrier of V, the carrier of K
w is right_complementable Element of the carrier of V
x is V1() V4( the carrier of V) V5( the carrier of K) Function-like V14( the carrier of V) quasi_total Element of Funcs ( the carrier of V, the carrier of K)
x . w is right_complementable Element of the carrier of K
w is V1() V4( the carrier of V) V5( the carrier of K) Function-like V14( the carrier of V) quasi_total Linear_Combination of V
Carrier w is V29() Element of bool the carrier of V
A is set
w . A is set
A is V1() V4( the carrier of V) V5( the carrier of K) Function-like V14( the carrier of V) quasi_total Linear_Combination of {qf}
Sum A is right_complementable Element of the carrier of V

the carrier of K is non empty non trivial set

the carrier of V is non empty set
0. V is V48(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
f is right_complementable Element of the carrier of V
qf is right_complementable Element of the carrier of K
qf * f is right_complementable Element of the carrier of V
the lmult of V is V1() V4([: the carrier of K, the carrier of V:]) V5( the carrier of V) Function-like non empty V14([: the carrier of K, the carrier of V:]) quasi_total Element of bool [:[: the carrier of K, the carrier of V:], the carrier of V:]
[: the carrier of K, the carrier of V:] is V1() non empty set
[:[: the carrier of K, the carrier of V:], the carrier of V:] is V1() non empty set
bool [:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set
the lmult of V . (qf,f) is right_complementable Element of the carrier of V
W is right_complementable Element of the carrier of K
W * f is right_complementable Element of the carrier of V
the lmult of V . (W,f) is right_complementable Element of the carrier of V
(qf * f) - (W * f) is right_complementable Element of the carrier of V
- (W * f) is right_complementable Element of the carrier of V
(qf * f) + (- (W * f)) is right_complementable Element of the carrier of V
the addF of V is V1() V4([: the carrier of V, the carrier of V:]) V5( the carrier of V) Function-like non empty V14([: the carrier of V, the carrier of V:]) quasi_total Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is V1() non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is V1() non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . ((qf * f),(- (W * f))) is right_complementable Element of the carrier of V
qf - W is right_complementable Element of the carrier of K
- W is right_complementable Element of the carrier of K
qf + (- W) is right_complementable Element of the carrier of K
the addF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like non empty V14([: the carrier of K, the carrier of K:]) quasi_total Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is V1() non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is V1() non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the addF of K . (qf,(- W)) is right_complementable Element of the carrier of K
(qf - W) * f is right_complementable Element of the carrier of V
the lmult of V . ((qf - W),f) is right_complementable Element of the carrier of V
0. K is V48(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

qV is right_complementable Element of the carrier of V
x is right_complementable Element of the carrier of V
W is right_complementable Element of the carrier of V
qV + x is right_complementable Element of the carrier of V
the addF of V is V1() V4([: the carrier of V, the carrier of V:]) V5( the carrier of V) Function-like non empty V14([: the carrier of V, the carrier of V:]) quasi_total Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is V1() non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is V1() non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . (qV,x) is right_complementable Element of the carrier of V
W |-- (f,qf) is Element of [: the carrier of V, the carrier of V:]
[qV,x] is non empty Element of [: the carrier of V, the carrier of V:]
{qV,x} is V29() set
{qV} is trivial V29() set
{{qV,x},{qV}} is V29() V33() set
[qV,x] `1 is right_complementable Element of the carrier of V
[qV,x] `2 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
W |-- (f,qf) is Element of [: the carrier of V, the carrier of V:]
[: the carrier of V, the carrier of V:] is V1() non empty set
qV is right_complementable Element of the carrier of V
x is right_complementable Element of the carrier of V
[qV,x] is non empty Element of [: the carrier of V, the carrier of V:]
{qV,x} is V29() set
{qV} is trivial V29() set
{{qV,x},{qV}} is V29() V33() set
qV + x is right_complementable Element of the carrier of V
the addF of V is V1() V4([: the carrier of V, the carrier of V:]) V5( the carrier of V) Function-like non empty V14([: the carrier of V, the carrier of V:]) quasi_total Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[:[: the carrier of V, the carrier of V:], the carrier of V:] is V1() non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . (qV,x) is right_complementable Element of the carrier of V
(W |-- (f,qf)) `1 is right_complementable Element of the carrier of V
(W |-- (f,qf)) `2 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
W |-- (f,qf) is Element of [: the carrier of V, the carrier of V:]
[: the carrier of V, the carrier of V:] is V1() non empty set
qV is right_complementable Element of the carrier of V
x is right_complementable Element of the carrier of V
[qV,x] is non empty Element of [: the carrier of V, the carrier of V:]
{qV,x} is V29() set
{qV} is trivial V29() set
{{qV,x},{qV}} is V29() V33() set
(W |-- (f,qf)) `1 is right_complementable Element of the carrier of V
(W |-- (f,qf)) `2 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
W |-- (f,qf) is Element of [: the carrier of V, the carrier of V:]
[: the carrier of V, the carrier of V:] is V1() non empty set
qV is right_complementable Element of the carrier of V
x is right_complementable Element of the carrier of V
[qV,x] is non empty Element of [: the carrier of V, the carrier of V:]
{qV,x} is V29() set
{qV} is trivial V29() set
{{qV,x},{qV}} is V29() V33() set
W |-- (qf,f) is Element of [: the carrier of V, the carrier of V:]
[x,qV] is non empty Element of [: the carrier of V, the carrier of V:]
{x,qV} is V29() set
{x} is trivial V29() set
{{x,qV},{x}} is V29() V33() set
(W |-- (f,qf)) `1 is right_complementable Element of the carrier of V
(W |-- (f,qf)) `2 is right_complementable Element of the carrier of V
x + qV is right_complementable Element of the carrier of V
the addF of V is V1() V4([: the carrier of V, the carrier of V:]) V5( the carrier of V) Function-like non empty V14([: the carrier of V, the carrier of V:]) quasi_total Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[:[: the carrier of V, the carrier of V:], the carrier of V:] is V1() 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,qV) is right_complementable Element of the carrier of V

the carrier of V is non empty set
0. V is V48(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
W |-- (f,qf) is Element of [: the carrier of V, the carrier of V:]
[: the carrier of V, the carrier of V:] is V1() non empty set
[W,(0. V)] is non empty Element of [: the carrier of V, the carrier of V:]
{W,(0. V)} is V29() set
{W} is trivial V29() set
{{W,(0. V)},{W}} is V29() V33() set
W + (0. V) is right_complementable Element of the carrier of V
the addF of V is V1() V4([: the carrier of V, the carrier of V:]) V5( the carrier of V) Function-like non empty V14([: the carrier of V, the carrier of V:]) quasi_total Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[:[: the carrier of V, the carrier of V:], the carrier of V:] is V1() 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,(0. V)) is right_complementable Element of the carrier of V

the carrier of V is non empty set
0. V is V48(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
W |-- (f,qf) is Element of [: the carrier of V, the carrier of V:]
[: the carrier of V, the carrier of V:] is V1() non empty set
[(0. V),W] is non empty Element of [: the carrier of V, the carrier of V:]
{(0. V),W} is V29() set
{(0. V)} is trivial V29() set
{{(0. V),W},{(0. V)}} is V29() V33() set
W |-- (qf,f) is Element of [: the carrier of V, the carrier of V:]
[W,(0. V)] is non empty Element of [: the carrier of V, the carrier of V:]
{W,(0. V)} is V29() set
{W} is trivial V29() set
{{W,(0. V)},{W}} is V29() V33() set

the carrier of V is non empty set

the carrier of f is non empty set

W is right_complementable Element of the carrier of V
the carrier of qf is non empty set

the carrier of V is non empty set
the carrier of qV is non empty set
the carrier of W is non empty set
the carrier of x is non empty set

A is right_complementable Element of the carrier of V
v is right_complementable Element of the carrier of W
a is right_complementable Element of the carrier of W
a is right_complementable Element of the carrier of W
a + a is right_complementable Element of the carrier of W
the addF of W is V1() V4([: the carrier of W, the carrier of W:]) V5( the carrier of W) Function-like non empty V14([: the carrier of W, the carrier of W:]) quasi_total Element of bool [:[: the carrier of W, the carrier of W:], the carrier of W:]
[: the carrier of W, the carrier of W:] is V1() non empty set
[:[: the carrier of W, the carrier of W:], the carrier of W:] is V1() 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,a) is right_complementable Element of the carrier of W
b is right_complementable Element of the carrier of V
s0 is right_complementable Element of the carrier of V
b + s0 is right_complementable Element of the carrier of V
the addF of V is V1() V4([: the carrier of V, the carrier of V:]) V5( the carrier of V) Function-like non empty V14([: the carrier of V, the carrier of V:]) quasi_total Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is V1() non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is V1() 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,s0) is right_complementable Element of the carrier of V
v 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 . (v,a) 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
the addF of W . (a,b) is right_complementable Element of the carrier of W

the carrier of V is non empty set

the carrier of f is non empty set
qf is right_complementable Element of the carrier of V
{qf} is trivial V29() 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 f
{W} is trivial V29() Element of bool the carrier of f
bool the carrier of f is non empty set

x is right_complementable Element of the carrier of V
the carrier of K is non empty non trivial set
w is right_complementable Element of the carrier of K
w * W is right_complementable Element of the carrier of f
the lmult of f is V1() V4([: the carrier of K, the carrier of f:]) V5( the carrier of f) Function-like non empty V14([: the carrier of K, the carrier of f:]) quasi_total Element of bool [:[: the carrier of K, the carrier of f:], the carrier of f:]
[: the carrier of K, the carrier of f:] is V1() non empty set
[:[: the carrier of K, the carrier of f:], the carrier of f:] is V1() non empty set
bool [:[: the carrier of K, the carrier of f:], the carrier of f:] is non empty set
the lmult of f . (w,W) is right_complementable Element of the carrier of f
w * qf is right_complementable Element of the carrier of V
the lmult of V is V1() V4([: the carrier of K, the carrier of V:]) V5( the carrier of V) Function-like non empty V14([: the carrier of K, the carrier of V:]) quasi_total Element of bool [:[: the carrier of K, the carrier of V:], the carrier of V:]
[: the carrier of K, the carrier of V:] is V1() non empty set
[:[: the carrier of K, the carrier of V:], the carrier of V:] is V1() non empty set
bool [:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set
the lmult of V . (w,qf) is right_complementable Element of the carrier of V
w is right_complementable Element of the carrier of K
w * qf is right_complementable Element of the carrier of V
the lmult of V . (w,qf) is right_complementable Element of the carrier of V
w * W is right_complementable Element of the carrier of f
the lmult of f . (w,W) is right_complementable Element of the carrier of f

the carrier of V is non empty set
f is right_complementable Element of the carrier of V
{f} is trivial V29() Element of bool the carrier of V
bool the carrier of V is non empty set

the carrier of (qf + ()) is non empty set
W is right_complementable Element of the carrier of (qf + ())
{W} is trivial V29() Element of bool the carrier of (qf + ())
bool the carrier of (qf + ()) is non empty set

the addF of (qf + ()) is V1() V4([: the carrier of (qf + ()), the carrier of (qf + ()):]) V5( the carrier of (qf + ())) Function-like non empty V14([: the carrier of (qf + ()), the carrier of (qf + ()):]) quasi_total Element of bool [:[: the carrier of (qf + ()), the carrier of (qf + ()):], the carrier of (qf + ()):]
[: the carrier of (qf + ()), the carrier of (qf + ()):] is V1() non empty set
[:[: the carrier of (qf + ()), the carrier of (qf + ()):], the carrier of (qf + ()):] is V1() non empty set
bool [:[: the carrier of (qf + ()), the carrier of (qf + ()):], the carrier of (qf + ()):] is non empty set
the ZeroF of (qf + ()) is right_complementable Element of the carrier of (qf + ())
the lmult of (qf + ()) is V1() V4([: the carrier of K, the carrier of (qf + ()):]) V5( the carrier of (qf + ())) Function-like non empty V14([: the carrier of K, the carrier of (qf + ()):]) quasi_total Element of bool [:[: the carrier of K, the carrier of (qf + ()):], the carrier of (qf + ()):]
the carrier of K is non empty non trivial set
[: the carrier of K, the carrier of (qf + ()):] is V1() non empty set
[:[: the carrier of K, the carrier of (qf + ()):], the carrier of (qf + ()):] is V1() non empty set
bool [:[: the carrier of K, the carrier of (qf + ()):], the carrier of (qf + ()):] is non empty set
VectSpStr(# the carrier of (qf + ()), the addF of (qf + ()), the ZeroF of (qf + ()), the lmult of (qf + ()) #) is non empty strict VectSpStr over K

x is right_complementable Element of the carrier of (qf + ())
w is right_complementable Element of the carrier of K
w * W is right_complementable Element of the carrier of (qf + ())
the lmult of (qf + ()) . (w,W) is right_complementable Element of the carrier of (qf + ())
0. K is V48(K) right_complementable Element of the carrier of K
the ZeroF of K is right_complementable Element of the carrier of K
0. (qf + ()) is V48(qf + ()) right_complementable Element of the carrier of (qf + ())
0. K is V48(K) right_complementable Element of the carrier of K
the ZeroF of K is right_complementable Element of the carrier of K
1_ K is right_complementable Element of the carrier of K
1. K is V48(K) right_complementable Element of the carrier of K
the OneF of K is right_complementable Element of the carrier of K
(1_ K) * W is right_complementable Element of the carrier of (qf + ())
the lmult of (qf + ()) . ((1_ K),W) is right_complementable Element of the carrier of (qf + ())
w " is right_complementable Element of the carrier of K
(w ") * w is right_complementable Element of the carrier of K
the multF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like non empty V14([: the carrier of K, the carrier of K:]) quasi_total Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is V1() non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is V1() non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K . ((w "),w) is right_complementable Element of the carrier of K
((w ") * w) * W is right_complementable Element of the carrier of (qf + ())
the lmult of (qf + ()) . (((w ") * w),W) is right_complementable Element of the carrier of (qf + ())
(w ") * (w * W) is right_complementable Element of the carrier of (qf + ())
the lmult of (qf + ()) . ((w "),(w * W)) is right_complementable Element of the carrier of (qf + ())
0. K is V48(K) right_complementable Element of the carrier of K
the ZeroF of K is right_complementable Element of the carrier of K
0. (qf + ()) is V48(qf + ()) right_complementable Element of the carrier of (qf + ())

the carrier of V is non empty set
f is right_complementable Element of the carrier of V
{f} is trivial V29() Element of bool the carrier of V
bool the carrier of V is non empty set

the carrier of (qf + ()) is non empty set
W is right_complementable Element of the carrier of (qf + ())
{W} is trivial V29() Element of bool the carrier of (qf + ())
bool the carrier of (qf + ()) is non empty set

W |-- (qV,()) is Element of [: the carrier of (qf + ()), the carrier of (qf + ()):]
[: the carrier of (qf + ()), the carrier of (qf + ()):] is V1() non empty set
the carrier of qV is non empty set
0. qV is V48(qV) right_complementable Element of the carrier of qV
the ZeroF of qV is right_complementable Element of the carrier of qV
[(0. qV),W] is non empty Element of [: the carrier of qV, the carrier of (qf + ()):]
[: the carrier of qV, the carrier of (qf + ()):] is V1() non empty set
{(0. qV),W} is V29() set
{(0. qV)} is trivial V29() set
{{(0. qV),W},{(0. qV)}} is V29() V33() set
0. (qf + ()) is V48(qf + ()) right_complementable Element of the carrier of (qf + ())
the ZeroF of (qf + ()) is right_complementable Element of the carrier of (qf + ())
[(0. (qf + ())),W] is non empty Element of [: the carrier of (qf + ()), the carrier of (qf + ()):]
{(0. (qf + ())),W} is V29() set
{(0. (qf + ()))} is trivial V29() set
{{(0. (qf + ())),W},{(0. (qf + ()))}} is V29() V33() set

the carrier of V is non empty set
0. V is V48(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
f is right_complementable Element of the carrier of V
{f} is trivial V29() Element of bool the carrier of V
bool the carrier of V is non empty set

the carrier of (qf + ()) is non empty set
W is right_complementable Element of the carrier of (qf + ())
{W} is trivial V29() Element of bool the carrier of (qf + ())
bool the carrier of (qf + ()) is non empty set

x is right_complementable Element of the carrier of (qf + ())
x |-- (qV,()) is Element of [: the carrier of (qf + ()), the carrier of (qf + ()):]
[: the carrier of (qf + ()), the carrier of (qf + ()):] is V1() non empty set
[x,(0. V)] is non empty Element of [: the carrier of (qf + ()), the carrier of V:]
[: the carrier of (qf + ()), the carrier of V:] is V1() non empty set
{x,(0. V)} is V29() set
{x} is trivial V29() set
{{x,(0. V)},{x}} is V29() V33() set
0. (qf + ()) is V48(qf + ()) right_complementable Element of the carrier of (qf + ())
the ZeroF of (qf + ()) is right_complementable Element of the carrier of (qf + ())
[x,(0. (qf + ()))] is non empty Element of [: the carrier of (qf + ()), the carrier of (qf + ()):]
{x,(0. (qf + ()))} is V29() set
{{x,(0. (qf + ()))},{x}} is V29() V33() set

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

f |-- (qf,W) is Element of [: the carrier of V, the carrier of V:]
[: the carrier of V, the carrier of V:] is V1() non empty set
(f |-- (qf,W)) `1 is right_complementable Element of the carrier of V
(f |-- (qf,W)) `2 is right_complementable Element of the carrier of V
[((f |-- (qf,W)) `1),((f |-- (qf,W)) `2)] is non empty Element of [: the carrier of V, the carrier of V:]
{((f |-- (qf,W)) `1),((f |-- (qf,W)) `2)} is V29() set
{((f |-- (qf,W)) `1)} is trivial V29() set
{{((f |-- (qf,W)) `1),((f |-- (qf,W)) `2)},{((f |-- (qf,W)) `1)}} is V29() V33() set

the carrier of K is non empty non trivial set

the carrier of V is non empty set
f is right_complementable Element of the carrier of V
{f} is trivial V29() Element of bool the carrier of V
bool the carrier of V is non empty set

the carrier of (qf + ()) is non empty set
the carrier of qf is non empty set
W is right_complementable Element of the carrier of (qf + ())
{W} is trivial V29() Element of bool the carrier of (qf + ())
bool the carrier of (qf + ()) is non empty set

x is right_complementable Element of the carrier of (qf + ())
x |-- (qV,()) is Element of [: the carrier of (qf + ()), the carrier of (qf + ()):]
[: the carrier of (qf + ()), the carrier of (qf + ()):] is V1() non empty set
w is right_complementable Element of the carrier of (qf + ())
A is right_complementable Element of the carrier of (qf + ())
[w,A] is non empty Element of [: the carrier of (qf + ()), the carrier of (qf + ()):]
{w,A} is V29() set
{w} is trivial V29() set
{{w,A},{w}} is V29() V33() set
a is right_complementable Element of the carrier of K
a * W is right_complementable Element of the carrier of (qf + ())
the lmult of (qf + ()) is V1() V4([: the carrier of K, the carrier of (qf + ()):]) V5( the carrier of (qf + ())) Function-like non empty V14([: the carrier of K, the carrier of (qf + ()):]) quasi_total Element of bool [:[: the carrier of K, the carrier of (qf + ()):], the carrier of (qf + ()):]
[: the carrier of K, the carrier of (qf + ()):] is V1() non empty set
[:[: the carrier of K, the carrier of (qf + ()):], the carrier of (qf + ()):] is V1() non empty set
bool [:[: the carrier of K, the carrier of (qf + ()):], the carrier of (qf + ()):] is non empty set
the lmult of (qf + ()) . (a,W) is right_complementable Element of the carrier of (qf + ())
v is right_complementable Element of the carrier of qf
a * f is right_complementable Element of the carrier of V
the lmult of V is V1() V4([: the carrier of K, the carrier of V:]) V5( the carrier of V) Function-like non empty V14([: the carrier of K, the carrier of V:]) quasi_total Element of bool [:[: the carrier of K, the carrier of V:], the carrier of V:]
[: the carrier of K, the carrier of V:] is V1() non empty set
[:[: the carrier of K, the carrier of V:], the carrier of V:] is V1() non empty set
bool [:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set
the lmult of V . (a,f) is right_complementable Element of the carrier of V
[v,(a * f)] is non empty Element of [: the carrier of qf, the carrier of V:]
[: the carrier of qf, the carrier of V:] is V1() non empty set
{v,(a * f)} is V29() set
{v} is trivial V29() set
{{v,(a * f)},{v}} is V29() V33() set

the carrier of K is non empty non trivial set

the carrier of V is non empty set
f is right_complementable Element of the carrier of V
{f} is trivial V29() Element of bool the carrier of V
bool the carrier of V is non empty set

the carrier of (qf + ()) is non empty set
the carrier of qf is non empty set
W is right_complementable Element of the carrier of (qf + ())
{W} is trivial V29() Element of bool the carrier of (qf + ())