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,b1 #) where b1 is Relation-like the carrier of R -defined the carrier of C -valued V6() total quasi_total Element of Maps (R,C) : ( b1 is additive & b1 is homogeneous ) } is set
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
{ [b1,b2] where b1 is non empty right_complementable V97() V98() Element of GroupObjects R, b2 is Relation-like [: the carrier of UN,1:] -defined 1 -valued V6() total quasi_total Element of Funcs ([: the carrier of UN,1:],1) : verum } is set
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
{ [b1,b2] where b1 is non empty right_complementable V97() V98() Element of GroupObjects UN, b2 is Relation-like [: the carrier of R,1:] -defined 1 -valued V6() total quasi_total Element of Funcs ([: the carrier of R,1:],1) : verum } is set
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
{ [b1,b2] where b1 is non empty right_complementable V97() V98() Element of GroupObjects UN, b2 is Relation-like [: the carrier of R,1:] -defined 1 -valued V6() total quasi_total Element of Funcs ([: the carrier of R,1:],1) : verum } is set
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
{ [b1,b2] where b1 is non empty right_complementable V97() V98() Element of GroupObjects UN, b2 is Relation-like [: the carrier of R,1:] -defined 1 -valued V6() total quasi_total Element of Funcs ([: the carrier of R,1:],1) : verum } is set
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,b1,b2) where b1, b2 is non empty right_complementable V96() V97() V98() strict V149(UN) V150(UN) V151(UN) V152(UN) (UN,R) : verum } is set
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,b1,b2) where b1, b2 is non empty right_complementable V96() V97() V98() strict V149(UN) V150(UN) V151(UN) V152(UN) (UN,R) : verum } is set
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
{ b1 where b1 is Element of the carrier' of (UN,R) : ( dom b1 = a & cod b1 = a ) } 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
{ [b1,b2] where b1 is non empty right_complementable V97() V98() Element of GroupObjects UN, b2 is Relation-like [: the carrier of R,1:] -defined 1 -valued V6() total quasi_total Element of Funcs ([: the carrier of R,1:],1) : verum } is set
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