:: MODCAT_1 semantic presentation

K132() is Element of bool K128()

K128() is set

bool K128() is set

K47() is set

bool K47() is set

bool K132() is set

{} is empty set

1 is non empty set

{{},1} is non empty set

K133() is empty Element of K132()

2 is non empty set

K266(K133(),1,2) is set

[:K266(K133(),1,2),K266(K133(),1,2):] is set

[:[:K266(K133(),1,2),K266(K133(),1,2):],K266(K133(),1,2):] is set

bool [:[:K266(K133(),1,2),K266(K133(),1,2):],K266(K133(),1,2):] is set

bool [:K266(K133(),1,2),K266(K133(),1,2):] is set

[:1,1:] is set

bool [:1,1:] is set

[:[:1,1:],1:] is set

bool [:[:1,1:],1:] is set

Trivial-addLoopStr is addLoopStr

op2 is Relation-like [:1,1:] -defined 1 -valued V6() total quasi_total Element of bool [:[:1,1:],1:]

op0 is empty Element of 1

addLoopStr(# 1,op2,op0 #) is strict addLoopStr

UN is non empty right_complementable V96() V97() V98() V138() well-unital V146() doubleLoopStr

TrivialLMod UN is non empty right_complementable V96() V97() V98() strict V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

{(TrivialLMod UN)} is non empty set

C is Element of {(TrivialLMod UN)}

UN is non empty right_complementable V96() V97() V98() V138() well-unital V146() doubleLoopStr

R is non empty (UN)

C is Element of R

UN is non empty right_complementable V96() V97() V98() V138() well-unital V146() doubleLoopStr

R is non empty (UN)

the non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) (UN,R) is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

UN is non empty right_complementable V96() V97() V98() V138() well-unital V146() doubleLoopStr

the non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

ID the non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN is strict LModMorphism-like Morphism of the non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN, the non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

{(ID the non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN)} is non empty set

C is Element of {(ID the non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN)}

UN is non empty right_complementable V96() V97() V98() V138() well-unital V146() doubleLoopStr

R is non empty (UN)

C is Element of R

UN is non empty right_complementable V96() V97() V98() V138() well-unital V146() doubleLoopStr

R is non empty (UN)

the LModMorphism-like (UN,R) is LModMorphism-like (UN,R)

UN is non empty right_complementable V96() V97() V98() V138() well-unital V146() doubleLoopStr

R is strict LModMorphism-like LModMorphismStr over UN

{R} is non empty set

C is Element of {R}

UN is non empty right_complementable V96() V97() V98() V138() well-unital V146() doubleLoopStr

R is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

C is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

ZERO (R,C) is strict LModMorphism-like Morphism of R,C

{(ZERO (R,C))} is non empty set

a is non empty (UN)

G is LModMorphism-like (UN,a)

UN is non empty set

R is non empty right_complementable V96() V97() V98() V138() well-unital V146() doubleLoopStr

C is non empty right_complementable V96() V97() V98() V149(R) V150(R) V151(R) V152(R) VectSpStr over R

a is non empty right_complementable V96() V97() V98() V149(R) V150(R) V151(R) V152(R) VectSpStr over R

G is Element of UN

G is Element of UN

G is non empty (R)

x is LModMorphism-like (R,G)

UN is non empty right_complementable V96() V97() V98() V138() well-unital V146() doubleLoopStr

R is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

C is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

a is strict LModMorphism-like Morphism of R,C

{a} is non empty set

G is Element of {a}

UN is non empty right_complementable V96() V97() V98() V138() well-unital V146() doubleLoopStr

R is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

C is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

ZeroMap (R,C) is Relation-like the carrier of R -defined the carrier of C -valued V6() non empty total quasi_total additive homogeneous Element of bool [: the carrier of R, the carrier of C:]

the carrier of R is non empty set

the carrier of C is non empty set

[: the carrier of R, the carrier of C:] is set

bool [: the carrier of R, the carrier of C:] is set

Funcs ( the carrier of R, the carrier of C) is V9() non empty FUNCTION_DOMAIN of the carrier of R, the carrier of C

Maps (R,C) is non empty MapsSet of R,C

{ LModMorphismStr(# R,C,b

a is Relation-like the carrier of R -defined the carrier of C -valued V6() total quasi_total Element of Maps (R,C)

LModMorphismStr(# R,C,a #) is strict LModMorphismStr over UN

x is non empty set

ii is set

x1 is strict LModMorphism-like Morphism of R,C

dom x1 is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

the Dom of x1 is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

cod x1 is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

the Cod of x1 is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

the Fun of x1 is Relation-like the carrier of the Dom of x1 -defined the carrier of the Cod of x1 -valued V6() non empty total quasi_total Element of bool [: the carrier of the Dom of x1, the carrier of the Cod of x1:]

the carrier of the Dom of x1 is non empty set

the carrier of the Cod of x1 is non empty set

[: the carrier of the Dom of x1, the carrier of the Cod of x1:] is set

bool [: the carrier of the Dom of x1, the carrier of the Cod of x1:] is set

x2 is Relation-like the carrier of R -defined the carrier of C -valued V6() non empty total quasi_total Element of bool [: the carrier of R, the carrier of C:]

G is Relation-like the carrier of R -defined the carrier of C -valued V6() total quasi_total Element of Maps (R,C)

LModMorphismStr(# R,C,G #) is strict LModMorphismStr over UN

ii is set

x1 is Relation-like the carrier of R -defined the carrier of C -valued V6() total quasi_total Element of Maps (R,C)

LModMorphismStr(# R,C,x1 #) is strict LModMorphismStr over UN

ii is Element of x

ii is non empty (UN,R,C)

x1 is set

x2 is set

a is non empty (UN,R,C)

G is non empty (UN,R,C)

x is set

UN is non empty right_complementable V96() V97() V98() V138() well-unital V146() doubleLoopStr

R is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

C is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

a is non empty (UN,R,C)

G is Element of a

UN is non empty right_complementable V96() V97() V98() V138() well-unital V146() doubleLoopStr

R is set

C is set

a is set

G is set

x is set

[G,x] is set

ii is non empty right_complementable V96() V97() V98() strict V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

the carrier of ii is non empty set

the addF of ii is Relation-like [: the carrier of ii, the carrier of ii:] -defined the carrier of ii -valued V6() total quasi_total Element of bool [:[: the carrier of ii, the carrier of ii:], the carrier of ii:]

[: the carrier of ii, the carrier of ii:] is set

[:[: the carrier of ii, the carrier of ii:], the carrier of ii:] is set

bool [:[: the carrier of ii, the carrier of ii:], the carrier of ii:] is set

the ZeroF of ii is Element of the carrier of ii

addLoopStr(# the carrier of ii, the addF of ii, the ZeroF of ii #) is strict addLoopStr

the lmult of ii is Relation-like [: the carrier of UN, the carrier of ii:] -defined the carrier of ii -valued V6() total quasi_total Element of bool [:[: the carrier of UN, the carrier of ii:], the carrier of ii:]

the carrier of UN is non empty set

[: the carrier of UN, the carrier of ii:] is set

[:[: the carrier of UN, the carrier of ii:], the carrier of ii:] is set

bool [:[: the carrier of UN, the carrier of ii:], the carrier of ii:] is set

ii is non empty right_complementable V96() V97() V98() strict V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

the carrier of ii is non empty set

the addF of ii is Relation-like [: the carrier of ii, the carrier of ii:] -defined the carrier of ii -valued V6() total quasi_total Element of bool [:[: the carrier of ii, the carrier of ii:], the carrier of ii:]

[: the carrier of ii, the carrier of ii:] is set

[:[: the carrier of ii, the carrier of ii:], the carrier of ii:] is set

bool [:[: the carrier of ii, the carrier of ii:], the carrier of ii:] is set

the ZeroF of ii is Element of the carrier of ii

addLoopStr(# the carrier of ii, the addF of ii, the ZeroF of ii #) is strict addLoopStr

the lmult of ii is Relation-like [: the carrier of UN, the carrier of ii:] -defined the carrier of ii -valued V6() total quasi_total Element of bool [:[: the carrier of UN, the carrier of ii:], the carrier of ii:]

the carrier of UN is non empty set

[: the carrier of UN, the carrier of ii:] is set

[:[: the carrier of UN, the carrier of ii:], the carrier of ii:] is set

bool [:[: the carrier of UN, the carrier of ii:], the carrier of ii:] is set

x1 is set

x2 is set

[x1,x2] is set

G is non empty right_complementable V96() V97() V98() strict V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

the carrier of G is non empty set

the addF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued V6() total quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set

the ZeroF of G is Element of the carrier of G

addLoopStr(# the carrier of G, the addF of G, the ZeroF of G #) is strict addLoopStr

the lmult of G is Relation-like [: the carrier of UN, the carrier of G:] -defined the carrier of G -valued V6() total quasi_total Element of bool [:[: the carrier of UN, the carrier of G:], the carrier of G:]

[: the carrier of UN, the carrier of G:] is set

[:[: the carrier of UN, the carrier of G:], the carrier of G:] is set

bool [:[: the carrier of UN, the carrier of G:], the carrier of G:] is set

G is non empty right_complementable V96() V97() V98() strict V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

the carrier of G is non empty set

the addF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued V6() total quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set

the ZeroF of G is Element of the carrier of G

addLoopStr(# the carrier of G, the addF of G, the ZeroF of G #) is strict addLoopStr

the lmult of G is Relation-like [: the carrier of UN, the carrier of G:] -defined the carrier of G -valued V6() total quasi_total Element of bool [:[: the carrier of UN, the carrier of G:], the carrier of G:]

[: the carrier of UN, the carrier of G:] is set

[:[: the carrier of UN, the carrier of G:], the carrier of G:] is set

bool [:[: the carrier of UN, the carrier of G:], the carrier of G:] is set

UN is non empty right_complementable V96() V97() V98() V138() well-unital V146() doubleLoopStr

the carrier of UN is non empty set

[: the carrier of UN,1:] is set

Funcs ([: the carrier of UN,1:],1) is V9() non empty FUNCTION_DOMAIN of [: the carrier of UN,1:],1

TrivialLMod UN is non empty right_complementable V96() V97() V98() strict V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

R is non empty universal set

GroupObjects R is non empty Group_DOMAIN-like set

{ [b

pr2 ( the carrier of UN,1) is Relation-like [: the carrier of UN,1:] -defined 1 -valued V6() total quasi_total Element of bool [:[: the carrier of UN,1:],1:]

[:[: the carrier of UN,1:],1:] is set

bool [:[: the carrier of UN,1:],1:] is set

VectSpStr(# 1,op2,op0,(pr2 ( the carrier of UN,1)) #) is strict VectSpStr over UN

the carrier of (TrivialLMod UN) is non empty set

the addF of (TrivialLMod UN) is Relation-like [: the carrier of (TrivialLMod UN), the carrier of (TrivialLMod UN):] -defined the carrier of (TrivialLMod UN) -valued V6() total quasi_total Element of bool [:[: the carrier of (TrivialLMod UN), the carrier of (TrivialLMod UN):], the carrier of (TrivialLMod UN):]

[: the carrier of (TrivialLMod UN), the carrier of (TrivialLMod UN):] is set

[:[: the carrier of (TrivialLMod UN), the carrier of (TrivialLMod UN):], the carrier of (TrivialLMod UN):] is set

bool [:[: the carrier of (TrivialLMod UN), the carrier of (TrivialLMod UN):], the carrier of (TrivialLMod UN):] is set

the ZeroF of (TrivialLMod UN) is Element of the carrier of (TrivialLMod UN)

addLoopStr(# the carrier of (TrivialLMod UN), the addF of (TrivialLMod UN), the ZeroF of (TrivialLMod UN) #) is strict addLoopStr

the lmult of (TrivialLMod UN) is Relation-like [: the carrier of UN, the carrier of (TrivialLMod UN):] -defined the carrier of (TrivialLMod UN) -valued V6() total quasi_total Element of bool [:[: the carrier of UN, the carrier of (TrivialLMod UN):], the carrier of (TrivialLMod UN):]

[: the carrier of UN, the carrier of (TrivialLMod UN):] is set

[:[: the carrier of UN, the carrier of (TrivialLMod UN):], the carrier of (TrivialLMod UN):] is set

bool [:[: the carrier of UN, the carrier of (TrivialLMod UN):], the carrier of (TrivialLMod UN):] is set

G is Relation-like [: the carrier of UN,1:] -defined 1 -valued V6() total quasi_total Element of bool [:[: the carrier of UN,1:],1:]

a is non empty right_complementable V97() V98() Element of GroupObjects R

x is Relation-like [: the carrier of UN,1:] -defined 1 -valued V6() total quasi_total Element of Funcs ([: the carrier of UN,1:],1)

[a,x] is set

ii is set

UN is non empty universal set

GroupObjects UN is non empty Group_DOMAIN-like set

R is non empty right_complementable V96() V97() V98() V138() well-unital V146() doubleLoopStr

the carrier of R is non empty set

[: the carrier of R,1:] is set

Funcs ([: the carrier of R,1:],1) is V9() non empty FUNCTION_DOMAIN of [: the carrier of R,1:],1

{ [b

a is set

G is set

x is set

a is set

G is set

ii is set

x is set

a is set

G is set

x is set

ii is set

ii is set

UN is non empty universal set

R is non empty right_complementable V96() V97() V98() V138() well-unital V146() doubleLoopStr

TrivialLMod R is non empty right_complementable V96() V97() V98() strict V149(R) V150(R) V151(R) V152(R) VectSpStr over R

(UN,R) is set

GroupObjects UN is non empty Group_DOMAIN-like set

the carrier of R is non empty set

[: the carrier of R,1:] is set

Funcs ([: the carrier of R,1:],1) is V9() non empty FUNCTION_DOMAIN of [: the carrier of R,1:],1

{ [b

C is set

UN is non empty universal set

R is non empty right_complementable V96() V97() V98() V138() well-unital V146() doubleLoopStr

(UN,R) is set

UN is non empty universal set

R is non empty right_complementable V96() V97() V98() V138() well-unital V146() doubleLoopStr

(UN,R) is non empty set

C is Element of (UN,R)

GroupObjects UN is non empty Group_DOMAIN-like set

the carrier of R is non empty set

[: the carrier of R,1:] is set

Funcs ([: the carrier of R,1:],1) is V9() non empty FUNCTION_DOMAIN of [: the carrier of R,1:],1

{ [b

G is set

x is set

ii is set

[x,ii] is set

x1 is non empty right_complementable V96() V97() V98() strict V149(R) V150(R) V151(R) V152(R) VectSpStr over R

the carrier of x1 is non empty set

the addF of x1 is Relation-like [: the carrier of x1, the carrier of x1:] -defined the carrier of x1 -valued V6() total quasi_total Element of bool [:[: the carrier of x1, the carrier of x1:], the carrier of x1:]

[: the carrier of x1, the carrier of x1:] is set

[:[: the carrier of x1, the carrier of x1:], the carrier of x1:] is set

bool [:[: the carrier of x1, the carrier of x1:], the carrier of x1:] is set

the ZeroF of x1 is Element of the carrier of x1

addLoopStr(# the carrier of x1, the addF of x1, the ZeroF of x1 #) is strict addLoopStr

the lmult of x1 is Relation-like [: the carrier of R, the carrier of x1:] -defined the carrier of x1 -valued V6() total quasi_total Element of bool [:[: the carrier of R, the carrier of x1:], the carrier of x1:]

[: the carrier of R, the carrier of x1:] is set

[:[: the carrier of R, the carrier of x1:], the carrier of x1:] is set

bool [:[: the carrier of R, the carrier of x1:], the carrier of x1:] is set

UN is non empty universal set

R is non empty right_complementable V96() V97() V98() V138() well-unital V146() doubleLoopStr

(UN,R) is non empty set

C is Element of (UN,R)

UN is non empty right_complementable V96() V97() V98() V138() well-unital V146() doubleLoopStr

R is non empty (UN)

the non empty right_complementable V96() V97() V98() strict V149(UN) V150(UN) V151(UN) V152(UN) (UN,R) is non empty right_complementable V96() V97() V98() strict V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

(UN, the non empty right_complementable V96() V97() V98() strict V149(UN) V150(UN) V151(UN) V152(UN) (UN,R), the non empty right_complementable V96() V97() V98() strict V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)) is non empty (UN, the non empty right_complementable V96() V97() V98() strict V149(UN) V150(UN) V151(UN) V152(UN) (UN,R), the non empty right_complementable V96() V97() V98() strict V149(UN) V150(UN) V151(UN) V152(UN) (UN,R))

{ (UN,b

ZERO ( the non empty right_complementable V96() V97() V98() strict V149(UN) V150(UN) V151(UN) V152(UN) (UN,R), the non empty right_complementable V96() V97() V98() strict V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)) is strict LModMorphism-like Morphism of the non empty right_complementable V96() V97() V98() strict V149(UN) V150(UN) V151(UN) V152(UN) (UN,R), the non empty right_complementable V96() V97() V98() strict V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

union { (UN,b

x is non empty set

ii is set

x1 is set

x2 is non empty right_complementable V96() V97() V98() strict V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

G is non empty right_complementable V96() V97() V98() strict V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

(UN,x2,G) is non empty (UN,x2,G)

x1 is non empty right_complementable V96() V97() V98() strict V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

x2 is non empty right_complementable V96() V97() V98() strict V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

(UN,x1,x2) is non empty (UN,x1,x2)

ii is Element of x

x1 is non empty right_complementable V96() V97() V98() strict V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

x2 is non empty right_complementable V96() V97() V98() strict V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

ii is non empty (UN)

x1 is set

x2 is set

G is non empty right_complementable V96() V97() V98() strict V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

ii is non empty right_complementable V96() V97() V98() strict V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

C is non empty (UN)

a is non empty (UN)

G is set

x is non empty right_complementable V96() V97() V98() strict V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

ii is non empty right_complementable V96() V97() V98() strict V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

x is non empty right_complementable V96() V97() V98() strict V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

ii is non empty right_complementable V96() V97() V98() strict V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

UN is non empty right_complementable V96() V97() V98() V138() well-unital V146() doubleLoopStr

R is non empty (UN)

(UN,R) is non empty (UN)

C is LModMorphism-like (UN,(UN,R))

dom C is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

a is non empty right_complementable V96() V97() V98() strict V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

G is non empty right_complementable V96() V97() V98() strict V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

x is LModMorphism-like Morphism of a,G

dom x is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

cod C is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

a is non empty right_complementable V96() V97() V98() strict V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

G is non empty right_complementable V96() V97() V98() strict V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

x is LModMorphism-like Morphism of a,G

cod x is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

UN is non empty right_complementable V96() V97() V98() V138() well-unital V146() doubleLoopStr

R is non empty (UN)

C is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

ID C is strict LModMorphism-like Morphism of C,C

(UN,R) is non empty (UN)

a is non empty right_complementable V96() V97() V98() strict V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

ID a is strict LModMorphism-like Morphism of a,a

UN is non empty right_complementable V96() V97() V98() V138() well-unital V146() doubleLoopStr

R is non empty (UN)

(UN,R) is non empty (UN)

[:(UN,R),R:] is set

bool [:(UN,R),R:] is set

C is Relation-like (UN,R) -defined R -valued V6() non empty total quasi_total Element of bool [:(UN,R),R:]

a is LModMorphism-like (UN,(UN,R))

C . a is Element of R

(UN,R,a) is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

dom a is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

C is Relation-like (UN,R) -defined R -valued V6() non empty total quasi_total Element of bool [:(UN,R),R:]

a is Relation-like (UN,R) -defined R -valued V6() non empty total quasi_total Element of bool [:(UN,R),R:]

G is LModMorphism-like (UN,(UN,R))

C . G is Element of R

(UN,R,G) is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

dom G is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

a . G is Element of R

C is Relation-like (UN,R) -defined R -valued V6() non empty total quasi_total Element of bool [:(UN,R),R:]

a is LModMorphism-like (UN,(UN,R))

C . a is Element of R

(UN,R,a) is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

cod a is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

C is Relation-like (UN,R) -defined R -valued V6() non empty total quasi_total Element of bool [:(UN,R),R:]

a is Relation-like (UN,R) -defined R -valued V6() non empty total quasi_total Element of bool [:(UN,R),R:]

G is LModMorphism-like (UN,(UN,R))

C . G is Element of R

(UN,R,G) is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

cod G is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

a . G is Element of R

UN is non empty right_complementable V96() V97() V98() V138() well-unital V146() doubleLoopStr

R is non empty (UN)

(UN,R) is non empty (UN)

a is LModMorphism-like (UN,(UN,R))

(UN,R,a) is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

dom a is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

G is LModMorphism-like (UN,(UN,R))

(UN,R,G) is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

cod G is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

x is non empty right_complementable V96() V97() V98() strict V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

ii is non empty right_complementable V96() V97() V98() strict V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

x1 is non empty right_complementable V96() V97() V98() strict V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

x2 is non empty right_complementable V96() V97() V98() strict V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

UN is non empty right_complementable V96() V97() V98() V138() well-unital V146() doubleLoopStr

R is non empty (UN)

(UN,R) is non empty (UN)

a is LModMorphism-like (UN,(UN,R))

(UN,R,a) is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

dom a is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

G is LModMorphism-like (UN,(UN,R))

(UN,R,G) is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

cod G is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

a * G is strict LModMorphism-like LModMorphismStr over UN

ii is non empty right_complementable V96() V97() V98() strict V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

x1 is non empty right_complementable V96() V97() V98() strict V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

x is non empty right_complementable V96() V97() V98() strict V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

G is LModMorphism-like Morphism of ii,x1

x2 is LModMorphism-like Morphism of x,ii

G * x2 is strict LModMorphism-like LModMorphismStr over UN

G *' x2 is strict LModMorphism-like Morphism of x,x1

UN is non empty right_complementable V96() V97() V98() V138() well-unital V146() doubleLoopStr

R is non empty (UN)

(UN,R) is non empty (UN)

C is LModMorphism-like (UN,(UN,R))

dom C is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

a is LModMorphism-like (UN,(UN,R))

cod a is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

C * a is strict LModMorphism-like LModMorphismStr over UN

(UN,R,C) is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

(UN,R,a) is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

UN is non empty right_complementable V96() V97() V98() V138() well-unital V146() doubleLoopStr

R is non empty (UN)

(UN,R) is non empty (UN)

[:(UN,R),(UN,R):] is set

[:[:(UN,R),(UN,R):],(UN,R):] is set

bool [:[:(UN,R),(UN,R):],(UN,R):] is set

a is LModMorphism-like (UN,(UN,R))

(UN,R,a) is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

dom a is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

G is LModMorphism-like (UN,(UN,R))

(UN,R,G) is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

cod G is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

a * G is strict LModMorphism-like LModMorphismStr over UN

a is Relation-like [:(UN,R),(UN,R):] -defined (UN,R) -valued V6() Element of bool [:[:(UN,R),(UN,R):],(UN,R):]

dom a is Relation-like (UN,R) -defined (UN,R) -valued Element of bool [:(UN,R),(UN,R):]

bool [:(UN,R),(UN,R):] is set

G is LModMorphism-like (UN,(UN,R))

x is LModMorphism-like (UN,(UN,R))

[G,x] is set

(UN,R,G) is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

dom G is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

(UN,R,x) is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

cod x is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

ii is LModMorphism-like (UN,(UN,R))

(UN,R,ii) is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

dom ii is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

x1 is LModMorphism-like (UN,(UN,R))

(UN,R,x1) is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

cod x1 is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

[ii,x1] is set

x2 is LModMorphism-like (UN,(UN,R))

G is LModMorphism-like (UN,(UN,R))

[x2,G] is set

a . (x2,G) is set

x2 * G is strict LModMorphism-like LModMorphismStr over UN

a is Relation-like [:(UN,R),(UN,R):] -defined (UN,R) -valued V6() Element of bool [:[:(UN,R),(UN,R):],(UN,R):]

dom a is Relation-like (UN,R) -defined (UN,R) -valued Element of bool [:(UN,R),(UN,R):]

bool [:(UN,R),(UN,R):] is set

G is Relation-like [:(UN,R),(UN,R):] -defined (UN,R) -valued V6() Element of bool [:[:(UN,R),(UN,R):],(UN,R):]

dom G is Relation-like (UN,R) -defined (UN,R) -valued Element of bool [:(UN,R),(UN,R):]

ii is set

x1 is LModMorphism-like (UN,(UN,R))

x2 is LModMorphism-like (UN,(UN,R))

[x1,x2] is set

(UN,R,x1) is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

dom x1 is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

(UN,R,x2) is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

cod x2 is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

ii is set

x1 is set

[ii,x1] is set

a . (ii,x1) is set

G . (ii,x1) is set

x2 is LModMorphism-like (UN,(UN,R))

G is LModMorphism-like (UN,(UN,R))

a . (x2,G) is set

x2 * G is strict LModMorphism-like LModMorphismStr over UN

ii is set

x1 is LModMorphism-like (UN,(UN,R))

x2 is LModMorphism-like (UN,(UN,R))

[x1,x2] is set

(UN,R,x1) is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

dom x1 is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

(UN,R,x2) is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

cod x2 is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

UN is non empty right_complementable V96() V97() V98() V138() well-unital V146() doubleLoopStr

R is non empty (UN)

(UN,R) is non empty (UN)

[:(UN,R),(UN,R):] is set

(UN,R) is Relation-like [:(UN,R),(UN,R):] -defined (UN,R) -valued V6() Element of bool [:[:(UN,R),(UN,R):],(UN,R):]

[:[:(UN,R),(UN,R):],(UN,R):] is set

bool [:[:(UN,R),(UN,R):],(UN,R):] is set

dom (UN,R) is Relation-like (UN,R) -defined (UN,R) -valued Element of bool [:(UN,R),(UN,R):]

bool [:(UN,R),(UN,R):] is set

C is LModMorphism-like (UN,(UN,R))

a is LModMorphism-like (UN,(UN,R))

[C,a] is set

dom C is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

cod a is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) VectSpStr over UN

(UN,R,C) is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

(UN,R,a) is non empty right_complementable V96() V97() V98() V149(UN) V150(UN) V151(UN) V152(UN) (UN,R)

UN is non empty universal set

R is non empty right_complementable V96() V97() V98() V138() well-unital V146() doubleLoopStr

(UN,R) is non empty (R)

(R,(UN,R)) is non empty (R)

(R,(UN,R)) is Relation-like (R,(UN,R)) -defined (UN,R) -valued V6() non empty total quasi_total Element of bool [:(R,(UN,R)),(UN,R):]

[:(R,(UN,R)),(UN,R):] is set

bool [:(R,(UN,R)),(UN,R):] is set

(R,(UN,R)) is Relation-like (R,(UN,R)) -defined (UN,R) -valued V6() non empty total quasi_total Element of bool [:(R,(UN,R)),(UN,R):]

(R,(UN,R)) is Relation-like [:(R,(UN,R)),(R,(UN,R)):] -defined (R,(UN,R)) -valued V6() Element of bool [:[:(R,(UN,R)),(R,(UN,R)):],(R,(UN,R)):]

[:(R,(UN,R)),(R,(UN,R)):] is set

[:[:(R,(UN,R)),(R,(UN,R)):],(R,(UN,R)):] is set

bool [:[:(R,(UN,R)),(R,(UN,R)):],(R,(UN,R)):] is set

CatStr(# (UN,R),(R,(UN,R)),(R,(UN,R)),(R,(UN,R)),(R,(UN,R)) #) is strict CatStr

UN is non empty universal set

R is non empty right_complementable V96() V97() V98() V138() well-unital V146() doubleLoopStr

(UN,R) is strict CatStr

(UN,R) is non empty (R)

(R,(UN,R)) is non empty (R)

(R,(UN,R)) is Relation-like (R,(UN,R)) -defined (UN,R) -valued V6() non empty total quasi_total Element of bool [:(R,(UN,R)),(UN,R):]

[:(R,(UN,R)),(UN,R):] is set

bool [:(R,(UN,R)),(UN,R):] is set

(R,(UN,R)) is Relation-like (R,(UN,R)) -defined (UN,R) -valued V6() non empty total quasi_total Element of bool [:(R,(UN,R)),(UN,R):]

(R,(UN,R)) is Relation-like [:(R,(UN,R)),(R,(UN,R)):] -defined (R,(UN,R)) -valued V6() Element of bool [:[:(R,(UN,R)),(R,(UN,R)):],(R,(UN,R)):]

[:(R,(UN,R)),(R,(UN,R)):] is set

[:[:(R,(UN,R)),(R,(UN,R)):],(R,(UN,R)):] is set

bool [:[:(R,(UN,R)),(R,(UN,R)):],(R,(UN,R)):] is set

CatStr(# (UN,R),(R,(UN,R)),(R,(UN,R)),(R,(UN,R)),(R,(UN,R)) #) is strict CatStr

UN is non empty universal set

R is non empty right_complementable V96() V97() V98() V138() well-unital V146() doubleLoopStr

(UN,R) is non empty non void V53() strict CatStr

(UN,R) is non empty (R)

(R,(UN,R)) is non empty (R)

(R,(UN,R)) is Relation-like (R,(UN,R)) -defined (UN,R) -valued V6() non empty total quasi_total Element of bool [:(R,(UN,R)),(UN,R):]

[:(R,(UN,R)),(UN,R):] is set

bool [:(R,(UN,R)),(UN,R):] is set

(R,(UN,R)) is Relation-like (R,(UN,R)) -defined (UN,R) -valued V6() non empty total quasi_total Element of bool [:(R,(UN,R)),(UN,R):]

(R,(UN,R)) is Relation-like [:(R,(UN,R)),(R,(UN,R)):] -defined (R,(UN,R)) -valued V6() Element of bool [:[:(R,(UN,R)),(R,(UN,R)):],(R,(UN,R)):]

[:(R,(UN,R)),(R,(UN,R)):] is set

[:[:(R,(UN,R)),(R,(UN,R)):],(R,(UN,R)):] is set

bool [:[:(R,(UN,R)),(R,(UN,R)):],(R,(UN,R)):] is set

CatStr(# (UN,R),(R,(UN,R)),(R,(UN,R)),(R,(UN,R)),(R,(UN,R)) #) is strict CatStr

the carrier' of (UN,R) is non empty set

[: the carrier' of (UN,R), the carrier' of (UN,R):] is set

the Comp of (UN,R) is Relation-like [: the carrier' of (UN,R), the carrier' of (UN,R):] -defined the carrier' of (UN,R) -valued V6() Element of bool [:[: the carrier' of (UN,R), the carrier' of (UN,R):], the carrier' of (UN,R):]

[:[: the carrier' of (UN,R), the carrier' of (UN,R):], the carrier' of (UN,R):] is set

bool [:[: the carrier' of (UN,R), the carrier' of (UN,R):], the carrier' of (UN,R):] is set

dom the Comp of (UN,R) is Relation-like the carrier' of (UN,R) -defined the carrier' of (UN,R) -valued Element of bool [: the carrier' of (UN,R), the carrier' of (UN,R):]

bool [: the carrier' of (UN,R), the carrier' of (UN,R):] is set

x is Element of the carrier' of (UN,R)

G is Element of the carrier' of (UN,R)

[x,G] is set

dom x is Element of the carrier of (UN,R)

the carrier of (UN,R) is non empty set

the Source of (UN,R) is Relation-like the carrier' of (UN,R) -defined the carrier of (UN,R) -valued V6() non empty total quasi_total Element of bool [: the carrier' of (UN,R), the carrier of (UN,R):]

[: the carrier' of (UN,R), the carrier of (UN,R):] is set

bool [: the carrier' of (UN,R), the carrier of (UN,R):] is set

the Source of (UN,R) . x is Element of the carrier of (UN,R)

cod G is Element of the carrier of (UN,R)

the Target of (UN,R) is Relation-like the carrier' of (UN,R) -defined the carrier of (UN,R) -valued V6() non empty total quasi_total Element of bool [: the carrier' of (UN,R), the carrier of (UN,R):]

the Target of (UN,R) . G is Element of the carrier of (UN,R)

ii is LModMorphism-like (R,(R,(UN,R)))

(R,(UN,R),ii) is non empty right_complementable V96() V97() V98() V149(R) V150(R) V151(R) V152(R) (R,(UN,R))

cod ii is non empty right_complementable V96() V97() V98() V149(R) V150(R) V151(R) V152(R) VectSpStr over R

x1 is LModMorphism-like (R,(R,(UN,R)))

(R,(UN,R),x1) is non empty right_complementable V96() V97() V98() V149(R) V150(R) V151(R) V152(R) (R,(UN,R))

dom x1 is non empty right_complementable V96() V97() V98() V149(R) V150(R) V151(R) V152(R) VectSpStr over R

R is non empty right_complementable V96() V97() V98() V138() well-unital V146() doubleLoopStr

UN is non empty universal set

(UN,R) is non empty (R)

(R,(UN,R)) is non empty (R)

a is LModMorphism-like (R,(R,(UN,R)))

G is non empty right_complementable V96() V97() V98() strict V149(R) V150(R) V151(R) V152(R) (R,(UN,R))

x is non empty right_complementable V96() V97() V98() strict V149(R) V150(R) V151(R) V152(R) (R,(UN,R))

UN is non empty universal set

R is non empty right_complementable V96() V97() V98() V138() well-unital V146() doubleLoopStr

(UN,R) is non empty non void V53() strict CatStr

(UN,R) is non empty (R)

(R,(UN,R)) is non empty (R)

(R,(UN,R)) is Relation-like (R,(UN,R)) -defined (UN,R) -valued V6() non empty total quasi_total Element of bool [:(R,(UN,R)),(UN,R):]

[:(R,(UN,R)),(UN,R):] is set

bool [:(R,(UN,R)),(UN,R):] is set

(R,(UN,R)) is Relation-like (R,(UN,R)) -defined (UN,R) -valued V6() non empty total quasi_total Element of bool [:(R,(UN,R)),(UN,R):]

(R,(UN,R)) is Relation-like [:(R,(UN,R)),(R,(UN,R)):] -defined (R,(UN,R)) -valued V6() Element of bool [:[:(R,(UN,R)),(R,(UN,R)):],(R,(UN,R)):]

[:(R,(UN,R)),(R,(UN,R)):] is set

[:[:(R,(UN,R)),(R,(UN,R)):],(R,(UN,R)):] is set

bool [:[:(R,(UN,R)),(R,(UN,R)):],(R,(UN,R)):] is set

CatStr(# (UN,R),(R,(UN,R)),(R,(UN,R)),(R,(UN,R)),(R,(UN,R)) #) is strict CatStr

the carrier' of (UN,R) is non empty set

x is Element of the carrier' of (UN,R)

dom x is Element of the carrier of (UN,R)

the carrier of (UN,R) is non empty set

the Source of (UN,R) is Relation-like the carrier' of (UN,R) -defined the carrier of (UN,R) -valued V6() non empty total quasi_total Element of bool [: the carrier' of (UN,R), the carrier of (UN,R):]

[: the carrier' of (UN,R), the carrier of (UN,R):] is set

bool [: the carrier' of (UN,R), the carrier of (UN,R):] is set

the Source of (UN,R) . x is Element of the carrier of (UN,R)

cod x is Element of the carrier of (UN,R)

the Target of (UN,R) is Relation-like the carrier' of (UN,R) -defined the carrier of (UN,R) -valued V6() non empty total quasi_total Element of bool [: the carrier' of (UN,R), the carrier of (UN,R):]

the Target of (UN,R) . x is Element of the carrier of (UN,R)

ii is strict LModMorphism-like (R,(R,(UN,R)))

dom ii is non empty right_complementable V96() V97() V98() V149(R) V150(R) V151(R) V152(R) VectSpStr over R

cod ii is non empty right_complementable V96() V97() V98() V149(R) V150(R) V151(R) V152(R) VectSpStr over R

(R,(UN,R),ii) is non empty right_complementable V96() V97() V98() V149(R) V150(R) V151(R) V152(R) (R,(UN,R))

(R,(UN,R),ii) is non empty right_complementable V96() V97() V98() V149(R) V150(R) V151(R) V152(R) (R,(UN,R))

UN is non empty universal set

R is non empty right_complementable V96() V97() V98() V138() well-unital V146() doubleLoopStr

(UN,R) is non empty non void V53() strict CatStr

(UN,R) is non empty (R)

(R,(UN,R)) is non empty (R)

(R,(UN,R)) is Relation-like (R,(UN,R)) -defined (UN,R) -valued V6() non empty total quasi_total Element of bool [:(R,(UN,R)),(UN,R):]

[:(R,(UN,R)),(UN,R):] is set

bool [:(R,(UN,R)),(UN,R):] is set

(R,(UN,R)) is Relation-like (R,(UN,R)) -defined (UN,R) -valued V6() non empty total quasi_total Element of bool [:(R,(UN,R)),(UN,R):]

(R,(UN,R)) is Relation-like [:(R,(UN,R)),(R,(UN,R)):] -defined (R,(UN,R)) -valued V6() Element of bool [:[:(R,(UN,R)),(R,(UN,R)):],(R,(UN,R)):]

[:(R,(UN,R)),(R,(UN,R)):] is set

[:[:(R,(UN,R)),(R,(UN,R)):],(R,(UN,R)):] is set

bool [:[:(R,(UN,R)),(R,(UN,R)):],(R,(UN,R)):] is set

CatStr(# (UN,R),(R,(UN,R)),(R,(UN,R)),(R,(UN,R)),(R,(UN,R)) #) is strict CatStr

the carrier' of (UN,R) is non empty set

dom (R,(UN,R)) is Relation-like (R,(UN,R)) -defined (R,(UN,R)) -valued Element of bool [:(R,(UN,R)),(R,(UN,R)):]

bool [:(R,(UN,R)),(R,(UN,R)):] is set

x is Element of the carrier' of (UN,R)

ii is Element of the carrier' of (UN,R)

dom ii is Element of the carrier of (UN,R)

the carrier of (UN,R) is non empty set

the Source of (UN,R) is Relation-like the carrier' of (UN,R) -defined the carrier of (UN,R) -valued V6() non empty total quasi_total Element of bool [: the carrier' of (UN,R), the carrier of (UN,R):]

[: the carrier' of (UN,R), the carrier of (UN,R):] is set

bool [: the carrier' of (UN,R), the carrier of (UN,R):] is set

the Source of (UN,R) . ii is Element of the carrier of (UN,R)

cod x is Element of the carrier of (UN,R)

the Target of (UN,R) is Relation-like the carrier' of (UN,R) -defined the carrier of (UN,R) -valued V6() non empty total quasi_total Element of bool [: the carrier' of (UN,R), the carrier of (UN,R):]

the Target of (UN,R) . x is Element of the carrier of (UN,R)

ii (*) x is Element of the carrier' of (UN,R)

dom x is Element of the carrier of (UN,R)

the Source of (UN,R) . x is Element of the carrier of (UN,R)

cod ii is Element of the carrier of (UN,R)

the Target of (UN,R) . ii is Element of the carrier of (UN,R)

x1 is strict LModMorphism-like (R,(R,(UN,R)))

x2 is strict LModMorphism-like (R,(R,(UN,R)))

dom x2 is non empty right_complementable V96() V97() V98() V149(R) V150(R) V151(R) V152(R) VectSpStr over R

cod x1 is non empty right_complementable V96() V97() V98() V149(R) V150(R) V151(R) V152(R) VectSpStr over R

[x2,x1] is set

x2 * x1 is strict LModMorphism-like LModMorphismStr over R

dom x1 is non empty right_complementable V96() V97() V98() V149(R) V150(R) V151(R) V152(R) VectSpStr over R

cod x2 is non empty right_complementable V96() V97() V98() V149(R) V150(R) V151(R) V152(R) VectSpStr over R

[ii,x] is set

[: the carrier' of (UN,R), the carrier' of (UN,R):] is set

the Comp of (UN,R) is Relation-like [: the carrier' of (UN,R), the carrier' of (UN,R):] -defined the carrier' of (UN,R) -valued V6() Element of bool [:[: the carrier' of (UN,R), the carrier' of (UN,R):], the carrier' of (UN,R):]

[:[: the carrier' of (UN,R), the carrier' of (UN,R):], the carrier' of (UN,R):] is set

bool [:[: the carrier' of (UN,R), the carrier' of (UN,R):], the carrier' of (UN,R):] is set

dom the Comp of (UN,R) is Relation-like the carrier' of (UN,R) -defined the carrier' of (UN,R) -valued Element of bool [: the carrier' of (UN,R), the carrier' of (UN,R):]

bool [: the carrier' of (UN,R), the carrier' of (UN,R):] is set

(R,(UN,R)) . (x2,x1) is set

UN is non empty universal set

R is non empty right_complementable V96() V97() V98() V138() well-unital V146() doubleLoopStr

(UN,R) is non empty non void V53() strict CatStr

(UN,R) is non empty (R)

(R,(UN,R)) is non empty (R)

(R,(UN,R)) is Relation-like (R,(UN,R)) -defined (UN,R) -valued V6() non empty total quasi_total Element of bool [:(R,(UN,R)),(UN,R):]

[:(R,(UN,R)),(UN,R):] is set

bool [:(R,(UN,R)),(UN,R):] is set

(R,(UN,R)) is Relation-like (R,(UN,R)) -defined (UN,R) -valued V6() non empty total quasi_total Element of bool [:(R,(UN,R)),(UN,R):]

(R,(UN,R)) is Relation-like [:(R,(UN,R)),(R,(UN,R)):] -defined (R,(UN,R)) -valued V6() Element of bool [:[:(R,(UN,R)),(R,(UN,R)):],(R,(UN,R)):]

[:(R,(UN,R)),(R,(UN,R)):] is set

[:[:(R,(UN,R)),(R,(UN,R)):],(R,(UN,R)):] is set

bool [:[:(R,(UN,R)),(R,(UN,R)):],(R,(UN,R)):] is set

CatStr(# (UN,R),(R,(UN,R)),(R,(UN,R)),(R,(UN,R)),(R,(UN,R)) #) is strict CatStr

the carrier' of (UN,R) is non empty set

G is Element of the carrier' of (UN,R)

dom G is Element of the carrier of (UN,R)

the carrier of (UN,R) is non empty set

the Source of (UN,R) is Relation-like the carrier' of (UN,R) -defined the carrier of (UN,R) -valued V6() non empty total quasi_total Element of bool [: the carrier' of (UN,R), the carrier of (UN,R):]

[: the carrier' of (UN,R), the carrier of (UN,R):] is set

bool [: the carrier' of (UN,R), the carrier of (UN,R):] is set

the Source of (UN,R) . G is Element of the carrier of (UN,R)

a is Element of the carrier' of (UN,R)

cod a is Element of the carrier of (UN,R)

the Target of (UN,R) is Relation-like the carrier' of (UN,R) -defined the carrier of (UN,R) -valued V6() non empty total quasi_total Element of bool [: the carrier' of (UN,R), the carrier of (UN,R):]

the Target of (UN,R) . a is Element of the carrier of (UN,R)

G (*) a is Element of the carrier' of (UN,R)

dom (G (*) a) is Element of the carrier of (UN,R)

the Source of (UN,R) . (G (*) a) is Element of the carrier of (UN,R)

dom a is Element of the carrier of (UN,R)

the Source of (UN,R) . a is Element of the carrier of (UN,R)

cod (G (*) a) is Element of the carrier of (UN,R)

the Target of (UN,R) . (G (*) a) is Element of the carrier of (UN,R)

cod G is Element of the carrier of (UN,R)

the Target of (UN,R) . G is Element of the carrier of (UN,R)

x is strict LModMorphism-like (R,(R,(UN,R)))

dom x is non empty right_complementable V96() V97() V98() V149(R) V150(R) V151(R) V152(R) VectSpStr over R

ii is strict LModMorphism-like (R,(R,(UN,R)))

cod ii is non empty right_complementable V96() V97() V98() V149(R) V150(R) V151(R) V152(R) VectSpStr over R

x * ii is strict LModMorphism-like LModMorphismStr over R

dom (x * ii) is non empty right_complementable V96() V97() V98() V149(R) V150(R) V151(R) V152(R) VectSpStr over R

dom ii is non empty right_complementable V96() V97() V98() V149(R) V150(R) V151(R) V152(R) VectSpStr over R

cod (x * ii) is non empty right_complementable V96() V97() V98() V149(R) V150(R) V151(R) V152(R) VectSpStr over R

cod x is non empty right_complementable V96() V97() V98() V149(R) V150(R) V151(R) V152(R) VectSpStr over R

x1 is strict LModMorphism-like (R,(R,(UN,R)))

UN is non empty universal set

R is non empty right_complementable V96() V97() V98() V138() well-unital V146() doubleLoopStr

(UN,R) is non empty non void V53() strict CatStr

(UN,R) is non empty (R)

(R,(UN,R)) is non empty (R)

(R,(UN,R)) is Relation-like (R,(UN,R)) -defined (UN,R) -valued V6() non empty total quasi_total Element of bool [:(R,(UN,R)),(UN,R):]

[:(R,(UN,R)),(UN,R):] is set

bool [:(R,(UN,R)),(UN,R):] is set

(R,(UN,R)) is Relation-like (R,(UN,R)) -defined (UN,R) -valued V6() non empty total quasi_total Element of bool [:(R,(UN,R)),(UN,R):]

(R,(UN,R)) is Relation-like [:(R,(UN,R)),(R,(UN,R)):] -defined (R,(UN,R)) -valued V6() Element of bool [:[:(R,(UN,R)),(R,(UN,R)):],(R,(UN,R)):]

[:(R,(UN,R)),(R,(UN,R)):] is set

[:[:(R,(UN,R)),(R,(UN,R)):],(R,(UN,R)):] is set

bool [:[:(R,(UN,R)),(R,(UN,R)):],(R,(UN,R)):] is set

CatStr(# (UN,R),(R,(UN,R)),(R,(UN,R)),(R,(UN,R)),(R,(UN,R)) #) is strict CatStr

the carrier' of (UN,R) is non empty set

x is Element of the carrier' of (UN,R)

dom x is Element of the carrier of (UN,R)

the carrier of (UN,R) is non empty set

the Source of (UN,R) is Relation-like the carrier' of (UN,R) -defined the carrier of (UN,R) -valued V6() non empty total quasi_total Element of bool [: the carrier' of (UN,R), the carrier of (UN,R):]

[: the carrier' of (UN,R), the carrier of (UN,R):] is set

bool [: the carrier' of (UN,R), the carrier of (UN,R):] is set

the Source of (UN,R) . x is Element of the carrier of (UN,R)

G is Element of the carrier' of (UN,R)

cod G is Element of the carrier of (UN,R)

the Target of (UN,R) is Relation-like the carrier' of (UN,R) -defined the carrier of (UN,R) -valued V6() non empty total quasi_total Element of bool [: the carrier' of (UN,R), the carrier of (UN,R):]

the Target of (UN,R) . G is Element of the carrier of (UN,R)

dom G is Element of the carrier of (UN,R)

the Source of (UN,R) . G is Element of the carrier of (UN,R)

a is Element of the carrier' of (UN,R)

cod a is Element of the carrier of (UN,R)

the Target of (UN,R) . a is Element of the carrier of (UN,R)

G (*) a is Element of the carrier' of (UN,R)

x (*) (G (*) a) is Element of the carrier' of (UN,R)

x (*) G is Element of the carrier' of (UN,R)

(x (*) G) (*) a is Element of the carrier' of (UN,R)

x2 is strict LModMorphism-like (R,(R,(UN,R)))

x1 is strict LModMorphism-like (R,(R,(UN,R)))

x2 * x1 is strict LModMorphism-like LModMorphismStr over R

dom (x (*) G) is Element of the carrier of (UN,R)

the Source of (UN,R) . (x (*) G) is Element of the carrier of (UN,R)

dom x2 is non empty right_complementable V96() V97() V98() V149(R) V150(R) V151(R) V152(R) VectSpStr over R

cod x1 is non empty right_complementable V96() V97() V98() V149(R) V150(R) V151(R) V152(R) VectSpStr over R

dom x1 is non empty right_complementable V96() V97() V98() V149(R) V150(R) V151(R) V152(R) VectSpStr over R

ii is strict LModMorphism-like (R,(R,(UN,R)))

cod ii is non empty right_complementable V96() V97() V98() V149(R) V150(R) V151(R) V152(R) VectSpStr over R

x1 * ii is strict LModMorphism-like LModMorphismStr over R

cod (G (*) a) is Element of the carrier of (UN,R)

the Target of (UN,R) . (G (*) a) is Element of the carrier of (UN,R)

G is strict LModMorphism-like (R,(R,(UN,R)))

x2 * G is strict LModMorphism-like LModMorphismStr over R

ii is strict LModMorphism-like (R,(R,(UN,R)))

ii * ii is strict LModMorphism-like LModMorphismStr over R

UN is non empty universal set

R is non empty right_complementable V96() V97() V98() V138() well-unital V146() doubleLoopStr

(UN,R) is non empty non void V53() strict CatStr

(UN,R) is non empty (R)

(R,(UN,R)) is non empty (R)

(R,(UN,R)) is Relation-like (R,(UN,R)) -defined (UN,R) -valued V6() non empty total quasi_total Element of bool [:(R,(UN,R)),(UN,R):]

[:(R,(UN,R)),(UN,R):] is set

bool [:(R,(UN,R)),(UN,R):] is set

(R,(UN,R)) is Relation-like (R,(UN,R)) -defined (UN,R) -valued V6() non empty total quasi_total Element of bool [:(R,(UN,R)),(UN,R):]

(R,(UN,R)) is Relation-like [:(R,(UN,R)),(R,(UN,R)):] -defined (R,(UN,R)) -valued V6() Element of bool [:[:(R,(UN,R)),(R,(UN,R)):],(R,(UN,R)):]

[:(R,(UN,R)),(R,(UN,R)):] is set

[:[:(R,(UN,R)),(R,(UN,R)):],(R,(UN,R)):] is set

bool [:[:(R,(UN,R)),(R,(UN,R)):],(R,(UN,R)):] is set

CatStr(# (UN,R),(R,(UN,R)),(R,(UN,R)),(R,(UN,R)),(R,(UN,R)) #) is strict CatStr

the carrier' of (UN,R) is non empty set

a is Element of the carrier' of (UN,R)

the Comp of (UN,R) is Relation-like [: the carrier' of (UN,R), the carrier' of (UN,R):] -defined the carrier' of (UN,R) -valued V6() Element of bool [:[: the carrier' of (UN,R), the carrier' of (UN,R):], the carrier' of (UN,R):]

[: the carrier' of (UN,R), the carrier' of (UN,R):] is set

[:[: the carrier' of (UN,R), the carrier' of (UN,R):], the carrier' of (UN,R):] is set

bool [:[: the carrier' of (UN,R), the carrier' of (UN,R):], the carrier' of (UN,R):] is set

dom the Comp of (UN,R) is Relation-like set

cod a is Element of the carrier of (UN,R)

the carrier of (UN,R) is non empty set

the Target of (UN,R) is Relation-like the carrier' of (UN,R) -defined the carrier of (UN,R) -valued V6() non empty total quasi_total Element of bool [: the carrier' of (UN,R), the carrier of (UN,R):]

[: the carrier' of (UN,R), the carrier of (UN,R):] is set

bool [: the carrier' of (UN,R), the carrier of (UN,R):] is set

the Target of (UN,R) . a is Element of the carrier of (UN,R)

G is Element of the carrier' of (UN,R)

[G,a] is set

dom G is Element of the carrier of (UN,R)

the Source of (UN,R) is Relation-like the carrier' of (UN,R) -defined the carrier of (UN,R) -valued V6() non empty total quasi_total Element of bool [: the carrier' of (UN,R), the carrier of (UN,R):]

the Source of (UN,R) . G is Element of the carrier of (UN,R)

x is Element of the carrier' of (UN,R)

dom x is Element of the carrier of (UN,R)

the Source of (UN,R) . x is Element of the carrier of (UN,R)

[x,a] is set

the carrier' of (UN,R) is non empty set

a is Element of the carrier' of (UN,R)

cod a is Element of the carrier of (UN,R)

the carrier of (UN,R) is non empty set

the Target of (UN,R) is Relation-like the carrier' of (UN,R) -defined the carrier of (UN,R) -valued V6() non empty total quasi_total Element of bool [: the carrier' of (UN,R), the carrier of (UN,R):]

[: the carrier' of (UN,R), the carrier of (UN,R):] is set

bool [: the carrier' of (UN,R), the carrier of (UN,R):] is set

the Target of (UN,R) . a is Element of the carrier of (UN,R)

dom a is Element of the carrier of (UN,R)

the Source of (UN,R) is Relation-like the carrier' of (UN,R) -defined the carrier of (UN,R) -valued V6() non empty total quasi_total Element of bool [: the carrier' of (UN,R), the carrier of (UN,R):]

the Source of (UN,R) . a is Element of the carrier of (UN,R)

G is Element of the carrier' of (UN,R)

dom G is Element of the carrier of (UN,R)

the Source of (UN,R) . G is Element of the carrier of (UN,R)

G (*) a is Element of the carrier' of (UN,R)

dom (G (*) a) is Element of the carrier of (UN,R)

the Source of (UN,R) . (G (*) a) is Element of the carrier of (UN,R)

cod (G (*) a) is Element of the carrier of (UN,R)

the Target of (UN,R) . (G (*) a) is Element of the carrier of (UN,R)

cod G is Element of the carrier of (UN,R)

the Target of (UN,R) . G is Element of the carrier of (UN,R)

the carrier' of (UN,R) is non empty set

a is Element of the carrier' of (UN,R)

cod a is Element of the carrier of (UN,R)

the carrier of (UN,R) is non empty set

the Target of (UN,R) is Relation-like the carrier' of (UN,R) -defined the carrier of (UN,R) -valued V6() non empty total quasi_total Element of bool [: the carrier' of (UN,R), the carrier of (UN,R):]

[: the carrier' of (UN,R), the carrier of (UN,R):] is set

bool [: the carrier' of (UN,R), the carrier of (UN,R):] is set

the Target of (UN,R) . a is Element of the carrier of (UN,R)

x is Element of the carrier' of (UN,R)

dom x is Element of the carrier of (UN,R)

the Source of (UN,R) is Relation-like the carrier' of (UN,R) -defined the carrier of (UN,R) -valued V6() non empty total quasi_total Element of bool [: the carrier' of (UN,R), the carrier of (UN,R):]

the Source of (UN,R) . x is Element of the carrier of (UN,R)

G is Element of the carrier' of (UN,R)

cod G is Element of the carrier of (UN,R)

the Target of (UN,R) . G is Element of the carrier of (UN,R)

dom G is Element of the carrier of (UN,R)

the Source of (UN,R) . G is Element of the carrier of (UN,R)

G (*) a is Element of the carrier' of (UN,R)

x (*) (G (*) a) is Element of the carrier' of (UN,R)

x (*) G is Element of the carrier' of (UN,R)

(x (*) G) (*) a is Element of the carrier' of (UN,R)

the carrier of (UN,R) is non empty set

a is Element of the carrier of (UN,R)

Hom (a,a) is Element of bool the carrier' of (UN,R)

the carrier' of (UN,R) is non empty set

bool the carrier' of (UN,R) is set

{ b

GroupObjects UN is non empty Group_DOMAIN-like set

the carrier of R is non empty set

[: the carrier of R,1:] is set

Funcs ([: the carrier of R,1:],1) is V9() non empty FUNCTION_DOMAIN of [: the carrier of R,1:],1

{ [b

G is non empty right_complementable V96() V97() V98() V149(R) V150(R) V151(R) V152(R) (R,(UN,R))

x is set

(R,(UN,R),G) is strict LModMorphism-like (R,(R,(UN,R)))

ID G is strict LModMorphism-like Morphism of G,G

x1 is set

x2 is set

[x1,x2] is set

ii is non empty right_complementable V96() V97() V98() strict V149(R) V150(R) V151(R) V152(R) VectSpStr over R

the carrier of ii is non empty set

the addF of ii is Relation-like [: the carrier of ii, the carrier of ii:] -defined the carrier of ii -valued V6() total quasi_total Element of bool [:[: the carrier of ii, the carrier of ii:], the carrier of ii:]

[: the carrier of ii, the carrier of ii:] is set

[:[: the carrier of ii, the carrier of ii:], the carrier of ii:] is set

bool [:[: the carrier of ii, the carrier of ii:], the carrier of ii:] is set

the ZeroF of ii is Element of the carrier of ii

addLoopStr(# the carrier of ii, the addF of ii, the ZeroF of ii #) is strict addLoopStr

the lmult of ii is Relation-like [: the carrier of R, the carrier of ii:] -defined the carrier of ii -valued V6() total quasi_total Element of bool [:[: the carrier of R, the carrier of ii:], the carrier of ii:]

[: the carrier of R, the carrier of ii:] is set

[:[: the carrier of R, the carrier of ii:], the carrier of ii:] is set

bool [:[: the carrier of R, the carrier of ii:], the carrier of ii:] is set

ii is Element of the carrier' of (UN,R)

dom ii is Element of the carrier of (UN,R)

the Source of (UN,R) is Relation-like the carrier' of (UN,R) -defined the carrier of (UN,R) -valued V6() non empty total quasi_total Element of bool [: the carrier' of (UN,R), the carrier of (UN,R):]

[: the carrier' of (UN,R), the carrier of (UN,R):] is set

bool [: the carrier' of (UN,R), the carrier of (UN,R):] is set

the Source of (UN,R) . ii is Element of the carrier of (UN,R)

ia is LModMorphismStr over R

dom ia is non empty right_complementable V96() V97() V98() V149(R) V150(R) V151(R) V152(R) VectSpStr over R

cod ii is Element of the carrier of (UN,R)

the Target of (UN,R) is Relation-like the carrier' of (UN,R) -defined the carrier of (UN,R) -valued V6() non empty total quasi_total Element of bool [: the carrier' of (UN,R), the carrier of (UN,R):]

the Target of (UN,R) . ii is Element of the carrier of (UN,R)

cod ia is non empty right_complementable V96() V97() V98() V149(R) V150(R) V151(R) V152(R) VectSpStr over R