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