K92() is Element of bool K88()
K88() is set
bool K88() is non empty set
K242() is strict doubleLoopStr
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
the V1() non-empty empty-yielding Function-like one-to-one constant functional empty trivial V29() V30() V33() set is V1() non-empty empty-yielding Function-like one-to-one constant functional empty trivial V29() V30() V33() set
1 is non empty set
{{},1} is V29() set
K is doubleLoopStr
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 right_complementable 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) 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 associative right-distributive left-distributive distributive left_unital 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
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 doubleLoopStr
(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
K is non empty right_complementable add-associative right_zeroed associative right-distributive left-distributive distributive left_unital doubleLoopStr
(K) is non empty right_complementable add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital 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
K is non empty non degenerated non trivial right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive left_unital doubleLoopStr
(K) is non empty non trivial right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital 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
K is non empty right_complementable add-associative right_zeroed associative right-distributive left-distributive distributive left_unital doubleLoopStr
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
f is non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over 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
K is non empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of V is non empty set
(0). V is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
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 non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
qf is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
f /\ qf is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace 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
K is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
the carrier of K is non empty non trivial set
V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
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
Lin {qf} is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
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
K is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
the carrier of K is non empty non trivial set
V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
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
K is non empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of V is non empty set
f is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
qf is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
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
K is non empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of V is non empty set
f is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
qf is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace 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
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
K is non empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of V is non empty set
f is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
qf is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace 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
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
K is non empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of V is non empty set
f is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
qf is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace 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
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
K is non empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
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 non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
qf is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace 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
K is non empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
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 non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
qf is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace 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
K is non empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of V is non empty set
f is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
the carrier of f is non empty set
qf is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of f
W is right_complementable Element of the carrier of V
the carrier of qf is non empty set
K is non empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
W is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
f is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
qf is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
f + qf is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
qV is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of W
x is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of W
qV + x is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of W
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
w is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
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
K is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of V is non empty set
f is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
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
Lin {qf} is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
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
Lin {W} is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of f
qV is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
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
K is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
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
Lin {f} is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
qf is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
qf + (Lin {f}) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
the carrier of (qf + (Lin {f})) is non empty set
W is right_complementable Element of the carrier of (qf + (Lin {f}))
{W} is trivial V29() Element of bool the carrier of (qf + (Lin {f}))
bool the carrier of (qf + (Lin {f})) is non empty set
Lin {W} is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of qf + (Lin {f})
qV is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of qf + (Lin {f})
the addF of (qf + (Lin {f})) is V1() V4([: the carrier of (qf + (Lin {f})), the carrier of (qf + (Lin {f})):]) V5( the carrier of (qf + (Lin {f}))) Function-like non empty V14([: the carrier of (qf + (Lin {f})), the carrier of (qf + (Lin {f})):]) quasi_total Element of bool [:[: the carrier of (qf + (Lin {f})), the carrier of (qf + (Lin {f})):], the carrier of (qf + (Lin {f})):]
[: the carrier of (qf + (Lin {f})), the carrier of (qf + (Lin {f})):] is V1() non empty set
[:[: the carrier of (qf + (Lin {f})), the carrier of (qf + (Lin {f})):], the carrier of (qf + (Lin {f})):] is V1() non empty set
bool [:[: the carrier of (qf + (Lin {f})), the carrier of (qf + (Lin {f})):], the carrier of (qf + (Lin {f})):] is non empty set
the ZeroF of (qf + (Lin {f})) is right_complementable Element of the carrier of (qf + (Lin {f}))
the lmult of (qf + (Lin {f})) is V1() V4([: the carrier of K, the carrier of (qf + (Lin {f})):]) V5( the carrier of (qf + (Lin {f}))) Function-like non empty V14([: the carrier of K, the carrier of (qf + (Lin {f})):]) quasi_total Element of bool [:[: the carrier of K, the carrier of (qf + (Lin {f})):], the carrier of (qf + (Lin {f})):]
the carrier of K is non empty non trivial set
[: the carrier of K, the carrier of (qf + (Lin {f})):] is V1() non empty set
[:[: the carrier of K, the carrier of (qf + (Lin {f})):], the carrier of (qf + (Lin {f})):] is V1() non empty set
bool [:[: the carrier of K, the carrier of (qf + (Lin {f})):], the carrier of (qf + (Lin {f})):] is non empty set
VectSpStr(# the carrier of (qf + (Lin {f})), the addF of (qf + (Lin {f})), the ZeroF of (qf + (Lin {f})), the lmult of (qf + (Lin {f})) #) is non empty strict VectSpStr over K
qV + (Lin {W}) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of qf + (Lin {f})
qV /\ (Lin {W}) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of qf + (Lin {f})
(0). (qf + (Lin {f})) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of qf + (Lin {f})
x is right_complementable Element of the carrier of (qf + (Lin {f}))
w is right_complementable Element of the carrier of K
w * W is right_complementable Element of the carrier of (qf + (Lin {f}))
the lmult of (qf + (Lin {f})) . (w,W) is right_complementable Element of the carrier of (qf + (Lin {f}))
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 + (Lin {f})) is V48(qf + (Lin {f})) right_complementable Element of the carrier of (qf + (Lin {f}))
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 + (Lin {f}))
the lmult of (qf + (Lin {f})) . ((1_ K),W) is right_complementable Element of the carrier of (qf + (Lin {f}))
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 + (Lin {f}))
the lmult of (qf + (Lin {f})) . (((w ") * w),W) is right_complementable Element of the carrier of (qf + (Lin {f}))
(w ") * (w * W) is right_complementable Element of the carrier of (qf + (Lin {f}))
the lmult of (qf + (Lin {f})) . ((w "),(w * W)) is right_complementable Element of the carrier of (qf + (Lin {f}))
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 + (Lin {f})) is V48(qf + (Lin {f})) right_complementable Element of the carrier of (qf + (Lin {f}))
K is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
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
Lin {f} is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
qf is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
qf + (Lin {f}) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
the carrier of (qf + (Lin {f})) is non empty set
W is right_complementable Element of the carrier of (qf + (Lin {f}))
{W} is trivial V29() Element of bool the carrier of (qf + (Lin {f}))
bool the carrier of (qf + (Lin {f})) is non empty set
Lin {W} is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of qf + (Lin {f})
qV is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of qf + (Lin {f})
W |-- (qV,(Lin {W})) is Element of [: the carrier of (qf + (Lin {f})), the carrier of (qf + (Lin {f})):]
[: the carrier of (qf + (Lin {f})), the carrier of (qf + (Lin {f})):] 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 + (Lin {f})):]
[: the carrier of qV, the carrier of (qf + (Lin {f})):] 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 + (Lin {f})) is V48(qf + (Lin {f})) right_complementable Element of the carrier of (qf + (Lin {f}))
the ZeroF of (qf + (Lin {f})) is right_complementable Element of the carrier of (qf + (Lin {f}))
[(0. (qf + (Lin {f}))),W] is non empty Element of [: the carrier of (qf + (Lin {f})), the carrier of (qf + (Lin {f})):]
{(0. (qf + (Lin {f}))),W} is V29() set
{(0. (qf + (Lin {f})))} is trivial V29() set
{{(0. (qf + (Lin {f}))),W},{(0. (qf + (Lin {f})))}} is V29() V33() set
K is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
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
Lin {f} is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
qf is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
qf + (Lin {f}) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
the carrier of (qf + (Lin {f})) is non empty set
W is right_complementable Element of the carrier of (qf + (Lin {f}))
{W} is trivial V29() Element of bool the carrier of (qf + (Lin {f}))
bool the carrier of (qf + (Lin {f})) is non empty set
Lin {W} is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of qf + (Lin {f})
qV is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of qf + (Lin {f})
x is right_complementable Element of the carrier of (qf + (Lin {f}))
x |-- (qV,(Lin {W})) is Element of [: the carrier of (qf + (Lin {f})), the carrier of (qf + (Lin {f})):]
[: the carrier of (qf + (Lin {f})), the carrier of (qf + (Lin {f})):] is V1() non empty set
[x,(0. V)] is non empty Element of [: the carrier of (qf + (Lin {f})), the carrier of V:]
[: the carrier of (qf + (Lin {f})), 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 + (Lin {f})) is V48(qf + (Lin {f})) right_complementable Element of the carrier of (qf + (Lin {f}))
the ZeroF of (qf + (Lin {f})) is right_complementable Element of the carrier of (qf + (Lin {f}))
[x,(0. (qf + (Lin {f})))] is non empty Element of [: the carrier of (qf + (Lin {f})), the carrier of (qf + (Lin {f})):]
{x,(0. (qf + (Lin {f})))} is V29() set
{{x,(0. (qf + (Lin {f})))},{x}} is V29() V33() set
K is non empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of V is non empty set
f is right_complementable Element of the carrier of V
qf is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
W is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace 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
K is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
the carrier of K is non empty non trivial set
V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
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
Lin {f} is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
qf is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
qf + (Lin {f}) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
the carrier of (qf + (Lin {f})) is non empty set
the carrier of qf is non empty set
W is right_complementable Element of the carrier of (qf + (Lin {f}))
{W} is trivial V29() Element of bool the carrier of (qf + (Lin {f}))
bool the carrier of (qf + (Lin {f})) is non empty set
Lin {W} is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of qf + (Lin {f})
qV is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of qf + (Lin {f})
x is right_complementable Element of the carrier of (qf + (Lin {f}))
x |-- (qV,(Lin {W})) is Element of [: the carrier of (qf + (Lin {f})), the carrier of (qf + (Lin {f})):]
[: the carrier of (qf + (Lin {f})), the carrier of (qf + (Lin {f})):] is V1() non empty set
w is right_complementable Element of the carrier of (qf + (Lin {f}))
A is right_complementable Element of the carrier of (qf + (Lin {f}))
[w,A] is non empty Element of [: the carrier of (qf + (Lin {f})), the carrier of (qf + (Lin {f})):]
{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 + (Lin {f}))
the lmult of (qf + (Lin {f})) is V1() V4([: the carrier of K, the carrier of (qf + (Lin {f})):]) V5( the carrier of (qf + (Lin {f}))) Function-like non empty V14([: the carrier of K, the carrier of (qf + (Lin {f})):]) quasi_total Element of bool [:[: the carrier of K, the carrier of (qf + (Lin {f})):], the carrier of (qf + (Lin {f})):]
[: the carrier of K, the carrier of (qf + (Lin {f})):] is V1() non empty set
[:[: the carrier of K, the carrier of (qf + (Lin {f})):], the carrier of (qf + (Lin {f})):] is V1() non empty set
bool [:[: the carrier of K, the carrier of (qf + (Lin {f})):], the carrier of (qf + (Lin {f})):] is non empty set
the lmult of (qf + (Lin {f})) . (a,W) is right_complementable Element of the carrier of (qf + (Lin {f}))
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
K is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
the carrier of K is non empty non trivial set
V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
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
Lin {f} is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
qf is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
qf + (Lin {f}) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
the carrier of (qf + (Lin {f})) is non empty set
the carrier of qf is non empty set
W is right_complementable Element of the carrier of (qf + (Lin {f}))
{W} is trivial V29() Element of bool the carrier of (qf + (Lin {f}))
bool the carrier of (qf + (Lin {f})) is non empty set
Lin {W} is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of qf + (Lin {f})
qV is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of qf + (Lin {f})
x is right_complementable Element of the carrier of (qf + (Lin {f}))
x |-- (qV,(Lin {W})) is Element of [: the carrier of (qf + (Lin {f})), the carrier of (qf + (Lin {f})):]
[: the carrier of (qf + (Lin {f})), the carrier of (qf + (Lin {f})):] is V1() non empty set
w is right_complementable Element of the carrier of (qf + (Lin {f}))
w |-- (qV,(Lin {W})) is Element of [: the carrier of (qf + (Lin {f})), the carrier of (qf + (Lin {f})):]
x + w is right_complementable Element of the carrier of (qf + (Lin {f}))
the addF of (qf + (Lin {f})) is V1() V4([: the carrier of (qf + (Lin {f})), the carrier of (qf + (Lin {f})):]) V5( the carrier of (qf + (Lin {f}))) Function-like non empty V14([: the carrier of (qf + (Lin {f})), the carrier of (qf + (Lin {f})):]) quasi_total Element of bool [:[: the carrier of (qf + (Lin {f})), the carrier of (qf + (Lin {f})):], the carrier of (qf + (Lin {f})):]
[:[: the carrier of (qf + (Lin {f})), the carrier of (qf + (Lin {f})):], the carrier of (qf + (Lin {f})):] is V1() non empty set
bool [:[: the carrier of (qf + (Lin {f})), the carrier of (qf + (Lin {f})):], the carrier of (qf + (Lin {f})):] is non empty set
the addF of (qf + (Lin {f})) . (x,w) is right_complementable Element of the carrier of (qf + (Lin {f}))
(x + w) |-- (qV,(Lin {W})) is Element of [: the carrier of (qf + (Lin {f})), the carrier of (qf + (Lin {f})):]
A is right_complementable Element of the carrier of qf
v is right_complementable Element of the carrier of qf
A + v is right_complementable Element of the carrier of qf
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 addF of qf . (A,v) is right_complementable Element of the carrier of qf
a is right_complementable Element of the carrier of K
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
[A,(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
{A,(a * f)} is V29() set
{A} is trivial V29() set
{{A,(a * f)},{A}} is V29() V33() set
a is right_complementable Element of the carrier of K
a * f is right_complementable Element of the carrier of V
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:]
{v,(a * f)} is V29() set
{v} is trivial V29() set
{{v,(a * f)},{v}} is V29() V33() set
a + a 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 . (a,a) is right_complementable Element of the carrier of K
(a + a) * f is right_complementable Element of the carrier of V
the lmult of V . ((a + a),f) is right_complementable Element of the carrier of V
[(A + v),((a + a) * f)] is non empty Element of [: the carrier of qf, the carrier of V:]
{(A + v),((a + a) * f)} is V29() set
{(A + v)} is trivial V29() set
{{(A + v),((a + a) * f)},{(A + v)}} is V29() V33() set
a * W is right_complementable Element of the carrier of (qf + (Lin {f}))
the lmult of (qf + (Lin {f})) is V1() V4([: the carrier of K, the carrier of (qf + (Lin {f})):]) V5( the carrier of (qf + (Lin {f}))) Function-like non empty V14([: the carrier of K, the carrier of (qf + (Lin {f})):]) quasi_total Element of bool [:[: the carrier of K, the carrier of (qf + (Lin {f})):], the carrier of (qf + (Lin {f})):]
[: the carrier of K, the carrier of (qf + (Lin {f})):] is V1() non empty set
[:[: the carrier of K, the carrier of (qf + (Lin {f})):], the carrier of (qf + (Lin {f})):] is V1() non empty set
bool [:[: the carrier of K, the carrier of (qf + (Lin {f})):], the carrier of (qf + (Lin {f})):] is non empty set
the lmult of (qf + (Lin {f})) . (a,W) is right_complementable Element of the carrier of (qf + (Lin {f}))
s0 is right_complementable Element of the carrier of (qf + (Lin {f}))
(a + a) * W is right_complementable Element of the carrier of (qf + (Lin {f}))
the lmult of (qf + (Lin {f})) . ((a + a),W) is right_complementable Element of the carrier of (qf + (Lin {f}))
b is right_complementable Element of the carrier of (qf + (Lin {f}))
b + s0 is right_complementable Element of the carrier of (qf + (Lin {f}))
the addF of (qf + (Lin {f})) . (b,s0) is right_complementable Element of the carrier of (qf + (Lin {f}))
x2 is right_complementable Element of the carrier of V
s2 is right_complementable Element of the carrier of V
x2 + s2 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 . (x2,s2) is right_complementable Element of the carrier of V
a * W is right_complementable Element of the carrier of (qf + (Lin {f}))
the lmult of (qf + (Lin {f})) . (a,W) is right_complementable Element of the carrier of (qf + (Lin {f}))
s0 + (a * W) is right_complementable Element of the carrier of (qf + (Lin {f}))
the addF of (qf + (Lin {f})) . (s0,(a * W)) is right_complementable Element of the carrier of (qf + (Lin {f}))
b + (a * W) is right_complementable Element of the carrier of (qf + (Lin {f}))
the addF of (qf + (Lin {f})) . (b,(a * W)) is right_complementable Element of the carrier of (qf + (Lin {f}))
(b + (a * W)) + s0 is right_complementable Element of the carrier of (qf + (Lin {f}))
the addF of (qf + (Lin {f})) . ((b + (a * W)),s0) is right_complementable Element of the carrier of (qf + (Lin {f}))
((b + (a * W)) + s0) + (a * W) is right_complementable Element of the carrier of (qf + (Lin {f}))
the addF of (qf + (Lin {f})) . (((b + (a * W)) + s0),(a * W)) is right_complementable Element of the carrier of (qf + (Lin {f}))
(b + s0) + (a * W) is right_complementable Element of the carrier of (qf + (Lin {f}))
the addF of (qf + (Lin {f})) . ((b + s0),(a * W)) is right_complementable Element of the carrier of (qf + (Lin {f}))
((b + s0) + (a * W)) + (a * W) is right_complementable Element of the carrier of (qf + (Lin {f}))
the addF of (qf + (Lin {f})) . (((b + s0) + (a * W)),(a * W)) is right_complementable Element of the carrier of (qf + (Lin {f}))
(a * W) + (a * W) is right_complementable Element of the carrier of (qf + (Lin {f}))
the addF of (qf + (Lin {f})) . ((a * W),(a * W)) is right_complementable Element of the carrier of (qf + (Lin {f}))
(b + s0) + ((a * W) + (a * W)) is right_complementable Element of the carrier of (qf + (Lin {f}))
the addF of (qf + (Lin {f})) . ((b + s0),((a * W) + (a * W))) is right_complementable Element of the carrier of (qf + (Lin {f}))
(b + s0) + ((a + a) * W) is right_complementable Element of the carrier of (qf + (Lin {f}))
the addF of (qf + (Lin {f})) . ((b + s0),((a + a) * W)) is right_complementable Element of the carrier of (qf + (Lin {f}))
K is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
the carrier of K is non empty non trivial set
V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
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
Lin {f} is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
qf is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
qf + (Lin {f}) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
the carrier of (qf + (Lin {f})) is non empty set
the carrier of qf is non empty set
W is right_complementable Element of the carrier of (qf + (Lin {f}))
{W} is trivial V29() Element of bool the carrier of (qf + (Lin {f}))
bool the carrier of (qf + (Lin {f})) is non empty set
Lin {W} is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of qf + (Lin {f})
qV is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of qf + (Lin {f})
x is right_complementable Element of the carrier of (qf + (Lin {f}))
x |-- (qV,(Lin {W})) is Element of [: the carrier of (qf + (Lin {f})), the carrier of (qf + (Lin {f})):]
[: the carrier of (qf + (Lin {f})), the carrier of (qf + (Lin {f})):] is V1() non empty set
w is right_complementable Element of the carrier of qf
v is right_complementable Element of the carrier of K
v * 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 . (v,f) is right_complementable Element of the carrier of V
[w,(v * 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
{w,(v * f)} is V29() set
{w} is trivial V29() set
{{w,(v * f)},{w}} is V29() V33() set
A is right_complementable Element of the carrier of K
A * x is right_complementable Element of the carrier of (qf + (Lin {f}))
the lmult of (qf + (Lin {f})) is V1() V4([: the carrier of K, the carrier of (qf + (Lin {f})):]) V5( the carrier of (qf + (Lin {f}))) Function-like non empty V14([: the carrier of K, the carrier of (qf + (Lin {f})):]) quasi_total Element of bool [:[: the carrier of K, the carrier of (qf + (Lin {f})):], the carrier of (qf + (Lin {f})):]
[: the carrier of K, the carrier of (qf + (Lin {f})):] is V1() non empty set
[:[: the carrier of K, the carrier of (qf + (Lin {f})):], the carrier of (qf + (Lin {f})):] is V1() non empty set
bool [:[: the carrier of K, the carrier of (qf + (Lin {f})):], the carrier of (qf + (Lin {f})):] is non empty set
the lmult of (qf + (Lin {f})) . (A,x) is right_complementable Element of the carrier of (qf + (Lin {f}))
(A * x) |-- (qV,(Lin {W})) is Element of [: the carrier of (qf + (Lin {f})), the carrier of (qf + (Lin {f})):]
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
A * v 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 . (A,v) is right_complementable Element of the carrier of K
(A * v) * f is right_complementable Element of the carrier of V
the lmult of V . ((A * v),f) is right_complementable Element of the carrier of V
[(A * w),((A * v) * f)] is non empty Element of [: the carrier of qf, the carrier of V:]
{(A * w),((A * v) * f)} is V29() set
{(A * w)} is trivial V29() set
{{(A * w),((A * v) * f)},{(A * w)}} is V29() V33() set
v * W is right_complementable Element of the carrier of (qf + (Lin {f}))
the lmult of (qf + (Lin {f})) . (v,W) is right_complementable Element of the carrier of (qf + (Lin {f}))
a is right_complementable Element of the carrier of (qf + (Lin {f}))
a + (v * W) is right_complementable Element of the carrier of (qf + (Lin {f}))
the addF of (qf + (Lin {f})) is V1() V4([: the carrier of (qf + (Lin {f})), the carrier of (qf + (Lin {f})):]) V5( the carrier of (qf + (Lin {f}))) Function-like non empty V14([: the carrier of (qf + (Lin {f})), the carrier of (qf + (Lin {f})):]) quasi_total Element of bool [:[: the carrier of (qf + (Lin {f})), the carrier of (qf + (Lin {f})):], the carrier of (qf + (Lin {f})):]
[:[: the carrier of (qf + (Lin {f})), the carrier of (qf + (Lin {f})):], the carrier of (qf + (Lin {f})):] is V1() non empty set
bool [:[: the carrier of (qf + (Lin {f})), the carrier of (qf + (Lin {f})):], the carrier of (qf + (Lin {f})):] is non empty set
the addF of (qf + (Lin {f})) . (a,(v * W)) is right_complementable Element of the carrier of (qf + (Lin {f}))
A * (a + (v * W)) is right_complementable Element of the carrier of (qf + (Lin {f}))
the lmult of (qf + (Lin {f})) . (A,(a + (v * W))) is right_complementable Element of the carrier of (qf + (Lin {f}))
A * a is right_complementable Element of the carrier of (qf + (Lin {f}))
the lmult of (qf + (Lin {f})) . (A,a) is right_complementable Element of the carrier of (qf + (Lin {f}))
A * (v * W) is right_complementable Element of the carrier of (qf + (Lin {f}))
the lmult of (qf + (Lin {f})) . (A,(v * W)) is right_complementable Element of the carrier of (qf + (Lin {f}))
(A * a) + (A * (v * W)) is right_complementable Element of the carrier of (qf + (Lin {f}))
the addF of (qf + (Lin {f})) . ((A * a),(A * (v * W))) is right_complementable Element of the carrier of (qf + (Lin {f}))
(A * v) * W is right_complementable Element of the carrier of (qf + (Lin {f}))
the lmult of (qf + (Lin {f})) . ((A * v),W) is right_complementable Element of the carrier of (qf + (Lin {f}))
(A * a) + ((A * v) * W) is right_complementable Element of the carrier of (qf + (Lin {f}))
the addF of (qf + (Lin {f})) . ((A * a),((A * v) * W)) is right_complementable Element of the carrier of (qf + (Lin {f}))
a is right_complementable Element of the carrier of V
A * a is right_complementable Element of the carrier of V
the lmult of V . (A,a) is right_complementable Element of the carrier of V
K is non empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
f is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
{ b1 where b1 is Coset of f : verum } is set
the carrier of V is non empty set
bool the carrier of V is non empty set
bool (bool the carrier of V) is non empty set
W is set
qV is Coset of f
the carrier of f is non empty set
K is non empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
f is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
(K,V,f) is non empty Element of bool (bool the carrier of V)
the carrier of V is non empty set
bool the carrier of V is non empty set
bool (bool the carrier of V) is non empty set
{ b1 where b1 is Coset of f : verum } is set
[:(K,V,f),(K,V,f):] is V1() non empty set
[:[:(K,V,f),(K,V,f):],(K,V,f):] is V1() non empty set
bool [:[:(K,V,f),(K,V,f):],(K,V,f):] is non empty set
W is Element of (K,V,f)
x is Coset of f
w is right_complementable Element of the carrier of V
w + f is Element of bool the carrier of V
{ (w + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
qV is Element of (K,V,f)
A is Coset of f
v is right_complementable Element of the carrier of V
v + f is Element of bool the carrier of V
{ (v + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
w + 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:] 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 . (w,v) is right_complementable Element of the carrier of V
(w + v) + f is Element of bool the carrier of V
{ ((w + v) + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
a is Coset of f
a is Element of (K,V,f)
b is Element of (K,V,f)
s0 is right_complementable Element of the carrier of V
s0 + f is Element of bool the carrier of V
{ (s0 + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
x2 is right_complementable Element of the carrier of V
x2 + f is Element of bool the carrier of V
{ (x2 + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
s0 + x2 is right_complementable Element of the carrier of V
the addF of V . (s0,x2) is right_complementable Element of the carrier of V
(s0 + x2) + f is Element of bool the carrier of V
{ ((s0 + x2) + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
s2 is right_complementable Element of the carrier of V
w + s2 is right_complementable Element of the carrier of V
the addF of V . (w,s2) is right_complementable Element of the carrier of V
c is right_complementable Element of the carrier of V
v + c is right_complementable Element of the carrier of V
the addF of V . (v,c) is right_complementable Element of the carrier of V
s2 + c is right_complementable Element of the carrier of V
the addF of V . (s2,c) is right_complementable Element of the carrier of V
s2 + w is right_complementable Element of the carrier of V
the addF of V . (s2,w) is right_complementable Element of the carrier of V
(s2 + w) + v is right_complementable Element of the carrier of V
the addF of V . ((s2 + w),v) is right_complementable Element of the carrier of V
((s2 + w) + v) + c is right_complementable Element of the carrier of V
the addF of V . (((s2 + w) + v),c) is right_complementable Element of the carrier of V
s2 + (w + v) is right_complementable Element of the carrier of V
the addF of V . (s2,(w + v)) is right_complementable Element of the carrier of V
(s2 + (w + v)) + c is right_complementable Element of the carrier of V
the addF of V . ((s2 + (w + v)),c) is right_complementable Element of the carrier of V
(w + v) + (s2 + c) is right_complementable Element of the carrier of V
the addF of V . ((w + v),(s2 + c)) is right_complementable Element of the carrier of V
W is V1() V4([:(K,V,f),(K,V,f):]) V5((K,V,f)) Function-like non empty V14([:(K,V,f),(K,V,f):]) quasi_total Element of bool [:[:(K,V,f),(K,V,f):],(K,V,f):]
qV is V1() V4([:(K,V,f),(K,V,f):]) V5((K,V,f)) Function-like non empty V14([:(K,V,f),(K,V,f):]) quasi_total Element of bool [:[:(K,V,f),(K,V,f):],(K,V,f):]
x is Element of (K,V,f)
w is Element of (K,V,f)
qV . (x,w) is Element of (K,V,f)
A is right_complementable Element of the carrier of V
A + f is Element of bool the carrier of V
{ (A + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
v is right_complementable Element of the carrier of V
v + f is Element of bool the carrier of V
{ (v + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
A + v is right_complementable Element of the carrier of V
the addF of V . (A,v) is right_complementable Element of the carrier of V
(A + v) + f is Element of bool the carrier of V
{ ((A + v) + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
W is V1() V4([:(K,V,f),(K,V,f):]) V5((K,V,f)) Function-like non empty V14([:(K,V,f),(K,V,f):]) quasi_total Element of bool [:[:(K,V,f),(K,V,f):],(K,V,f):]
qV is V1() V4([:(K,V,f),(K,V,f):]) V5((K,V,f)) Function-like non empty V14([:(K,V,f),(K,V,f):]) quasi_total Element of bool [:[:(K,V,f),(K,V,f):],(K,V,f):]
x is Element of (K,V,f)
A is Coset of f
v is right_complementable Element of the carrier of V
v + f is Element of bool the carrier of V
{ (v + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
w is Element of (K,V,f)
a is Coset of f
a is right_complementable Element of the carrier of V
a + f is Element of bool the carrier of V
{ (a + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
W . (x,w) is Element of (K,V,f)
v + a 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 . (v,a) is right_complementable Element of the carrier of V
(v + a) + f is Element of bool the carrier of V
{ ((v + a) + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
qV . (x,w) is Element of (K,V,f)
K is non empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
f is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
the carrier of f is non empty set
the carrier of V is non empty set
bool the carrier of V is non empty set
(K,V,f) is non empty Element of bool (bool the carrier of V)
bool (bool the carrier of V) is non empty set
{ b1 where b1 is Coset of f : verum } is 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
(0. V) + f is Element of bool the carrier of V
{ ((0. V) + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
K is non empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of K is non empty set
f is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
(K,V,f) is non empty Element of bool (bool the carrier of V)
the carrier of V is non empty set
bool the carrier of V is non empty set
bool (bool the carrier of V) is non empty set
{ b1 where b1 is Coset of f : verum } is set
[: the carrier of K,(K,V,f):] is V1() non empty set
[:[: the carrier of K,(K,V,f):],(K,V,f):] is V1() non empty set
bool [:[: the carrier of K,(K,V,f):],(K,V,f):] is non empty set
x is Element of (K,V,f)
w is Coset of f
A is right_complementable Element of the carrier of V
A + f is Element of bool the carrier of V
{ (A + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
qV is right_complementable Element of the carrier of K
qV * A 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 . (qV,A) is right_complementable Element of the carrier of V
(qV * A) + f is Element of bool the carrier of V
{ ((qV * A) + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
v is Coset of f
a is Element of (K,V,f)
a is Element of (K,V,f)
b is right_complementable Element of the carrier of V
b + f is Element of bool the carrier of V
{ (b + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
qV * b is right_complementable Element of the carrier of V
the lmult of V . (qV,b) is right_complementable Element of the carrier of V
(qV * b) + f is Element of bool the carrier of V
{ ((qV * b) + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
s0 is right_complementable Element of the carrier of V
A + 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 . (A,s0) is right_complementable Element of the carrier of V
qV * s0 is right_complementable Element of the carrier of V
the lmult of V . (qV,s0) is right_complementable Element of the carrier of V
(qV * A) + (qV * s0) is right_complementable Element of the carrier of V
the addF of V . ((qV * A),(qV * s0)) is right_complementable Element of the carrier of V
qV is V1() V4([: the carrier of K,(K,V,f):]) V5((K,V,f)) Function-like non empty V14([: the carrier of K,(K,V,f):]) quasi_total Element of bool [:[: the carrier of K,(K,V,f):],(K,V,f):]
x is right_complementable Element of the carrier of K
w is Element of (K,V,f)
qV . (x,w) is Element of (K,V,f)
A is right_complementable Element of the carrier of V
A + f is Element of bool the carrier of V
{ (A + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
x * A is right_complementable Element of the carrier of V
the lmult of V . (x,A) is right_complementable Element of the carrier of V
(x * A) + f is Element of bool the carrier of V
{ ((x * A) + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
qV is V1() V4([: the carrier of K,(K,V,f):]) V5((K,V,f)) Function-like non empty V14([: the carrier of K,(K,V,f):]) quasi_total Element of bool [:[: the carrier of K,(K,V,f):],(K,V,f):]
x is V1() V4([: the carrier of K,(K,V,f):]) V5((K,V,f)) Function-like non empty V14([: the carrier of K,(K,V,f):]) quasi_total Element of bool [:[: the carrier of K,(K,V,f):],(K,V,f):]
v is Element of (K,V,f)
a is Coset of f
a is right_complementable Element of the carrier of V
a + f is Element of bool the carrier of V
{ (a + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
A is right_complementable Element of the carrier of K
qV . (A,v) is Element of (K,V,f)
A * a 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,a) is right_complementable Element of the carrier of V
(A * a) + f is Element of bool the carrier of V
{ ((A * a) + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
x . (A,v) is Element of (K,V,f)
K is non empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
f is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
(K,V,f) is non empty Element of bool (bool the carrier of V)
the carrier of V is non empty set
bool the carrier of V is non empty set
bool (bool the carrier of V) is non empty set
{ b1 where b1 is Coset of f : verum } is set
[:(K,V,f),(K,V,f):] is V1() non empty set
(K,V,f) is V1() V4([:(K,V,f),(K,V,f):]) V5((K,V,f)) Function-like non empty V14([:(K,V,f),(K,V,f):]) quasi_total Element of bool [:[:(K,V,f),(K,V,f):],(K,V,f):]
[:[:(K,V,f),(K,V,f):],(K,V,f):] is V1() non empty set
bool [:[:(K,V,f),(K,V,f):],(K,V,f):] is non empty set
(K,V,f) is Element of (K,V,f)
the carrier of f is non empty set
the carrier of K is non empty set
[: the carrier of K,(K,V,f):] is V1() non empty set
(K,V,f) is V1() V4([: the carrier of K,(K,V,f):]) V5((K,V,f)) Function-like non empty V14([: the carrier of K,(K,V,f):]) quasi_total Element of bool [:[: the carrier of K,(K,V,f):],(K,V,f):]
[:[: the carrier of K,(K,V,f):],(K,V,f):] is V1() non empty set
bool [:[: the carrier of K,(K,V,f):],(K,V,f):] is non empty set
VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #) is non empty strict VectSpStr over K
the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #) is non empty set
A is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
0. VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #) is V48( VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)) Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
the ZeroF of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #) is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
A + (0. VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)) is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
the addF of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #) is V1() V4([: the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #), the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #):]) V5( the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)) Function-like non empty V14([: the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #), the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #):]) quasi_total Element of bool [:[: the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #), the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #):], the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #):]
[: the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #), the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #):] is V1() non empty set
[:[: the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #), the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #):], the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #):] is V1() non empty set
bool [:[: the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #), the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #):], the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #):] is non empty set
the addF of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #) . (A,(0. VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #))) is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
v is Coset of f
a is right_complementable Element of the carrier of V
a + f is Element of bool the carrier of V
{ (a + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is 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
(0. V) + f is Element of bool the carrier of V
{ ((0. V) + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
a + (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:] 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 . (a,(0. V)) is right_complementable Element of the carrier of V
(a + (0. V)) + f is Element of bool the carrier of V
{ ((a + (0. V)) + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #) is non empty set
A is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
0. VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #) is V48( VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)) Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
the ZeroF of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #) is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
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
(0. V) + f is Element of bool the carrier of V
{ ((0. V) + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
v is Coset of f
a is right_complementable Element of the carrier of V
a + f is Element of bool the carrier of V
{ (a + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
- a is right_complementable Element of the carrier of V
(- a) + f is Element of bool the carrier of V
{ ((- a) + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
b is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
A + b is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
the addF of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #) is V1() V4([: the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #), the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #):]) V5( the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)) Function-like non empty V14([: the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #), the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #):]) quasi_total Element of bool [:[: the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #), the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #):], the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #):]
[: the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #), the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #):] is V1() non empty set
[:[: the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #), the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #):], the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #):] is V1() non empty set
bool [:[: the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #), the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #):], the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #):] is non empty set
the addF of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #) . (A,b) is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
a + (- a) 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 . (a,(- a)) is right_complementable Element of the carrier of V
(a + (- a)) + f is Element of bool the carrier of V
{ ((a + (- a)) + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #) is non empty set
a is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
b is Coset of f
a is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
s0 is Coset of f
x2 is right_complementable Element of the carrier of V
x2 + f is Element of bool the carrier of V
{ (x2 + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
A is right_complementable Element of the carrier of K
(K,V,f) . (A,a) is set
A * a is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
the lmult of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #) is V1() V4([: the carrier of K, the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #):]) V5( the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)) Function-like non empty V14([: the carrier of K, the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #):]) quasi_total Element of bool [:[: the carrier of K, the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #):], the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #):]
[: the carrier of K, the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #):] is V1() non empty set
[:[: the carrier of K, the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #):], the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #):] is V1() non empty set
bool [:[: the carrier of K, the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #):], the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #):] is non empty set
the lmult of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #) . (A,a) is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
A * x2 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,x2) is right_complementable Element of the carrier of V
(A * x2) + f is Element of bool the carrier of V
{ ((A * x2) + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
s2 is right_complementable Element of the carrier of V
s2 + f is Element of bool the carrier of V
{ (s2 + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
(K,V,f) . (a,a) is set
s2 + x2 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 . (s2,x2) is right_complementable Element of the carrier of V
(s2 + x2) + f is Element of bool the carrier of V
{ ((s2 + x2) + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
(K,V,f) . (A,a) is set
A * s2 is right_complementable Element of the carrier of V
the lmult of V . (A,s2) is right_complementable Element of the carrier of V
(A * s2) + f is Element of bool the carrier of V
{ ((A * s2) + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
a + a is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
the addF of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #) is V1() V4([: the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #), the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #):]) V5( the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)) Function-like non empty V14([: the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #), the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #):]) quasi_total Element of bool [:[: the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #), the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #):], the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #):]
[: the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #), the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #):] is V1() non empty set
[:[: the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #), the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #):], the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #):] is V1() non empty set
bool [:[: the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #), the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #):], the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #):] is non empty set
the addF of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #) . (a,a) is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
A * (a + a) is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
the lmult of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #) . (A,(a + a)) is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
(K,V,f) . (A,( the addF of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #) . (a,a))) is set
A * (s2 + x2) is right_complementable Element of the carrier of V
the lmult of V . (A,(s2 + x2)) is right_complementable Element of the carrier of V
(A * (s2 + x2)) + f is Element of bool the carrier of V
{ ((A * (s2 + x2)) + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
(A * s2) + (A * x2) is right_complementable Element of the carrier of V
the addF of V . ((A * s2),(A * x2)) is right_complementable Element of the carrier of V
((A * s2) + (A * x2)) + f is Element of bool the carrier of V
{ (((A * s2) + (A * x2)) + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
A * a is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
the lmult of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #) . (A,a) is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
(A * a) + (A * a) is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
the addF of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #) . ((A * a),(A * a)) is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
v is right_complementable Element of the carrier of K
(K,V,f) . (v,a) is set
v * s2 is right_complementable Element of the carrier of V
the lmult of V . (v,s2) is right_complementable Element of the carrier of V
(v * s2) + f is Element of bool the carrier of V
{ ((v * s2) + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
A + v 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 . (A,v) is right_complementable Element of the carrier of K
(A + v) * a is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
the lmult of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #) . ((A + v),a) is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
(A + v) * s2 is right_complementable Element of the carrier of V
the lmult of V . ((A + v),s2) is right_complementable Element of the carrier of V
((A + v) * s2) + f is Element of bool the carrier of V
{ (((A + v) * s2) + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
(A * s2) + (v * s2) is right_complementable Element of the carrier of V
the addF of V . ((A * s2),(v * s2)) is right_complementable Element of the carrier of V
((A * s2) + (v * s2)) + f is Element of bool the carrier of V
{ (((A * s2) + (v * s2)) + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
v * a is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
the lmult of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #) . (v,a) is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
(A * a) + (v * a) is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
the addF of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #) . ((A * a),(v * a)) is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
A * v 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 . (A,v) is right_complementable Element of the carrier of K
(A * v) * a is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
the lmult of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #) . ((A * v),a) is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
(A * v) * s2 is right_complementable Element of the carrier of V
the lmult of V . ((A * v),s2) is right_complementable Element of the carrier of V
((A * v) * s2) + f is Element of bool the carrier of V
{ (((A * v) * s2) + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
A * (v * s2) is right_complementable Element of the carrier of V
the lmult of V . (A,(v * s2)) is right_complementable Element of the carrier of V
(A * (v * s2)) + f is Element of bool the carrier of V
{ ((A * (v * s2)) + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
(K,V,f) . (A,(v * a)) is set
A * (v * a) is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
the lmult of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #) . (A,(v * a)) is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
1_ K is right_complementable Element of the carrier of K
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) * a is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
the lmult of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #) . ((1_ K),a) is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
(1_ K) * s2 is right_complementable Element of the carrier of V
the lmult of V . ((1_ K),s2) is right_complementable Element of the carrier of V
((1_ K) * s2) + f is Element of bool the carrier of V
{ (((1_ K) * s2) + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
A is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
v is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
A + v is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
the addF of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #) . (A,v) is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
v + A is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
the addF of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #) . (v,A) is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
a is Coset of f
a is right_complementable Element of the carrier of V
a + f is Element of bool the carrier of V
{ (a + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
b is Coset of f
s0 is right_complementable Element of the carrier of V
s0 + f is Element of bool the carrier of V
{ (s0 + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
a + s0 is right_complementable Element of the carrier of V
the addF of V . (a,s0) is right_complementable Element of the carrier of V
(a + s0) + f is Element of bool the carrier of V
{ ((a + s0) + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
A is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
v is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
A + v is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
the addF of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #) . (A,v) is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
a is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
(A + v) + a is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
the addF of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #) . ((A + v),a) is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
v + a is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
the addF of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #) . (v,a) is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
A + (v + a) is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
the addF of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #) . (A,(v + a)) is Element of the carrier of VectSpStr(# (K,V,f),(K,V,f),(K,V,f),(K,V,f) #)
a is Coset of f
b is right_complementable Element of the carrier of V
b + f is Element of bool the carrier of V
{ (b + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
s0 is Coset of f
x2 is right_complementable Element of the carrier of V
x2 + f is Element of bool the carrier of V
{ (x2 + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
s2 is Coset of f
c is right_complementable Element of the carrier of V
c + f is Element of bool the carrier of V
{ (c + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
(K,V,f) . (v,a) is set
x2 + c is right_complementable Element of the carrier of V
the addF of V . (x2,c) is right_complementable Element of the carrier of V
(x2 + c) + f is Element of bool the carrier of V
{ ((x2 + c) + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
(K,V,f) . (A,v) is set
b + x2 is right_complementable Element of the carrier of V
the addF of V . (b,x2) is right_complementable Element of the carrier of V
(b + x2) + f is Element of bool the carrier of V
{ ((b + x2) + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
(b + x2) + c is right_complementable Element of the carrier of V
the addF of V . ((b + x2),c) is right_complementable Element of the carrier of V
((b + x2) + c) + f is Element of bool the carrier of V
{ (((b + x2) + c) + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
b + (x2 + c) is right_complementable Element of the carrier of V
the addF of V . (b,(x2 + c)) is right_complementable Element of the carrier of V
(b + (x2 + c)) + f is Element of bool the carrier of V
{ ((b + (x2 + c)) + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
A is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of A is non empty set
[: the carrier of A, the carrier of A:] is V1() non empty set
the addF of A is V1() V4([: the carrier of A, the carrier of A:]) V5( the carrier of A) Function-like non empty V14([: the carrier of A, the carrier of A:]) quasi_total Element of bool [:[: the carrier of A, the carrier of A:], the carrier of A:]
[:[: the carrier of A, the carrier of A:], the carrier of A:] is V1() non empty set
bool [:[: the carrier of A, the carrier of A:], the carrier of A:] is non empty set
0. A is V48(A) right_complementable Element of the carrier of A
the ZeroF of A is right_complementable Element of the carrier of A
[: the carrier of K, the carrier of A:] is V1() non empty set
the lmult of A is V1() V4([: the carrier of K, the carrier of A:]) V5( the carrier of A) Function-like non empty V14([: the carrier of K, the carrier of A:]) quasi_total Element of bool [:[: the carrier of K, the carrier of A:], the carrier of A:]
[:[: the carrier of K, the carrier of A:], the carrier of A:] is V1() non empty set
bool [:[: the carrier of K, the carrier of A:], the carrier of A:] is non empty set
qf is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of qf is non empty set
[: the carrier of qf, the carrier of qf:] is V1() 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:], 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
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
[: the carrier of K, the carrier of qf:] is V1() non empty set
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:], 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
W is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of W is non empty set
[: the carrier of W, the carrier of W:] is V1() non empty set
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:], 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
0. W is V48(W) right_complementable Element of the carrier of W
the ZeroF of W is right_complementable Element of the carrier of W
[: the carrier of K, the carrier of W:] is V1() non empty set
the lmult of W is V1() V4([: the carrier of K, the carrier of W:]) V5( the carrier of W) Function-like non empty V14([: the carrier of K, the carrier of W:]) quasi_total Element of bool [:[: the carrier of K, the carrier of W:], the carrier of W:]
[:[: the carrier of K, the carrier of W:], the carrier of W:] is V1() non empty set
bool [:[: the carrier of K, the carrier of W:], the carrier of W:] is non empty set
K is non empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
0. V is V48(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
f is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
(K,V,f) is Element of (K,V,f)
bool the carrier of V is non empty set
(K,V,f) is non empty Element of bool (bool the carrier of V)
bool (bool the carrier of V) is non empty set
{ b1 where b1 is Coset of f : verum } is set
the carrier of f is non empty set
(0. V) + f is Element of bool the carrier of V
{ ((0. V) + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
(K,V,f) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
0. (K,V,f) is V48((K,V,f)) right_complementable Element of the carrier of (K,V,f)
the carrier of (K,V,f) is non empty set
the ZeroF of (K,V,f) is right_complementable Element of the carrier of (K,V,f)
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
K is non empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of V is non empty set
f is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
(K,V,f) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of (K,V,f) is non empty set
qf is right_complementable Element of the carrier of (K,V,f)
(K,V,f) is non empty Element of bool (bool the carrier of V)
bool the carrier of V is non empty set
bool (bool the carrier of V) is non empty set
{ b1 where b1 is Coset of f : verum } is set
x is Coset of f
K is non empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of V is non empty set
f is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
(K,V,f) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of (K,V,f) is non empty set
qf is right_complementable Element of the carrier of V
qf + f is Element of bool the carrier of V
bool the carrier of V is non empty set
{ (qf + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
(K,V,f) is non empty Element of bool (bool the carrier of V)
bool (bool the carrier of V) is non empty set
{ b1 where b1 is Coset of f : verum } is set
K is non empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
f is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
(K,V,f) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of (K,V,f) is non empty set
qf is Coset of f
(K,V,f) is non empty Element of bool (bool the carrier of V)
the carrier of V is non empty set
bool the carrier of V is non empty set
bool (bool the carrier of V) is non empty set
{ b1 where b1 is Coset of f : verum } is set
K is non empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
the carrier of K is non empty set
V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of V is non empty set
f is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
(K,V,f) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of (K,V,f) is non empty set
the lmult of (K,V,f) is V1() V4([: the carrier of K, the carrier of (K,V,f):]) V5( the carrier of (K,V,f)) Function-like non empty V14([: the carrier of K, the carrier of (K,V,f):]) quasi_total Element of bool [:[: the carrier of K, the carrier of (K,V,f):], the carrier of (K,V,f):]
[: the carrier of K, the carrier of (K,V,f):] is V1() non empty set
[:[: the carrier of K, the carrier of (K,V,f):], the carrier of (K,V,f):] is V1() non empty set
bool [:[: the carrier of K, the carrier of (K,V,f):], the carrier of (K,V,f):] is non empty set
qV is right_complementable Element of the carrier of (K,V,f)
x is right_complementable Element of the carrier of V
x + f is Element of bool the carrier of V
bool the carrier of V is non empty set
{ (x + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
w is right_complementable Element of the carrier of K
w * qV is right_complementable Element of the carrier of (K,V,f)
the lmult of (K,V,f) . (w,qV) is right_complementable Element of the carrier of (K,V,f)
w * x 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,x) is right_complementable Element of the carrier of V
(w * x) + f is Element of bool the carrier of V
{ ((w * x) + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
{ b1 where b1 is Coset of f : verum } is set
(K,V,f) is non empty Element of bool (bool the carrier of V)
bool (bool the carrier of V) is non empty set
(K,V,f) is V1() V4([: the carrier of K,(K,V,f):]) V5((K,V,f)) Function-like non empty V14([: the carrier of K,(K,V,f):]) quasi_total Element of bool [:[: the carrier of K,(K,V,f):],(K,V,f):]
[: the carrier of K,(K,V,f):] is V1() non empty set
[:[: the carrier of K,(K,V,f):],(K,V,f):] is V1() non empty set
bool [:[: the carrier of K,(K,V,f):],(K,V,f):] is non empty set
A is Element of (K,V,f)
(K,V,f) . (w,A) is Element of (K,V,f)
K is non empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of V is non empty set
f is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
(K,V,f) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of (K,V,f) is non empty set
W is right_complementable Element of the carrier of (K,V,f)
qV is right_complementable Element of the carrier of (K,V,f)
W + qV is right_complementable Element of the carrier of (K,V,f)
the addF of (K,V,f) is V1() V4([: the carrier of (K,V,f), the carrier of (K,V,f):]) V5( the carrier of (K,V,f)) Function-like non empty V14([: the carrier of (K,V,f), the carrier of (K,V,f):]) quasi_total Element of bool [:[: the carrier of (K,V,f), the carrier of (K,V,f):], the carrier of (K,V,f):]
[: the carrier of (K,V,f), the carrier of (K,V,f):] is V1() non empty set
[:[: the carrier of (K,V,f), the carrier of (K,V,f):], the carrier of (K,V,f):] is V1() non empty set
bool [:[: the carrier of (K,V,f), the carrier of (K,V,f):], the carrier of (K,V,f):] is non empty set
the addF of (K,V,f) . (W,qV) is right_complementable Element of the carrier of (K,V,f)
x is right_complementable Element of the carrier of V
x + f is Element of bool the carrier of V
bool the carrier of V is non empty set
{ (x + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
w is right_complementable Element of the carrier of V
w + f is Element of bool the carrier of V
{ (w + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
x + w 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 . (x,w) is right_complementable Element of the carrier of V
(x + w) + f is Element of bool the carrier of V
{ ((x + w) + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
{ b1 where b1 is Coset of f : verum } is set
(K,V,f) is non empty Element of bool (bool the carrier of V)
bool (bool the carrier of V) is non empty set
(K,V,f) is V1() V4([:(K,V,f),(K,V,f):]) V5((K,V,f)) Function-like non empty V14([:(K,V,f),(K,V,f):]) quasi_total Element of bool [:[:(K,V,f),(K,V,f):],(K,V,f):]
[:(K,V,f),(K,V,f):] is V1() non empty set
[:[:(K,V,f),(K,V,f):],(K,V,f):] is V1() non empty set
bool [:[:(K,V,f),(K,V,f):],(K,V,f):] is non empty set
A is Element of (K,V,f)
v is Element of (K,V,f)
(K,V,f) . (A,v) is Element of (K,V,f)
K is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
the carrier of K is non empty non trivial set
V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of V is non empty set
f is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
the carrier of f is non empty set
[: the carrier of f, the carrier of K:] is V1() non empty set
bool [: the carrier of f, the carrier of K:] is non empty set
qf is V1() V4( the carrier of f) V5( the carrier of K) Function-like non empty V14( the carrier of f) quasi_total additive homogeneous 0-preserving Element of bool [: the carrier of f, the carrier of K:]
W is right_complementable Element of the carrier of V
{W} is trivial V29() Element of bool the carrier of V
bool the carrier of V is non empty set
Lin {W} is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
f + (Lin {W}) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
the carrier of (f + (Lin {W})) is non empty set
[: the carrier of (f + (Lin {W})), the carrier of K:] is V1() non empty set
bool [: the carrier of (f + (Lin {W})), the carrier of K:] is non empty set
qV is right_complementable Element of the carrier of (f + (Lin {W}))
w is right_complementable Element of the carrier of K
x is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of f + (Lin {W})
{qV} is trivial V29() Element of bool the carrier of (f + (Lin {W}))
bool the carrier of (f + (Lin {W})) is non empty set
Lin {qV} is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of f + (Lin {W})
A is right_complementable Element of the carrier of (f + (Lin {W}))
A |-- (x,(Lin {qV})) is Element of [: the carrier of (f + (Lin {W})), the carrier of (f + (Lin {W})):]
[: the carrier of (f + (Lin {W})), the carrier of (f + (Lin {W})):] is V1() non empty set
(A |-- (x,(Lin {qV}))) `1 is right_complementable Element of the carrier of (f + (Lin {W}))
(A |-- (x,(Lin {qV}))) `2 is right_complementable Element of the carrier of (f + (Lin {W}))
v is right_complementable Element of the carrier of f
a is right_complementable Element of the carrier of K
a * W 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,W) is right_complementable Element of the carrier of V
[v,(a * W)] is non empty Element of [: the carrier of f, the carrier of V:]
[: the carrier of f, the carrier of V:] is V1() non empty set
{v,(a * W)} is V29() set
{v} is trivial V29() set
{{v,(a * W)},{v}} is V29() V33() set
qf . v is right_complementable Element of the carrier of K
a * 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 . (a,w) is right_complementable Element of the carrier of K
(qf . v) + (a * 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 addF of K . ((qf . v),(a * w)) is right_complementable Element of the carrier of K
a is right_complementable Element of the carrier of f
qf . a is right_complementable Element of the carrier of K
b is right_complementable Element of the carrier of K
b * W is right_complementable Element of the carrier of V
the lmult of V . (b,W) is right_complementable Element of the carrier of V
b * w is right_complementable Element of the carrier of K
the multF of K . (b,w) is right_complementable Element of the carrier of K
(qf . a) + (b * w) is right_complementable Element of the carrier of K
the addF of K . ((qf . a),(b * w)) is right_complementable Element of the carrier of K
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
A is V1() V4( the carrier of (f + (Lin {W}))) V5( the carrier of K) Function-like non empty V14( the carrier of (f + (Lin {W}))) quasi_total Element of bool [: the carrier of (f + (Lin {W})), the carrier of K:]
v is set
dom qf is non empty Element of bool the carrier of f
bool the carrier of f is non empty set
a is right_complementable Element of the carrier of f
a is right_complementable Element of the carrier of (f + (Lin {W}))
a |-- (x,(Lin {qV})) is Element of [: the carrier of (f + (Lin {W})), the carrier of (f + (Lin {W})):]
[: the carrier of (f + (Lin {W})), the carrier of (f + (Lin {W})):] is V1() 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
[a,(0. V)] is non empty Element of [: the carrier of (f + (Lin {W})), the carrier of V:]
[: the carrier of (f + (Lin {W})), the carrier of V:] is V1() non empty set
{a,(0. V)} is V29() set
{a} is trivial V29() set
{{a,(0. V)},{a}} is V29() V33() 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
(0. K) * W 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 . ((0. K),W) is right_complementable Element of the carrier of V
[a,((0. K) * W)] is non empty Element of [: the carrier of (f + (Lin {W})), the carrier of V:]
{a,((0. K) * W)} is V29() set
{{a,((0. K) * W)},{a}} is V29() V33() set
(a |-- (x,(Lin {qV}))) `1 is right_complementable Element of the carrier of (f + (Lin {W}))
(a |-- (x,(Lin {qV}))) `2 is right_complementable Element of the carrier of (f + (Lin {W}))
qf . v is set
qf . a is right_complementable Element of the carrier of K
(qf . a) + (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 . ((qf . a),(0. K)) is right_complementable Element of the carrier of K
(0. K) * 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 multF of K . ((0. K),w) is right_complementable Element of the carrier of K
(qf . a) + ((0. K) * w) is right_complementable Element of the carrier of K
the addF of K . ((qf . a),((0. K) * w)) is right_complementable Element of the carrier of K
A . v is set
qV |-- (x,(Lin {qV})) is Element of [: the carrier of (f + (Lin {W})), the carrier of (f + (Lin {W})):]
the carrier of x is non empty set
0. x is V48(x) right_complementable Element of the carrier of x
the ZeroF of x is right_complementable Element of the carrier of x
[(0. x),qV] is non empty Element of [: the carrier of x, the carrier of (f + (Lin {W})):]
[: the carrier of x, the carrier of (f + (Lin {W})):] is V1() non empty set
{(0. x),qV} is V29() set
{(0. x)} is trivial V29() set
{{(0. x),qV},{(0. x)}} is V29() V33() set
(qV |-- (x,(Lin {qV}))) `1 is right_complementable Element of the carrier of (f + (Lin {W}))
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 is V1() V4( the carrier of (f + (Lin {W}))) V5( the carrier of K) Function-like non empty V14( the carrier of (f + (Lin {W}))) quasi_total Element of bool [: the carrier of (f + (Lin {W})), the carrier of K:]
a is right_complementable Element of the carrier of (f + (Lin {W}))
a is right_complementable Element of the carrier of (f + (Lin {W}))
a + a is right_complementable Element of the carrier of (f + (Lin {W}))
the addF of (f + (Lin {W})) is V1() V4([: the carrier of (f + (Lin {W})), the carrier of (f + (Lin {W})):]) V5( the carrier of (f + (Lin {W}))) Function-like non empty V14([: the carrier of (f + (Lin {W})), the carrier of (f + (Lin {W})):]) quasi_total Element of bool [:[: the carrier of (f + (Lin {W})), the carrier of (f + (Lin {W})):], the carrier of (f + (Lin {W})):]
[:[: the carrier of (f + (Lin {W})), the carrier of (f + (Lin {W})):], the carrier of (f + (Lin {W})):] is V1() non empty set
bool [:[: the carrier of (f + (Lin {W})), the carrier of (f + (Lin {W})):], the carrier of (f + (Lin {W})):] is non empty set
the addF of (f + (Lin {W})) . (a,a) is right_complementable Element of the carrier of (f + (Lin {W}))
v . (a + a) is right_complementable Element of the carrier of K
v . a is right_complementable Element of the carrier of K
v . a is right_complementable Element of the carrier of K
(v . a) + (v . a) is right_complementable Element of the carrier of K
the addF of K . ((v . a),(v . a)) is right_complementable Element of the carrier of K
a |-- (x,(Lin {qV})) is Element of [: the carrier of (f + (Lin {W})), the carrier of (f + (Lin {W})):]
b is right_complementable Element of the carrier of f
s0 is right_complementable Element of the carrier of K
s0 * W is right_complementable Element of the carrier of V
the lmult of V . (s0,W) is right_complementable Element of the carrier of V
[b,(s0 * W)] is non empty Element of [: the carrier of f, the carrier of V:]
[: the carrier of f, the carrier of V:] is V1() non empty set
{b,(s0 * W)} is V29() set
{b} is trivial V29() set
{{b,(s0 * W)},{b}} is V29() V33() set
(a |-- (x,(Lin {qV}))) `1 is right_complementable Element of the carrier of (f + (Lin {W}))
(a |-- (x,(Lin {qV}))) `2 is right_complementable Element of the carrier of (f + (Lin {W}))
a |-- (x,(Lin {qV})) is Element of [: the carrier of (f + (Lin {W})), the carrier of (f + (Lin {W})):]
x2 is right_complementable Element of the carrier of f
s2 is right_complementable Element of the carrier of K
s2 * W is right_complementable Element of the carrier of V
the lmult of V . (s2,W) is right_complementable Element of the carrier of V
[x2,(s2 * W)] is non empty Element of [: the carrier of f, the carrier of V:]
{x2,(s2 * W)} is V29() set
{x2} is trivial V29() set
{{x2,(s2 * W)},{x2}} is V29() V33() set
(a |-- (x,(Lin {qV}))) `1 is right_complementable Element of the carrier of (f + (Lin {W}))
(a |-- (x,(Lin {qV}))) `2 is right_complementable Element of the carrier of (f + (Lin {W}))
a + a is right_complementable Element of the carrier of (f + (Lin {W}))
(a + a) |-- (x,(Lin {qV})) is Element of [: the carrier of (f + (Lin {W})), the carrier of (f + (Lin {W})):]
b + x2 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 . (b,x2) is right_complementable Element of the carrier of f
s0 + s2 is right_complementable Element of the carrier of K
the addF of K . (s0,s2) is right_complementable Element of the carrier of K
(s0 + s2) * W is right_complementable Element of the carrier of V
the lmult of V . ((s0 + s2),W) is right_complementable Element of the carrier of V
[(b + x2),((s0 + s2) * W)] is non empty Element of [: the carrier of f, the carrier of V:]
{(b + x2),((s0 + s2) * W)} is V29() set
{(b + x2)} is trivial V29() set
{{(b + x2),((s0 + s2) * W)},{(b + x2)}} is V29() V33() set
((a + a) |-- (x,(Lin {qV}))) `1 is right_complementable Element of the carrier of (f + (Lin {W}))
((a + a) |-- (x,(Lin {qV}))) `2 is right_complementable Element of the carrier of (f + (Lin {W}))
v . (a + a) is right_complementable Element of the carrier of K
qf . (b + x2) is right_complementable Element of the carrier of K
(s0 + s2) * w is right_complementable Element of the carrier of K
the multF of K . ((s0 + s2),w) is right_complementable Element of the carrier of K
(qf . (b + x2)) + ((s0 + s2) * w) is right_complementable Element of the carrier of K
the addF of K . ((qf . (b + x2)),((s0 + s2) * w)) is right_complementable Element of the carrier of K
s0 * w is right_complementable Element of the carrier of K
the multF of K . (s0,w) is right_complementable Element of the carrier of K
s2 * w is right_complementable Element of the carrier of K
the multF of K . (s2,w) is right_complementable Element of the carrier of K
(s0 * w) + (s2 * w) is right_complementable Element of the carrier of K
the addF of K . ((s0 * w),(s2 * w)) is right_complementable Element of the carrier of K
(qf . (b + x2)) + ((s0 * w) + (s2 * w)) is right_complementable Element of the carrier of K
the addF of K . ((qf . (b + x2)),((s0 * w) + (s2 * w))) is right_complementable Element of the carrier of K
qf . b is right_complementable Element of the carrier of K
qf . x2 is right_complementable Element of the carrier of K
(qf . b) + (qf . x2) is right_complementable Element of the carrier of K
the addF of K . ((qf . b),(qf . x2)) is right_complementable Element of the carrier of K
((qf . b) + (qf . x2)) + ((s0 * w) + (s2 * w)) is right_complementable Element of the carrier of K
the addF of K . (((qf . b) + (qf . x2)),((s0 * w) + (s2 * w))) is right_complementable Element of the carrier of K
((qf . b) + (qf . x2)) + (s0 * w) is right_complementable Element of the carrier of K
the addF of K . (((qf . b) + (qf . x2)),(s0 * w)) is right_complementable Element of the carrier of K
(((qf . b) + (qf . x2)) + (s0 * w)) + (s2 * w) is right_complementable Element of the carrier of K
the addF of K . ((((qf . b) + (qf . x2)) + (s0 * w)),(s2 * w)) is right_complementable Element of the carrier of K
(qf . b) + (s0 * w) is right_complementable Element of the carrier of K
the addF of K . ((qf . b),(s0 * w)) is right_complementable Element of the carrier of K
((qf . b) + (s0 * w)) + (qf . x2) is right_complementable Element of the carrier of K
the addF of K . (((qf . b) + (s0 * w)),(qf . x2)) is right_complementable Element of the carrier of K
(((qf . b) + (s0 * w)) + (qf . x2)) + (s2 * w) is right_complementable Element of the carrier of K
the addF of K . ((((qf . b) + (s0 * w)) + (qf . x2)),(s2 * w)) is right_complementable Element of the carrier of K
(qf . x2) + (s2 * w) is right_complementable Element of the carrier of K
the addF of K . ((qf . x2),(s2 * w)) is right_complementable Element of the carrier of K
((qf . b) + (s0 * w)) + ((qf . x2) + (s2 * w)) is right_complementable Element of the carrier of K
the addF of K . (((qf . b) + (s0 * w)),((qf . x2) + (s2 * w))) is right_complementable Element of the carrier of K
(v . a) + ((qf . x2) + (s2 * w)) is right_complementable Element of the carrier of K
the addF of K . ((v . a),((qf . x2) + (s2 * w))) is right_complementable Element of the carrier of K
(v . a) + (v . a) is right_complementable Element of the carrier of K
a is right_complementable Element of the carrier of (f + (Lin {W}))
v . a is right_complementable Element of the carrier of K
a is right_complementable Element of the carrier of K
a * a is right_complementable Element of the carrier of (f + (Lin {W}))
the lmult of (f + (Lin {W})) is V1() V4([: the carrier of K, the carrier of (f + (Lin {W})):]) V5( the carrier of (f + (Lin {W}))) Function-like non empty V14([: the carrier of K, the carrier of (f + (Lin {W})):]) quasi_total Element of bool [:[: the carrier of K, the carrier of (f + (Lin {W})):], the carrier of (f + (Lin {W})):]
[: the carrier of K, the carrier of (f + (Lin {W})):] is V1() non empty set
[:[: the carrier of K, the carrier of (f + (Lin {W})):], the carrier of (f + (Lin {W})):] is V1() non empty set
bool [:[: the carrier of K, the carrier of (f + (Lin {W})):], the carrier of (f + (Lin {W})):] is non empty set
the lmult of (f + (Lin {W})) . (a,a) is right_complementable Element of the carrier of (f + (Lin {W}))
v . (a * a) is right_complementable Element of the carrier of K
a * (v . a) is right_complementable Element of the carrier of K
the multF of K . (a,(v . a)) is right_complementable Element of the carrier of K
a |-- (x,(Lin {qV})) is Element of [: the carrier of (f + (Lin {W})), the carrier of (f + (Lin {W})):]
b is right_complementable Element of the carrier of f
s0 is right_complementable Element of the carrier of K
s0 * W is right_complementable Element of the carrier of V
the lmult of V . (s0,W) is right_complementable Element of the carrier of V
[b,(s0 * W)] is non empty Element of [: the carrier of f, the carrier of V:]
[: the carrier of f, the carrier of V:] is V1() non empty set
{b,(s0 * W)} is V29() set
{b} is trivial V29() set
{{b,(s0 * W)},{b}} is V29() V33() set
(a |-- (x,(Lin {qV}))) `1 is right_complementable Element of the carrier of (f + (Lin {W}))
(a |-- (x,(Lin {qV}))) `2 is right_complementable Element of the carrier of (f + (Lin {W}))
(a * a) |-- (x,(Lin {qV})) is Element of [: the carrier of (f + (Lin {W})), the carrier of (f + (Lin {W})):]
a * b 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 . (a,b) is right_complementable Element of the carrier of f
a * s0 is right_complementable Element of the carrier of K
the multF of K . (a,s0) is right_complementable Element of the carrier of K
(a * s0) * W is right_complementable Element of the carrier of V
the lmult of V . ((a * s0),W) is right_complementable Element of the carrier of V
[(a * b),((a * s0) * W)] is non empty Element of [: the carrier of f, the carrier of V:]
{(a * b),((a * s0) * W)} is V29() set
{(a * b)} is trivial V29() set
{{(a * b),((a * s0) * W)},{(a * b)}} is V29() V33() set
((a * a) |-- (x,(Lin {qV}))) `1 is right_complementable Element of the carrier of (f + (Lin {W}))
((a * a) |-- (x,(Lin {qV}))) `2 is right_complementable Element of the carrier of (f + (Lin {W}))
qf . (a * b) is right_complementable Element of the carrier of K
(a * s0) * w is right_complementable Element of the carrier of K
the multF of K . ((a * s0),w) is right_complementable Element of the carrier of K
(qf . (a * b)) + ((a * s0) * w) is right_complementable Element of the carrier of K
the addF of K . ((qf . (a * b)),((a * s0) * w)) is right_complementable Element of the carrier of K
qf . b is right_complementable Element of the carrier of K
a * (qf . b) is right_complementable Element of the carrier of K
the multF of K . (a,(qf . b)) is right_complementable Element of the carrier of K
(a * (qf . b)) + ((a * s0) * w) is right_complementable Element of the carrier of K
the addF of K . ((a * (qf . b)),((a * s0) * w)) is right_complementable Element of the carrier of K
s0 * w is right_complementable Element of the carrier of K
the multF of K . (s0,w) is right_complementable Element of the carrier of K
a * (s0 * w) is right_complementable Element of the carrier of K
the multF of K . (a,(s0 * w)) is right_complementable Element of the carrier of K
(a * (qf . b)) + (a * (s0 * w)) is right_complementable Element of the carrier of K
the addF of K . ((a * (qf . b)),(a * (s0 * w))) is right_complementable Element of the carrier of K
(qf . b) + (s0 * w) is right_complementable Element of the carrier of K
the addF of K . ((qf . b),(s0 * w)) is right_complementable Element of the carrier of K
a * ((qf . b) + (s0 * w)) is right_complementable Element of the carrier of K
the multF of K . (a,((qf . b) + (s0 * w))) is right_complementable Element of the carrier of K
a * (v . a) is right_complementable Element of the carrier of K
a is V1() V4( the carrier of (f + (Lin {W}))) V5( the carrier of K) Function-like non empty V14( the carrier of (f + (Lin {W}))) quasi_total additive homogeneous 0-preserving Element of bool [: the carrier of (f + (Lin {W})), the carrier of K:]
a | the carrier of f is V1() V4( the carrier of f) V4( the carrier of (f + (Lin {W}))) V5( the carrier of K) Function-like Element of bool [: the carrier of (f + (Lin {W})), the carrier of K:]
a . qV is right_complementable Element of the carrier of K
dom a is non empty Element of bool the carrier of (f + (Lin {W}))
(dom a) /\ the carrier of f is Element of bool the carrier of (f + (Lin {W}))
(qV |-- (x,(Lin {qV}))) `2 is right_complementable Element of the carrier of (f + (Lin {W}))
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 V
the lmult of V . ((1_ K),W) is right_complementable Element of the carrier of V
qf . (0. f) is right_complementable Element of the carrier of K
(1_ K) * w is right_complementable Element of the carrier of K
the multF of K . ((1_ K),w) is right_complementable Element of the carrier of K
(qf . (0. f)) + ((1_ K) * w) is right_complementable Element of the carrier of K
the addF of K . ((qf . (0. f)),((1_ K) * w)) is right_complementable Element of the carrier of K
(0. K) + ((1_ K) * w) is right_complementable Element of the carrier of K
the addF of K . ((0. K),((1_ K) * w)) is right_complementable Element of the carrier of K
(0. K) + w is right_complementable Element of the carrier of K
the addF of K . ((0. K),w) is right_complementable Element of the carrier of K
K is non empty right_zeroed addLoopStr
V is non empty VectSpStr over K
the carrier of V is non empty set
the carrier of K is non empty set
[: 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
0Functional V is V1() V4( the carrier of V) V5( the carrier of K) Function-like non empty V14( the carrier of V) quasi_total additive 0-preserving Element of bool [: the carrier of V, the carrier of K:]
K is non empty right_complementable add-associative right_zeroed doubleLoopStr
V is non empty right_zeroed VectSpStr over K
the carrier of V is non empty set
the carrier of K is non empty set
[: 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
f 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:]
0. V is V48(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
f . (0. V) is right_complementable Element of the carrier of K
(0. V) + (0. V) is 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 . ((0. V),(0. V)) is Element of the carrier of V
f . ((0. V) + (0. V)) is right_complementable Element of the carrier of K
(f . (0. V)) + (f . (0. V)) 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 . ((f . (0. V)),(f . (0. V))) is right_complementable Element of the carrier of K
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
K is non empty right_complementable add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
V is non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of V is non empty set
the carrier of K is non empty set
[: 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
f 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:]
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 . (0. V) is right_complementable Element of the carrier of K
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. K) * (0. V) 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 . ((0. K),(0. V)) is right_complementable Element of the carrier of V
f . ((0. K) * (0. V)) is right_complementable Element of the carrier of K
(0. K) * (f . (0. V)) 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 . ((0. K),(f . (0. V))) is right_complementable Element of the carrier of K
K is non empty ZeroStr
V is non empty VectSpStr over K
0Functional V is V1() V4( the carrier of V) V5( the carrier of K) Function-like non empty V14( the carrier of V) quasi_total 0-preserving Element of bool [: the carrier of V, the carrier of K:]
the carrier of V is non empty set
the carrier of K is non empty set
[: 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
f is set
K48((0Functional V)) is non empty set
qf is set
(0Functional V) . f is set
(0Functional V) . qf is set
dom (0Functional V) is non empty Element of bool the carrier of V
bool the carrier of V is non empty set
qV is Element of the carrier of V
(0Functional V) . 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
x is Element of the carrier of V
(0Functional V) . x is Element of the carrier of K
K is non empty ZeroStr
V is non empty VectSpStr over K
the carrier of V is non empty set
the carrier of K is non empty set
[: 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
0Functional V is V1() V4( the carrier of V) V5( the carrier of K) Function-like constant non empty V14( the carrier of V) quasi_total 0-preserving Element of bool [: the carrier of V, the carrier of K:]
K is non empty right_complementable add-associative right_zeroed doubleLoopStr
V is non empty right_zeroed VectSpStr over K
the carrier of V is non empty set
the carrier of K is non empty set
[: 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
f is V1() V4( the carrier of V) V5( the carrier of K) Function-like non empty V14( the carrier of V) quasi_total 0-preserving Element of bool [: the carrier of V, the carrier of K:]
0Functional V is V1() V4( the carrier of V) V5( the carrier of K) Function-like constant non empty V14( the carrier of V) quasi_total additive 0-preserving Element of bool [: the carrier of V, the carrier of K:]
0. V is V48(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
f . (0. V) is right_complementable Element of the carrier of K
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
dom f is non empty Element of bool the carrier of V
bool the carrier of V is non empty set
qf is Element of the carrier of V
f . qf is right_complementable Element of the carrier of K
(0Functional V) . qf is right_complementable Element of the carrier of K
qf is set
W is set
f . qf is set
qV is Element of the carrier of V
(0Functional V) . qV is right_complementable Element of the carrier of K
x is Element of the carrier of V
(0Functional V) . x is right_complementable Element of the carrier of K
f . W is set
K is non empty right_complementable add-associative right_zeroed doubleLoopStr
V is non empty right_zeroed VectSpStr over K
the carrier of V is non empty set
the carrier of K is non empty set
[: 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
0Functional V is V1() V4( the carrier of V) V5( the carrier of K) Function-like constant non empty V14( the carrier of V) quasi_total additive 0-preserving Element of bool [: the carrier of V, the carrier of K:]
K is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
V is non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of V is non empty non trivial set
the carrier of K is non empty non trivial set
[: 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
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
Lin {f} is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f}
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 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
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 non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f}) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f})) is non empty set
the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} /\ (Lin {f}) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
(0). V is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
the carrier of (Lin {f}) is non empty set
the carrier of the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} is non empty set
the carrier of the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} /\ the carrier of (Lin {f}) is set
the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} /\ (Lin {f})) is non empty set
{(0. V)} is trivial V29() Element of bool the carrier of V
[: the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f})), the carrier of K:] is V1() non empty set
bool [: the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f})), the carrier of K:] is non empty set
0Functional the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} is V1() V4( the carrier of the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f}) V5( the carrier of K) Function-like constant non empty V14( the carrier of the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f}) quasi_total additive homogeneous 0-preserving Element of bool [: the carrier of the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f}, the carrier of K:]
[: the carrier of the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f}, the carrier of K:] is V1() non empty set
bool [: the carrier of the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f}, the carrier of K:] is non empty set
W is right_complementable Element of the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f}))
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
qV is V1() V4( the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f}))) V5( the carrier of K) Function-like non empty V14( the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f}))) quasi_total additive homogeneous 0-preserving Element of bool [: the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f})), the carrier of K:]
qV | the carrier of the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} is V1() V4( the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f}))) V4( the carrier of the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f}) V4( the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f}))) V5( the carrier of K) Function-like Element of bool [: the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f})), the carrier of K:]
qV . W is right_complementable Element of the carrier of K
x 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:]
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 . (w,A) is right_complementable Element of the carrier of V
x . (w + A) is right_complementable Element of the carrier of K
x . w is right_complementable Element of the carrier of K
x . A is right_complementable Element of the carrier of K
(x . w) + (x . A) 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 . ((x . w),(x . A)) is right_complementable Element of the carrier of K
w + A is right_complementable Element of the carrier of V
v is right_complementable Element of the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f}))
a is right_complementable Element of the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f}))
v + a is right_complementable Element of the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f}))
the addF of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f})) is V1() V4([: the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f})), the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f})):]) V5( the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f}))) Function-like non empty V14([: the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f})), the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f})):]) quasi_total Element of bool [:[: the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f})), the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f})):], the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f})):]
[: the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f})), the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f})):] is V1() non empty set
[:[: the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f})), the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f})):], the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f})):] is V1() non empty set
bool [:[: the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f})), the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f})):], the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f})):] is non empty set
the addF of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f})) . (v,a) is right_complementable Element of the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f}))
w is right_complementable Element of the carrier of V
x . w is right_complementable Element of the carrier of K
A is right_complementable Element of the carrier of K
A * w is right_complementable Element of the carrier of V
the lmult of V . (A,w) is right_complementable Element of the carrier of V
x . (A * w) is right_complementable Element of the carrier of K
A * (x . 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 . (A,(x . w)) is right_complementable Element of the carrier of K
the lmult of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f})) is V1() V4([: the carrier of K, the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f})):]) V5( the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f}))) Function-like non empty V14([: the carrier of K, the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f})):]) quasi_total Element of bool [:[: the carrier of K, the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f})):], the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f})):]
[: the carrier of K, the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f})):] is V1() non empty set
[:[: the carrier of K, the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f})):], the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f})):] is V1() non empty set
bool [:[: the carrier of K, the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f})):], the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f})):] is non empty set
v is right_complementable Element of the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f}))
the lmult of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f})) . (A,v) is right_complementable Element of the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f}))
A * v is right_complementable Element of the carrier of ( the non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f} + (Lin {f}))
dom x is non empty Element of bool the carrier of V
w is V1() V4( the carrier of V) V5( the carrier of K) Function-like non empty V14( the carrier of V) quasi_total homogeneous 0-preserving Element of bool [: the carrier of V, the carrier of K:]
w . (0. V) is right_complementable Element of the carrier of K
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
[f,(1_ K)] is non empty Element of [: the carrier of V, the carrier of K:]
{f,(1_ K)} is V29() set
{f} is trivial V29() set
{{f,(1_ K)},{f}} is V29() V33() 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
[(0. V),(0. K)] is non empty Element of [: the carrier of V, the carrier of K:]
{(0. V),(0. K)} is V29() set
{(0. V)} is trivial V29() set
{{(0. V),(0. K)},{(0. V)}} is V29() V33() set
dom x is non empty Element of bool the carrier of V
w is V1() V4( the carrier of V) V5( the carrier of K) Function-like non empty V14( the carrier of V) quasi_total homogeneous 0-preserving Element of bool [: the carrier of V, the carrier of K:]
w . (0. V) is right_complementable Element of the carrier of K
a is set
{a} is trivial V29() set
a is set
{a} is trivial V29() set
K is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
V is non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of V is non empty non trivial set
the carrier of K is non empty non trivial set
[: 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
f 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:]
K is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
V is non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of V is non empty non trivial 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
Lin {f} is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
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
the carrier of K is non empty non trivial set
[: 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
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
qf is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f}
the carrier of qf is non empty set
0Functional qf is V1() V4( the carrier of qf) V5( the carrier of K) Function-like constant non empty V14( the carrier of qf) quasi_total additive homogeneous 0-preserving Element of bool [: the carrier of qf, the carrier of K:]
[: the carrier of qf, the carrier of K:] is V1() non empty set
bool [: the carrier of qf, the carrier of K:] is non empty set
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 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
VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is non empty strict VectSpStr over K
qf + (Lin {f}) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
the carrier of (qf + (Lin {f})) is non empty set
qf /\ (Lin {f}) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
(0). V is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
the carrier of (Lin {f}) is non empty set
the carrier of qf /\ the carrier of (Lin {f}) is set
the carrier of (qf /\ (Lin {f})) is non empty set
{(0. V)} is trivial V29() Element of bool the carrier of V
[: the carrier of (qf + (Lin {f})), the carrier of K:] is V1() non empty set
bool [: the carrier of (qf + (Lin {f})), the carrier of K:] is non empty set
W is right_complementable Element of the carrier of (qf + (Lin {f}))
qV is V1() V4( the carrier of (qf + (Lin {f}))) V5( the carrier of K) Function-like non empty V14( the carrier of (qf + (Lin {f}))) quasi_total additive homogeneous 0-preserving Element of bool [: the carrier of (qf + (Lin {f})), the carrier of K:]
qV | the carrier of qf is V1() V4( the carrier of qf) V4( the carrier of (qf + (Lin {f}))) V5( the carrier of K) Function-like Element of bool [: the carrier of (qf + (Lin {f})), the carrier of K:]
qV . W is right_complementable Element of the carrier of K
x 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:]
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 . (w,A) is right_complementable Element of the carrier of V
x . (w + A) is right_complementable Element of the carrier of K
x . w is right_complementable Element of the carrier of K
x . A is right_complementable Element of the carrier of K
(x . w) + (x . A) 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 . ((x . w),(x . A)) is right_complementable Element of the carrier of K
w + A is right_complementable Element of the carrier of V
v is right_complementable Element of the carrier of (qf + (Lin {f}))
a is right_complementable Element of the carrier of (qf + (Lin {f}))
v + a is right_complementable Element of the carrier of (qf + (Lin {f}))
the addF of (qf + (Lin {f})) is V1() V4([: the carrier of (qf + (Lin {f})), the carrier of (qf + (Lin {f})):]) V5( the carrier of (qf + (Lin {f}))) Function-like non empty V14([: the carrier of (qf + (Lin {f})), the carrier of (qf + (Lin {f})):]) quasi_total Element of bool [:[: the carrier of (qf + (Lin {f})), the carrier of (qf + (Lin {f})):], the carrier of (qf + (Lin {f})):]
[: the carrier of (qf + (Lin {f})), the carrier of (qf + (Lin {f})):] is V1() non empty set
[:[: the carrier of (qf + (Lin {f})), the carrier of (qf + (Lin {f})):], the carrier of (qf + (Lin {f})):] is V1() non empty set
bool [:[: the carrier of (qf + (Lin {f})), the carrier of (qf + (Lin {f})):], the carrier of (qf + (Lin {f})):] is non empty set
the addF of (qf + (Lin {f})) . (v,a) is right_complementable Element of the carrier of (qf + (Lin {f}))
w is right_complementable Element of the carrier of V
x . w is right_complementable Element of the carrier of K
A is right_complementable Element of the carrier of K
A * w is right_complementable Element of the carrier of V
the lmult of V . (A,w) is right_complementable Element of the carrier of V
x . (A * w) is right_complementable Element of the carrier of K
A * (x . 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 . (A,(x . w)) is right_complementable Element of the carrier of K
the lmult of (qf + (Lin {f})) is V1() V4([: the carrier of K, the carrier of (qf + (Lin {f})):]) V5( the carrier of (qf + (Lin {f}))) Function-like non empty V14([: the carrier of K, the carrier of (qf + (Lin {f})):]) quasi_total Element of bool [:[: the carrier of K, the carrier of (qf + (Lin {f})):], the carrier of (qf + (Lin {f})):]
[: the carrier of K, the carrier of (qf + (Lin {f})):] is V1() non empty set
[:[: the carrier of K, the carrier of (qf + (Lin {f})):], the carrier of (qf + (Lin {f})):] is V1() non empty set
bool [:[: the carrier of K, the carrier of (qf + (Lin {f})):], the carrier of (qf + (Lin {f})):] is non empty set
v is right_complementable Element of the carrier of (qf + (Lin {f}))
the lmult of (qf + (Lin {f})) . (A,v) is right_complementable Element of the carrier of (qf + (Lin {f}))
A * v is right_complementable Element of the carrier of (qf + (Lin {f}))
w is V1() V4( the carrier of V) V5( the carrier of K) Function-like non empty V14( the carrier of V) quasi_total additive homogeneous 0-preserving Element of bool [: the carrier of V, the carrier of K:]
dom w is non empty Element of bool the carrier of V
w . (0. V) is right_complementable Element of the carrier of K
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
A is V1() V4( the carrier of V) V5( the carrier of K) Function-like non constant non empty non trivial V14( the carrier of V) quasi_total additive homogeneous 0-preserving Element of bool [: the carrier of V, the carrier of K:]
A . f is right_complementable Element of the carrier of K
A | the carrier of qf is V1() V4( the carrier of V) V4( the carrier of qf) V4( the carrier of V) V5( the carrier of K) Function-like Element of bool [: the carrier of V, the carrier of K:]
W is V1() V4( the carrier of V) V5( the carrier of K) Function-like non constant non empty non trivial V14( the carrier of V) quasi_total additive homogeneous 0-preserving Element of bool [: the carrier of V, the carrier of K:]
W . f is right_complementable Element of the carrier of K
W | the carrier of qf is V1() V4( the carrier of V) V4( the carrier of qf) V4( the carrier of V) V5( the carrier of K) Function-like Element of bool [: the carrier of V, the carrier of K:]
qV is V1() V4( the carrier of V) V5( the carrier of K) Function-like non constant non empty non trivial V14( the carrier of V) quasi_total additive homogeneous 0-preserving Element of bool [: the carrier of V, the carrier of K:]
qV . f is right_complementable Element of the carrier of K
qV | the carrier of qf is V1() V4( the carrier of V) V4( the carrier of qf) V4( the carrier of V) V5( the carrier of K) Function-like Element of bool [: the carrier of V, the carrier of K:]
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 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
VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is non empty strict VectSpStr over K
qf + (Lin {f}) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
x is right_complementable Element of the carrier of V
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 . (w,A) is right_complementable Element of the carrier of V
v is right_complementable Element of the carrier of K
v * f is right_complementable Element of the carrier of V
the lmult of V . (v,f) is right_complementable Element of the carrier of V
W . w is right_complementable Element of the carrier of K
(qV | the carrier of qf) . w is set
qV . w is right_complementable Element of the carrier of K
W . x is right_complementable Element of the carrier of K
W . (v * f) is right_complementable Element of the carrier of K
(W . w) + (W . (v * f)) 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 . ((W . w),(W . (v * f))) is right_complementable Element of the carrier of K
v * (W . f) 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,(W . f)) is right_complementable Element of the carrier of K
(W . w) + (v * (W . f)) is right_complementable Element of the carrier of K
the addF of K . ((W . w),(v * (W . f))) is right_complementable Element of the carrier of K
qV . (v * f) is right_complementable Element of the carrier of K
(W . w) + (qV . (v * f)) is right_complementable Element of the carrier of K
the addF of K . ((W . w),(qV . (v * f))) is right_complementable Element of the carrier of K
qV . x is right_complementable Element of the carrier of K
K is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
the carrier of K is non empty non trivial 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 non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of V is non empty non trivial set
[: 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
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 V1() V4( the carrier of V) V5( the carrier of K) Function-like non constant non empty non trivial V14( the carrier of V) quasi_total 0-preserving Element of bool [: the carrier of V, the carrier of K:]
f . (0. V) is right_complementable Element of the carrier of K
qf is set
dom f is non empty non trivial Element of bool the carrier of V
bool the carrier of V is non empty set
W is set
f . qf is set
qV is right_complementable Element of the carrier of V
f . qV is right_complementable Element of the carrier of K
x is right_complementable Element of the carrier of V
f . x is right_complementable Element of the carrier of K
f . W is set
K is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
the carrier of K is non empty non trivial set
V is non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of V is non empty non trivial 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
Lin {f} is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace 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 non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f}
(K,V,f,W) is V1() V4( the carrier of V) V5( the carrier of K) Function-like non constant non empty non trivial V14( the carrier of V) quasi_total additive homogeneous 0-preserving Element of bool [: the carrier of V, 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
(K,V,f,W) . (qf * f) is right_complementable Element of the carrier of K
(K,V,f,W) . f is right_complementable Element of the carrier of K
qf * ((K,V,f,W) . f) 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 . (qf,((K,V,f,W) . f)) 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
qf * (1_ K) is right_complementable Element of the carrier of K
the multF of K . (qf,(1_ K)) is right_complementable Element of the carrier of K
K is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
the carrier of K is non empty non trivial 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 non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of V is non empty non trivial 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
Lin {f} is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
qf is right_complementable Element of the carrier of V
W is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f}
(K,V,f,W) is V1() V4( the carrier of V) V5( the carrier of K) Function-like non constant non empty non trivial V14( the carrier of V) quasi_total additive homogeneous 0-preserving Element of bool [: the carrier of V, 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
(K,V,f,W) . qf is right_complementable Element of the carrier of K
the carrier of W is non empty set
(K,V,f,W) | the carrier of W is V1() V4( the carrier of V) V4( the carrier of W) V4( the carrier of V) V5( the carrier of K) Function-like Element of bool [: the carrier of V, the carrier of K:]
((K,V,f,W) | the carrier of W) . qf is set
0Functional W is V1() V4( the carrier of W) V5( the carrier of K) Function-like constant non empty V14( the carrier of W) quasi_total additive homogeneous 0-preserving Element of bool [: the carrier of W, the carrier of K:]
[: the carrier of W, the carrier of K:] is V1() non empty set
bool [: the carrier of W, the carrier of K:] is non empty set
w is right_complementable Element of the carrier of W
(0Functional W) . w is right_complementable Element of the carrier of K
K is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
the carrier of K is non empty non trivial set
V is non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of V is non empty non trivial 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
Lin {f} is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
qf 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 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,f) is right_complementable Element of the carrier of V
(W * f) + qf 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 . ((W * f),qf) is right_complementable Element of the carrier of V
qV is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Linear_Compl of Lin {f}
(K,V,f,qV) is V1() V4( the carrier of V) V5( the carrier of K) Function-like non constant non empty non trivial V14( the carrier of V) quasi_total additive homogeneous 0-preserving Element of bool [: the carrier of V, 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
(K,V,f,qV) . ((W * f) + qf) is right_complementable Element of the carrier of K
(K,V,f,qV) . (W * f) is right_complementable Element of the carrier of K
(K,V,f,qV) . qf is right_complementable Element of the carrier of K
((K,V,f,qV) . (W * f)) + ((K,V,f,qV) . qf) 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 . (((K,V,f,qV) . (W * f)),((K,V,f,qV) . qf)) is right_complementable Element of the carrier of K
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
((K,V,f,qV) . (W * f)) + (0. K) is right_complementable Element of the carrier of K
the addF of K . (((K,V,f,qV) . (W * f)),(0. K)) is right_complementable Element of the carrier of K
K is non empty addLoopStr
the carrier of K is non empty set
V is non empty VectSpStr over K
the carrier of V is non empty set
[: 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
f 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:]
qf 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:]
f - qf 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:]
- qf 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:]
f + (- qf) 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:]
W is Element of the carrier of V
(f - qf) . W is Element of the carrier of K
f . W is Element of the carrier of K
qf . W is Element of the carrier of K
(f . W) - (qf . W) is Element of the carrier 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 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 . W),(- (qf . W))) is Element of the carrier 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
K is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
V is non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
V *' is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of V is non empty non trivial set
the carrier of K is non empty non trivial set
[: 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
the V1() V4( the carrier of V) V5( the carrier of K) Function-like non constant non empty non trivial V14( the carrier of V) quasi_total additive homogeneous 0-preserving Element of bool [: the carrier of V, the carrier of K:] is V1() V4( the carrier of V) V5( the carrier of K) Function-like non constant non empty non trivial V14( the carrier of V) quasi_total additive homogeneous 0-preserving Element of bool [: the carrier of V, the carrier of K:]
0Functional V is V1() V4( the carrier of V) V5( the carrier of K) Function-like constant non empty V14( the carrier of V) quasi_total additive homogeneous 0-preserving Element of bool [: the carrier of V, the carrier of K:]
the carrier of (V *') is non empty set
qf is right_complementable Element of the carrier of (V *')
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 *')
K is non empty ZeroStr
V is non empty VectSpStr over K
the carrier of V is non empty set
the carrier of K is non empty set
[: 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
f 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:]
0. K is V48(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
{ b1 where b1 is Element of the carrier of V : f . b1 = 0. K } is set
bool the carrier of V is non empty set
W is set
qV is Element of the carrier of V
f . qV is Element of the carrier of K
K is non empty right_zeroed addLoopStr
V is non empty VectSpStr over K
the carrier of V is non empty set
the carrier of K is non empty set
[: 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
f is V1() V4( the carrier of V) V5( the carrier of K) Function-like non empty V14( the carrier of V) quasi_total 0-preserving Element of bool [: the carrier of V, the carrier of K:]
(K,V,f) is Element of bool the carrier of V
bool the carrier of V 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
{ b1 where b1 is Element of the carrier of V : f . b1 = 0. K } is set
0. V is V48(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
f . (0. V) is Element of the carrier of K
K is non empty right_complementable add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
the carrier of K is non empty set
V is non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of V is non empty set
[: 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
f is V1() V4( the carrier of V) V5( the carrier of K) Function-like non empty V14( the carrier of V) quasi_total additive homogeneous 0-preserving Element of bool [: the carrier of V, the carrier of K:]
(K,V,f) is non empty Element of bool the carrier of V
bool the carrier of V 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
{ b1 where b1 is Element of the carrier of V : f . b1 = 0. K } is set
W is right_complementable Element of the carrier of V
qV is right_complementable Element of the carrier of V
W + 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:] 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 . (W,qV) is right_complementable Element of the carrier of V
f . (W + qV) is right_complementable Element of the carrier of K
(0. 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 . ((0. K),(0. K)) is right_complementable Element of the carrier of K
x is right_complementable Element of the carrier of V
f . x is right_complementable Element of the carrier of K
w is right_complementable Element of the carrier of V
f . w is right_complementable Element of the carrier of K
W is right_complementable Element of the carrier of K
qV is right_complementable Element of the carrier of V
W * qV 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,qV) is right_complementable Element of the carrier of V
f . (W * qV) is right_complementable Element of the carrier of K
W * (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 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,(0. K)) is right_complementable Element of the carrier of K
x is right_complementable Element of the carrier of V
f . x is right_complementable Element of the carrier of K
K is non empty ZeroStr
V is non empty VectSpStr over K
the carrier of V is non empty set
the carrier of K is non empty set
[: 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
K is non empty non degenerated non trivial doubleLoopStr
V is non empty non trivial VectSpStr over K
the carrier of V is non empty non trivial set
the carrier of K is non empty non trivial set
[: 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
f 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:]
0. V is V48(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
f . (0. V) 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,V,f) is Element of bool the carrier of V
bool the carrier of V is non empty set
{ b1 where b1 is Element of the carrier of V : f . b1 = 0. K } is set
qf is set
W is Element of the carrier of V
W is Element of the carrier of V
f . W is Element of the carrier of K
W is Element of the carrier of V
{(0. V)} is trivial V29() Element of bool the carrier of V
dom f is non empty Element of bool the carrier of V
qf is Element of the carrier of V
f . qf is Element of the carrier of K
K is non empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of V is non empty set
the carrier of K is non empty set
[: 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
f is V1() V4( the carrier of V) V5( the carrier of K) Function-like non empty V14( the carrier of V) quasi_total additive homogeneous 0-preserving Element of bool [: the carrier of V, the carrier of K:]
(K,V,f) is non empty Element of bool the carrier of V
bool the carrier of V 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
{ b1 where b1 is Element of the carrier of V : f . b1 = 0. K } is set
qf is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
the carrier of qf is non empty set
W is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
the carrier of W is non empty set
K is non empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of V is non empty set
the carrier of K is non empty set
[: 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
f is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
the carrier of f is non empty set
qf is V1() V4( the carrier of V) V5( the carrier of K) Function-like non empty V14( the carrier of V) quasi_total additive 0-preserving Element of bool [: the carrier of V, the carrier of K:]
(K,V,qf) is non empty Element of bool the carrier of V
bool the carrier of V 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
{ b1 where b1 is Element of the carrier of V : qf . b1 = 0. K } is set
(K,V,f) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of (K,V,f) is non empty set
[: the carrier of (K,V,f), the carrier of K:] is V1() non empty set
bool [: the carrier of (K,V,f), the carrier of K:] is non empty set
(K,V,f) is V1() V4([:(K,V,f),(K,V,f):]) V5((K,V,f)) Function-like non empty V14([:(K,V,f),(K,V,f):]) quasi_total Element of bool [:[:(K,V,f),(K,V,f):],(K,V,f):]
(K,V,f) is non empty Element of bool (bool the carrier of V)
bool (bool the carrier of V) is non empty set
{ b1 where b1 is Coset of f : verum } is set
[:(K,V,f),(K,V,f):] is V1() non empty set
[:[:(K,V,f),(K,V,f):],(K,V,f):] is V1() non empty set
bool [:[:(K,V,f),(K,V,f):],(K,V,f):] is non empty set
w is right_complementable Element of the carrier of (K,V,f)
A is right_complementable Element of the carrier of V
A + f is Element of bool the carrier of V
{ (A + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
qf . A is right_complementable Element of the carrier of K
v is right_complementable Element of the carrier of K
a is right_complementable Element of the carrier of V
a + f is Element of bool the carrier of V
{ (a + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
qf . a is right_complementable Element of the carrier of K
a is right_complementable Element of the carrier of V
a + a 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 . (a,a) is right_complementable Element of the carrier of V
qf . a is right_complementable Element of the carrier of K
(qf . a) + (qf . a) 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 . a),(qf . a)) is right_complementable Element of the carrier of K
b is right_complementable Element of the carrier of V
qf . b is right_complementable Element of the carrier of K
w is V1() V4( the carrier of (K,V,f)) V5( the carrier of K) Function-like non empty V14( the carrier of (K,V,f)) quasi_total Element of bool [: the carrier of (K,V,f), the carrier of K:]
[: the carrier of (K,V,f), the carrier of (K,V,f):] is V1() non empty set
the addF of (K,V,f) is V1() V4([: the carrier of (K,V,f), the carrier of (K,V,f):]) V5( the carrier of (K,V,f)) Function-like non empty V14([: the carrier of (K,V,f), the carrier of (K,V,f):]) quasi_total Element of bool [:[: the carrier of (K,V,f), the carrier of (K,V,f):], the carrier of (K,V,f):]
[:[: the carrier of (K,V,f), the carrier of (K,V,f):], the carrier of (K,V,f):] is V1() non empty set
bool [:[: the carrier of (K,V,f), the carrier of (K,V,f):], the carrier of (K,V,f):] is non empty set
v is right_complementable Element of the carrier of (K,V,f)
a is right_complementable Element of the carrier of V
a + f is Element of bool the carrier of V
{ (a + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
a is right_complementable Element of the carrier of (K,V,f)
b is right_complementable Element of the carrier of V
b + f is Element of bool the carrier of V
{ (b + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
(K,V,f) . (v,a) is set
a + b 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 . (a,b) is right_complementable Element of the carrier of V
(a + b) + f is Element of bool the carrier of V
{ ((a + b) + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
A is V1() V4( the carrier of (K,V,f)) V5( the carrier of K) Function-like non empty V14( the carrier of (K,V,f)) quasi_total Element of bool [: the carrier of (K,V,f), the carrier of K:]
v + a is right_complementable Element of the carrier of (K,V,f)
the addF of (K,V,f) . (v,a) is right_complementable Element of the carrier of (K,V,f)
A . (v + a) is right_complementable Element of the carrier of K
qf . (a + b) is right_complementable Element of the carrier of K
qf . a is right_complementable Element of the carrier of K
qf . b is right_complementable Element of the carrier of K
(qf . a) + (qf . b) 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 . a),(qf . b)) is right_complementable Element of the carrier of K
A . v is right_complementable Element of the carrier of K
(A . v) + (qf . b) is right_complementable Element of the carrier of K
the addF of K . ((A . v),(qf . b)) is right_complementable Element of the carrier of K
A . a is right_complementable Element of the carrier of K
(A . v) + (A . a) is right_complementable Element of the carrier of K
the addF of K . ((A . v),(A . a)) is right_complementable Element of the carrier of K
v is V1() V4( the carrier of (K,V,f)) V5( the carrier of K) Function-like non empty V14( the carrier of (K,V,f)) quasi_total additive 0-preserving Element of bool [: the carrier of (K,V,f), the carrier of K:]
a is right_complementable Element of the carrier of (K,V,f)
a is right_complementable Element of the carrier of V
a + f is Element of bool the carrier of V
{ (a + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
v . a is right_complementable Element of the carrier of K
qf . a is right_complementable Element of the carrier of K
qV is V1() V4( the carrier of (K,V,f)) V5( the carrier of K) Function-like non empty V14( the carrier of (K,V,f)) quasi_total additive 0-preserving Element of bool [: the carrier of (K,V,f), the carrier of K:]
x is V1() V4( the carrier of (K,V,f)) V5( the carrier of K) Function-like non empty V14( the carrier of (K,V,f)) quasi_total additive 0-preserving Element of bool [: the carrier of (K,V,f), the carrier of K:]
w is right_complementable Element of the carrier of (K,V,f)
A is right_complementable Element of the carrier of V
A + f is Element of bool the carrier of V
{ (A + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
qV . w is right_complementable Element of the carrier of K
qf . A is right_complementable Element of the carrier of K
x . w is right_complementable Element of the carrier of K
K is non empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
the carrier of K is non empty set
V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of V is non empty set
[: 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
f is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
the carrier of f is non empty set
(K,V,f) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
qf is V1() V4( the carrier of V) V5( the carrier of K) Function-like non empty V14( the carrier of V) quasi_total additive homogeneous 0-preserving Element of bool [: the carrier of V, the carrier of K:]
(K,V,qf) is non empty Element of bool the carrier of V
bool the carrier of V 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
{ b1 where b1 is Element of the carrier of V : qf . b1 = 0. K } is set
(K,V,f,qf) is V1() V4( the carrier of (K,V,f)) V5( the carrier of K) Function-like non empty V14( the carrier of (K,V,f)) quasi_total additive 0-preserving Element of bool [: the carrier of (K,V,f), the carrier of K:]
the carrier of (K,V,f) is non empty set
[: the carrier of (K,V,f), the carrier of K:] is V1() non empty set
bool [: the carrier of (K,V,f), the carrier of K:] is non empty set
(K,V,f) is non empty Element of bool (bool the carrier of V)
bool (bool the carrier of V) is non empty set
{ b1 where b1 is Coset of f : verum } is set
w is right_complementable Element of the carrier of (K,V,f)
v is Coset of f
a is right_complementable Element of the carrier of V
a + f is Element of bool the carrier of V
{ (a + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
A is right_complementable Element of the carrier of K
A * w is right_complementable Element of the carrier of (K,V,f)
the lmult of (K,V,f) is V1() V4([: the carrier of K, the carrier of (K,V,f):]) V5( the carrier of (K,V,f)) Function-like non empty V14([: the carrier of K, the carrier of (K,V,f):]) quasi_total Element of bool [:[: the carrier of K, the carrier of (K,V,f):], the carrier of (K,V,f):]
[: the carrier of K, the carrier of (K,V,f):] is V1() non empty set
[:[: the carrier of K, the carrier of (K,V,f):], the carrier of (K,V,f):] is V1() non empty set
bool [:[: the carrier of K, the carrier of (K,V,f):], the carrier of (K,V,f):] is non empty set
the lmult of (K,V,f) . (A,w) is right_complementable Element of the carrier of (K,V,f)
(K,V,f) is V1() V4([: the carrier of K,(K,V,f):]) V5((K,V,f)) Function-like non empty V14([: the carrier of K,(K,V,f):]) quasi_total Element of bool [:[: the carrier of K,(K,V,f):],(K,V,f):]
[: the carrier of K,(K,V,f):] is V1() non empty set
[:[: the carrier of K,(K,V,f):],(K,V,f):] is V1() non empty set
bool [:[: the carrier of K,(K,V,f):],(K,V,f):] is non empty set
(K,V,f) . (A,w) is set
A * a 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,a) is right_complementable Element of the carrier of V
(A * a) + f is Element of bool the carrier of V
{ ((A * a) + b1) where b1 is right_complementable Element of the carrier of V : b1 in f } is set
(K,V,f,qf) . (A * w) is right_complementable Element of the carrier of K
qf . (A * a) is right_complementable Element of the carrier of K
qf . a is right_complementable Element of the carrier of K
A * (qf . a) 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 . (A,(qf . a)) is right_complementable Element of the carrier of K
(K,V,f,qf) . w is right_complementable Element of the carrier of K
A * ((K,V,f,qf) . w) is right_complementable Element of the carrier of K
the multF of K . (A,((K,V,f,qf) . w)) is right_complementable Element of the carrier of K
K is non empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of V is non empty set
the carrier of K is non empty set
[: 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
f is V1() V4( the carrier of V) V5( the carrier of K) Function-like non empty V14( the carrier of V) quasi_total additive homogeneous 0-preserving Element of bool [: the carrier of V, the carrier of K:]
(K,V,f) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
(K,V,(K,V,f),f) is V1() V4( the carrier of (K,V,(K,V,f))) V5( the carrier of K) Function-like non empty V14( the carrier of (K,V,(K,V,f))) quasi_total additive 0-preserving Element of bool [: the carrier of (K,V,(K,V,f)), the carrier of K:]
(K,V,(K,V,f)) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of (K,V,(K,V,f)) is non empty set
[: the carrier of (K,V,(K,V,f)), the carrier of K:] is V1() non empty set
bool [: the carrier of (K,V,(K,V,f)), the carrier of K:] is non empty set
the carrier of (K,V,f) is non empty set
(K,V,f) is non empty Element of bool the carrier of V
bool the carrier of V 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
{ b1 where b1 is Element of the carrier of V : f . b1 = 0. K } is set
K is non empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
the carrier of K is non empty set
V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of V is non empty set
[: 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
f is V1() V4( the carrier of V) V5( the carrier of K) Function-like non empty V14( the carrier of V) quasi_total additive homogeneous 0-preserving Element of bool [: the carrier of V, the carrier of K:]
(K,V,f) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
(K,V,(K,V,f)) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of (K,V,(K,V,f)) is non empty set
(K,V,f) is V1() V4( the carrier of (K,V,(K,V,f))) V5( the carrier of K) Function-like non empty V14( the carrier of (K,V,(K,V,f))) quasi_total additive homogeneous 0-preserving Element of bool [: the carrier of (K,V,(K,V,f)), the carrier of K:]
[: the carrier of (K,V,(K,V,f)), the carrier of K:] is V1() non empty set
bool [: the carrier of (K,V,(K,V,f)), the carrier of K:] is non empty set
(K,V,(K,V,f),f) is V1() V4( the carrier of (K,V,(K,V,f))) V5( the carrier of K) Function-like non empty V14( the carrier of (K,V,(K,V,f))) quasi_total additive 0-preserving Element of bool [: the carrier of (K,V,(K,V,f)), the carrier of K:]
qf is right_complementable Element of the carrier of (K,V,(K,V,f))
(K,V,f) . qf is right_complementable Element of the carrier of K
W is right_complementable Element of the carrier of V
W + (K,V,f) is Element of bool the carrier of V
bool the carrier of V is non empty set
{ (W + b1) where b1 is right_complementable Element of the carrier of V : b1 in (K,V,f) } is set
f . W is right_complementable Element of the carrier of K
the carrier of (K,V,f) is non empty set
(K,V,f) is non empty Element of bool 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
{ b1 where b1 is Element of the carrier of V : f . b1 = 0. K } is set
K is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
V is non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of V is non empty non trivial set
the carrier of K is non empty non trivial set
[: 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
f is V1() V4( the carrier of V) V5( the carrier of K) Function-like non constant non empty non trivial V14( the carrier of V) quasi_total additive homogeneous 0-preserving Element of bool [: the carrier of V, the carrier of K:]
(K,V,f) is V1() V4( the carrier of (K,V,(K,V,f))) V5( the carrier of K) Function-like non empty V14( the carrier of (K,V,(K,V,f))) quasi_total additive homogeneous 0-preserving Element of bool [: the carrier of (K,V,(K,V,f)), the carrier of K:]
(K,V,f) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
(K,V,(K,V,f)) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of (K,V,(K,V,f)) is non empty set
[: the carrier of (K,V,(K,V,f)), the carrier of K:] is V1() non empty set
bool [: the carrier of (K,V,(K,V,f)), the carrier of K:] is non empty set
(K,V,(K,V,f),f) is V1() V4( the carrier of (K,V,(K,V,f))) V5( the carrier of K) Function-like non empty V14( the carrier of (K,V,(K,V,f))) quasi_total additive 0-preserving Element of bool [: the carrier of (K,V,(K,V,f)), the carrier of K:]
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
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
x is right_complementable Element of the carrier of V
f . x is right_complementable Element of the carrier of K
x + (K,V,f) is Element of bool the carrier of V
bool the carrier of V is non empty set
{ (x + b1) where b1 is right_complementable Element of the carrier of V : b1 in (K,V,f) } is set
0Functional (K,V,(K,V,f)) is V1() V4( the carrier of (K,V,(K,V,f))) V5( the carrier of K) Function-like constant non empty V14( the carrier of (K,V,(K,V,f))) quasi_total additive homogeneous 0-preserving Element of bool [: the carrier of (K,V,(K,V,f)), the carrier of K:]
w is right_complementable Element of the carrier of (K,V,(K,V,f))
(K,V,f) . w is right_complementable Element of the carrier of K
K is non empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
the carrier of V is non empty set
the carrier of K is non empty set
[: 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
f is V1() V4( the carrier of V) V5( the carrier of K) Function-like non empty V14( the carrier of V) quasi_total additive homogeneous 0-preserving Element of bool [: the carrier of V, the carrier of K:]
(K,V,f) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
(K,V,(K,V,f)) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
(K,V,f) is V1() V4( the carrier of (K,V,(K,V,f))) V5( the carrier of K) Function-like non empty V14( the carrier of (K,V,(K,V,f))) quasi_total additive homogeneous 0-preserving Element of bool [: the carrier of (K,V,(K,V,f)), the carrier of K:]
the carrier of (K,V,(K,V,f)) is non empty set
[: the carrier of (K,V,(K,V,f)), the carrier of K:] is V1() non empty set
bool [: the carrier of (K,V,(K,V,f)), the carrier of K:] is non empty set
(K,V,(K,V,f),f) is V1() V4( the carrier of (K,V,(K,V,f))) V5( the carrier of K) Function-like non empty V14( the carrier of (K,V,(K,V,f))) quasi_total additive 0-preserving Element of bool [: the carrier of (K,V,(K,V,f)), the carrier of K:]
the carrier of (K,V,f) is non empty set
(K,V,f) is non empty Element of bool the carrier of V
bool the carrier of V 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
{ b1 where b1 is Element of the carrier of V : f . b1 = 0. K } is set
(K,V,(K,V,f)) is non empty Element of bool (bool the carrier of V)
bool (bool the carrier of V) is non empty set
{ b1 where b1 is Coset of (K,V,f) : verum } is set
(K,(K,V,(K,V,f)),(K,V,f)) is non empty Element of bool the carrier of (K,V,(K,V,f))
bool the carrier of (K,V,(K,V,f)) is non empty set
{ b1 where b1 is Element of the carrier of (K,V,(K,V,f)) : (K,V,f) . b1 = 0. K } is set
0. (K,V,(K,V,f)) is V48((K,V,(K,V,f))) right_complementable Element of the carrier of (K,V,(K,V,f))
the ZeroF of (K,V,(K,V,f)) is right_complementable Element of the carrier of (K,V,(K,V,f))
{(0. (K,V,(K,V,f)))} is trivial V29() Element of bool the carrier of (K,V,(K,V,f))
x is set
w is right_complementable Element of the carrier of (K,V,(K,V,f))
(K,V,f) . w is right_complementable Element of the carrier of K
A is Coset of (K,V,f)
v is right_complementable Element of the carrier of V
v + (K,V,f) is Element of bool the carrier of V
{ (v + b1) where b1 is right_complementable Element of the carrier of V : b1 in (K,V,f) } is set
f . v is right_complementable Element of the carrier of K
(K,V,(K,V,f)) is Element of (K,V,(K,V,f))
x is set
(K,V,f) . (0. (K,V,(K,V,f))) is right_complementable Element of the carrier of K