:: MOD_4 semantic presentation

K117() is Element of bool K113()
K113() is set
bool K113() is non empty set
K112() is set
bool K112() is non empty set
bool K117() is non empty set
{} is empty Function-like functional set
1 is non empty set
K2({},1) is non empty set
K is non empty addMagma
the carrier of K is non empty set
id K is non empty Relation-like the carrier of K -defined the carrier of K -valued Function-like V17( the carrier of K) quasi_total additive Element of bool [: the carrier of K, the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
bool [: the carrier of K, the carrier of K:] is non empty set
K97( the carrier of K) is non empty Relation-like the carrier of K -defined the carrier of K -valued Function-like one-to-one V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of K:]
rng (id K) is set
K is non empty set
V is non empty set
[:K,V:] is non empty set
W is non empty set
[:[:K,V:],W:] is non empty set
bool [:[:K,V:],W:] is non empty set
f is non empty Relation-like [:K,V:] -defined W -valued Function-like V17([:K,V:]) quasi_total Element of bool [:[:K,V:],W:]
~ f is Relation-like Function-like set
[:V,K:] is non empty set
[:[:V,K:],W:] is non empty set
bool [:[:V,K:],W:] is non empty set
K is non empty set
V is non empty set
W is non empty set
[:V,W:] is non empty set
[:[:V,W:],K:] is non empty set
bool [:[:V,W:],K:] is non empty set
f is non empty Relation-like [:V,W:] -defined K -valued Function-like V17([:V,W:]) quasi_total Element of bool [:[:V,W:],K:]
(V,W,K,f) is non empty Relation-like [:W,V:] -defined K -valued Function-like V17([:W,V:]) quasi_total Element of bool [:[:W,V:],K:]
[:W,V:] is non empty set
[:[:W,V:],K:] is non empty set
bool [:[:W,V:],K:] is non empty set
J is Element of V
a is Element of W
f . (J,a) is Element of K
(V,W,K,f) . (a,J) is Element of K
dom f is Relation-like set
[J,a] is Element of [:V,W:]
[a,J] is Element of [:W,V:]
dom (V,W,K,f) is Relation-like set
K is non empty doubleLoopStr
the carrier of K is non empty set
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is Element of the carrier of K
the OneF of K is Element of the carrier of K
0. K is V46(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty strict doubleLoopStr
K is non empty doubleLoopStr
(K) is strict doubleLoopStr
the carrier of K is non empty set
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is Element of the carrier of K
the OneF of K is Element of the carrier of K
0. K is V46(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty strict doubleLoopStr
K is non empty unital right_unital well-unital left_unital doubleLoopStr
(K) is non empty strict doubleLoopStr
the carrier of K is non empty set
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is Element of the carrier of K
the OneF of K is Element of the carrier of K
0. K is V46(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty strict doubleLoopStr
the carrier of (K) is non empty set
W is Element of the carrier of (K)
V is Element of the carrier of (K)
V * W is Element of the carrier of (K)
the multF of (K) is non empty Relation-like [: the carrier of (K), the carrier of (K):] -defined the carrier of (K) -valued Function-like V17([: 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 non empty set
[:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
bool [:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
the multF of (K) . (V,W) is Element of the carrier of (K)
W * V is Element of the carrier of (K)
the multF of (K) . (W,V) is Element of the carrier of (K)
J is Element of the carrier of K
f is Element of the carrier of K
J * f is Element of the carrier of K
the multF of K . (J,f) is Element of the carrier of K
f * J is Element of the carrier of K
the multF of K . (f,J) is Element of the carrier of K
K is non empty unital right_unital well-unital left_unital doubleLoopStr
(K) is non empty strict doubleLoopStr
the carrier of K is non empty set
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is Element of the carrier of K
the OneF of K is Element of the carrier of K
0. K is V46(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty strict doubleLoopStr
the carrier of (K) is non empty set
V 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)
V * (1. (K)) is Element of the carrier of (K)
the multF of (K) is non empty Relation-like [: the carrier of (K), the carrier of (K):] -defined the carrier of (K) -valued Function-like V17([: 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 non empty set
[:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
bool [:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
the multF of (K) . (V,(1. (K))) is Element of the carrier of (K)
(1. (K)) * V is Element of the carrier of (K)
the multF of (K) . ((1. (K)),V) is Element of the carrier of (K)
K is non empty right_complementable add-associative right_zeroed doubleLoopStr
(K) is non empty strict doubleLoopStr
the carrier of K is non empty set
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is right_complementable Element of the carrier of K
the OneF of K is right_complementable Element of the carrier of K
0. K is V46(K) right_complementable Element of the carrier of K
the ZeroF of K is right_complementable Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty strict doubleLoopStr
the carrier of (K) is non empty set
0. (K) is V46((K)) Element of the carrier of (K)
the ZeroF of (K) is Element of the carrier of (K)
W is Element of the carrier of (K)
f is Element of the carrier of (K)
W + f is Element of the carrier of (K)
the addF of (K) is non empty Relation-like [: the carrier of (K), the carrier of (K):] -defined the carrier of (K) -valued Function-like V17([: 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 non empty set
[:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
bool [:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
the addF of (K) . (W,f) is Element of the carrier of (K)
J is Element of the carrier of (K)
(W + f) + J is Element of the carrier of (K)
the addF of (K) . ((W + f),J) is Element of the carrier of (K)
f + J is Element of the carrier of (K)
the addF of (K) . (f,J) is Element of the carrier of (K)
W + (f + J) is Element of the carrier of (K)
the addF of (K) . (W,(f + J)) is Element of the carrier of (K)
W + (0. (K)) is Element of the carrier of (K)
the addF of (K) . (W,(0. (K))) is Element of the carrier of (K)
a is right_complementable Element of the carrier of K
x is right_complementable Element of the carrier of K
a + x is right_complementable Element of the carrier of K
the addF of K . (a,x) is right_complementable Element of the carrier of K
z is right_complementable Element of the carrier of K
(a + x) + z is right_complementable Element of the carrier of K
the addF of K . ((a + x),z) is right_complementable Element of the carrier of K
x + z is right_complementable Element of the carrier of K
the addF of K . (x,z) is right_complementable Element of the carrier of K
a + (x + z) is right_complementable Element of the carrier of K
the addF of K . (a,(x + z)) is right_complementable Element of the carrier of K
a + (0. K) is right_complementable Element of the carrier of K
the addF of K . (a,(0. K)) is right_complementable Element of the carrier of K
K is non empty right_complementable add-associative right_zeroed doubleLoopStr
(K) is non empty strict doubleLoopStr
the carrier of K is non empty set
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is right_complementable Element of the carrier of K
the OneF of K is right_complementable Element of the carrier of K
0. K is V46(K) right_complementable Element of the carrier of K
the ZeroF of K is right_complementable Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty strict doubleLoopStr
the carrier of (K) is non empty set
V is Element of the carrier of (K)
W is Element of the carrier of (K)
f is Element of the carrier of (K)
W + f is Element of the carrier of (K)
the addF of (K) is non empty Relation-like [: the carrier of (K), the carrier of (K):] -defined the carrier of (K) -valued Function-like V17([: 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 non empty set
[:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
bool [:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
the addF of (K) . (W,f) is Element of the carrier of (K)
V + (W + f) is Element of the carrier of (K)
the addF of (K) . (V,(W + f)) is Element of the carrier of (K)
V + W is Element of the carrier of (K)
the addF of (K) . (V,W) is Element of the carrier of (K)
(V + W) + f is Element of the carrier of (K)
the addF of (K) . ((V + W),f) is Element of the carrier of (K)
0. (K) is V46((K)) Element of the carrier of (K)
the ZeroF of (K) is Element of the carrier of (K)
V is Element of the carrier of (K)
V + (0. (K)) is Element of the carrier of (K)
the addF of (K) is non empty Relation-like [: the carrier of (K), the carrier of (K):] -defined the carrier of (K) -valued Function-like V17([: 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 non empty set
[:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
bool [:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
the addF of (K) . (V,(0. (K))) is Element of the carrier of (K)
V is Element of the carrier of (K)
W is right_complementable Element of the carrier of K
- W is right_complementable Element of the carrier of K
f is Element of the carrier of (K)
V + f is Element of the carrier of (K)
the addF of (K) is non empty Relation-like [: the carrier of (K), the carrier of (K):] -defined the carrier of (K) -valued Function-like V17([: 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 non empty set
[:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
bool [:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
the addF of (K) . (V,f) is Element of the carrier of (K)
W + (- W) is right_complementable Element of the carrier of K
the addF of K . (W,(- W)) is right_complementable Element of the carrier of K
K is non empty right_complementable add-associative right_zeroed doubleLoopStr
the carrier of K is non empty set
(K) is non empty right_complementable strict add-associative right_zeroed doubleLoopStr
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is right_complementable Element of the carrier of K
the OneF of K is right_complementable Element of the carrier of K
0. K is V46(K) right_complementable Element of the carrier of K
the ZeroF of K is right_complementable Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty strict doubleLoopStr
the carrier of (K) is non empty set
V is right_complementable Element of the carrier of K
W is right_complementable Element of the carrier of K
V + W is right_complementable Element of the carrier of K
the addF of K . (V,W) is right_complementable Element of the carrier of K
V * W is right_complementable Element of the carrier of K
the multF of K . (V,W) is right_complementable Element of the carrier of K
- V is right_complementable Element of the carrier of K
f is right_complementable Element of the carrier of (K)
J is right_complementable Element of the carrier of (K)
f + J is right_complementable Element of the carrier of (K)
the addF of (K) is non empty Relation-like [: the carrier of (K), the carrier of (K):] -defined the carrier of (K) -valued Function-like V17([: 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 non empty set
[:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
bool [:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
the addF of (K) . (f,J) is right_complementable Element of the carrier of (K)
J * f is right_complementable Element of the carrier of (K)
the multF of (K) is non empty Relation-like [: the carrier of (K), the carrier of (K):] -defined the carrier of (K) -valued Function-like V17([: 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) . (J,f) is right_complementable Element of the carrier of (K)
- f is right_complementable Element of the carrier of (K)
a is right_complementable Element of the carrier of K
a + V is right_complementable Element of the carrier of K
the addF of K . (a,V) is right_complementable Element of the carrier of K
(- f) + f is right_complementable Element of the carrier of (K)
the addF of (K) . ((- f),f) is right_complementable Element of the carrier of (K)
0. (K) is V46((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 doubleLoopStr
(K) is non empty strict doubleLoopStr
the carrier of K is non empty set
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is Element of the carrier of K
the OneF of K is Element of the carrier of K
0. K is V46(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty strict doubleLoopStr
the carrier of (K) is non empty set
the addF of (K) is non empty Relation-like [: the carrier of (K), the carrier of (K):] -defined the carrier of (K) -valued Function-like V17([: 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 non empty set
[:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
bool [:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
the ZeroF of (K) is Element of the carrier of (K)
addLoopStr(# the carrier of (K), the addF of (K), the ZeroF of (K) #) is non empty strict addLoopStr
addLoopStr(# the carrier of K, the addF of K, the ZeroF of K #) is non empty strict addLoopStr
comp (K) is non empty Relation-like the carrier of (K) -defined the carrier of (K) -valued Function-like V17( the carrier of (K)) quasi_total Element of bool [: the carrier of (K), the carrier of (K):]
bool [: the carrier of (K), the carrier of (K):] is non empty set
comp K is non empty Relation-like the carrier of K -defined the carrier of K -valued Function-like V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of K:]
bool [: the carrier of K, the carrier of K:] is non empty set
V is set
(comp (K)) . V is set
(comp K) . V is set
W is Element of the carrier of K
- W is Element of the carrier of K
f is Element of the carrier of (K)
- f is Element of the carrier of (K)
dom (comp (K)) is set
dom (comp K) is set
V is set
K is non empty doubleLoopStr
the carrier of K is non empty set
(K) is non empty strict doubleLoopStr
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is Element of the carrier of K
the OneF of K is Element of the carrier of K
0. K is V46(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty strict doubleLoopStr
the carrier of (K) is non empty set
V is Element of the carrier of K
W is Element of the carrier of K
f is Element of the carrier of K
J is Element of the carrier of K
V + W is Element of the carrier of K
the addF of K . (V,W) is Element of the carrier of K
(V + W) + f is Element of the carrier of K
the addF of K . ((V + W),f) is Element of the carrier of K
W + f is Element of the carrier of K
the addF of K . (W,f) is Element of the carrier of K
V + (W + f) is Element of the carrier of K
the addF of K . (V,(W + f)) is Element of the carrier of K
V * W is Element of the carrier of K
the multF of K . (V,W) is Element of the carrier of K
(V * W) * f is Element of the carrier of K
the multF of K . ((V * W),f) is Element of the carrier of K
W * f is Element of the carrier of K
the multF of K . (W,f) is Element of the carrier of K
V * (W * f) is Element of the carrier of K
the multF of K . (V,(W * f)) is Element of the carrier of K
V * (W + f) is Element of the carrier of K
the multF of K . (V,(W + f)) is Element of the carrier of K
(W + f) * V is Element of the carrier of K
the multF of K . ((W + f),V) is Element of the carrier of K
f * J is Element of the carrier of K
the multF of K . (f,J) is Element of the carrier of K
(V * W) + (f * J) is Element of the carrier of K
the addF of K . ((V * W),(f * J)) is Element of the carrier of K
a is Element of the carrier of (K)
x is Element of the carrier of (K)
z is Element of the carrier of (K)
p is Element of the carrier of (K)
a + x is Element of the carrier of (K)
the addF of (K) is non empty Relation-like [: the carrier of (K), the carrier of (K):] -defined the carrier of (K) -valued Function-like V17([: 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 non empty set
[:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
bool [:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
the addF of (K) . (a,x) is Element of the carrier of (K)
(a + x) + z is Element of the carrier of (K)
the addF of (K) . ((a + x),z) is Element of the carrier of (K)
x + z is Element of the carrier of (K)
the addF of (K) . (x,z) is Element of the carrier of (K)
a + (x + z) is Element of the carrier of (K)
the addF of (K) . (a,(x + z)) is Element of the carrier of (K)
x * a is Element of the carrier of (K)
the multF of (K) is non empty Relation-like [: the carrier of (K), the carrier of (K):] -defined the carrier of (K) -valued Function-like V17([: 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) . (x,a) is Element of the carrier of (K)
z * (x * a) is Element of the carrier of (K)
the multF of (K) . (z,(x * a)) is Element of the carrier of (K)
z * x is Element of the carrier of (K)
the multF of (K) . (z,x) is Element of the carrier of (K)
(z * x) * a is Element of the carrier of (K)
the multF of (K) . ((z * x),a) is Element of the carrier of (K)
(x + z) * a is Element of the carrier of (K)
the multF of (K) . ((x + z),a) is Element of the carrier of (K)
a * (x + z) is Element of the carrier of (K)
the multF of (K) . (a,(x + z)) is Element of the carrier of (K)
p * z is Element of the carrier of (K)
the multF of (K) . (p,z) is Element of the carrier of (K)
(x * a) + (p * z) is Element of the carrier of (K)
the addF of (K) . ((x * a),(p * z)) is Element of the carrier of (K)
W is non empty right_complementable add-associative right_zeroed doubleLoopStr
the carrier of W is non empty set
(W) is non empty right_complementable strict add-associative right_zeroed doubleLoopStr
the addF of W is non empty Relation-like [: the carrier of W, the carrier of W:] -defined the carrier of W -valued Function-like V17([: 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 non empty set
[:[: the carrier of W, the carrier of W:], the carrier of W:] is non empty set
bool [:[: the carrier of W, the carrier of W:], the carrier of W:] is non empty set
the multF of W is non empty Relation-like [: the carrier of W, the carrier of W:] -defined the carrier of W -valued Function-like V17([: the carrier of W, the carrier of W:]) quasi_total Element of bool [:[: the carrier of W, the carrier of W:], the carrier of W:]
( the carrier of W, the carrier of W, the carrier of W, the multF of W) is non empty Relation-like [: the carrier of W, the carrier of W:] -defined the carrier of W -valued Function-like V17([: 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:]
1. W is right_complementable Element of the carrier of W
the OneF of W is right_complementable Element of the carrier of W
0. W is V46(W) right_complementable Element of the carrier of W
the ZeroF of W is right_complementable Element of the carrier of W
doubleLoopStr(# the carrier of W, the addF of W,( the carrier of W, the carrier of W, the carrier of W, the multF of W),(1. W),(0. W) #) is non empty strict doubleLoopStr
the carrier of (W) is non empty set
K is non empty unital doubleLoopStr
1. K is Element of the carrier of K
the carrier of K is non empty set
the OneF of K is Element of the carrier of K
(K) is non empty strict doubleLoopStr
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
0. K is V46(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty strict doubleLoopStr
1. (K) is Element of the carrier of (K)
the carrier of (K) is non empty set
the OneF of (K) is Element of the carrier of (K)
V is non empty right_complementable add-associative right_zeroed doubleLoopStr
0. V is V46(V) right_complementable Element of the carrier of V
the carrier of V is non empty set
the ZeroF of V is right_complementable Element of the carrier of V
(V) is non empty right_complementable strict add-associative right_zeroed doubleLoopStr
the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the multF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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, the multF of V) is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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:]
1. V is right_complementable Element of the carrier of V
the OneF of V is right_complementable Element of the carrier of V
doubleLoopStr(# the carrier of V, the addF of V,( the carrier of V, the carrier of V, the carrier of V, the multF of V),(1. V),(0. V) #) is non empty strict doubleLoopStr
0. (V) is V46((V)) right_complementable Element of the carrier of (V)
the carrier of (V) is non empty set
the ZeroF of (V) is right_complementable Element of the carrier of (V)
f is right_complementable Element of the carrier of W
z is right_complementable Element of the carrier of (W)
J is right_complementable Element of the carrier of W
p is right_complementable Element of the carrier of (W)
a is right_complementable Element of the carrier of W
q is right_complementable Element of the carrier of (W)
x is right_complementable Element of the carrier of W
a is right_complementable Element of the carrier of (W)
f + J is right_complementable Element of the carrier of W
the addF of W . (f,J) is right_complementable Element of the carrier of W
z + p is right_complementable Element of the carrier of (W)
the addF of (W) is non empty Relation-like [: the carrier of (W), the carrier of (W):] -defined the carrier of (W) -valued Function-like V17([: 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 non empty set
[:[: the carrier of (W), the carrier of (W):], the carrier of (W):] is non empty set
bool [:[: the carrier of (W), the carrier of (W):], the carrier of (W):] is non empty set
the addF of (W) . (z,p) is right_complementable Element of the carrier of (W)
f * J is right_complementable Element of the carrier of W
the multF of W . (f,J) is right_complementable Element of the carrier of W
p * z is right_complementable Element of the carrier of (W)
the multF of (W) is non empty Relation-like [: the carrier of (W), the carrier of (W):] -defined the carrier of (W) -valued Function-like V17([: 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 multF of (W) . (p,z) is right_complementable Element of the carrier of (W)
- f is right_complementable Element of the carrier of W
- z is right_complementable Element of the carrier of (W)
(f + J) + a is right_complementable Element of the carrier of W
the addF of W . ((f + J),a) is right_complementable Element of the carrier of W
(z + p) + q is right_complementable Element of the carrier of (W)
the addF of (W) . ((z + p),q) is right_complementable Element of the carrier of (W)
J + a is right_complementable Element of the carrier of W
the addF of W . (J,a) is right_complementable Element of the carrier of W
f + (J + a) is right_complementable Element of the carrier of W
the addF of W . (f,(J + a)) is right_complementable Element of the carrier of W
p + q is right_complementable Element of the carrier of (W)
the addF of (W) . (p,q) is right_complementable Element of the carrier of (W)
z + (p + q) is right_complementable Element of the carrier of (W)
the addF of (W) . (z,(p + q)) is right_complementable Element of the carrier of (W)
(f * J) * a is right_complementable Element of the carrier of W
the multF of W . ((f * J),a) is right_complementable Element of the carrier of W
q * (p * z) is right_complementable Element of the carrier of (W)
the multF of (W) . (q,(p * z)) is right_complementable Element of the carrier of (W)
J * a is right_complementable Element of the carrier of W
the multF of W . (J,a) is right_complementable Element of the carrier of W
f * (J * a) is right_complementable Element of the carrier of W
the multF of W . (f,(J * a)) is right_complementable Element of the carrier of W
q * p is right_complementable Element of the carrier of (W)
the multF of (W) . (q,p) is right_complementable Element of the carrier of (W)
(q * p) * z is right_complementable Element of the carrier of (W)
the multF of (W) . ((q * p),z) is right_complementable Element of the carrier of (W)
f * (J + a) is right_complementable Element of the carrier of W
the multF of W . (f,(J + a)) is right_complementable Element of the carrier of W
(p + q) * z is right_complementable Element of the carrier of (W)
the multF of (W) . ((p + q),z) is right_complementable Element of the carrier of (W)
(J + a) * f is right_complementable Element of the carrier of W
the multF of W . ((J + a),f) is right_complementable Element of the carrier of W
z * (p + q) is right_complementable Element of the carrier of (W)
the multF of (W) . (z,(p + q)) is right_complementable Element of the carrier of (W)
a * x is right_complementable Element of the carrier of W
the multF of W . (a,x) is right_complementable Element of the carrier of W
(f * J) + (a * x) is right_complementable Element of the carrier of W
the addF of W . ((f * J),(a * x)) is right_complementable Element of the carrier of W
a * q is right_complementable Element of the carrier of (W)
the multF of (W) . (a,q) is right_complementable Element of the carrier of (W)
(p * z) + (a * q) is right_complementable Element of the carrier of (W)
the addF of (W) . ((p * z),(a * q)) is right_complementable Element of the carrier of (W)
K is non empty Abelian doubleLoopStr
(K) is non empty strict doubleLoopStr
the carrier of K is non empty set
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is Element of the carrier of K
the OneF of K is Element of the carrier of K
0. K is V46(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty strict doubleLoopStr
the carrier of (K) is non empty set
V is Element of the carrier of (K)
W is Element of the carrier of (K)
V + W is Element of the carrier of (K)
the addF of (K) is non empty Relation-like [: the carrier of (K), the carrier of (K):] -defined the carrier of (K) -valued Function-like V17([: 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 non empty set
[:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
bool [:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
the addF of (K) . (V,W) is Element of the carrier of (K)
W + V is Element of the carrier of (K)
the addF of (K) . (W,V) is Element of the carrier of (K)
f is Element of the carrier of K
J is Element of the carrier of K
f + J is Element of the carrier of K
the addF of K . (f,J) is Element of the carrier of K
J + f is Element of the carrier of K
the addF of K . (J,f) is Element of the carrier of K
K is non empty add-associative doubleLoopStr
(K) is non empty strict doubleLoopStr
the carrier of K is non empty set
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is Element of the carrier of K
the OneF of K is Element of the carrier of K
0. K is V46(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty strict doubleLoopStr
the carrier of (K) is non empty set
V is Element of the carrier of (K)
W is Element of the carrier of (K)
V + W is Element of the carrier of (K)
the addF of (K) is non empty Relation-like [: the carrier of (K), the carrier of (K):] -defined the carrier of (K) -valued Function-like V17([: 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 non empty set
[:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
bool [:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
the addF of (K) . (V,W) is Element of the carrier of (K)
f is Element of the carrier of (K)
(V + W) + f is Element of the carrier of (K)
the addF of (K) . ((V + W),f) is Element of the carrier of (K)
W + f is Element of the carrier of (K)
the addF of (K) . (W,f) is Element of the carrier of (K)
V + (W + f) is Element of the carrier of (K)
the addF of (K) . (V,(W + f)) is Element of the carrier of (K)
J is Element of the carrier of K
a is Element of the carrier of K
J + a is Element of the carrier of K
the addF of K . (J,a) is Element of the carrier of K
x is Element of the carrier of K
(J + a) + x is Element of the carrier of K
the addF of K . ((J + a),x) is Element of the carrier of K
a + x is Element of the carrier of K
the addF of K . (a,x) is Element of the carrier of K
J + (a + x) is Element of the carrier of K
the addF of K . (J,(a + x)) is Element of the carrier of K
K is non empty right_zeroed doubleLoopStr
(K) is non empty strict doubleLoopStr
the carrier of K is non empty set
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is Element of the carrier of K
the OneF of K is Element of the carrier of K
0. K is V46(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty strict doubleLoopStr
the carrier of (K) is non empty set
V is Element of the carrier of (K)
0. (K) is V46((K)) Element of the carrier of (K)
the ZeroF of (K) is Element of the carrier of (K)
V + (0. (K)) is Element of the carrier of (K)
the addF of (K) is non empty Relation-like [: the carrier of (K), the carrier of (K):] -defined the carrier of (K) -valued Function-like V17([: 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 non empty set
[:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
bool [:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
the addF of (K) . (V,(0. (K))) is Element of the carrier of (K)
W is Element of the carrier of K
W + (0. K) is Element of the carrier of K
the addF of K . (W,(0. K)) is Element of the carrier of K
K is non empty right_complementable doubleLoopStr
(K) is non empty strict doubleLoopStr
the carrier of K is non empty set
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is right_complementable Element of the carrier of K
the OneF of K is right_complementable Element of the carrier of K
0. K is V46(K) right_complementable Element of the carrier of K
the ZeroF of K is right_complementable Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty strict doubleLoopStr
the carrier of (K) is non empty set
V is Element of the carrier of (K)
W is right_complementable Element of the carrier of K
f is right_complementable Element of the carrier of K
W + f is right_complementable Element of the carrier of K
the addF of K . (W,f) is right_complementable Element of the carrier of K
J is Element of the carrier of (K)
V + J is Element of the carrier of (K)
the addF of (K) is non empty Relation-like [: the carrier of (K), the carrier of (K):] -defined the carrier of (K) -valued Function-like V17([: 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 non empty set
[:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
bool [:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
the addF of (K) . (V,J) is Element of the carrier of (K)
0. (K) is V46((K)) Element of the carrier of (K)
the ZeroF of (K) is Element of the carrier of (K)
K is non empty associative doubleLoopStr
(K) is non empty strict doubleLoopStr
the carrier of K is non empty set
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is Element of the carrier of K
the OneF of K is Element of the carrier of K
0. K is V46(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty strict doubleLoopStr
the carrier of (K) is non empty set
V is Element of the carrier of (K)
W is Element of the carrier of (K)
V * W is Element of the carrier of (K)
the multF of (K) is non empty Relation-like [: the carrier of (K), the carrier of (K):] -defined the carrier of (K) -valued Function-like V17([: 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 non empty set
[:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
bool [:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
the multF of (K) . (V,W) is Element of the carrier of (K)
f is Element of the carrier of (K)
(V * W) * f is Element of the carrier of (K)
the multF of (K) . ((V * W),f) is Element of the carrier of (K)
W * f is Element of the carrier of (K)
the multF of (K) . (W,f) is Element of the carrier of (K)
V * (W * f) is Element of the carrier of (K)
the multF of (K) . (V,(W * f)) is Element of the carrier of (K)
x is Element of the carrier of K
a is Element of the carrier of K
J is Element of the carrier of K
a * J is Element of the carrier of K
the multF of K . (a,J) is Element of the carrier of K
x * (a * J) is Element of the carrier of K
the multF of K . (x,(a * J)) is Element of the carrier of K
x * a is Element of the carrier of K
the multF of K . (x,a) is Element of the carrier of K
(x * a) * J is Element of the carrier of K
the multF of K . ((x * a),J) is Element of the carrier of K
K is non empty right-distributive left-distributive distributive doubleLoopStr
(K) is non empty strict doubleLoopStr
the carrier of K is non empty set
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is Element of the carrier of K
the OneF of K is Element of the carrier of K
0. K is V46(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty strict doubleLoopStr
the carrier of (K) is non empty set
V is Element of the carrier of (K)
W is Element of the carrier of (K)
f is Element of the carrier of (K)
W + f is Element of the carrier of (K)
the addF of (K) is non empty Relation-like [: the carrier of (K), the carrier of (K):] -defined the carrier of (K) -valued Function-like V17([: 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 non empty set
[:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
bool [:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
the addF of (K) . (W,f) is Element of the carrier of (K)
V * (W + f) is Element of the carrier of (K)
the multF of (K) is non empty Relation-like [: the carrier of (K), the carrier of (K):] -defined the carrier of (K) -valued Function-like V17([: the carrier of (K), the carrier of (K):]) quasi_total Element of bool [:[: the carrier of (K), the carrier of (K):], the carrier of (K):]
the multF of (K) . (V,(W + f)) is Element of the carrier of (K)
V * W is Element of the carrier of (K)
the multF of (K) . (V,W) is Element of the carrier of (K)
V * f is Element of the carrier of (K)
the multF of (K) . (V,f) is Element of the carrier of (K)
(V * W) + (V * f) is Element of the carrier of (K)
the addF of (K) . ((V * W),(V * f)) is Element of the carrier of (K)
(W + f) * V is Element of the carrier of (K)
the multF of (K) . ((W + f),V) is Element of the carrier of (K)
W * V is Element of the carrier of (K)
the multF of (K) . (W,V) is Element of the carrier of (K)
f * V is Element of the carrier of (K)
the multF of (K) . (f,V) is Element of the carrier of (K)
(W * V) + (f * V) is Element of the carrier of (K)
the addF of (K) . ((W * V),(f * V)) is Element of the carrier of (K)
a is Element of the carrier of K
x is Element of the carrier of K
a + x is Element of the carrier of K
the addF of K . (a,x) is Element of the carrier of K
J is Element of the carrier of K
(a + x) * J is Element of the carrier of K
the multF of K . ((a + x),J) is Element of the carrier of K
a * J is Element of the carrier of K
the multF of K . (a,J) is Element of the carrier of K
x * J is Element of the carrier of K
the multF of K . (x,J) is Element of the carrier of K
(a * J) + (x * J) is Element of the carrier of K
the addF of K . ((a * J),(x * J)) is Element of the carrier of K
J * (a + x) is Element of the carrier of K
the multF of K . (J,(a + x)) is Element of the carrier of K
J * a is Element of the carrier of K
the multF of K . (J,a) is Element of the carrier of K
J * x is Element of the carrier of K
the multF of K . (J,x) is Element of the carrier of K
(J * a) + (J * x) is Element of the carrier of K
the addF of K . ((J * a),(J * x)) is Element of the carrier of K
K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
(K) is non empty right_complementable strict unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of K is non empty set
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is right_complementable Element of the carrier of K
the OneF of K is right_complementable Element of the carrier of K
0. K is V46(K) right_complementable Element of the carrier of K
the ZeroF of K is right_complementable Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty strict doubleLoopStr
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
(K) is non empty right_complementable strict unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of K is non empty non trivial set
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is V46(K) right_complementable Element of the carrier of K
the OneF of K is right_complementable Element of the carrier of K
0. K is V46(K) right_complementable Element of the carrier of K
the ZeroF of K is right_complementable Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty non trivial strict doubleLoopStr
the carrier of (K) is non empty set
0. (K) is V46((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 right_complementable Element of the carrier of (K)
the OneF of (K) is right_complementable Element of the carrier of (K)
W is right_complementable Element of the carrier of (K)
f is right_complementable Element of the carrier of K
1_ K is right_complementable Element of the carrier of K
J is right_complementable Element of the carrier of K
f * J is right_complementable Element of the carrier of K
the multF of K . (f,J) is right_complementable Element of the carrier of K
a is right_complementable Element of the carrier of (K)
a * W is right_complementable Element of the carrier of (K)
the multF of (K) is non empty Relation-like [: the carrier of (K), the carrier of (K):] -defined the carrier of (K) -valued Function-like V17([: 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 non empty set
[:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
bool [:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
the multF of (K) . (a,W) is right_complementable Element of the carrier of (K)
f is right_complementable Element of the carrier of (K)
f * W is right_complementable Element of the carrier of (K)
the multF of (K) is non empty Relation-like [: the carrier of (K), the carrier of (K):] -defined the carrier of (K) -valued Function-like V17([: 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 non empty set
[:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
bool [:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
the multF of (K) . (f,W) is right_complementable Element of the carrier of (K)
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
(K) is non empty right_complementable strict unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of K is non empty non trivial set
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is V46(K) right_complementable Element of the carrier of K
the OneF of K is right_complementable Element of the carrier of K
0. K is V46(K) right_complementable Element of the carrier of K
the ZeroF of K is right_complementable Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty non trivial strict doubleLoopStr
K is non empty commutative doubleLoopStr
the carrier of K is non empty set
V is Element of the carrier of K
W is Element of the carrier of K
V * W is Element of the carrier of K
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K . (V,W) is Element of the carrier of K
W * V is Element of the carrier of K
the multF of K . (W,V) is Element of the carrier of K
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
(K) is non empty non degenerated non trivial right_complementable almost_left_invertible strict unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of K is non empty non trivial set
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is V46(K) right_complementable Element of the carrier of K
the OneF of K is right_complementable Element of the carrier of K
0. K is V46(K) right_complementable Element of the carrier of K
the ZeroF of K is right_complementable Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty non trivial strict doubleLoopStr
the carrier of (K) is non empty non trivial set
W is right_complementable Element of the carrier of (K)
f is right_complementable Element of the carrier of (K)
W * f is right_complementable Element of the carrier of (K)
the multF of (K) is non empty Relation-like [: the carrier of (K), the carrier of (K):] -defined the carrier of (K) -valued Function-like V17([: 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 non empty set
[:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
bool [:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
the multF of (K) . (W,f) is right_complementable Element of the carrier of (K)
f * W is right_complementable Element of the carrier of (K)
the multF of (K) . (f,W) is right_complementable Element of the carrier of (K)
a is right_complementable Element of the carrier of K
J is right_complementable Element of the carrier of K
a * J is right_complementable Element of the carrier of K
the multF of K . (a,J) is right_complementable Element of the carrier of K
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
(K) is non empty non degenerated non trivial right_complementable almost_left_invertible strict unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of K is non empty non trivial set
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is V46(K) right_complementable Element of the carrier of K
the OneF of K is right_complementable Element of the carrier of K
0. K is V46(K) right_complementable Element of the carrier of K
the ZeroF of K is right_complementable Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty non trivial strict doubleLoopStr
K is non empty doubleLoopStr
(K) is non empty strict doubleLoopStr
the carrier of K is non empty set
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is Element of the carrier of K
the OneF of K is Element of the carrier of K
0. K is V46(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty strict doubleLoopStr
V is non empty VectSpStr over K
the carrier of V is non empty set
the carrier of (K) is non empty set
[: the carrier of V, the carrier of (K):] is non empty set
[:[: the carrier of V, the carrier of (K):], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of (K):], the carrier of V:] is non empty set
[: the carrier of V, the carrier of K:] is non empty set
the lmult of V is non empty Relation-like [: the carrier of K, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set
( the carrier of K, the carrier of V, the carrier of V, the lmult of V) is non empty Relation-like [: the carrier of V, the carrier of K:] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of K:]) quasi_total Element of bool [:[: the carrier of V, the carrier of K:], the carrier of V:]
[:[: the carrier of V, the carrier of K:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of K:], the carrier of V:] is non empty set
the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
0. V is V46(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
W is non empty Relation-like [: the carrier of V, the carrier of (K):] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of (K):]) quasi_total Element of bool [:[: the carrier of V, the carrier of (K):], the carrier of V:]
RightModStr(# the carrier of V, the addF of V,(0. V),W #) is non empty strict RightModStr over (K)
f is non empty Relation-like [: the carrier of V, the carrier of (K):] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of (K):]) quasi_total Element of bool [:[: the carrier of V, the carrier of (K):], the carrier of V:]
RightModStr(# the carrier of V, the addF of V,(0. V),f #) is non empty strict RightModStr over (K)
f is strict RightModStr over (K)
J is strict RightModStr over (K)
W is non empty Relation-like [: the carrier of V, the carrier of (K):] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of (K):]) quasi_total Element of bool [:[: the carrier of V, the carrier of (K):], the carrier of V:]
RightModStr(# the carrier of V, the addF of V,(0. V),W #) is non empty strict RightModStr over (K)
K is non empty doubleLoopStr
V is non empty VectSpStr over K
(K,V) is strict RightModStr over (K)
(K) is non empty strict doubleLoopStr
the carrier of K is non empty set
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is Element of the carrier of K
the OneF of K is Element of the carrier of K
0. K is V46(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty strict doubleLoopStr
the carrier of V is non empty set
the carrier of (K) is non empty set
[: the carrier of V, the carrier of (K):] is non empty set
[:[: the carrier of V, the carrier of (K):], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of (K):], the carrier of V:] is non empty set
the lmult of V is non empty Relation-like [: the carrier of K, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set
( the carrier of K, the carrier of V, the carrier of V, the lmult of V) is non empty Relation-like [: the carrier of V, the carrier of K:] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of K:]) quasi_total Element of bool [:[: the carrier of V, the carrier of K:], the carrier of V:]
[: the carrier of V, the carrier of K:] is non empty set
[:[: the carrier of V, the carrier of K:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of K:], the carrier of V:] is non empty set
the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
0. V is V46(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
W is non empty Relation-like [: the carrier of V, the carrier of (K):] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of (K):]) quasi_total Element of bool [:[: the carrier of V, the carrier of (K):], the carrier of V:]
RightModStr(# the carrier of V, the addF of V,(0. V),W #) is non empty strict RightModStr over (K)
the carrier of (K,V) is set
K is non empty doubleLoopStr
V is non empty VectSpStr over K
(K,V) is non empty strict RightModStr over (K)
(K) is non empty strict doubleLoopStr
the carrier of K is non empty set
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is Element of the carrier of K
the OneF of K is Element of the carrier of K
0. K is V46(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty strict doubleLoopStr
the carrier of (K,V) is non empty set
the addF of (K,V) is non empty Relation-like [: the carrier of (K,V), the carrier of (K,V):] -defined the carrier of (K,V) -valued Function-like V17([: the carrier of (K,V), the carrier of (K,V):]) quasi_total Element of bool [:[: the carrier of (K,V), the carrier of (K,V):], the carrier of (K,V):]
[: the carrier of (K,V), the carrier of (K,V):] is non empty set
[:[: the carrier of (K,V), the carrier of (K,V):], the carrier of (K,V):] is non empty set
bool [:[: the carrier of (K,V), the carrier of (K,V):], the carrier of (K,V):] is non empty set
the ZeroF of (K,V) is Element of the carrier of (K,V)
addLoopStr(# the carrier of (K,V), the addF of (K,V), the ZeroF of (K,V) #) is non empty strict addLoopStr
the carrier of V is non empty set
the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the ZeroF of V is Element of the carrier of V
addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) is non empty strict addLoopStr
the carrier of (K) is non empty set
[: the carrier of V, the carrier of (K):] is non empty set
[:[: the carrier of V, the carrier of (K):], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of (K):], the carrier of V:] is non empty set
the lmult of V is non empty Relation-like [: the carrier of K, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set
( the carrier of K, the carrier of V, the carrier of V, the lmult of V) is non empty Relation-like [: the carrier of V, the carrier of K:] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of K:]) quasi_total Element of bool [:[: the carrier of V, the carrier of K:], the carrier of V:]
[: the carrier of V, the carrier of K:] is non empty set
[:[: the carrier of V, the carrier of K:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of K:], the carrier of V:] is non empty set
0. V is V46(V) Element of the carrier of V
W is non empty Relation-like [: the carrier of V, the carrier of (K):] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of (K):]) quasi_total Element of bool [:[: the carrier of V, the carrier of (K):], the carrier of V:]
RightModStr(# the carrier of V, the addF of V,(0. V),W #) is non empty strict RightModStr over (K)
f is set
K is non empty doubleLoopStr
the carrier of K is non empty set
V is non empty VectSpStr over K
the carrier of V is non empty set
[: the carrier of K, the carrier of V:] is non empty set
[:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set
W is non empty Relation-like [: the carrier of K, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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, the carrier of V,W) is non empty Relation-like [: the carrier of V, the carrier of K:] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of K:]) quasi_total Element of bool [:[: the carrier of V, the carrier of K:], the carrier of V:]
[: the carrier of V, the carrier of K:] is non empty set
[:[: the carrier of V, the carrier of K:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of K:], the carrier of V:] is non empty set
(K,V) is non empty strict RightModStr over (K)
(K) is non empty strict doubleLoopStr
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is Element of the carrier of K
the OneF of K is Element of the carrier of K
0. K is V46(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty strict doubleLoopStr
the carrier of (K,V) is non empty set
the carrier of (K) is non empty set
[: the carrier of (K,V), the carrier of (K):] is non empty set
[:[: the carrier of (K,V), the carrier of (K):], the carrier of (K,V):] is non empty set
bool [:[: the carrier of (K,V), the carrier of (K):], the carrier of (K,V):] is non empty set
the addF of (K,V) is non empty Relation-like [: the carrier of (K,V), the carrier of (K,V):] -defined the carrier of (K,V) -valued Function-like V17([: the carrier of (K,V), the carrier of (K,V):]) quasi_total Element of bool [:[: the carrier of (K,V), the carrier of (K,V):], the carrier of (K,V):]
[: the carrier of (K,V), the carrier of (K,V):] is non empty set
[:[: the carrier of (K,V), the carrier of (K,V):], the carrier of (K,V):] is non empty set
bool [:[: the carrier of (K,V), the carrier of (K,V):], the carrier of (K,V):] is non empty set
the ZeroF of (K,V) is Element of the carrier of (K,V)
addLoopStr(# the carrier of (K,V), the addF of (K,V), the ZeroF of (K,V) #) is non empty strict addLoopStr
the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the ZeroF of V is Element of the carrier of V
addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) is non empty strict addLoopStr
K is non empty doubleLoopStr
(K) is non empty strict doubleLoopStr
the carrier of K is non empty set
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is Element of the carrier of K
the OneF of K is Element of the carrier of K
0. K is V46(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty strict doubleLoopStr
the carrier of (K) is non empty set
V is non empty VectSpStr over K
(K,V) is non empty strict RightModStr over (K)
the carrier of (K,V) is non empty set
the rmult of (K,V) is non empty Relation-like [: the carrier of (K,V), the carrier of (K):] -defined the carrier of (K,V) -valued Function-like V17([: the carrier of (K,V), the carrier of (K):]) quasi_total Element of bool [:[: the carrier of (K,V), the carrier of (K):], the carrier of (K,V):]
[: the carrier of (K,V), the carrier of (K):] is non empty set
[:[: the carrier of (K,V), the carrier of (K):], the carrier of (K,V):] is non empty set
bool [:[: the carrier of (K,V), the carrier of (K):], the carrier of (K,V):] is non empty set
the lmult of V is non empty Relation-like [: the carrier of K, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 V is non empty set
[: the carrier of K, the carrier of V:] is non empty set
[:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set
(K,V, the lmult of V) is non empty Relation-like [: the carrier of (K,V), the carrier of (K):] -defined the carrier of (K,V) -valued Function-like V17([: the carrier of (K,V), the carrier of (K):]) quasi_total Element of bool [:[: the carrier of (K,V), the carrier of (K):], the carrier of (K,V):]
( the carrier of K, the carrier of V, the carrier of V, the lmult of V) is non empty Relation-like [: the carrier of V, the carrier of K:] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of K:]) quasi_total Element of bool [:[: the carrier of V, the carrier of K:], the carrier of V:]
[: the carrier of V, the carrier of K:] is non empty set
[:[: the carrier of V, the carrier of K:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of K:], the carrier of V:] is non empty set
[: the carrier of V, the carrier of (K):] is non empty set
[:[: the carrier of V, the carrier of (K):], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of (K):], the carrier of V:] is non empty set
the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
0. V is V46(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
W is non empty Relation-like [: the carrier of V, the carrier of (K):] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of (K):]) quasi_total Element of bool [:[: the carrier of V, the carrier of (K):], the carrier of V:]
RightModStr(# the carrier of V, the addF of V,(0. V),W #) is non empty strict RightModStr over (K)
K is non empty doubleLoopStr
(K) is non empty strict doubleLoopStr
the carrier of K is non empty set
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is Element of the carrier of K
the OneF of K is Element of the carrier of K
0. K is V46(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty strict doubleLoopStr
the carrier of (K) is non empty set
V is non empty RightModStr over K
the carrier of V is non empty set
[: the carrier of (K), the carrier of V:] is non empty set
[:[: the carrier of (K), the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of (K), the carrier of V:], the carrier of V:] is non empty set
[: the carrier of K, the carrier of V:] is non empty set
the rmult of V is non empty Relation-like [: the carrier of V, the carrier of K:] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of K:]) quasi_total Element of bool [:[: the carrier of V, the carrier of K:], the carrier of V:]
[: the carrier of V, the carrier of K:] is non empty set
[:[: the carrier of V, the carrier of K:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of K:], the carrier of V:] is non empty set
( the carrier of V, the carrier of K, the carrier of V, the rmult of V) is non empty Relation-like [: the carrier of K, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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:], the carrier of V:] is non empty set
bool [:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set
the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
0. V is V46(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
W is non empty Relation-like [: the carrier of (K), the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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:]
VectSpStr(# the carrier of V, the addF of V,(0. V),W #) is non empty strict VectSpStr over (K)
f is non empty Relation-like [: the carrier of (K), the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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:]
VectSpStr(# the carrier of V, the addF of V,(0. V),f #) is non empty strict VectSpStr over (K)
f is strict VectSpStr over (K)
J is strict VectSpStr over (K)
W is non empty Relation-like [: the carrier of (K), the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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:]
VectSpStr(# the carrier of V, the addF of V,(0. V),W #) is non empty strict VectSpStr over (K)
K is non empty doubleLoopStr
V is non empty RightModStr over K
(K,V) is strict VectSpStr over (K)
(K) is non empty strict doubleLoopStr
the carrier of K is non empty set
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is Element of the carrier of K
the OneF of K is Element of the carrier of K
0. K is V46(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty strict doubleLoopStr
the carrier of (K) is non empty set
the carrier of V is non empty set
[: the carrier of (K), the carrier of V:] is non empty set
[:[: the carrier of (K), the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of (K), the carrier of V:], the carrier of V:] is non empty set
the rmult of V is non empty Relation-like [: the carrier of V, the carrier of K:] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of K:]) quasi_total Element of bool [:[: the carrier of V, the carrier of K:], the carrier of V:]
[: the carrier of V, the carrier of K:] is non empty set
[:[: the carrier of V, the carrier of K:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of K:], the carrier of V:] is non empty set
( the carrier of V, the carrier of K, the carrier of V, the rmult of V) is non empty Relation-like [: the carrier of K, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set
the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
0. V is V46(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
W is non empty Relation-like [: the carrier of (K), the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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:]
VectSpStr(# the carrier of V, the addF of V,(0. V),W #) is non empty strict VectSpStr over (K)
the carrier of (K,V) is set
K is non empty doubleLoopStr
V is non empty RightModStr over K
(K,V) is non empty strict VectSpStr over (K)
(K) is non empty strict doubleLoopStr
the carrier of K is non empty set
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is Element of the carrier of K
the OneF of K is Element of the carrier of K
0. K is V46(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty strict doubleLoopStr
the carrier of (K,V) is non empty set
the addF of (K,V) is non empty Relation-like [: the carrier of (K,V), the carrier of (K,V):] -defined the carrier of (K,V) -valued Function-like V17([: the carrier of (K,V), the carrier of (K,V):]) quasi_total Element of bool [:[: the carrier of (K,V), the carrier of (K,V):], the carrier of (K,V):]
[: the carrier of (K,V), the carrier of (K,V):] is non empty set
[:[: the carrier of (K,V), the carrier of (K,V):], the carrier of (K,V):] is non empty set
bool [:[: the carrier of (K,V), the carrier of (K,V):], the carrier of (K,V):] is non empty set
the ZeroF of (K,V) is Element of the carrier of (K,V)
addLoopStr(# the carrier of (K,V), the addF of (K,V), the ZeroF of (K,V) #) is non empty strict addLoopStr
the carrier of V is non empty set
the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the ZeroF of V is Element of the carrier of V
addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) is non empty strict addLoopStr
the carrier of (K) is non empty set
[: the carrier of (K), the carrier of V:] is non empty set
[:[: the carrier of (K), the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of (K), the carrier of V:], the carrier of V:] is non empty set
the rmult of V is non empty Relation-like [: the carrier of V, the carrier of K:] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of K:]) quasi_total Element of bool [:[: the carrier of V, the carrier of K:], the carrier of V:]
[: the carrier of V, the carrier of K:] is non empty set
[:[: the carrier of V, the carrier of K:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of K:], the carrier of V:] is non empty set
( the carrier of V, the carrier of K, the carrier of V, the rmult of V) is non empty Relation-like [: the carrier of K, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set
0. V is V46(V) Element of the carrier of V
W is non empty Relation-like [: the carrier of (K), the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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:]
VectSpStr(# the carrier of V, the addF of V,(0. V),W #) is non empty strict VectSpStr over (K)
f is set
K is non empty doubleLoopStr
V is non empty RightModStr over K
the carrier of V is non empty set
the carrier of K is non empty set
[: the carrier of V, the carrier of K:] is non empty set
[:[: the carrier of V, the carrier of K:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of K:], the carrier of V:] is non empty set
W is non empty Relation-like [: the carrier of V, the carrier of K:] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of K:]) quasi_total Element of bool [:[: the carrier of V, the carrier of K:], the carrier of V:]
( the carrier of V, the carrier of K, the carrier of V,W) is non empty Relation-like [: the carrier of K, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set
(K) is non empty strict doubleLoopStr
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is Element of the carrier of K
the OneF of K is Element of the carrier of K
0. K is V46(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty strict doubleLoopStr
the carrier of (K) is non empty set
(K,V) is non empty strict VectSpStr over (K)
the carrier of (K,V) is non empty set
[: the carrier of (K), the carrier of (K,V):] is non empty set
[:[: the carrier of (K), the carrier of (K,V):], the carrier of (K,V):] is non empty set
bool [:[: the carrier of (K), the carrier of (K,V):], the carrier of (K,V):] is non empty set
the addF of (K,V) is non empty Relation-like [: the carrier of (K,V), the carrier of (K,V):] -defined the carrier of (K,V) -valued Function-like V17([: the carrier of (K,V), the carrier of (K,V):]) quasi_total Element of bool [:[: the carrier of (K,V), the carrier of (K,V):], the carrier of (K,V):]
[: the carrier of (K,V), the carrier of (K,V):] is non empty set
[:[: the carrier of (K,V), the carrier of (K,V):], the carrier of (K,V):] is non empty set
bool [:[: the carrier of (K,V), the carrier of (K,V):], the carrier of (K,V):] is non empty set
the ZeroF of (K,V) is Element of the carrier of (K,V)
addLoopStr(# the carrier of (K,V), the addF of (K,V), the ZeroF of (K,V) #) is non empty strict addLoopStr
the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the ZeroF of V is Element of the carrier of V
addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) is non empty strict addLoopStr
f is non empty Relation-like [: the carrier of (K), the carrier of (K,V):] -defined the carrier of (K,V) -valued Function-like V17([: the carrier of (K), the carrier of (K,V):]) quasi_total Element of bool [:[: the carrier of (K), the carrier of (K,V):], the carrier of (K,V):]
K is non empty doubleLoopStr
(K) is non empty strict doubleLoopStr
the carrier of K is non empty set
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is Element of the carrier of K
the OneF of K is Element of the carrier of K
0. K is V46(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty strict doubleLoopStr
the carrier of (K) is non empty set
V is non empty RightModStr over K
(K,V) is non empty strict VectSpStr over (K)
the carrier of (K,V) is non empty set
the lmult of (K,V) is non empty Relation-like [: the carrier of (K), the carrier of (K,V):] -defined the carrier of (K,V) -valued Function-like V17([: the carrier of (K), the carrier of (K,V):]) quasi_total Element of bool [:[: the carrier of (K), the carrier of (K,V):], the carrier of (K,V):]
[: the carrier of (K), the carrier of (K,V):] is non empty set
[:[: the carrier of (K), the carrier of (K,V):], the carrier of (K,V):] is non empty set
bool [:[: the carrier of (K), the carrier of (K,V):], the carrier of (K,V):] is non empty set
the rmult of V is non empty Relation-like [: the carrier of V, the carrier of K:] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of K:]) quasi_total Element of bool [:[: the carrier of V, the carrier of K:], the carrier of V:]
the carrier of V is non empty set
[: the carrier of V, the carrier of K:] is non empty set
[:[: the carrier of V, the carrier of K:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of K:], the carrier of V:] is non empty set
(K,V, the rmult of V) is non empty Relation-like [: the carrier of (K), the carrier of (K,V):] -defined the carrier of (K,V) -valued Function-like V17([: the carrier of (K), the carrier of (K,V):]) quasi_total Element of bool [:[: the carrier of (K), the carrier of (K,V):], the carrier of (K,V):]
( the carrier of V, the carrier of K, the carrier of V, the rmult of V) is non empty Relation-like [: the carrier of K, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set
[: the carrier of (K), the carrier of V:] is non empty set
[:[: the carrier of (K), the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of (K), the carrier of V:], the carrier of V:] is non empty set
the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
0. V is V46(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
W is non empty Relation-like [: the carrier of (K), the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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:]
VectSpStr(# the carrier of V, the addF of V,(0. V),W #) is non empty strict VectSpStr over (K)
K is non empty doubleLoopStr
the carrier of K is non empty set
V is non empty VectSpStr over K
the carrier of V is non empty set
[: the carrier of K, the carrier of V:] is non empty set
[:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set
(K) is non empty strict doubleLoopStr
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is Element of the carrier of K
the OneF of K is Element of the carrier of K
0. K is V46(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty strict doubleLoopStr
the carrier of (K) is non empty set
(K,V) is non empty strict RightModStr over (K)
the carrier of (K,V) is non empty set
f is Element of the carrier of K
J is Element of the carrier of (K)
a is Element of the carrier of V
x is Element of the carrier of (K,V)
W is non empty Relation-like [: the carrier of K, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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:]
(K,V,W) is non empty Relation-like [: the carrier of (K,V), the carrier of (K):] -defined the carrier of (K,V) -valued Function-like V17([: the carrier of (K,V), the carrier of (K):]) quasi_total Element of bool [:[: the carrier of (K,V), the carrier of (K):], the carrier of (K,V):]
[: the carrier of (K,V), the carrier of (K):] is non empty set
[:[: the carrier of (K,V), the carrier of (K):], the carrier of (K,V):] is non empty set
bool [:[: the carrier of (K,V), the carrier of (K):], the carrier of (K,V):] is non empty set
( the carrier of K, the carrier of V, the carrier of V,W) is non empty Relation-like [: the carrier of V, the carrier of K:] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of K:]) quasi_total Element of bool [:[: the carrier of V, the carrier of K:], the carrier of V:]
[: the carrier of V, the carrier of K:] is non empty set
[:[: the carrier of V, the carrier of K:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of K:], the carrier of V:] is non empty set
(K,V,W) . (x,J) is Element of the carrier of (K,V)
W . (f,a) is Element of the carrier of V
K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of K is non empty set
the carrier of V is non empty set
(K) is non empty right_complementable strict unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is right_complementable Element of the carrier of K
the OneF of K is right_complementable Element of the carrier of K
0. K is V46(K) right_complementable Element of the carrier of K
the ZeroF of K is right_complementable Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty strict doubleLoopStr
W is non empty VectSpStr over K
the carrier of W is non empty set
(K,W) is non empty strict RightModStr over (K)
f is non empty RightModStr over V
the carrier of f is non empty set
J is right_complementable Element of the carrier of K
a is right_complementable Element of the carrier of V
x is Element of the carrier of W
J * x is Element of the carrier of W
the lmult of W is non empty Relation-like [: the carrier of K, the carrier of W:] -defined the carrier of W -valued Function-like V17([: the carrier of K, the carrier of W:]) quasi_total Element of bool [:[: the carrier of K, the carrier of W:], the carrier of W:]
[: the carrier of K, the carrier of W:] is non empty set
[:[: the carrier of K, the carrier of W:], the carrier of W:] is non empty set
bool [:[: the carrier of K, the carrier of W:], the carrier of W:] is non empty set
the lmult of W . (J,x) is Element of the carrier of W
z is Element of the carrier of f
z * a is Element of the carrier of f
the carrier of (K,W) is non empty set
the carrier of (K) is non empty set
(K,W, the lmult of W) is non empty Relation-like [: the carrier of (K,W), the carrier of (K):] -defined the carrier of (K,W) -valued Function-like V17([: the carrier of (K,W), the carrier of (K):]) quasi_total Element of bool [:[: the carrier of (K,W), the carrier of (K):], the carrier of (K,W):]
[: the carrier of (K,W), the carrier of (K):] is non empty set
[:[: the carrier of (K,W), the carrier of (K):], the carrier of (K,W):] is non empty set
bool [:[: the carrier of (K,W), the carrier of (K):], the carrier of (K,W):] is non empty set
( the carrier of K, the carrier of W, the carrier of W, the lmult of W) is non empty Relation-like [: the carrier of W, the carrier of K:] -defined the carrier of W -valued Function-like V17([: the carrier of W, the carrier of K:]) quasi_total Element of bool [:[: the carrier of W, the carrier of K:], the carrier of W:]
[: the carrier of W, the carrier of K:] is non empty set
[:[: the carrier of W, the carrier of K:], the carrier of W:] is non empty set
bool [:[: the carrier of W, the carrier of K:], the carrier of W:] is non empty set
the rmult of (K,W) is non empty Relation-like [: the carrier of (K,W), the carrier of (K):] -defined the carrier of (K,W) -valued Function-like V17([: the carrier of (K,W), the carrier of (K):]) quasi_total Element of bool [:[: the carrier of (K,W), the carrier of (K):], the carrier of (K,W):]
(K,W, the lmult of W) . (z,a) is set
K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
W is non empty VectSpStr over K
the carrier of W is non empty set
(K,W) is non empty strict RightModStr over (K)
(K) is non empty right_complementable strict unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of K is non empty set
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is right_complementable Element of the carrier of K
the OneF of K is right_complementable Element of the carrier of K
0. K is V46(K) right_complementable Element of the carrier of K
the ZeroF of K is right_complementable Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty strict doubleLoopStr
the carrier of (K,W) is non empty set
the addF of (K,W) is non empty Relation-like [: the carrier of (K,W), the carrier of (K,W):] -defined the carrier of (K,W) -valued Function-like V17([: the carrier of (K,W), the carrier of (K,W):]) quasi_total Element of bool [:[: the carrier of (K,W), the carrier of (K,W):], the carrier of (K,W):]
[: the carrier of (K,W), the carrier of (K,W):] is non empty set
[:[: the carrier of (K,W), the carrier of (K,W):], the carrier of (K,W):] is non empty set
bool [:[: the carrier of (K,W), the carrier of (K,W):], the carrier of (K,W):] is non empty set
the ZeroF of (K,W) is Element of the carrier of (K,W)
addLoopStr(# the carrier of (K,W), the addF of (K,W), the ZeroF of (K,W) #) is non empty strict addLoopStr
the addF of W is non empty Relation-like [: the carrier of W, the carrier of W:] -defined the carrier of W -valued Function-like V17([: 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 non empty set
[:[: the carrier of W, the carrier of W:], the carrier of W:] is non empty set
bool [:[: the carrier of W, the carrier of W:], the carrier of W:] is non empty set
the ZeroF of W is Element of the carrier of W
addLoopStr(# the carrier of W, the addF of W, the ZeroF of W #) is non empty strict addLoopStr
f is non empty RightModStr over V
the carrier of f is non empty set
J is Element of the carrier of W
a is Element of the carrier of W
J + a is Element of the carrier of W
the addF of W . (J,a) is Element of the carrier of W
x is Element of the carrier of f
z is Element of the carrier of f
x + z is Element of the carrier of f
the addF of f is non empty Relation-like [: the carrier of f, the carrier of f:] -defined the carrier of f -valued Function-like V17([: 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 non empty set
[:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
bool [:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
the addF of f . (x,z) is Element of the carrier of f
K is non empty doubleLoopStr
V is non empty RightModStr over K
the carrier of V is non empty set
the carrier of K is non empty set
[: the carrier of V, the carrier of K:] is non empty set
[:[: the carrier of V, the carrier of K:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of K:], the carrier of V:] is non empty set
(K) is non empty strict doubleLoopStr
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is Element of the carrier of K
the OneF of K is Element of the carrier of K
0. K is V46(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty strict doubleLoopStr
the carrier of (K) is non empty set
(K,V) is non empty strict VectSpStr over (K)
the carrier of (K,V) is non empty set
f is Element of the carrier of K
J is Element of the carrier of (K)
a is Element of the carrier of V
x is Element of the carrier of (K,V)
W is non empty Relation-like [: the carrier of V, the carrier of K:] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of K:]) quasi_total Element of bool [:[: the carrier of V, the carrier of K:], the carrier of V:]
(K,V,W) is non empty Relation-like [: the carrier of (K), the carrier of (K,V):] -defined the carrier of (K,V) -valued Function-like V17([: the carrier of (K), the carrier of (K,V):]) quasi_total Element of bool [:[: the carrier of (K), the carrier of (K,V):], the carrier of (K,V):]
[: the carrier of (K), the carrier of (K,V):] is non empty set
[:[: the carrier of (K), the carrier of (K,V):], the carrier of (K,V):] is non empty set
bool [:[: the carrier of (K), the carrier of (K,V):], the carrier of (K,V):] is non empty set
( the carrier of V, the carrier of K, the carrier of V,W) is non empty Relation-like [: the carrier of K, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set
(K,V,W) . (J,x) is Element of the carrier of (K,V)
W . (a,f) is Element of the carrier of V
K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of K is non empty set
the carrier of V is non empty set
W is non empty VectSpStr over K
the carrier of W is non empty set
f is non empty RightModStr over V
the carrier of f is non empty set
(V,f) is non empty strict VectSpStr over (V)
(V) is non empty right_complementable strict unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the multF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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, the multF of V) is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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:]
1. V is right_complementable Element of the carrier of V
the OneF of V is right_complementable Element of the carrier of V
0. V is V46(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
doubleLoopStr(# the carrier of V, the addF of V,( the carrier of V, the carrier of V, the carrier of V, the multF of V),(1. V),(0. V) #) is non empty strict doubleLoopStr
J is right_complementable Element of the carrier of K
a is right_complementable Element of the carrier of V
x is Element of the carrier of W
J * x is Element of the carrier of W
the lmult of W is non empty Relation-like [: the carrier of K, the carrier of W:] -defined the carrier of W -valued Function-like V17([: the carrier of K, the carrier of W:]) quasi_total Element of bool [:[: the carrier of K, the carrier of W:], the carrier of W:]
[: the carrier of K, the carrier of W:] is non empty set
[:[: the carrier of K, the carrier of W:], the carrier of W:] is non empty set
bool [:[: the carrier of K, the carrier of W:], the carrier of W:] is non empty set
the lmult of W . (J,x) is Element of the carrier of W
z is Element of the carrier of f
z * a is Element of the carrier of f
the rmult of f is non empty Relation-like [: the carrier of f, the carrier of V:] -defined the carrier of f -valued Function-like V17([: the carrier of f, the carrier of V:]) quasi_total Element of bool [:[: the carrier of f, the carrier of V:], the carrier of f:]
[: the carrier of f, the carrier of V:] is non empty set
[:[: the carrier of f, the carrier of V:], the carrier of f:] is non empty set
bool [:[: the carrier of f, the carrier of V:], the carrier of f:] is non empty set
the carrier of (V) is non empty set
the carrier of (V,f) is non empty set
(V,f, the rmult of f) is non empty Relation-like [: the carrier of (V), the carrier of (V,f):] -defined the carrier of (V,f) -valued Function-like V17([: the carrier of (V), the carrier of (V,f):]) quasi_total Element of bool [:[: the carrier of (V), the carrier of (V,f):], the carrier of (V,f):]
[: the carrier of (V), the carrier of (V,f):] is non empty set
[:[: the carrier of (V), the carrier of (V,f):], the carrier of (V,f):] is non empty set
bool [:[: the carrier of (V), the carrier of (V,f):], the carrier of (V,f):] is non empty set
( the carrier of f, the carrier of V, the carrier of f, the rmult of f) is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of f -valued Function-like V17([: the carrier of V, the carrier of f:]) quasi_total Element of bool [:[: the carrier of V, the carrier of f:], the carrier of f:]
[: the carrier of V, the carrier of f:] is non empty set
[:[: the carrier of V, the carrier of f:], the carrier of f:] is non empty set
bool [:[: the carrier of V, the carrier of f:], the carrier of f:] is non empty set
the lmult of (V,f) is non empty Relation-like [: the carrier of (V), the carrier of (V,f):] -defined the carrier of (V,f) -valued Function-like V17([: the carrier of (V), the carrier of (V,f):]) quasi_total Element of bool [:[: the carrier of (V), the carrier of (V,f):], the carrier of (V,f):]
the rmult of f . (z,a) is Element of the carrier of f
K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
W is non empty VectSpStr over K
the carrier of W is non empty set
f is non empty RightModStr over V
the carrier of f is non empty set
(V,f) is non empty strict VectSpStr over (V)
(V) is non empty right_complementable strict unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of V is non empty set
the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the multF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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, the multF of V) is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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:]
1. V is right_complementable Element of the carrier of V
the OneF of V is right_complementable Element of the carrier of V
0. V is V46(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
doubleLoopStr(# the carrier of V, the addF of V,( the carrier of V, the carrier of V, the carrier of V, the multF of V),(1. V),(0. V) #) is non empty strict doubleLoopStr
the carrier of (V,f) is non empty set
the addF of (V,f) is non empty Relation-like [: the carrier of (V,f), the carrier of (V,f):] -defined the carrier of (V,f) -valued Function-like V17([: the carrier of (V,f), the carrier of (V,f):]) quasi_total Element of bool [:[: the carrier of (V,f), the carrier of (V,f):], the carrier of (V,f):]
[: the carrier of (V,f), the carrier of (V,f):] is non empty set
[:[: the carrier of (V,f), the carrier of (V,f):], the carrier of (V,f):] is non empty set
bool [:[: the carrier of (V,f), the carrier of (V,f):], the carrier of (V,f):] is non empty set
the ZeroF of (V,f) is Element of the carrier of (V,f)
addLoopStr(# the carrier of (V,f), the addF of (V,f), the ZeroF of (V,f) #) is non empty strict addLoopStr
the addF of f is non empty Relation-like [: the carrier of f, the carrier of f:] -defined the carrier of f -valued Function-like V17([: 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 non empty set
[:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
bool [:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
the ZeroF of f is Element of the carrier of f
addLoopStr(# the carrier of f, the addF of f, the ZeroF of f #) is non empty strict addLoopStr
J is Element of the carrier of W
a is Element of the carrier of W
J + a is Element of the carrier of W
the addF of W is non empty Relation-like [: the carrier of W, the carrier of W:] -defined the carrier of W -valued Function-like V17([: 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 non empty set
[:[: the carrier of W, the carrier of W:], the carrier of W:] is non empty set
bool [:[: the carrier of W, the carrier of W:], the carrier of W:] is non empty set
the addF of W . (J,a) is Element of the carrier of W
x is Element of the carrier of f
z is Element of the carrier of f
x + z is Element of the carrier of f
the addF of f . (x,z) is Element of the carrier of f
K is non empty strict doubleLoopStr
(K) is non empty strict doubleLoopStr
the carrier of K is non empty set
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is Element of the carrier of K
the OneF of K is Element of the carrier of K
0. K is V46(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty strict doubleLoopStr
V is non empty VectSpStr over K
(K,V) is non empty strict RightModStr over (K)
((K),(K,V)) is non empty strict VectSpStr over ((K))
((K)) is non empty strict doubleLoopStr
the carrier of (K) is non empty set
the addF of (K) is non empty Relation-like [: the carrier of (K), the carrier of (K):] -defined the carrier of (K) -valued Function-like V17([: 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 non empty set
[:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
bool [:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
the multF of (K) is non empty Relation-like [: the carrier of (K), the carrier of (K):] -defined the carrier of (K) -valued Function-like V17([: 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), the carrier of (K), the multF of (K)) is non empty Relation-like [: the carrier of (K), the carrier of (K):] -defined the carrier of (K) -valued Function-like V17([: 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):]
1. (K) is Element of the carrier of (K)
the OneF of (K) is Element of the carrier of (K)
0. (K) is V46((K)) Element of the carrier of (K)
the ZeroF of (K) is Element of the carrier of (K)
doubleLoopStr(# the carrier of (K), the addF of (K),( the carrier of (K), the carrier of (K), the carrier of (K), the multF of (K)),(1. (K)),(0. (K)) #) is non empty strict doubleLoopStr
the carrier of V is non empty set
the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the ZeroF of V is Element of the carrier of V
the lmult of V is non empty Relation-like [: the carrier of K, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set
VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is non empty strict VectSpStr over K
the rmult of (K,V) is non empty Relation-like [: the carrier of (K,V), the carrier of (K):] -defined the carrier of (K,V) -valued Function-like V17([: the carrier of (K,V), the carrier of (K):]) quasi_total Element of bool [:[: the carrier of (K,V), the carrier of (K):], the carrier of (K,V):]
the carrier of (K,V) is non empty set
[: the carrier of (K,V), the carrier of (K):] is non empty set
[:[: the carrier of (K,V), the carrier of (K):], the carrier of (K,V):] is non empty set
bool [:[: the carrier of (K,V), the carrier of (K):], the carrier of (K,V):] is non empty set
((K),(K,V), the rmult of (K,V)) is non empty Relation-like [: the carrier of ((K)), the carrier of ((K),(K,V)):] -defined the carrier of ((K),(K,V)) -valued Function-like V17([: the carrier of ((K)), the carrier of ((K),(K,V)):]) quasi_total Element of bool [:[: the carrier of ((K)), the carrier of ((K),(K,V)):], the carrier of ((K),(K,V)):]
the carrier of ((K)) is non empty set
the carrier of ((K),(K,V)) is non empty set
[: the carrier of ((K)), the carrier of ((K),(K,V)):] is non empty set
[:[: the carrier of ((K)), the carrier of ((K),(K,V)):], the carrier of ((K),(K,V)):] is non empty set
bool [:[: the carrier of ((K)), the carrier of ((K),(K,V)):], the carrier of ((K),(K,V)):] is non empty set
( the carrier of (K,V), the carrier of (K), the carrier of (K,V), the rmult of (K,V)) is non empty Relation-like [: the carrier of (K), the carrier of (K,V):] -defined the carrier of (K,V) -valued Function-like V17([: the carrier of (K), the carrier of (K,V):]) quasi_total Element of bool [:[: the carrier of (K), the carrier of (K,V):], the carrier of (K,V):]
[: the carrier of (K), the carrier of (K,V):] is non empty set
[:[: the carrier of (K), the carrier of (K,V):], the carrier of (K,V):] is non empty set
bool [:[: the carrier of (K), the carrier of (K,V):], the carrier of (K,V):] is non empty set
(K,V, the lmult of V) is non empty Relation-like [: the carrier of (K,V), the carrier of (K):] -defined the carrier of (K,V) -valued Function-like V17([: the carrier of (K,V), the carrier of (K):]) quasi_total Element of bool [:[: the carrier of (K,V), the carrier of (K):], the carrier of (K,V):]
( the carrier of K, the carrier of V, the carrier of V, the lmult of V) is non empty Relation-like [: the carrier of V, the carrier of K:] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of K:]) quasi_total Element of bool [:[: the carrier of V, the carrier of K:], the carrier of V:]
[: the carrier of V, the carrier of K:] is non empty set
[:[: the carrier of V, the carrier of K:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of K:], the carrier of V:] is non empty set
((K),(K,V),(K,V, the lmult of V)) is non empty Relation-like [: the carrier of ((K)), the carrier of ((K),(K,V)):] -defined the carrier of ((K),(K,V)) -valued Function-like V17([: the carrier of ((K)), the carrier of ((K),(K,V)):]) quasi_total Element of bool [:[: the carrier of ((K)), the carrier of ((K),(K,V)):], the carrier of ((K),(K,V)):]
( the carrier of (K,V), the carrier of (K), the carrier of (K,V),(K,V, the lmult of V)) is non empty Relation-like [: the carrier of (K), the carrier of (K,V):] -defined the carrier of (K,V) -valued Function-like V17([: the carrier of (K), the carrier of (K,V):]) quasi_total Element of bool [:[: the carrier of (K), the carrier of (K,V):], the carrier of (K,V):]
the addF of ((K),(K,V)) is non empty Relation-like [: the carrier of ((K),(K,V)), the carrier of ((K),(K,V)):] -defined the carrier of ((K),(K,V)) -valued Function-like V17([: the carrier of ((K),(K,V)), the carrier of ((K),(K,V)):]) quasi_total Element of bool [:[: the carrier of ((K),(K,V)), the carrier of ((K),(K,V)):], the carrier of ((K),(K,V)):]
[: the carrier of ((K),(K,V)), the carrier of ((K),(K,V)):] is non empty set
[:[: the carrier of ((K),(K,V)), the carrier of ((K),(K,V)):], the carrier of ((K),(K,V)):] is non empty set
bool [:[: the carrier of ((K),(K,V)), the carrier of ((K),(K,V)):], the carrier of ((K),(K,V)):] is non empty set
the ZeroF of ((K),(K,V)) is Element of the carrier of ((K),(K,V))
addLoopStr(# the carrier of ((K),(K,V)), the addF of ((K),(K,V)), the ZeroF of ((K),(K,V)) #) is non empty strict addLoopStr
the addF of (K,V) is non empty Relation-like [: the carrier of (K,V), the carrier of (K,V):] -defined the carrier of (K,V) -valued Function-like V17([: the carrier of (K,V), the carrier of (K,V):]) quasi_total Element of bool [:[: the carrier of (K,V), the carrier of (K,V):], the carrier of (K,V):]
[: the carrier of (K,V), the carrier of (K,V):] is non empty set
[:[: the carrier of (K,V), the carrier of (K,V):], the carrier of (K,V):] is non empty set
bool [:[: the carrier of (K,V), the carrier of (K,V):], the carrier of (K,V):] is non empty set
the ZeroF of (K,V) is Element of the carrier of (K,V)
addLoopStr(# the carrier of (K,V), the addF of (K,V), the ZeroF of (K,V) #) is non empty strict addLoopStr
addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) is non empty strict addLoopStr
K is non empty strict doubleLoopStr
(K) is non empty strict doubleLoopStr
the carrier of K is non empty set
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is Element of the carrier of K
the OneF of K is Element of the carrier of K
0. K is V46(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty strict doubleLoopStr
V is non empty RightModStr over K
(K,V) is non empty strict VectSpStr over (K)
((K),(K,V)) is non empty strict RightModStr over ((K))
((K)) is non empty strict doubleLoopStr
the carrier of (K) is non empty set
the addF of (K) is non empty Relation-like [: the carrier of (K), the carrier of (K):] -defined the carrier of (K) -valued Function-like V17([: 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 non empty set
[:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
bool [:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
the multF of (K) is non empty Relation-like [: the carrier of (K), the carrier of (K):] -defined the carrier of (K) -valued Function-like V17([: 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), the carrier of (K), the multF of (K)) is non empty Relation-like [: the carrier of (K), the carrier of (K):] -defined the carrier of (K) -valued Function-like V17([: 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):]
1. (K) is Element of the carrier of (K)
the OneF of (K) is Element of the carrier of (K)
0. (K) is V46((K)) Element of the carrier of (K)
the ZeroF of (K) is Element of the carrier of (K)
doubleLoopStr(# the carrier of (K), the addF of (K),( the carrier of (K), the carrier of (K), the carrier of (K), the multF of (K)),(1. (K)),(0. (K)) #) is non empty strict doubleLoopStr
the carrier of V is non empty set
the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the ZeroF of V is Element of the carrier of V
the rmult of V is non empty Relation-like [: the carrier of V, the carrier of K:] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of K:]) quasi_total Element of bool [:[: the carrier of V, the carrier of K:], the carrier of V:]
[: the carrier of V, the carrier of K:] is non empty set
[:[: the carrier of V, the carrier of K:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of K:], the carrier of V:] is non empty set
RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is non empty strict RightModStr over K
the lmult of (K,V) is non empty Relation-like [: the carrier of (K), the carrier of (K,V):] -defined the carrier of (K,V) -valued Function-like V17([: the carrier of (K), the carrier of (K,V):]) quasi_total Element of bool [:[: the carrier of (K), the carrier of (K,V):], the carrier of (K,V):]
the carrier of (K,V) is non empty set
[: the carrier of (K), the carrier of (K,V):] is non empty set
[:[: the carrier of (K), the carrier of (K,V):], the carrier of (K,V):] is non empty set
bool [:[: the carrier of (K), the carrier of (K,V):], the carrier of (K,V):] is non empty set
((K),(K,V), the lmult of (K,V)) is non empty Relation-like [: the carrier of ((K),(K,V)), the carrier of ((K)):] -defined the carrier of ((K),(K,V)) -valued Function-like V17([: the carrier of ((K),(K,V)), the carrier of ((K)):]) quasi_total Element of bool [:[: the carrier of ((K),(K,V)), the carrier of ((K)):], the carrier of ((K),(K,V)):]
the carrier of ((K),(K,V)) is non empty set
the carrier of ((K)) is non empty set
[: the carrier of ((K),(K,V)), the carrier of ((K)):] is non empty set
[:[: the carrier of ((K),(K,V)), the carrier of ((K)):], the carrier of ((K),(K,V)):] is non empty set
bool [:[: the carrier of ((K),(K,V)), the carrier of ((K)):], the carrier of ((K),(K,V)):] is non empty set
( the carrier of (K), the carrier of (K,V), the carrier of (K,V), the lmult of (K,V)) is non empty Relation-like [: the carrier of (K,V), the carrier of (K):] -defined the carrier of (K,V) -valued Function-like V17([: the carrier of (K,V), the carrier of (K):]) quasi_total Element of bool [:[: the carrier of (K,V), the carrier of (K):], the carrier of (K,V):]
[: the carrier of (K,V), the carrier of (K):] is non empty set
[:[: the carrier of (K,V), the carrier of (K):], the carrier of (K,V):] is non empty set
bool [:[: the carrier of (K,V), the carrier of (K):], the carrier of (K,V):] is non empty set
(K,V, the rmult of V) is non empty Relation-like [: the carrier of (K), the carrier of (K,V):] -defined the carrier of (K,V) -valued Function-like V17([: the carrier of (K), the carrier of (K,V):]) quasi_total Element of bool [:[: the carrier of (K), the carrier of (K,V):], the carrier of (K,V):]
( the carrier of V, the carrier of K, the carrier of V, the rmult of V) is non empty Relation-like [: the carrier of K, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set
((K),(K,V),(K,V, the rmult of V)) is non empty Relation-like [: the carrier of ((K),(K,V)), the carrier of ((K)):] -defined the carrier of ((K),(K,V)) -valued Function-like V17([: the carrier of ((K),(K,V)), the carrier of ((K)):]) quasi_total Element of bool [:[: the carrier of ((K),(K,V)), the carrier of ((K)):], the carrier of ((K),(K,V)):]
( the carrier of (K), the carrier of (K,V), the carrier of (K,V),(K,V, the rmult of V)) is non empty Relation-like [: the carrier of (K,V), the carrier of (K):] -defined the carrier of (K,V) -valued Function-like V17([: the carrier of (K,V), the carrier of (K):]) quasi_total Element of bool [:[: the carrier of (K,V), the carrier of (K):], the carrier of (K,V):]
the addF of ((K),(K,V)) is non empty Relation-like [: the carrier of ((K),(K,V)), the carrier of ((K),(K,V)):] -defined the carrier of ((K),(K,V)) -valued Function-like V17([: the carrier of ((K),(K,V)), the carrier of ((K),(K,V)):]) quasi_total Element of bool [:[: the carrier of ((K),(K,V)), the carrier of ((K),(K,V)):], the carrier of ((K),(K,V)):]
[: the carrier of ((K),(K,V)), the carrier of ((K),(K,V)):] is non empty set
[:[: the carrier of ((K),(K,V)), the carrier of ((K),(K,V)):], the carrier of ((K),(K,V)):] is non empty set
bool [:[: the carrier of ((K),(K,V)), the carrier of ((K),(K,V)):], the carrier of ((K),(K,V)):] is non empty set
the ZeroF of ((K),(K,V)) is Element of the carrier of ((K),(K,V))
addLoopStr(# the carrier of ((K),(K,V)), the addF of ((K),(K,V)), the ZeroF of ((K),(K,V)) #) is non empty strict addLoopStr
the addF of (K,V) is non empty Relation-like [: the carrier of (K,V), the carrier of (K,V):] -defined the carrier of (K,V) -valued Function-like V17([: the carrier of (K,V), the carrier of (K,V):]) quasi_total Element of bool [:[: the carrier of (K,V), the carrier of (K,V):], the carrier of (K,V):]
[: the carrier of (K,V), the carrier of (K,V):] is non empty set
[:[: the carrier of (K,V), the carrier of (K,V):], the carrier of (K,V):] is non empty set
bool [:[: the carrier of (K,V), the carrier of (K,V):], the carrier of (K,V):] is non empty set
the ZeroF of (K,V) is Element of the carrier of (K,V)
addLoopStr(# the carrier of (K,V), the addF of (K,V), the ZeroF of (K,V) #) is non empty strict addLoopStr
addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) is non empty strict addLoopStr
K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
(K) is non empty right_complementable strict unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of K is non empty set
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is right_complementable Element of the carrier of K
the OneF of K is right_complementable Element of the carrier of K
0. K is V46(K) right_complementable Element of the carrier of K
the ZeroF of K is right_complementable Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty strict doubleLoopStr
V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K
(K,V) is non empty strict RightModStr over (K)
the carrier of (K,V) is non empty set
the addF of (K,V) is non empty Relation-like [: the carrier of (K,V), the carrier of (K,V):] -defined the carrier of (K,V) -valued Function-like V17([: the carrier of (K,V), the carrier of (K,V):]) quasi_total Element of bool [:[: the carrier of (K,V), the carrier of (K,V):], the carrier of (K,V):]
[: the carrier of (K,V), the carrier of (K,V):] is non empty set
[:[: the carrier of (K,V), the carrier of (K,V):], the carrier of (K,V):] is non empty set
bool [:[: the carrier of (K,V), the carrier of (K,V):], the carrier of (K,V):] is non empty set
the ZeroF of (K,V) is Element of the carrier of (K,V)
addLoopStr(# the carrier of (K,V), the addF of (K,V), the ZeroF of (K,V) #) is non empty strict addLoopStr
the carrier of V is non empty set
the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the ZeroF of V is right_complementable Element of the carrier of V
addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) is non empty strict addLoopStr
x is right_complementable Element of the carrier of V
J is Element of the carrier of (K,V)
a is Element of the carrier of (K,V)
z is right_complementable Element of the carrier of V
J + a is Element of the carrier of (K,V)
the addF of (K,V) . (J,a) is Element of the carrier of (K,V)
x + z is right_complementable Element of the carrier of V
the addF of V . (x,z) is right_complementable Element of the carrier of V
J is Element of the carrier of (K,V)
a is Element of the carrier of (K,V)
J + a is Element of the carrier of (K,V)
the addF of (K,V) . (J,a) is Element of the carrier of (K,V)
a + J is Element of the carrier of (K,V)
the addF of (K,V) . (a,J) is Element of the carrier of (K,V)
z is right_complementable Element of the carrier of V
x is right_complementable Element of the carrier of V
z + x is right_complementable Element of the carrier of V
the addF of V . (z,x) is right_complementable Element of the carrier of V
J is Element of the carrier of (K,V)
a is Element of the carrier of (K,V)
x is Element of the carrier of (K,V)
J + a is Element of the carrier of (K,V)
the addF of (K,V) . (J,a) is Element of the carrier of (K,V)
(J + a) + x is Element of the carrier of (K,V)
the addF of (K,V) . ((J + a),x) is Element of the carrier of (K,V)
z is right_complementable Element of the carrier of V
p is right_complementable Element of the carrier of V
z + p is right_complementable Element of the carrier of V
the addF of V . (z,p) is right_complementable Element of the carrier of V
q is right_complementable Element of the carrier of V
(z + p) + q is right_complementable Element of the carrier of V
the addF of V . ((z + p),q) is right_complementable Element of the carrier of V
p + q is right_complementable Element of the carrier of V
the addF of V . (p,q) is right_complementable Element of the carrier of V
z + (p + q) is right_complementable Element of the carrier of V
the addF of V . (z,(p + q)) is right_complementable Element of the carrier of V
a + x is Element of the carrier of (K,V)
the addF of (K,V) . (a,x) is Element of the carrier of (K,V)
J + (a + x) is Element of the carrier of (K,V)
the addF of (K,V) . (J,(a + x)) is Element of the carrier of (K,V)
J is Element of the carrier of (K,V)
0. (K,V) is V46((K,V)) Element of the carrier of (K,V)
J + (0. (K,V)) is Element of the carrier of (K,V)
the addF of (K,V) . (J,(0. (K,V))) is Element of the carrier of (K,V)
a is right_complementable Element of the carrier of V
0. V is V46(V) right_complementable Element of the carrier of V
a + (0. V) is right_complementable Element of the carrier of V
the addF of V . (a,(0. V)) is right_complementable Element of the carrier of V
J is Element of the carrier of (K,V)
a is right_complementable Element of the carrier of V
x is right_complementable Element of the carrier of V
a + x is right_complementable Element of the carrier of V
the addF of V . (a,x) is right_complementable Element of the carrier of V
z is Element of the carrier of (K,V)
J + z is Element of the carrier of (K,V)
the addF of (K,V) . (J,z) is Element of the carrier of (K,V)
the carrier of (K) is non empty set
f is non empty RightModStr over (K)
the carrier of f is non empty set
x is Element of the carrier of f
z is Element of the carrier of f
J is right_complementable Element of the carrier of (K)
a is right_complementable Element of the carrier of (K)
b is right_complementable Element of the carrier of K
p is right_complementable Element of the carrier of V
b * p is right_complementable Element of the carrier of V
the lmult of V is non empty Relation-like [: the carrier of K, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set
the lmult of V . (b,p) is right_complementable Element of the carrier of V
x * a is Element of the carrier of f
a is right_complementable Element of the carrier of K
q is right_complementable Element of the carrier of V
a * q is right_complementable Element of the carrier of V
the lmult of V . (a,q) is right_complementable Element of the carrier of V
z * J is Element of the carrier of f
a * p is right_complementable Element of the carrier of V
the lmult of V . (a,p) is right_complementable Element of the carrier of V
x * J is Element of the carrier of f
x + z is Element of the carrier of f
the addF of f is non empty Relation-like [: the carrier of f, the carrier of f:] -defined the carrier of f -valued Function-like V17([: 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 non empty set
[:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
bool [:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
the addF of f . (x,z) is Element of the carrier of f
p + q is right_complementable Element of the carrier of V
the addF of V . (p,q) is right_complementable Element of the carrier of V
(x + z) * J is Element of the carrier of f
a * (p + q) is right_complementable Element of the carrier of V
the lmult of V . (a,(p + q)) is right_complementable Element of the carrier of V
(a * p) + (a * q) is right_complementable Element of the carrier of V
the addF of V . ((a * p),(a * q)) is right_complementable Element of the carrier of V
(x * J) + (z * J) is Element of the carrier of f
the addF of f . ((x * J),(z * J)) is Element of the carrier of f
J + a is right_complementable Element of the carrier of (K)
the addF of (K) is non empty Relation-like [: the carrier of (K), the carrier of (K):] -defined the carrier of (K) -valued Function-like V17([: 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 non empty set
[:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
bool [:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
the addF of (K) . (J,a) is right_complementable Element of the carrier of (K)
x * (J + a) is Element of the carrier of f
a + b is right_complementable Element of the carrier of K
the addF of K . (a,b) is right_complementable Element of the carrier of K
(a + b) * p is right_complementable Element of the carrier of V
the lmult of V . ((a + b),p) is right_complementable Element of the carrier of V
(a * p) + (b * p) is right_complementable Element of the carrier of V
the addF of V . ((a * p),(b * p)) is right_complementable Element of the carrier of V
(x * J) + (x * a) is Element of the carrier of f
the addF of f . ((x * J),(x * a)) is Element of the carrier of f
a * J is right_complementable Element of the carrier of (K)
the multF of (K) is non empty Relation-like [: the carrier of (K), the carrier of (K):] -defined the carrier of (K) -valued Function-like V17([: the carrier of (K), the carrier of (K):]) quasi_total Element of bool [:[: the carrier of (K), the carrier of (K):], the carrier of (K):]
the multF of (K) . (a,J) is right_complementable Element of the carrier of (K)
x * (a * J) is Element of the carrier of f
a * b is right_complementable Element of the carrier of K
the multF of K . (a,b) is right_complementable Element of the carrier of K
(a * b) * p is right_complementable Element of the carrier of V
the lmult of V . ((a * b),p) is right_complementable Element of the carrier of V
a * (b * p) is right_complementable Element of the carrier of V
the lmult of V . (a,(b * p)) is right_complementable Element of the carrier of V
(x * a) * J is Element of the carrier of f
1_ (K) is right_complementable Element of the carrier of (K)
1. (K) is right_complementable Element of the carrier of (K)
the OneF of (K) is right_complementable Element of the carrier of (K)
x * (1_ (K)) is Element of the carrier of f
1_ K is right_complementable Element of the carrier of K
(1_ K) * p is right_complementable Element of the carrier of V
the lmult of V . ((1_ K),p) is right_complementable Element of the carrier of V
K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K
(K,V) is non empty strict RightModStr over (K)
(K) is non empty right_complementable strict unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of K is non empty set
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is right_complementable Element of the carrier of K
the OneF of K is right_complementable Element of the carrier of K
0. K is V46(K) right_complementable Element of the carrier of K
the ZeroF of K is right_complementable Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty strict doubleLoopStr
K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
(K) is non empty right_complementable strict unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of K is non empty set
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is right_complementable Element of the carrier of K
the OneF of K is right_complementable Element of the carrier of K
0. K is V46(K) right_complementable Element of the carrier of K
the ZeroF of K is right_complementable Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty strict doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over K
(K,V) is non empty strict VectSpStr over (K)
the carrier of (K,V) is non empty set
the addF of (K,V) is non empty Relation-like [: the carrier of (K,V), the carrier of (K,V):] -defined the carrier of (K,V) -valued Function-like V17([: the carrier of (K,V), the carrier of (K,V):]) quasi_total Element of bool [:[: the carrier of (K,V), the carrier of (K,V):], the carrier of (K,V):]
[: the carrier of (K,V), the carrier of (K,V):] is non empty set
[:[: the carrier of (K,V), the carrier of (K,V):], the carrier of (K,V):] is non empty set
bool [:[: the carrier of (K,V), the carrier of (K,V):], the carrier of (K,V):] is non empty set
the ZeroF of (K,V) is Element of the carrier of (K,V)
addLoopStr(# the carrier of (K,V), the addF of (K,V), the ZeroF of (K,V) #) is non empty strict addLoopStr
the carrier of V is non empty set
the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the ZeroF of V is right_complementable Element of the carrier of V
addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) is non empty strict addLoopStr
x is right_complementable Element of the carrier of V
J is Element of the carrier of (K,V)
a is Element of the carrier of (K,V)
z is right_complementable Element of the carrier of V
J + a is Element of the carrier of (K,V)
the addF of (K,V) . (J,a) is Element of the carrier of (K,V)
x + z is right_complementable Element of the carrier of V
the addF of V . (x,z) is right_complementable Element of the carrier of V
J is Element of the carrier of (K,V)
a is Element of the carrier of (K,V)
J + a is Element of the carrier of (K,V)
the addF of (K,V) . (J,a) is Element of the carrier of (K,V)
a + J is Element of the carrier of (K,V)
the addF of (K,V) . (a,J) is Element of the carrier of (K,V)
z is right_complementable Element of the carrier of V
x is right_complementable Element of the carrier of V
z + x is right_complementable Element of the carrier of V
the addF of V . (z,x) is right_complementable Element of the carrier of V
J is Element of the carrier of (K,V)
a is Element of the carrier of (K,V)
x is Element of the carrier of (K,V)
J + a is Element of the carrier of (K,V)
the addF of (K,V) . (J,a) is Element of the carrier of (K,V)
(J + a) + x is Element of the carrier of (K,V)
the addF of (K,V) . ((J + a),x) is Element of the carrier of (K,V)
z is right_complementable Element of the carrier of V
p is right_complementable Element of the carrier of V
z + p is right_complementable Element of the carrier of V
the addF of V . (z,p) is right_complementable Element of the carrier of V
q is right_complementable Element of the carrier of V
(z + p) + q is right_complementable Element of the carrier of V
the addF of V . ((z + p),q) is right_complementable Element of the carrier of V
p + q is right_complementable Element of the carrier of V
the addF of V . (p,q) is right_complementable Element of the carrier of V
z + (p + q) is right_complementable Element of the carrier of V
the addF of V . (z,(p + q)) is right_complementable Element of the carrier of V
a + x is Element of the carrier of (K,V)
the addF of (K,V) . (a,x) is Element of the carrier of (K,V)
J + (a + x) is Element of the carrier of (K,V)
the addF of (K,V) . (J,(a + x)) is Element of the carrier of (K,V)
J is Element of the carrier of (K,V)
0. (K,V) is V46((K,V)) Element of the carrier of (K,V)
J + (0. (K,V)) is Element of the carrier of (K,V)
the addF of (K,V) . (J,(0. (K,V))) is Element of the carrier of (K,V)
a is right_complementable Element of the carrier of V
0. V is V46(V) right_complementable Element of the carrier of V
a + (0. V) is right_complementable Element of the carrier of V
the addF of V . (a,(0. V)) is right_complementable Element of the carrier of V
J is Element of the carrier of (K,V)
a is right_complementable Element of the carrier of V
x is right_complementable Element of the carrier of V
a + x is right_complementable Element of the carrier of V
the addF of V . (a,x) is right_complementable Element of the carrier of V
z is Element of the carrier of (K,V)
J + z is Element of the carrier of (K,V)
the addF of (K,V) . (J,z) is Element of the carrier of (K,V)
the carrier of (K) is non empty set
f is non empty VectSpStr over (K)
the carrier of f is non empty set
x is Element of the carrier of f
z is Element of the carrier of f
J is right_complementable Element of the carrier of (K)
a is right_complementable Element of the carrier of (K)
b is right_complementable Element of the carrier of K
p is right_complementable Element of the carrier of V
p * b is right_complementable Element of the carrier of V
a * x is Element of the carrier of f
the lmult of f is non empty Relation-like [: the carrier of (K), the carrier of f:] -defined the carrier of f -valued Function-like V17([: 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 non empty set
[:[: the carrier of (K), the carrier of f:], the carrier of f:] is non empty set
bool [:[: the carrier of (K), the carrier of f:], the carrier of f:] is non empty set
the lmult of f . (a,x) is Element of the carrier of f
a is right_complementable Element of the carrier of K
q is right_complementable Element of the carrier of V
q * a is right_complementable Element of the carrier of V
J * z is Element of the carrier of f
the lmult of f . (J,z) is Element of the carrier of f
p * a is right_complementable Element of the carrier of V
J * x is Element of the carrier of f
the lmult of f . (J,x) is Element of the carrier of f
x + z is Element of the carrier of f
the addF of f is non empty Relation-like [: the carrier of f, the carrier of f:] -defined the carrier of f -valued Function-like V17([: 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 non empty set
[:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
bool [:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
the addF of f . (x,z) is Element of the carrier of f
p + q is right_complementable Element of the carrier of V
the addF of V . (p,q) is right_complementable Element of the carrier of V
J * (x + z) is Element of the carrier of f
the lmult of f . (J,(x + z)) is Element of the carrier of f
(p + q) * a is right_complementable Element of the carrier of V
(p * a) + (q * a) is right_complementable Element of the carrier of V
the addF of V . ((p * a),(q * a)) is right_complementable Element of the carrier of V
(J * x) + (J * z) is Element of the carrier of f
the addF of f . ((J * x),(J * z)) is Element of the carrier of f
J + a is right_complementable Element of the carrier of (K)
the addF of (K) is non empty Relation-like [: the carrier of (K), the carrier of (K):] -defined the carrier of (K) -valued Function-like V17([: 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 non empty set
[:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
bool [:[: the carrier of (K), the carrier of (K):], the carrier of (K):] is non empty set
the addF of (K) . (J,a) is right_complementable Element of the carrier of (K)
(J + a) * x is Element of the carrier of f
the lmult of f . ((J + a),x) is Element of the carrier of f
a + b is right_complementable Element of the carrier of K
the addF of K . (a,b) is right_complementable Element of the carrier of K
p * (a + b) is right_complementable Element of the carrier of V
(p * a) + (p * b) is right_complementable Element of the carrier of V
the addF of V . ((p * a),(p * b)) is right_complementable Element of the carrier of V
(J * x) + (a * x) is Element of the carrier of f
the addF of f . ((J * x),(a * x)) is Element of the carrier of f
J * a is right_complementable Element of the carrier of (K)
the multF of (K) is non empty Relation-like [: the carrier of (K), the carrier of (K):] -defined the carrier of (K) -valued Function-like V17([: 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) . (J,a) is right_complementable Element of the carrier of (K)
b * a is right_complementable Element of the carrier of K
the multF of K . (b,a) is right_complementable Element of the carrier of K
(J * a) * x is Element of the carrier of f
the lmult of f . ((J * a),x) is Element of the carrier of f
p * (b * a) is right_complementable Element of the carrier of V
(p * b) * a is right_complementable Element of the carrier of V
J * (a * x) is Element of the carrier of f
the lmult of f . (J,(a * x)) is Element of the carrier of f
1_ (K) is right_complementable Element of the carrier of (K)
1. (K) is right_complementable Element of the carrier of (K)
the OneF of (K) is right_complementable Element of the carrier of (K)
(1_ (K)) * x is Element of the carrier of f
the lmult of f . ((1_ (K)),x) is Element of the carrier of f
1_ K is right_complementable Element of the carrier of K
p * (1_ K) is right_complementable Element of the carrier of V
K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over K
(K,V) is non empty strict VectSpStr over (K)
(K) is non empty right_complementable strict unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of K is non empty set
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is right_complementable Element of the carrier of K
the OneF of K is right_complementable Element of the carrier of K
0. K is V46(K) right_complementable Element of the carrier of K
the ZeroF of K is right_complementable Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty strict doubleLoopStr
K is non empty multMagma
the carrier of K is non empty set
V is non empty multMagma
the carrier of V is non empty set
[: the carrier of K, the carrier of V:] is non empty set
bool [: the carrier of K, the carrier of V:] is non empty set
K is non empty doubleLoopStr
the carrier of K is non empty set
V is non empty doubleLoopStr
the carrier of V is non empty set
[: the carrier of K, the carrier of V:] is non empty set
bool [: the carrier of K, the carrier of V:] is non empty set
K is non empty doubleLoopStr
the carrier of K is non empty set
V is non empty doubleLoopStr
the carrier of V is non empty set
[: the carrier of K, the carrier of V:] is non empty set
bool [: the carrier of K, the carrier of V:] is non empty set
W is non empty Relation-like the carrier of K -defined the carrier of V -valued Function-like V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of V:]
W is non empty Relation-like the carrier of K -defined the carrier of V -valued Function-like V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of V:]
K is non empty doubleLoopStr
the carrier of K is non empty set
V is non empty doubleLoopStr
the carrier of V is non empty set
[: the carrier of K, the carrier of V:] is non empty set
bool [: the carrier of K, the carrier of V:] is non empty set
K is non empty doubleLoopStr
the carrier of K is non empty set
V is non empty doubleLoopStr
the carrier of V is non empty set
[: the carrier of K, the carrier of V:] is non empty set
bool [: the carrier of K, the carrier of V:] is non empty set
K is non empty doubleLoopStr
the carrier of K is non empty set
V is non empty doubleLoopStr
the carrier of V is non empty set
[: the carrier of K, the carrier of V:] is non empty set
bool [: the carrier of K, the carrier of V:] is non empty set
K is non empty doubleLoopStr
the carrier of K is non empty set
[: the carrier of K, the carrier of K:] is non empty set
bool [: the carrier of K, the carrier of K:] is non empty set
K is non empty doubleLoopStr
the carrier of K is non empty set
[: the carrier of K, the carrier of K:] is non empty set
bool [: the carrier of K, the carrier of K:] is non empty set
1_ K is Element of the carrier of K
V is non empty Relation-like the carrier of K -defined the carrier of K -valued Function-like V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of K:]
V . (1_ K) is Element of the carrier of K
W is Element of the carrier of K
f is Element of the carrier of K
W * f is Element of the carrier of K
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K . (W,f) is Element of the carrier of K
V . (W * f) is Element of the carrier of K
V . W is Element of the carrier of K
V . f is Element of the carrier of K
(V . W) * (V . f) is Element of the carrier of K
the multF of K . ((V . W),(V . f)) is Element of the carrier of K
W is Element of the carrier of K
f is Element of the carrier of K
W * f is Element of the carrier of K
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K . (W,f) is Element of the carrier of K
V . (W * f) is Element of the carrier of K
V . W is Element of the carrier of K
V . f is Element of the carrier of K
(V . W) * (V . f) is Element of the carrier of K
the multF of K . ((V . W),(V . f)) is Element of the carrier of K
J is Element of the carrier of K
a is Element of the carrier of K
J * a is Element of the carrier of K
the multF of K . (J,a) is Element of the carrier of K
V . (J * a) is Element of the carrier of K
V . J is Element of the carrier of K
V . a is Element of the carrier of K
(V . J) * (V . a) is Element of the carrier of K
the multF of K . ((V . J),(V . a)) is Element of the carrier of K
K is non empty doubleLoopStr
the carrier of K is non empty set
[: the carrier of K, the carrier of K:] is non empty set
bool [: the carrier of K, the carrier of K:] is non empty set
1_ K is Element of the carrier of K
V is non empty Relation-like the carrier of K -defined the carrier of K -valued Function-like V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of K:]
V . (1_ K) is Element of the carrier of K
W is Element of the carrier of K
f is Element of the carrier of K
W * f is Element of the carrier of K
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K . (W,f) is Element of the carrier of K
V . (W * f) is Element of the carrier of K
V . f is Element of the carrier of K
V . W is Element of the carrier of K
(V . f) * (V . W) is Element of the carrier of K
the multF of K . ((V . f),(V . W)) is Element of the carrier of K
W is Element of the carrier of K
f is Element of the carrier of K
W * f is Element of the carrier of K
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K . (W,f) is Element of the carrier of K
V . (W * f) is Element of the carrier of K
V . f is Element of the carrier of K
V . W is Element of the carrier of K
(V . f) * (V . W) is Element of the carrier of K
the multF of K . ((V . f),(V . W)) is Element of the carrier of K
J is Element of the carrier of K
a is Element of the carrier of K
J * a is Element of the carrier of K
the multF of K . (J,a) is Element of the carrier of K
V . (J * a) is Element of the carrier of K
V . a is Element of the carrier of K
V . J is Element of the carrier of K
(V . a) * (V . J) is Element of the carrier of K
the multF of K . ((V . a),(V . J)) is Element of the carrier of K
K is non empty doubleLoopStr
the carrier of K is non empty set
id K is non empty Relation-like the carrier of K -defined the carrier of K -valued Function-like one-to-one V17( the carrier of K) quasi_total onto bijective unity-preserving additive multiplicative linear Element of bool [: the carrier of K, the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
bool [: the carrier of K, the carrier of K:] is non empty set
K97( the carrier of K) is non empty Relation-like the carrier of K -defined the carrier of K -valued Function-like one-to-one V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of K:]
1_ K is Element of the carrier of K
(id K) . (1_ K) is Element of the carrier of K
W is Element of the carrier of K
f is Element of the carrier of K
W * f is Element of the carrier of K
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K . (W,f) is Element of the carrier of K
(id K) . (W * f) is Element of the carrier of K
(id K) . W is Element of the carrier of K
(id K) . f is Element of the carrier of K
((id K) . W) * ((id K) . f) is Element of the carrier of K
the multF of K . (((id K) . W),((id K) . f)) is Element of the carrier of K
K is non empty doubleLoopStr
id K is non empty Relation-like the carrier of K -defined the carrier of K -valued Function-like one-to-one V17( the carrier of K) quasi_total onto bijective unity-preserving additive multiplicative linear Element of bool [: the carrier of K, the carrier of K:]
the carrier of K is non empty set
[: the carrier of K, the carrier of K:] is non empty set
bool [: the carrier of K, the carrier of K:] is non empty set
K97( the carrier of K) is non empty Relation-like the carrier of K -defined the carrier of K -valued Function-like one-to-one V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of K:]
K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of K is non empty set
0. K is V46(K) right_complementable Element of the carrier of K
the ZeroF of K is right_complementable Element of the carrier of K
V is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of V is non empty set
[: the carrier of K, the carrier of V:] is non empty set
bool [: the carrier of K, the carrier of V:] is non empty set
0. V is V46(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
W is non empty Relation-like the carrier of K -defined the carrier of V -valued Function-like V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of V:]
W . (0. K) is right_complementable Element of the carrier of V
(0. K) + (0. K) is right_complementable Element of the carrier of K
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the addF of K . ((0. K),(0. K)) is right_complementable Element of the carrier of K
(W . (0. K)) + (W . (0. K)) is right_complementable Element of the carrier of V
the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . ((W . (0. K)),(W . (0. K))) is right_complementable Element of the carrier of V
(W . (0. K)) + (0. V) is right_complementable Element of the carrier of V
the addF of V . ((W . (0. K)),(0. V)) is right_complementable Element of the carrier of V
K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of K is non empty set
V is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of V is non empty set
[: the carrier of V, the carrier of K:] is non empty set
bool [: the carrier of V, the carrier of K:] is non empty set
W is non empty Relation-like the carrier of V -defined the carrier of K -valued Function-like V17( the carrier of V) quasi_total Element of bool [: the carrier of V, the carrier of K:]
f is right_complementable Element of the carrier of V
- f is right_complementable Element of the carrier of V
W . (- f) is right_complementable Element of the carrier of K
W . f is right_complementable Element of the carrier of K
- (W . f) is right_complementable Element of the carrier of K
0. V is V46(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
0. K is V46(K) right_complementable Element of the carrier of K
the ZeroF of K is right_complementable Element of the carrier of K
f + (- f) is right_complementable Element of the carrier of V
the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . (f,(- f)) is right_complementable Element of the carrier of V
(W . f) + (- (W . f)) is right_complementable Element of the carrier of K
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the addF of K . ((W . f),(- (W . f))) is right_complementable Element of the carrier of K
(W . f) + (W . (- f)) is right_complementable Element of the carrier of K
the addF of K . ((W . f),(W . (- f))) is right_complementable Element of the carrier of K
W . (0. V) is right_complementable Element of the carrier of K
K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of K is non empty set
V is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of V is non empty set
[: the carrier of V, the carrier of K:] is non empty set
bool [: the carrier of V, the carrier of K:] is non empty set
W is non empty Relation-like the carrier of V -defined the carrier of K -valued Function-like V17( the carrier of V) quasi_total Element of bool [: the carrier of V, the carrier of K:]
f is right_complementable Element of the carrier of V
W . f is right_complementable Element of the carrier of K
J is right_complementable Element of the carrier of V
f - J is right_complementable Element of the carrier of V
- J is right_complementable Element of the carrier of V
f + (- J) is right_complementable Element of the carrier of V
the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . (f,(- J)) is right_complementable Element of the carrier of V
W . (f - J) is right_complementable Element of the carrier of K
W . J is right_complementable Element of the carrier of K
(W . f) - (W . J) is right_complementable Element of the carrier of K
- (W . J) is right_complementable Element of the carrier of K
(W . f) + (- (W . J)) is right_complementable Element of the carrier of K
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the addF of K . ((W . f),(- (W . J))) is right_complementable Element of the carrier of K
W . (- J) is right_complementable Element of the carrier of K
(W . f) + (W . (- J)) is right_complementable Element of the carrier of K
the addF of K . ((W . f),(W . (- J))) is right_complementable Element of the carrier of K
K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of K is non empty set
V is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of V is non empty set
[: the carrier of K, the carrier of V:] is non empty set
bool [: the carrier of K, the carrier of V:] is non empty set
W is non empty Relation-like the carrier of K -defined the carrier of V -valued Function-like V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of V:]
0. K is V46(K) right_complementable Element of the carrier of K
the ZeroF of K is right_complementable Element of the carrier of K
W . (0. K) is right_complementable Element of the carrier of V
0. V is V46(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 K
- f is right_complementable Element of the carrier of K
W . (- f) is right_complementable Element of the carrier of V
W . f is right_complementable Element of the carrier of V
- (W . f) is right_complementable Element of the carrier of V
J is right_complementable Element of the carrier of K
f - J is right_complementable Element of the carrier of K
- J is right_complementable Element of the carrier of K
f + (- J) is right_complementable Element of the carrier of K
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the addF of K . (f,(- J)) is right_complementable Element of the carrier of K
W . (f - J) is right_complementable Element of the carrier of V
W . J is right_complementable Element of the carrier of V
(W . f) - (W . J) is right_complementable Element of the carrier of V
- (W . J) is right_complementable Element of the carrier of V
(W . f) + (- (W . J)) is right_complementable Element of the carrier of V
the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . ((W . f),(- (W . J))) is right_complementable Element of the carrier of V
K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of K is non empty set
0. K is V46(K) right_complementable Element of the carrier of K
the ZeroF of K is right_complementable Element of the carrier of K
V is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of V is non empty set
[: the carrier of K, the carrier of V:] is non empty set
bool [: the carrier of K, the carrier of V:] is non empty set
0. V is V46(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
W is non empty Relation-like the carrier of K -defined the carrier of V -valued Function-like V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of V:]
W . (0. K) is right_complementable Element of the carrier of V
(0. K) + (0. K) is right_complementable Element of the carrier of K
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the addF of K . ((0. K),(0. K)) is right_complementable Element of the carrier of K
(W . (0. K)) + (W . (0. K)) is right_complementable Element of the carrier of V
the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . ((W . (0. K)),(W . (0. K))) is right_complementable Element of the carrier of V
(W . (0. K)) + (0. V) is right_complementable Element of the carrier of V
the addF of V . ((W . (0. K)),(0. V)) is right_complementable Element of the carrier of V
K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of K is non empty set
V is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of V is non empty set
[: the carrier of V, the carrier of K:] is non empty set
bool [: the carrier of V, the carrier of K:] is non empty set
W is non empty Relation-like the carrier of V -defined the carrier of K -valued Function-like V17( the carrier of V) quasi_total Element of bool [: the carrier of V, the carrier of K:]
f is right_complementable Element of the carrier of V
- f is right_complementable Element of the carrier of V
W . (- f) is right_complementable Element of the carrier of K
W . f is right_complementable Element of the carrier of K
- (W . f) is right_complementable Element of the carrier of K
0. V is V46(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
0. K is V46(K) right_complementable Element of the carrier of K
the ZeroF of K is right_complementable Element of the carrier of K
(W . f) + (- (W . f)) is right_complementable Element of the carrier of K
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the addF of K . ((W . f),(- (W . f))) is right_complementable Element of the carrier of K
f + (- f) is right_complementable Element of the carrier of V
the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . (f,(- f)) is right_complementable Element of the carrier of V
(W . f) + (W . (- f)) is right_complementable Element of the carrier of K
the addF of K . ((W . f),(W . (- f))) is right_complementable Element of the carrier of K
W . (0. V) is right_complementable Element of the carrier of K
K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of K is non empty set
V is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of V is non empty set
[: the carrier of V, the carrier of K:] is non empty set
bool [: the carrier of V, the carrier of K:] is non empty set
W is non empty Relation-like the carrier of V -defined the carrier of K -valued Function-like V17( the carrier of V) quasi_total Element of bool [: the carrier of V, the carrier of K:]
f is right_complementable Element of the carrier of V
W . f is right_complementable Element of the carrier of K
J is right_complementable Element of the carrier of V
f - J is right_complementable Element of the carrier of V
- J is right_complementable Element of the carrier of V
f + (- J) is right_complementable Element of the carrier of V
the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . (f,(- J)) is right_complementable Element of the carrier of V
W . (f - J) is right_complementable Element of the carrier of K
W . J is right_complementable Element of the carrier of K
(W . f) - (W . J) is right_complementable Element of the carrier of K
- (W . J) is right_complementable Element of the carrier of K
(W . f) + (- (W . J)) is right_complementable Element of the carrier of K
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the addF of K . ((W . f),(- (W . J))) is right_complementable Element of the carrier of K
W . (- J) is right_complementable Element of the carrier of K
(W . f) + (W . (- J)) is right_complementable Element of the carrier of K
the addF of K . ((W . f),(W . (- J))) is right_complementable Element of the carrier of K
K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of K is non empty set
V is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of V is non empty set
[: the carrier of K, the carrier of V:] is non empty set
bool [: the carrier of K, the carrier of V:] is non empty set
W is non empty Relation-like the carrier of K -defined the carrier of V -valued Function-like V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of V:]
0. K is V46(K) right_complementable Element of the carrier of K
the ZeroF of K is right_complementable Element of the carrier of K
W . (0. K) is right_complementable Element of the carrier of V
0. V is V46(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 K
- f is right_complementable Element of the carrier of K
W . (- f) is right_complementable Element of the carrier of V
W . f is right_complementable Element of the carrier of V
- (W . f) is right_complementable Element of the carrier of V
J is right_complementable Element of the carrier of K
f - J is right_complementable Element of the carrier of K
- J is right_complementable Element of the carrier of K
f + (- J) is right_complementable Element of the carrier of K
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the addF of K . (f,(- J)) is right_complementable Element of the carrier of K
W . (f - J) is right_complementable Element of the carrier of V
W . J is right_complementable Element of the carrier of V
(W . f) - (W . J) is right_complementable Element of the carrier of V
- (W . J) is right_complementable Element of the carrier of V
(W . f) + (- (W . J)) is right_complementable Element of the carrier of V
the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . ((W . f),(- (W . J))) is right_complementable Element of the carrier of V
K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
id K is non empty Relation-like the carrier of K -defined the carrier of K -valued Function-like one-to-one V17( the carrier of K) quasi_total onto bijective unity-preserving additive multiplicative linear (K,K) Element of bool [: the carrier of K, the carrier of K:]
the carrier of K is non empty set
[: the carrier of K, the carrier of K:] is non empty set
bool [: the carrier of K, the carrier of K:] is non empty set
K97( the carrier of K) is non empty Relation-like the carrier of K -defined the carrier of K -valued Function-like one-to-one V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of K:]
W is right_complementable Element of the carrier of K
f is right_complementable Element of the carrier of K
W * f is right_complementable Element of the carrier of K
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K . (W,f) is right_complementable Element of the carrier of K
(id K) . (W * f) is right_complementable Element of the carrier of K
(id K) . f is right_complementable Element of the carrier of K
(id K) . W is right_complementable Element of the carrier of K
((id K) . f) * ((id K) . W) is right_complementable Element of the carrier of K
the multF of K . (((id K) . f),((id K) . W)) is right_complementable Element of the carrier of K
1_ K is right_complementable Element of the carrier of K
1. K is right_complementable Element of the carrier of K
the OneF of K is right_complementable Element of the carrier of K
(id K) . (1_ K) is right_complementable Element of the carrier of K
W is right_complementable Element of the carrier of K
f is right_complementable Element of the carrier of K
W * f is right_complementable Element of the carrier of K
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K . (W,f) is right_complementable Element of the carrier of K
f * W is right_complementable Element of the carrier of K
the multF of K . (f,W) is right_complementable Element of the carrier of K
(id K) . f is right_complementable Element of the carrier of K
(id K) . (W * f) is right_complementable Element of the carrier of K
(id K) . W is right_complementable Element of the carrier of K
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
id K is non empty Relation-like the carrier of K -defined the carrier of K -valued Function-like one-to-one V17( the carrier of K) quasi_total onto bijective unity-preserving additive multiplicative linear (K,K) Element of bool [: the carrier of K, the carrier of K:]
the carrier of K is non empty non trivial set
[: the carrier of K, the carrier of K:] is non empty set
bool [: the carrier of K, the carrier of K:] is non empty set
K97( the carrier of K) is non empty Relation-like the carrier of K -defined the carrier of K -valued Function-like one-to-one V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of K:]
W is right_complementable Element of the carrier of K
f is right_complementable Element of the carrier of K
W * f is right_complementable Element of the carrier of K
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K . (W,f) is right_complementable Element of the carrier of K
(id K) . (W * f) is right_complementable Element of the carrier of K
(id K) . f is right_complementable Element of the carrier of K
(id K) . W is right_complementable Element of the carrier of K
((id K) . f) * ((id K) . W) is right_complementable Element of the carrier of K
the multF of K . (((id K) . f),((id K) . W)) is right_complementable Element of the carrier of K
1_ K is right_complementable Element of the carrier of K
1. K is V46(K) right_complementable Element of the carrier of K
the OneF of K is right_complementable Element of the carrier of K
(id K) . (1_ K) is right_complementable Element of the carrier of K
W is right_complementable Element of the carrier of K
f is right_complementable Element of the carrier of K
W * f is right_complementable Element of the carrier of K
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K . (W,f) is right_complementable Element of the carrier of K
f * W is right_complementable Element of the carrier of K
the multF of K . (f,W) is right_complementable Element of the carrier of K
(id K) . f is right_complementable Element of the carrier of K
(id K) . (W * f) is right_complementable Element of the carrier of K
(id K) . W is right_complementable Element of the carrier of K
K is non empty doubleLoopStr
the carrier of K is non empty set
V is non empty doubleLoopStr
the carrier of V is non empty set
[: the carrier of K, the carrier of V:] is non empty set
bool [: the carrier of K, the carrier of V:] is non empty set
W is non empty Relation-like the carrier of K -defined the carrier of V -valued Function-like V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of V:]
(V) is non empty strict doubleLoopStr
the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the multF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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, the multF of V) is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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:]
1. V is Element of the carrier of V
the OneF of V is Element of the carrier of V
0. V is V46(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
doubleLoopStr(# the carrier of V, the addF of V,( the carrier of V, the carrier of V, the carrier of V, the multF of V),(1. V),(0. V) #) is non empty strict doubleLoopStr
the carrier of (V) is non empty set
[: the carrier of K, the carrier of (V):] is non empty set
bool [: the carrier of K, the carrier of (V):] is non empty set
K is non empty right_complementable add-associative right_zeroed doubleLoopStr
the carrier of K is non empty set
V is non empty right_complementable unital right_unital well-unital left_unital add-associative right_zeroed doubleLoopStr
the carrier of V is non empty set
[: the carrier of K, the carrier of V:] is non empty set
bool [: the carrier of K, the carrier of V:] is non empty set
(V) is non empty right_complementable strict unital right_unital well-unital left_unital add-associative right_zeroed doubleLoopStr
the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the multF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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, the multF of V) is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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:]
1. V is right_complementable Element of the carrier of V
the OneF of V is right_complementable Element of the carrier of V
0. V is V46(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
doubleLoopStr(# the carrier of V, the addF of V,( the carrier of V, the carrier of V, the carrier of V, the multF of V),(1. V),(0. V) #) is non empty strict doubleLoopStr
W is non empty Relation-like the carrier of K -defined the carrier of V -valued Function-like V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of V:]
(K,V,W) is non empty Relation-like the carrier of K -defined the carrier of (V) -valued Function-like V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of (V):]
the carrier of (V) is non empty set
[: the carrier of K, the carrier of (V):] is non empty set
bool [: the carrier of K, the carrier of (V):] is non empty set
J is right_complementable Element of the carrier of K
a is right_complementable Element of the carrier of K
J + a is right_complementable Element of the carrier of K
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the addF of K . (J,a) is right_complementable Element of the carrier of K
(K,V,W) . (J + a) is right_complementable Element of the carrier of (V)
(K,V,W) . J is right_complementable Element of the carrier of (V)
(K,V,W) . a is right_complementable Element of the carrier of (V)
((K,V,W) . J) + ((K,V,W) . a) is right_complementable Element of the carrier of (V)
the addF of (V) is non empty Relation-like [: the carrier of (V), the carrier of (V):] -defined the carrier of (V) -valued Function-like V17([: 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 non empty set
[:[: the carrier of (V), the carrier of (V):], the carrier of (V):] is non empty set
bool [:[: the carrier of (V), the carrier of (V):], the carrier of (V):] is non empty set
the addF of (V) . (((K,V,W) . J),((K,V,W) . a)) is right_complementable Element of the carrier of (V)
W . J is right_complementable Element of the carrier of V
W . a is right_complementable Element of the carrier of V
(W . J) + (W . a) is right_complementable Element of the carrier of V
the addF of V . ((W . J),(W . a)) is right_complementable Element of the carrier of V
K is non empty right_complementable add-associative right_zeroed doubleLoopStr
the carrier of K is non empty set
V is non empty right_complementable unital right_unital well-unital left_unital add-associative right_zeroed doubleLoopStr
the carrier of V is non empty set
[: the carrier of K, the carrier of V:] is non empty set
bool [: the carrier of K, the carrier of V:] is non empty set
(V) is non empty right_complementable strict unital right_unital well-unital left_unital add-associative right_zeroed doubleLoopStr
the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the multF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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, the multF of V) is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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:]
1. V is right_complementable Element of the carrier of V
the OneF of V is right_complementable Element of the carrier of V
0. V is V46(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
doubleLoopStr(# the carrier of V, the addF of V,( the carrier of V, the carrier of V, the carrier of V, the multF of V),(1. V),(0. V) #) is non empty strict doubleLoopStr
W is non empty Relation-like the carrier of K -defined the carrier of V -valued Function-like V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of V:]
(K,V,W) is non empty Relation-like the carrier of K -defined the carrier of (V) -valued Function-like V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of (V):]
the carrier of (V) is non empty set
[: the carrier of K, the carrier of (V):] is non empty set
bool [: the carrier of K, the carrier of (V):] is non empty set
a is right_complementable Element of the carrier of K
x is right_complementable Element of the carrier of K
a * x is right_complementable Element of the carrier of K
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K . (a,x) is right_complementable Element of the carrier of K
(K,V,W) . (a * x) is right_complementable Element of the carrier of (V)
(K,V,W) . x is right_complementable Element of the carrier of (V)
(K,V,W) . a is right_complementable Element of the carrier of (V)
((K,V,W) . x) * ((K,V,W) . a) is right_complementable Element of the carrier of (V)
the multF of (V) is non empty Relation-like [: the carrier of (V), the carrier of (V):] -defined the carrier of (V) -valued Function-like V17([: 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 non empty set
[:[: the carrier of (V), the carrier of (V):], the carrier of (V):] is non empty set
bool [:[: the carrier of (V), the carrier of (V):], the carrier of (V):] is non empty set
the multF of (V) . (((K,V,W) . x),((K,V,W) . a)) is right_complementable Element of the carrier of (V)
W . a is right_complementable Element of the carrier of V
W . x is right_complementable Element of the carrier of V
(W . a) * (W . x) is right_complementable Element of the carrier of V
the multF of V . ((W . a),(W . x)) is right_complementable Element of the carrier of V
1_ K is right_complementable Element of the carrier of K
(K,V,W) . (1_ K) is right_complementable Element of the carrier of (V)
1_ V is right_complementable Element of the carrier of V
1_ (V) is right_complementable Element of the carrier of (V)
1. (V) is right_complementable Element of the carrier of (V)
the OneF of (V) is right_complementable Element of the carrier of (V)
a is right_complementable Element of the carrier of K
x is right_complementable Element of the carrier of K
a + x is right_complementable Element of the carrier of K
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the addF of K . (a,x) is right_complementable Element of the carrier of K
W . (a + x) is right_complementable Element of the carrier of V
W . a is right_complementable Element of the carrier of V
W . x is right_complementable Element of the carrier of V
(W . a) + (W . x) is right_complementable Element of the carrier of V
the addF of V . ((W . a),(W . x)) is right_complementable Element of the carrier of V
(K,V,W) . a is right_complementable Element of the carrier of (V)
(K,V,W) . x is right_complementable Element of the carrier of (V)
((K,V,W) . a) + ((K,V,W) . x) is right_complementable Element of the carrier of (V)
the addF of (V) is non empty Relation-like [: the carrier of (V), the carrier of (V):] -defined the carrier of (V) -valued Function-like V17([: 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 non empty set
[:[: the carrier of (V), the carrier of (V):], the carrier of (V):] is non empty set
bool [:[: the carrier of (V), the carrier of (V):], the carrier of (V):] is non empty set
the addF of (V) . (((K,V,W) . a),((K,V,W) . x)) is right_complementable Element of the carrier of (V)
a is right_complementable Element of the carrier of K
x is right_complementable Element of the carrier of K
a * x is right_complementable Element of the carrier of K
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K . (a,x) is right_complementable Element of the carrier of K
W . (a * x) is right_complementable Element of the carrier of V
W . a is right_complementable Element of the carrier of V
W . x is right_complementable Element of the carrier of V
(W . a) * (W . x) is right_complementable Element of the carrier of V
the multF of V . ((W . a),(W . x)) is right_complementable Element of the carrier of V
(K,V,W) . x is right_complementable Element of the carrier of (V)
(K,V,W) . a is right_complementable Element of the carrier of (V)
((K,V,W) . x) * ((K,V,W) . a) is right_complementable Element of the carrier of (V)
the multF of (V) is non empty Relation-like [: the carrier of (V), the carrier of (V):] -defined the carrier of (V) -valued Function-like V17([: 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 non empty set
[:[: the carrier of (V), the carrier of (V):], the carrier of (V):] is non empty set
bool [:[: the carrier of (V), the carrier of (V):], the carrier of (V):] is non empty set
the multF of (V) . (((K,V,W) . x),((K,V,W) . a)) is right_complementable Element of the carrier of (V)
W . (1_ K) is right_complementable Element of the carrier of V
K is non empty right_complementable add-associative right_zeroed doubleLoopStr
the carrier of K is non empty set
V is non empty right_complementable unital right_unital well-unital left_unital add-associative right_zeroed doubleLoopStr
the carrier of V is non empty set
[: the carrier of K, the carrier of V:] is non empty set
bool [: the carrier of K, the carrier of V:] is non empty set
(V) is non empty right_complementable strict unital right_unital well-unital left_unital add-associative right_zeroed doubleLoopStr
the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the multF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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, the multF of V) is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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:]
1. V is right_complementable Element of the carrier of V
the OneF of V is right_complementable Element of the carrier of V
0. V is V46(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
doubleLoopStr(# the carrier of V, the addF of V,( the carrier of V, the carrier of V, the carrier of V, the multF of V),(1. V),(0. V) #) is non empty strict doubleLoopStr
W is non empty Relation-like the carrier of K -defined the carrier of V -valued Function-like V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of V:]
(K,V,W) is non empty Relation-like the carrier of K -defined the carrier of (V) -valued Function-like V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of (V):]
the carrier of (V) is non empty set
[: the carrier of K, the carrier of (V):] is non empty set
bool [: the carrier of K, the carrier of (V):] is non empty set
a is right_complementable Element of the carrier of K
x is right_complementable Element of the carrier of K
a + x is right_complementable Element of the carrier of K
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the addF of K . (a,x) is right_complementable Element of the carrier of K
(K,V,W) . (a + x) is right_complementable Element of the carrier of (V)
(K,V,W) . a is right_complementable Element of the carrier of (V)
(K,V,W) . x is right_complementable Element of the carrier of (V)
((K,V,W) . a) + ((K,V,W) . x) is right_complementable Element of the carrier of (V)
the addF of (V) is non empty Relation-like [: the carrier of (V), the carrier of (V):] -defined the carrier of (V) -valued Function-like V17([: 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 non empty set
[:[: the carrier of (V), the carrier of (V):], the carrier of (V):] is non empty set
bool [:[: the carrier of (V), the carrier of (V):], the carrier of (V):] is non empty set
the addF of (V) . (((K,V,W) . a),((K,V,W) . x)) is right_complementable Element of the carrier of (V)
W . a is right_complementable Element of the carrier of V
W . x is right_complementable Element of the carrier of V
(W . a) + (W . x) is right_complementable Element of the carrier of V
the addF of V . ((W . a),(W . x)) is right_complementable Element of the carrier of V
a is right_complementable Element of the carrier of K
x is right_complementable Element of the carrier of K
a * x is right_complementable Element of the carrier of K
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K . (a,x) is right_complementable Element of the carrier of K
(K,V,W) . (a * x) is right_complementable Element of the carrier of (V)
(K,V,W) . a is right_complementable Element of the carrier of (V)
(K,V,W) . x is right_complementable Element of the carrier of (V)
((K,V,W) . a) * ((K,V,W) . x) is right_complementable Element of the carrier of (V)
the multF of (V) is non empty Relation-like [: the carrier of (V), the carrier of (V):] -defined the carrier of (V) -valued Function-like V17([: 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 non empty set
[:[: the carrier of (V), the carrier of (V):], the carrier of (V):] is non empty set
bool [:[: the carrier of (V), the carrier of (V):], the carrier of (V):] is non empty set
the multF of (V) . (((K,V,W) . a),((K,V,W) . x)) is right_complementable Element of the carrier of (V)
W . x is right_complementable Element of the carrier of V
W . a is right_complementable Element of the carrier of V
(W . x) * (W . a) is right_complementable Element of the carrier of V
the multF of V . ((W . x),(W . a)) is right_complementable Element of the carrier of V
1_ K is right_complementable Element of the carrier of K
(K,V,W) . (1_ K) is right_complementable Element of the carrier of (V)
1_ V is right_complementable Element of the carrier of V
1_ (V) is right_complementable Element of the carrier of (V)
1. (V) is right_complementable Element of the carrier of (V)
the OneF of (V) is right_complementable Element of the carrier of (V)
a is right_complementable Element of the carrier of K
x is right_complementable Element of the carrier of K
a + x is right_complementable Element of the carrier of K
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the addF of K . (a,x) is right_complementable Element of the carrier of K
W . (a + x) is right_complementable Element of the carrier of V
(K,V,W) . a is right_complementable Element of the carrier of (V)
(K,V,W) . x is right_complementable Element of the carrier of (V)
((K,V,W) . a) + ((K,V,W) . x) is right_complementable Element of the carrier of (V)
the addF of (V) is non empty Relation-like [: the carrier of (V), the carrier of (V):] -defined the carrier of (V) -valued Function-like V17([: 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 non empty set
[:[: the carrier of (V), the carrier of (V):], the carrier of (V):] is non empty set
bool [:[: the carrier of (V), the carrier of (V):], the carrier of (V):] is non empty set
the addF of (V) . (((K,V,W) . a),((K,V,W) . x)) is right_complementable Element of the carrier of (V)
W . a is right_complementable Element of the carrier of V
W . x is right_complementable Element of the carrier of V
(W . a) + (W . x) is right_complementable Element of the carrier of V
the addF of V . ((W . a),(W . x)) is right_complementable Element of the carrier of V
a is right_complementable Element of the carrier of K
x is right_complementable Element of the carrier of K
a * x is right_complementable Element of the carrier of K
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: the carrier of K, the carrier of K:]) quasi_total Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
the multF of K . (a,x) is right_complementable Element of the carrier of K
W . (a * x) is right_complementable Element of the carrier of V
(K,V,W) . a is right_complementable Element of the carrier of (V)
(K,V,W) . x is right_complementable Element of the carrier of (V)
((K,V,W) . a) * ((K,V,W) . x) is right_complementable Element of the carrier of (V)
the multF of (V) is non empty Relation-like [: the carrier of (V), the carrier of (V):] -defined the carrier of (V) -valued Function-like V17([: 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 multF of (V) . (((K,V,W) . a),((K,V,W) . x)) is right_complementable Element of the carrier of (V)
W . x is right_complementable Element of the carrier of V
W . a is right_complementable Element of the carrier of V
(W . x) * (W . a) is right_complementable Element of the carrier of V
the multF of V . ((W . x),(W . a)) is right_complementable Element of the carrier of V
W . (1_ K) is right_complementable Element of the carrier of V
K is non empty right_complementable add-associative right_zeroed doubleLoopStr
the carrier of K is non empty set
V is non empty right_complementable unital right_unital well-unital left_unital add-associative right_zeroed doubleLoopStr
the carrier of V is non empty set
[: the carrier of K, the carrier of V:] is non empty set
bool [: the carrier of K, the carrier of V:] is non empty set
(V) is non empty right_complementable strict unital right_unital well-unital left_unital add-associative right_zeroed doubleLoopStr
the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the multF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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, the multF of V) is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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:]
1. V is right_complementable Element of the carrier of V
the OneF of V is right_complementable Element of the carrier of V
0. V is V46(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
doubleLoopStr(# the carrier of V, the addF of V,( the carrier of V, the carrier of V, the carrier of V, the multF of V),(1. V),(0. V) #) is non empty strict doubleLoopStr
W is non empty Relation-like the carrier of K -defined the carrier of V -valued Function-like V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of V:]
(K,V,W) is non empty Relation-like the carrier of K -defined the carrier of (V) -valued Function-like V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of (V):]
the carrier of (V) is non empty set
[: the carrier of K, the carrier of (V):] is non empty set
bool [: the carrier of K, the carrier of (V):] is non empty set
K is non empty right_complementable add-associative right_zeroed doubleLoopStr
the carrier of K is non empty set
V is non empty right_complementable unital right_unital well-unital left_unital add-associative right_zeroed doubleLoopStr
the carrier of V is non empty set
[: the carrier of K, the carrier of V:] is non empty set
bool [: the carrier of K, the carrier of V:] is non empty set
(V) is non empty right_complementable strict unital right_unital well-unital left_unital add-associative right_zeroed doubleLoopStr
the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the multF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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, the multF of V) is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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:]
1. V is right_complementable Element of the carrier of V
the OneF of V is right_complementable Element of the carrier of V
0. V is V46(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
doubleLoopStr(# the carrier of V, the addF of V,( the carrier of V, the carrier of V, the carrier of V, the multF of V),(1. V),(0. V) #) is non empty strict doubleLoopStr
W is non empty Relation-like the carrier of K -defined the carrier of V -valued Function-like V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of V:]
(K,V,W) is non empty Relation-like the carrier of K -defined the carrier of (V) -valued Function-like V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of (V):]
the carrier of (V) is non empty set
[: the carrier of K, the carrier of (V):] is non empty set
bool [: the carrier of K, the carrier of (V):] is non empty set
K is non empty right_complementable add-associative right_zeroed doubleLoopStr
the carrier of K is non empty set
V is non empty right_complementable unital right_unital well-unital left_unital add-associative right_zeroed doubleLoopStr
the carrier of V is non empty set
[: the carrier of K, the carrier of V:] is non empty set
bool [: the carrier of K, the carrier of V:] is non empty set
(V) is non empty right_complementable strict unital right_unital well-unital left_unital add-associative right_zeroed doubleLoopStr
the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the multF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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, the multF of V) is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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:]
1. V is right_complementable Element of the carrier of V
the OneF of V is right_complementable Element of the carrier of V
0. V is V46(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
doubleLoopStr(# the carrier of V, the addF of V,( the carrier of V, the carrier of V, the carrier of V, the multF of V),(1. V),(0. V) #) is non empty strict doubleLoopStr
W is non empty Relation-like the carrier of K -defined the carrier of V -valued Function-like V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of V:]
(K,V,W) is non empty Relation-like the carrier of K -defined the carrier of (V) -valued Function-like V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of (V):]
the carrier of (V) is non empty set
[: the carrier of K, the carrier of (V):] is non empty set
bool [: the carrier of K, the carrier of (V):] is non empty set
K is non empty right_complementable add-associative right_zeroed doubleLoopStr
the carrier of K is non empty set
V is non empty right_complementable unital right_unital well-unital left_unital add-associative right_zeroed doubleLoopStr
the carrier of V is non empty set
[: the carrier of K, the carrier of V:] is non empty set
bool [: the carrier of K, the carrier of V:] is non empty set
(V) is non empty right_complementable strict unital right_unital well-unital left_unital add-associative right_zeroed doubleLoopStr
the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the multF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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, the multF of V) is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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:]
1. V is right_complementable Element of the carrier of V
the OneF of V is right_complementable Element of the carrier of V
0. V is V46(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
doubleLoopStr(# the carrier of V, the addF of V,( the carrier of V, the carrier of V, the carrier of V, the multF of V),(1. V),(0. V) #) is non empty strict doubleLoopStr
W is non empty Relation-like the carrier of K -defined the carrier of V -valued Function-like V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of V:]
(K,V,W) is non empty Relation-like the carrier of K -defined the carrier of (V) -valued Function-like V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of (V):]
the carrier of (V) is non empty set
[: the carrier of K, the carrier of (V):] is non empty set
bool [: the carrier of K, the carrier of (V):] is non empty set
K is non empty right_complementable add-associative right_zeroed doubleLoopStr
the carrier of K is non empty set
V is non empty right_complementable unital right_unital well-unital left_unital add-associative right_zeroed doubleLoopStr
the carrier of V is non empty set
[: the carrier of K, the carrier of V:] is non empty set
bool [: the carrier of K, the carrier of V:] is non empty set
(V) is non empty right_complementable strict unital right_unital well-unital left_unital add-associative right_zeroed doubleLoopStr
the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the multF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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, the multF of V) is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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:]
1. V is right_complementable Element of the carrier of V
the OneF of V is right_complementable Element of the carrier of V
0. V is V46(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
doubleLoopStr(# the carrier of V, the addF of V,( the carrier of V, the carrier of V, the carrier of V, the multF of V),(1. V),(0. V) #) is non empty strict doubleLoopStr
W is non empty Relation-like the carrier of K -defined the carrier of V -valued Function-like V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of V:]
(K,V,W) is non empty Relation-like the carrier of K -defined the carrier of (V) -valued Function-like V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of (V):]
the carrier of (V) is non empty set
[: the carrier of K, the carrier of (V):] is non empty set
bool [: the carrier of K, the carrier of (V):] is non empty set
K is non empty right_complementable add-associative right_zeroed doubleLoopStr
the carrier of K is non empty set
V is non empty right_complementable unital right_unital well-unital left_unital add-associative right_zeroed doubleLoopStr
the carrier of V is non empty set
[: the carrier of K, the carrier of V:] is non empty set
bool [: the carrier of K, the carrier of V:] is non empty set
(V) is non empty right_complementable strict unital right_unital well-unital left_unital add-associative right_zeroed doubleLoopStr
the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the multF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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, the multF of V) is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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:]
1. V is right_complementable Element of the carrier of V
the OneF of V is right_complementable Element of the carrier of V
0. V is V46(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
doubleLoopStr(# the carrier of V, the addF of V,( the carrier of V, the carrier of V, the carrier of V, the multF of V),(1. V),(0. V) #) is non empty strict doubleLoopStr
W is non empty Relation-like the carrier of K -defined the carrier of V -valued Function-like V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of V:]
(K,V,W) is non empty Relation-like the carrier of K -defined the carrier of (V) -valued Function-like V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of (V):]
the carrier of (V) is non empty set
[: the carrier of K, the carrier of (V):] is non empty set
bool [: the carrier of K, the carrier of (V):] is non empty set
K is non empty right_complementable unital right_unital well-unital left_unital add-associative right_zeroed doubleLoopStr
the carrier of K is non empty set
[: the carrier of K, the carrier of K:] is non empty set
bool [: the carrier of K, the carrier of K:] is non empty set
(K) is non empty right_complementable strict unital right_unital well-unital left_unital add-associative right_zeroed doubleLoopStr
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is right_complementable Element of the carrier of K
the OneF of K is right_complementable Element of the carrier of K
0. K is V46(K) right_complementable Element of the carrier of K
the ZeroF of K is right_complementable Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty strict doubleLoopStr
V is non empty Relation-like the carrier of K -defined the carrier of K -valued Function-like V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of K:]
(K,K,V) is non empty Relation-like the carrier of K -defined the carrier of (K) -valued Function-like V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of (K):]
the carrier of (K) is non empty set
[: the carrier of K, the carrier of (K):] is non empty set
bool [: the carrier of K, the carrier of (K):] is non empty set
K is non empty right_complementable unital right_unital well-unital left_unital add-associative right_zeroed doubleLoopStr
the carrier of K is non empty set
[: the carrier of K, the carrier of K:] is non empty set
bool [: the carrier of K, the carrier of K:] is non empty set
(K) is non empty right_complementable strict unital right_unital well-unital left_unital add-associative right_zeroed doubleLoopStr
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is right_complementable Element of the carrier of K
the OneF of K is right_complementable Element of the carrier of K
0. K is V46(K) right_complementable Element of the carrier of K
the ZeroF of K is right_complementable Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty strict doubleLoopStr
V is non empty Relation-like the carrier of K -defined the carrier of K -valued Function-like V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of K:]
(K,K,V) is non empty Relation-like the carrier of K -defined the carrier of (K) -valued Function-like V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of (K):]
the carrier of (K) is non empty set
[: the carrier of K, the carrier of (K):] is non empty set
bool [: the carrier of K, the carrier of (K):] is non empty set
K is non empty right_complementable unital right_unital well-unital left_unital add-associative right_zeroed doubleLoopStr
the carrier of K is non empty set
[: the carrier of K, the carrier of K:] is non empty set
bool [: the carrier of K, the carrier of K:] is non empty set
W is non empty right_complementable unital right_unital well-unital left_unital add-associative right_zeroed doubleLoopStr
the carrier of W is non empty set
[: the carrier of W, the carrier of W:] is non empty set
bool [: the carrier of W, the carrier of W:] is non empty set
V is non empty Relation-like the carrier of K -defined the carrier of K -valued Function-like V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of K:]
(K) is non empty right_complementable strict unital right_unital well-unital left_unital add-associative right_zeroed doubleLoopStr
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is right_complementable Element of the carrier of K
the OneF of K is right_complementable Element of the carrier of K
0. K is V46(K) right_complementable Element of the carrier of K
the ZeroF of K is right_complementable Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty strict doubleLoopStr
(K,K,V) is non empty Relation-like the carrier of K -defined the carrier of (K) -valued Function-like V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of (K):]
the carrier of (K) is non empty set
[: the carrier of K, the carrier of (K):] is non empty set
bool [: the carrier of K, the carrier of (K):] is non empty set
(W) is non empty right_complementable strict unital right_unital well-unital left_unital add-associative right_zeroed doubleLoopStr
the addF of W is non empty Relation-like [: the carrier of W, the carrier of W:] -defined the carrier of W -valued Function-like V17([: the carrier of W, the carrier of W:]) quasi_total Element of bool [:[: the carrier of W, the carrier of W:], the carrier of W:]
[:[: the carrier of W, the carrier of W:], the carrier of W:] is non empty set
bool [:[: the carrier of W, the carrier of W:], the carrier of W:] is non empty set
the multF of W is non empty Relation-like [: the carrier of W, the carrier of W:] -defined the carrier of W -valued Function-like V17([: the carrier of W, the carrier of W:]) quasi_total Element of bool [:[: the carrier of W, the carrier of W:], the carrier of W:]
( the carrier of W, the carrier of W, the carrier of W, the multF of W) is non empty Relation-like [: the carrier of W, the carrier of W:] -defined the carrier of W -valued Function-like V17([: 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:]
1. W is right_complementable Element of the carrier of W
the OneF of W is right_complementable Element of the carrier of W
0. W is V46(W) right_complementable Element of the carrier of W
the ZeroF of W is right_complementable Element of the carrier of W
doubleLoopStr(# the carrier of W, the addF of W,( the carrier of W, the carrier of W, the carrier of W, the multF of W),(1. W),(0. W) #) is non empty strict doubleLoopStr
f is non empty Relation-like the carrier of W -defined the carrier of W -valued Function-like V17( the carrier of W) quasi_total Element of bool [: the carrier of W, the carrier of W:]
(W,W,f) is non empty Relation-like the carrier of W -defined the carrier of (W) -valued Function-like V17( the carrier of W) quasi_total Element of bool [: the carrier of W, the carrier of (W):]
the carrier of (W) is non empty set
[: the carrier of W, the carrier of (W):] is non empty set
bool [: the carrier of W, the carrier of (W):] is non empty set
K is non empty right_complementable unital right_unital well-unital left_unital add-associative right_zeroed doubleLoopStr
the carrier of K is non empty set
[: the carrier of K, the carrier of K:] is non empty set
bool [: the carrier of K, the carrier of K:] is non empty set
W is non empty right_complementable unital right_unital well-unital left_unital add-associative right_zeroed doubleLoopStr
the carrier of W is non empty set
[: the carrier of W, the carrier of W:] is non empty set
bool [: the carrier of W, the carrier of W:] is non empty set
V is non empty Relation-like the carrier of K -defined the carrier of K -valued Function-like V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of K:]
(K) is non empty right_complementable strict unital right_unital well-unital left_unital add-associative right_zeroed doubleLoopStr
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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, the carrier of K, the multF of K) is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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:]
1. K is right_complementable Element of the carrier of K
the OneF of K is right_complementable Element of the carrier of K
0. K is V46(K) right_complementable Element of the carrier of K
the ZeroF of K is right_complementable Element of the carrier of K
doubleLoopStr(# the carrier of K, the addF of K,( the carrier of K, the carrier of K, the carrier of K, the multF of K),(1. K),(0. K) #) is non empty strict doubleLoopStr
(K,K,V) is non empty Relation-like the carrier of K -defined the carrier of (K) -valued Function-like V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of (K):]
the carrier of (K) is non empty set
[: the carrier of K, the carrier of (K):] is non empty set
bool [: the carrier of K, the carrier of (K):] is non empty set
(W) is non empty right_complementable strict unital right_unital well-unital left_unital add-associative right_zeroed doubleLoopStr
the addF of W is non empty Relation-like [: the carrier of W, the carrier of W:] -defined the carrier of W -valued Function-like V17([: the carrier of W, the carrier of W:]) quasi_total Element of bool [:[: the carrier of W, the carrier of W:], the carrier of W:]
[:[: the carrier of W, the carrier of W:], the carrier of W:] is non empty set
bool [:[: the carrier of W, the carrier of W:], the carrier of W:] is non empty set
the multF of W is non empty Relation-like [: the carrier of W, the carrier of W:] -defined the carrier of W -valued Function-like V17([: the carrier of W, the carrier of W:]) quasi_total Element of bool [:[: the carrier of W, the carrier of W:], the carrier of W:]
( the carrier of W, the carrier of W, the carrier of W, the multF of W) is non empty Relation-like [: the carrier of W, the carrier of W:] -defined the carrier of W -valued Function-like V17([: 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:]
1. W is right_complementable Element of the carrier of W
the OneF of W is right_complementable Element of the carrier of W
0. W is V46(W) right_complementable Element of the carrier of W
the ZeroF of W is right_complementable Element of the carrier of W
doubleLoopStr(# the carrier of W, the addF of W,( the carrier of W, the carrier of W, the carrier of W, the multF of W),(1. W),(0. W) #) is non empty strict doubleLoopStr
f is non empty Relation-like the carrier of W -defined the carrier of W -valued Function-like V17( the carrier of W) quasi_total Element of bool [: the carrier of W, the carrier of W:]
(W,W,f) is non empty Relation-like the carrier of W -defined the carrier of (W) -valued Function-like V17( the carrier of W) quasi_total Element of bool [: the carrier of W, the carrier of (W):]
the carrier of (W) is non empty set
[: the carrier of W, the carrier of (W):] is non empty set
bool [: the carrier of W, the carrier of (W):] is non empty set
K is non empty right_complementable add-associative right_zeroed addLoopStr
the carrier of K is non empty set
[: the carrier of K, the carrier of K:] is non empty set
bool [: the carrier of K, the carrier of K:] is non empty set
id K is non empty Relation-like the carrier of K -defined the carrier of K -valued Function-like one-to-one V17( the carrier of K) quasi_total onto bijective additive Element of bool [: the carrier of K, the carrier of K:]
K97( the carrier of K) is non empty Relation-like the carrier of K -defined the carrier of K -valued Function-like one-to-one V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of K:]
K is non empty right_complementable add-associative right_zeroed addLoopStr
the carrier of K is non empty set
0. K is V46(K) right_complementable Element of the carrier of K
the ZeroF of K is right_complementable Element of the carrier of K
V is non empty right_complementable add-associative right_zeroed addLoopStr
the carrier of V is non empty set
[: the carrier of K, the carrier of V:] is non empty set
bool [: the carrier of K, the carrier of V:] is non empty set
0. V is V46(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
W is non empty Relation-like the carrier of K -defined the carrier of V -valued Function-like V17( the carrier of K) quasi_total additive Element of bool [: the carrier of K, the carrier of V:]
W . (0. K) is right_complementable Element of the carrier of V
(0. K) + (0. K) is right_complementable Element of the carrier of K
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the addF of K . ((0. K),(0. K)) is right_complementable Element of the carrier of K
(W . (0. K)) + (W . (0. K)) is right_complementable Element of the carrier of V
the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . ((W . (0. K)),(W . (0. K))) is right_complementable Element of the carrier of V
(W . (0. K)) + (0. V) is right_complementable Element of the carrier of V
the addF of V . ((W . (0. K)),(0. V)) is right_complementable Element of the carrier of V
K is non empty right_complementable add-associative right_zeroed addLoopStr
the carrier of K is non empty set
V is non empty right_complementable add-associative right_zeroed addLoopStr
the carrier of V is non empty set
[: the carrier of V, the carrier of K:] is non empty set
bool [: the carrier of V, the carrier of K:] is non empty set
W is non empty Relation-like the carrier of V -defined the carrier of K -valued Function-like V17( the carrier of V) quasi_total additive Element of bool [: the carrier of V, the carrier of K:]
f is right_complementable Element of the carrier of V
- f is right_complementable Element of the carrier of V
W . (- f) is right_complementable Element of the carrier of K
W . f is right_complementable Element of the carrier of K
- (W . f) is right_complementable Element of the carrier of K
0. V is V46(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
0. K is V46(K) right_complementable Element of the carrier of K
the ZeroF of K is right_complementable Element of the carrier of K
f + (- f) is right_complementable Element of the carrier of V
the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . (f,(- f)) is right_complementable Element of the carrier of V
(W . f) + (W . (- f)) is right_complementable Element of the carrier of K
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the addF of K . ((W . f),(W . (- f))) is right_complementable Element of the carrier of K
W . (0. V) is right_complementable Element of the carrier of K
K is non empty right_complementable add-associative right_zeroed addLoopStr
the carrier of K is non empty set
V is non empty right_complementable add-associative right_zeroed addLoopStr
the carrier of V is non empty set
[: the carrier of V, the carrier of K:] is non empty set
bool [: the carrier of V, the carrier of K:] is non empty set
W is non empty Relation-like the carrier of V -defined the carrier of K -valued Function-like V17( the carrier of V) quasi_total additive Element of bool [: the carrier of V, the carrier of K:]
f is right_complementable Element of the carrier of V
W . f is right_complementable Element of the carrier of K
J is right_complementable Element of the carrier of V
f - J is right_complementable Element of the carrier of V
- J is right_complementable Element of the carrier of V
f + (- J) is right_complementable Element of the carrier of V
the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . (f,(- J)) is right_complementable Element of the carrier of V
W . (f - J) is right_complementable Element of the carrier of K
W . J is right_complementable Element of the carrier of K
(W . f) - (W . J) is right_complementable Element of the carrier of K
- (W . J) is right_complementable Element of the carrier of K
(W . f) + (- (W . J)) is right_complementable Element of the carrier of K
the addF of K is non empty Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the addF of K . ((W . f),(- (W . J))) is right_complementable Element of the carrier of K
W . (- J) is right_complementable Element of the carrier of K
(W . f) + (W . (- J)) is right_complementable Element of the carrier of K
the addF of K . ((W . f),(W . (- J))) is right_complementable Element of the carrier of K
K is non empty right_complementable add-associative right_zeroed addLoopStr
the carrier of K is non empty set
V is non empty right_complementable add-associative right_zeroed addLoopStr
the carrier of V is non empty set
[: the carrier of K, the carrier of V:] is non empty set
bool [: the carrier of K, the carrier of V:] is non empty set
f is non empty right_complementable add-associative right_zeroed addLoopStr
the carrier of f is non empty set
J is non empty right_complementable add-associative right_zeroed addLoopStr
the carrier of J is non empty set
[: the carrier of f, the carrier of J:] is non empty set
bool [: the carrier of f, the carrier of J:] is non empty set
z is non empty right_complementable add-associative right_zeroed addLoopStr
the carrier of z is non empty set
p is non empty right_complementable add-associative right_zeroed addLoopStr
the carrier of p is non empty set
[: the carrier of z, the carrier of p:] is non empty set
bool [: the carrier of z, the carrier of p:] is non empty set
W is non empty Relation-like the carrier of K -defined the carrier of V -valued Function-like V17( the carrier of K) quasi_total additive Element of bool [: the carrier of K, the carrier of V:]
0. K is V46(K) right_complementable Element of the carrier of K
the ZeroF of K is right_complementable Element of the carrier of K
W . (0. K) is right_complementable Element of the carrier of V
0. V is V46(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
a is non empty Relation-like the carrier of f -defined the carrier of J -valued Function-like V17( the carrier of f) quasi_total additive Element of bool [: the carrier of f, the carrier of J:]
x is right_complementable Element of the carrier of f
- x is right_complementable Element of the carrier of f
a . (- x) is right_complementable Element of the carrier of J
a . x is right_complementable Element of the carrier of J
- (a . x) is right_complementable Element of the carrier of J
q is non empty Relation-like the carrier of z -defined the carrier of p -valued Function-like V17( the carrier of z) quasi_total additive Element of bool [: the carrier of z, the carrier of p:]
a is right_complementable Element of the carrier of z
b is right_complementable Element of the carrier of z
a - b is right_complementable Element of the carrier of z
- b is right_complementable Element of the carrier of z
a + (- b) is right_complementable Element of the carrier of z
the addF of z is non empty Relation-like [: the carrier of z, the carrier of z:] -defined the carrier of z -valued Function-like V17([: the carrier of z, the carrier of z:]) quasi_total Element of bool [:[: the carrier of z, the carrier of z:], the carrier of z:]
[: the carrier of z, the carrier of z:] is non empty set
[:[: the carrier of z, the carrier of z:], the carrier of z:] is non empty set
bool [:[: the carrier of z, the carrier of z:], the carrier of z:] is non empty set
the addF of z . (a,(- b)) is right_complementable Element of the carrier of z
q . (a - b) is right_complementable Element of the carrier of p
q . a is right_complementable Element of the carrier of p
q . b is right_complementable Element of the carrier of p
(q . a) - (q . b) is right_complementable Element of the carrier of p
- (q . b) is right_complementable Element of the carrier of p
(q . a) + (- (q . b)) is right_complementable Element of the carrier of p
the addF of p is non empty Relation-like [: the carrier of p, the carrier of p:] -defined the carrier of p -valued Function-like V17([: the carrier of p, the carrier of p:]) quasi_total Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]
[: the carrier of p, the carrier of p:] is non empty set
[:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set
bool [:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set
the addF of p . ((q . a),(- (q . b))) is right_complementable Element of the carrier of p
K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
W is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K
the carrier of W is non empty set
f is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over V
the carrier of f is non empty set
ZeroMap (W,f) is non empty Relation-like the carrier of W -defined the carrier of f -valued Function-like V17( the carrier of W) quasi_total additive Element of bool [: the carrier of W, the carrier of f:]
[: the carrier of W, the carrier of f:] is non empty set
bool [: the carrier of W, the carrier of f:] is non empty set
0. f is V46(f) right_complementable Element of the carrier of f
the ZeroF of f is right_complementable Element of the carrier of f
K379( the carrier of f, the carrier of W,(0. f)) is non empty Relation-like the carrier of W -defined the carrier of f -valued Function-like V17( the carrier of W) quasi_total Element of bool [: the carrier of W, the carrier of f:]
a is right_complementable Element of the carrier of W
x is right_complementable Element of the carrier of W
a + x is right_complementable Element of the carrier of W
the addF of W is non empty Relation-like [: the carrier of W, the carrier of W:] -defined the carrier of W -valued Function-like V17([: 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 non empty set
[:[: the carrier of W, the carrier of W:], the carrier of W:] is non empty set
bool [:[: the carrier of W, the carrier of W:], the carrier of W:] is non empty set
the addF of W . (a,x) is right_complementable Element of the carrier of W
(ZeroMap (W,f)) . (a + x) is right_complementable Element of the carrier of f
(ZeroMap (W,f)) . a is right_complementable Element of the carrier of f
(ZeroMap (W,f)) . x is right_complementable Element of the carrier of f
((ZeroMap (W,f)) . a) + ((ZeroMap (W,f)) . x) is right_complementable Element of the carrier of f
the addF of f is non empty Relation-like [: the carrier of f, the carrier of f:] -defined the carrier of f -valued Function-like V17([: 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 non empty set
[:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
bool [:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
the addF of f . (((ZeroMap (W,f)) . a),((ZeroMap (W,f)) . x)) is right_complementable Element of the carrier of f
K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of K is non empty set
V is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of V is non empty set
[: the carrier of V, the carrier of K:] is non empty set
bool [: the carrier of V, the carrier of K:] is non empty set
W is non empty Relation-like the carrier of V -defined the carrier of K -valued Function-like V17( the carrier of V) quasi_total Element of bool [: the carrier of V, the carrier of K:]
f is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over V
the carrier of f is non empty set
J is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K
the carrier of J is non empty set
ZeroMap (f,J) is non empty Relation-like the carrier of f -defined the carrier of J -valued Function-like V17( the carrier of f) quasi_total additive Element of bool [: the carrier of f, the carrier of J:]
[: the carrier of f, the carrier of J:] is non empty set
bool [: the carrier of f, the carrier of J:] is non empty set
0. J is V46(J) right_complementable Element of the carrier of J
the ZeroF of J is right_complementable Element of the carrier of J
K379( the carrier of J, the carrier of f,(0. J)) is non empty Relation-like the carrier of f -defined the carrier of J -valued Function-like V17( the carrier of f) quasi_total Element of bool [: the carrier of f, the carrier of J:]
a is right_complementable Element of the carrier of V
W . a is right_complementable Element of the carrier of K
x is right_complementable Element of the carrier of f
a * x is right_complementable Element of the carrier of f
the lmult of f is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of f -valued Function-like V17([: the carrier of V, the carrier of f:]) quasi_total Element of bool [:[: the carrier of V, the carrier of f:], the carrier of f:]
[: the carrier of V, the carrier of f:] is non empty set
[:[: the carrier of V, the carrier of f:], the carrier of f:] is non empty set
bool [:[: the carrier of V, the carrier of f:], the carrier of f:] is non empty set
the lmult of f . (a,x) is right_complementable Element of the carrier of f
(ZeroMap (f,J)) . (a * x) is right_complementable Element of the carrier of J
(ZeroMap (f,J)) . x is right_complementable Element of the carrier of J
(W . a) * ((ZeroMap (f,J)) . x) is right_complementable Element of the carrier of J
the lmult of J is non empty Relation-like [: the carrier of K, the carrier of J:] -defined the carrier of J -valued Function-like V17([: the carrier of K, the carrier of J:]) quasi_total Element of bool [:[: the carrier of K, the carrier of J:], the carrier of J:]
[: the carrier of K, the carrier of J:] is non empty set
[:[: the carrier of K, the carrier of J:], the carrier of J:] is non empty set
bool [:[: the carrier of K, the carrier of J:], the carrier of J:] is non empty set
the lmult of J . ((W . a),((ZeroMap (f,J)) . x)) is right_complementable Element of the carrier of J
K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of K is non empty set
V is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of V is non empty set
[: the carrier of K, the carrier of V:] is non empty set
bool [: the carrier of K, the carrier of V:] is non empty set
f is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K
the carrier of f is non empty set
J is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over V
the carrier of J is non empty set
[: the carrier of f, the carrier of J:] is non empty set
bool [: the carrier of f, the carrier of J:] is non empty set
W is non empty Relation-like the carrier of K -defined the carrier of V -valued Function-like V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of V:]
ZeroMap (f,J) is non empty Relation-like the carrier of f -defined the carrier of J -valued Function-like V17( the carrier of f) quasi_total additive Element of bool [: the carrier of f, the carrier of J:]
0. J is V46(J) right_complementable Element of the carrier of J
the ZeroF of J is right_complementable Element of the carrier of J
K379( the carrier of J, the carrier of f,(0. J)) is non empty Relation-like the carrier of f -defined the carrier of J -valued Function-like V17( the carrier of f) quasi_total Element of bool [: the carrier of f, the carrier of J:]
a is right_complementable Element of the carrier of f
x is right_complementable Element of the carrier of f
a + x is right_complementable Element of the carrier of f
the addF of f is non empty Relation-like [: the carrier of f, the carrier of f:] -defined the carrier of f -valued Function-like V17([: 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 non empty set
[:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
bool [:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
the addF of f . (a,x) is right_complementable Element of the carrier of f
(ZeroMap (f,J)) . (a + x) is right_complementable Element of the carrier of J
(ZeroMap (f,J)) . a is right_complementable Element of the carrier of J
(ZeroMap (f,J)) . x is right_complementable Element of the carrier of J
((ZeroMap (f,J)) . a) + ((ZeroMap (f,J)) . x) is right_complementable Element of the carrier of J
the addF of J is non empty Relation-like [: the carrier of J, the carrier of J:] -defined the carrier of J -valued Function-like V17([: the carrier of J, the carrier of J:]) quasi_total Element of bool [:[: the carrier of J, the carrier of J:], the carrier of J:]
[: the carrier of J, the carrier of J:] is non empty set
[:[: the carrier of J, the carrier of J:], the carrier of J:] is non empty set
bool [:[: the carrier of J, the carrier of J:], the carrier of J:] is non empty set
the addF of J . (((ZeroMap (f,J)) . a),((ZeroMap (f,J)) . x)) is right_complementable Element of the carrier of J
z is right_complementable Element of the carrier of K
p is right_complementable Element of the carrier of f
z * p is right_complementable Element of the carrier of f
the lmult of f is non empty Relation-like [: the carrier of K, the carrier of f:] -defined the carrier of f -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of f:], the carrier of f:] is non empty set
bool [:[: the carrier of K, the carrier of f:], the carrier of f:] is non empty set
the lmult of f . (z,p) is right_complementable Element of the carrier of f
(ZeroMap (f,J)) . (z * p) is right_complementable Element of the carrier of J
W . z is right_complementable Element of the carrier of V
(ZeroMap (f,J)) . p is right_complementable Element of the carrier of J
(W . z) * ((ZeroMap (f,J)) . p) is right_complementable Element of the carrier of J
the lmult of J is non empty Relation-like [: the carrier of V, the carrier of J:] -defined the carrier of J -valued Function-like V17([: the carrier of V, the carrier of J:]) quasi_total Element of bool [:[: the carrier of V, the carrier of J:], the carrier of J:]
[: the carrier of V, the carrier of J:] is non empty set
[:[: the carrier of V, the carrier of J:], the carrier of J:] is non empty set
bool [:[: the carrier of V, the carrier of J:], the carrier of J:] is non empty set
the lmult of J . ((W . z),((ZeroMap (f,J)) . p)) is right_complementable Element of the carrier of J
K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of K is non empty set
V is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of V is non empty set
[: the carrier of K, the carrier of V:] is non empty set
bool [: the carrier of K, the carrier of V:] is non empty set
W is non empty Relation-like the carrier of K -defined the carrier of V -valued Function-like V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of V:]
f is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K
the carrier of f is non empty set
J is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over V
ZeroMap (f,J) is non empty Relation-like the carrier of f -defined the carrier of J -valued Function-like V17( the carrier of f) quasi_total additive Element of bool [: the carrier of f, the carrier of J:]
the carrier of J is non empty set
[: the carrier of f, the carrier of J:] is non empty set
bool [: the carrier of f, the carrier of J:] is non empty set
0. J is V46(J) right_complementable Element of the carrier of J
the ZeroF of J is right_complementable Element of the carrier of J
K379( the carrier of J, the carrier of f,(0. J)) is non empty Relation-like the carrier of f -defined the carrier of J -valued Function-like V17( the carrier of f) quasi_total Element of bool [: the carrier of f, the carrier of J:]
x is right_complementable Element of the carrier of f
z is right_complementable Element of the carrier of f
x + z is right_complementable Element of the carrier of f
the addF of f is non empty Relation-like [: the carrier of f, the carrier of f:] -defined the carrier of f -valued Function-like V17([: 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 non empty set
[:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
bool [:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
the addF of f . (x,z) is right_complementable Element of the carrier of f
(ZeroMap (f,J)) . (x + z) is right_complementable Element of the carrier of J
(ZeroMap (f,J)) . x is right_complementable Element of the carrier of J
(ZeroMap (f,J)) . z is right_complementable Element of the carrier of J
((ZeroMap (f,J)) . x) + ((ZeroMap (f,J)) . z) is right_complementable Element of the carrier of J
the addF of J is non empty Relation-like [: the carrier of J, the carrier of J:] -defined the carrier of J -valued Function-like V17([: the carrier of J, the carrier of J:]) quasi_total Element of bool [:[: the carrier of J, the carrier of J:], the carrier of J:]
[: the carrier of J, the carrier of J:] is non empty set
[:[: the carrier of J, the carrier of J:], the carrier of J:] is non empty set
bool [:[: the carrier of J, the carrier of J:], the carrier of J:] is non empty set
the addF of J . (((ZeroMap (f,J)) . x),((ZeroMap (f,J)) . z)) is right_complementable Element of the carrier of J
p is right_complementable Element of the carrier of K
q is right_complementable Element of the carrier of f
p * q is right_complementable Element of the carrier of f
the lmult of f is non empty Relation-like [: the carrier of K, the carrier of f:] -defined the carrier of f -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of f:], the carrier of f:] is non empty set
bool [:[: the carrier of K, the carrier of f:], the carrier of f:] is non empty set
the lmult of f . (p,q) is right_complementable Element of the carrier of f
(ZeroMap (f,J)) . (p * q) is right_complementable Element of the carrier of J
W . p is right_complementable Element of the carrier of V
(ZeroMap (f,J)) . q is right_complementable Element of the carrier of J
(W . p) * ((ZeroMap (f,J)) . q) is right_complementable Element of the carrier of J
the lmult of J is non empty Relation-like [: the carrier of V, the carrier of J:] -defined the carrier of J -valued Function-like V17([: the carrier of V, the carrier of J:]) quasi_total Element of bool [:[: the carrier of V, the carrier of J:], the carrier of J:]
[: the carrier of V, the carrier of J:] is non empty set
[:[: the carrier of V, the carrier of J:], the carrier of J:] is non empty set
bool [:[: the carrier of V, the carrier of J:], the carrier of J:] is non empty set
the lmult of J . ((W . p),((ZeroMap (f,J)) . q)) is right_complementable Element of the carrier of J
K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of K is non empty set
[: the carrier of K, the carrier of K:] is non empty set
bool [: the carrier of K, the carrier of K:] is non empty set
K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
id K is non empty Relation-like the carrier of K -defined the carrier of K -valued Function-like one-to-one V17( the carrier of K) quasi_total onto bijective unity-preserving additive multiplicative linear (K,K) Element of bool [: the carrier of K, the carrier of K:]
the carrier of K is non empty set
[: the carrier of K, the carrier of K:] is non empty set
bool [: the carrier of K, the carrier of K:] is non empty set
K97( the carrier of K) is non empty Relation-like the carrier of K -defined the carrier of K -valued Function-like one-to-one V17( the carrier of K) quasi_total Element of bool [: the carrier of K, the carrier of K:]
V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K
the carrier of V is non empty set
W is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K
the carrier of W is non empty set
[: the carrier of V, the carrier of W:] is non empty set
bool [: the carrier of V, the carrier of W:] is non empty set
f is non empty Relation-like the carrier of V -defined the carrier of W -valued Function-like V17( the carrier of V) quasi_total Element of bool [: the carrier of V, the carrier of W:]
a is right_complementable Element of the carrier of K
(id K) . a is right_complementable Element of the carrier of K
x is right_complementable Element of the carrier of V
a * x is right_complementable Element of the carrier of V
the lmult of V is non empty Relation-like [: the carrier of K, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set
the lmult of V . (a,x) is right_complementable Element of the carrier of V
f . (a * x) is right_complementable Element of the carrier of W
f . x is right_complementable Element of the carrier of W
((id K) . a) * (f . x) is right_complementable Element of the carrier of W
the lmult of W is non empty Relation-like [: the carrier of K, the carrier of W:] -defined the carrier of W -valued Function-like V17([: the carrier of K, the carrier of W:]) quasi_total Element of bool [:[: the carrier of K, the carrier of W:], the carrier of W:]
[: the carrier of K, the carrier of W:] is non empty set
[:[: the carrier of K, the carrier of W:], the carrier of W:] is non empty set
bool [:[: the carrier of K, the carrier of W:], the carrier of W:] is non empty set
the lmult of W . (((id K) . a),(f . x)) is right_complementable Element of the carrier of W
a is right_complementable Element of the carrier of K
(id K) . a is right_complementable Element of the carrier of K
x is right_complementable Element of the carrier of V
a * x is right_complementable Element of the carrier of V
the lmult of V . (a,x) is right_complementable Element of the carrier of V
f . (a * x) is right_complementable Element of the carrier of W
f . x is right_complementable Element of the carrier of W
a * (f . x) is right_complementable Element of the carrier of W
the lmult of W . (a,(f . x)) is right_complementable Element of the carrier of W
a is right_complementable Element of the carrier of V
x is right_complementable Element of the carrier of V
a + x is right_complementable Element of the carrier of V
the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . (a,x) is right_complementable Element of the carrier of V
f . (a + x) is right_complementable Element of the carrier of W
f . a is right_complementable Element of the carrier of W
f . x is right_complementable Element of the carrier of W
(f . a) + (f . x) is right_complementable Element of the carrier of W
the addF of W is non empty Relation-like [: the carrier of W, the carrier of W:] -defined the carrier of W -valued Function-like V17([: 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 non empty set
[:[: the carrier of W, the carrier of W:], the carrier of W:] is non empty set
bool [:[: the carrier of W, the carrier of W:], the carrier of W:] is non empty set
the addF of W . ((f . a),(f . x)) is right_complementable Element of the carrier of W
z is right_complementable Element of the carrier of K
p is right_complementable Element of the carrier of V
z * p is right_complementable Element of the carrier of V
the lmult of V . (z,p) is right_complementable Element of the carrier of V
f . (z * p) is right_complementable Element of the carrier of W
f . p is right_complementable Element of the carrier of W
z * (f . p) is right_complementable Element of the carrier of W
the lmult of W . (z,(f . p)) is right_complementable Element of the carrier of W
q is right_complementable Element of the carrier of K
a is right_complementable Element of the carrier of V
q * a is right_complementable Element of the carrier of V
the lmult of V . (q,a) is right_complementable Element of the carrier of V
f . (q * a) is right_complementable Element of the carrier of W
(id K) . q is right_complementable Element of the carrier of K
f . a is right_complementable Element of the carrier of W
((id K) . q) * (f . a) is right_complementable Element of the carrier of W
the lmult of W . (((id K) . q),(f . a)) is right_complementable Element of the carrier of W
b is right_complementable Element of the carrier of K
c₁₃ is right_complementable Element of the carrier of V
b * c₁₃ is right_complementable Element of the carrier of V
the lmult of V . (b,c₁₃) is right_complementable Element of the carrier of V
f . (b * c₁₃) is right_complementable Element of the carrier of W
f . c₁₃ is right_complementable Element of the carrier of W
b * (f . c₁₃) is right_complementable Element of the carrier of W
the lmult of W . (b,(f . c₁₃)) is right_complementable Element of the carrier of W
K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr