:: VECTSP10 semantic presentation

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</