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