:: ALTCAT_4 semantic presentation

K154() is M2( bool K150())
K150() is set
bool K150() is non empty set
K116() is set
bool K116() is non empty set
bool K154() is non empty set
{} is set

1 is non empty set
{{},1} is set
C is non empty with_units reflexive AltCatStr
the carrier of C is non empty set
i is M2( the carrier of C)
<^i,i^> is set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the Arrows of C . (i,i) is set
[i,i] is V15() set
{i,i} is set
{i} is set
{{i,i},{i}} is set
the Arrows of C . [i,i] is set

the carrier of C is non empty set
i is M2( the carrier of C)
o1 is M2( the carrier of C)
<^i,o1^> is set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the Arrows of C . (i,o1) is set
[i,o1] is V15() set
{i,o1} is set
{i} is set
{{i,o1},{i}} is set
the Arrows of C . [i,o1] is set
idm o1 is M2(<^o1,o1^>)
<^o1,o1^> is non empty set
the Arrows of C . (o1,o1) is set
[o1,o1] is V15() set
{o1,o1} is set
{o1} is set
{{o1,o1},{o1}} is set
the Arrows of C . [o1,o1] is set
o2 is M2( the carrier of C)
<^i,o2^> is set
the Arrows of C . (i,o2) is set
[i,o2] is V15() set
{i,o2} is set
{{i,o2},{i}} is set
the Arrows of C . [i,o2] is set
<^o1,o2^> is set
the Arrows of C . (o1,o2) is set
[o1,o2] is V15() set
{o1,o2} is set
{{o1,o2},{o1}} is set
the Arrows of C . [o1,o2] is set
<^o2,o1^> is set
the Arrows of C . (o2,o1) is set
[o2,o1] is V15() set
{o2,o1} is set
{o2} is set
{{o2,o1},{o2}} is set
the Arrows of C . [o2,o1] is set
o1 is M2(<^i,o1^>)
o2 is M2(<^i,o2^>)
p1 is M2(<^o1,o2^>)
p1 * o1 is M2(<^i,o2^>)
p1 " is M2(<^o2,o1^>)
(p1 ") * p1 is M2(<^o1,o1^>)
(p1 ") * o2 is M2(<^i,o1^>)
((p1 ") * p1) * o1 is M2(<^i,o1^>)

the carrier of C is non empty set
i is M2( the carrier of C)
idm i is M2(<^i,i^>)
<^i,i^> is non empty set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the Arrows of C . (i,i) is set
[i,i] is V15() set
{i,i} is set
{i} is set
{{i,i},{i}} is set
the Arrows of C . [i,i] is set
o1 is M2( the carrier of C)
<^i,o1^> is set
the Arrows of C . (i,o1) is set
[i,o1] is V15() set
{i,o1} is set
{{i,o1},{i}} is set
the Arrows of C . [i,o1] is set
o2 is M2( the carrier of C)
<^o2,o1^> is set
the Arrows of C . (o2,o1) is set
[o2,o1] is V15() set
{o2,o1} is set
{o2} is set
{{o2,o1},{o2}} is set
the Arrows of C . [o2,o1] is set
<^o2,i^> is set
the Arrows of C . (o2,i) is set
[o2,i] is V15() set
{o2,i} is set
{{o2,i},{o2}} is set
the Arrows of C . [o2,i] is set
<^i,o2^> is set
the Arrows of C . (i,o2) is set
[i,o2] is V15() set
{i,o2} is set
{{i,o2},{i}} is set
the Arrows of C . [i,o2] is set
o1 is M2(<^i,o1^>)
o2 is M2(<^o2,o1^>)
p1 is M2(<^o2,i^>)
o1 * p1 is M2(<^o2,o1^>)
p1 " is M2(<^i,o2^>)
p1 * (p1 ") is M2(<^i,i^>)
o2 * (p1 ") is M2(<^i,o1^>)
o1 * (p1 * (p1 ")) is M2(<^i,o1^>)

the carrier of C is non empty set
i is M2( the carrier of C)
o1 is M2( the carrier of C)
<^i,o1^> is set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the Arrows of C . (i,o1) is set
[i,o1] is V15() set
{i,o1} is set
{i} is set
{{i,o1},{i}} is set
the Arrows of C . [i,o1] is set
<^o1,i^> is set
the Arrows of C . (o1,i) is set
[o1,i] is V15() set
{o1,i} is set
{o1} is set
{{o1,i},{o1}} is set
the Arrows of C . [o1,i] is set
o2 is M2(<^i,o1^>)
o2 " is M2(<^o1,i^>)
(o2 ") " is M2(<^i,o1^>)
(o2 ") * ((o2 ") ") is M2(<^i,i^>)
<^i,i^> is non empty set
the Arrows of C . (i,i) is set
[i,i] is V15() set
{i,i} is set
{{i,i},{i}} is set
the Arrows of C . [i,i] is set
(o2 ") * o2 is M2(<^i,i^>)
idm i is M2(<^i,i^>)
((o2 ") ") * (o2 ") is M2(<^o1,o1^>)
<^o1,o1^> is non empty set
the Arrows of C . (o1,o1) is set
[o1,o1] is V15() set
{o1,o1} is set
{{o1,o1},{o1}} is set
the Arrows of C . [o1,o1] is set
idm o1 is M2(<^o1,o1^>)
o2 * (o2 ") is M2(<^o1,o1^>)
C is non empty with_units reflexive AltCatStr
the carrier of C is non empty set
i is M2( the carrier of C)
idm i is M2(<^i,i^>)
<^i,i^> is non empty set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the Arrows of C . (i,i) is set
[i,i] is V15() set
{i,i} is set
{i} is set
{{i,i},{i}} is set
the Arrows of C . [i,i] is set
o1 is M2( the carrier of C)
<^i,o1^> is set
the Arrows of C . (i,o1) is set
[i,o1] is V15() set
{i,o1} is set
{{i,o1},{i}} is set
the Arrows of C . [i,o1] is set
o2 is M2(<^i,o1^>)
o2 * (idm i) is M2(<^i,o1^>)
o1 is M2(<^i,o1^>)
o1 * (idm i) is M2(<^i,o1^>)
o1 is M2( the carrier of C)
<^o1,i^> is set
the Arrows of C . (o1,i) is set
[o1,i] is V15() set
{o1,i} is set
{o1} is set
{{o1,i},{o1}} is set
the Arrows of C . [o1,i] is set
o2 is M2(<^o1,i^>)
(idm i) * o2 is M2(<^o1,i^>)
o1 is M2(<^o1,i^>)
(idm i) * o1 is M2(<^o1,i^>)
C is non empty with_units reflexive AltCatStr
the carrier of C is non empty set
i is M2( the carrier of C)
idm i is M2(<^i,i^>)
<^i,i^> is non empty set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the Arrows of C . (i,i) is set
[i,i] is V15() set
{i,i} is set
{i} is set
{{i,i},{i}} is set
the Arrows of C . [i,i] is set

the carrier of C is non empty set
i is M2( the carrier of C)

<^i,i^> is non empty set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the Arrows of C . (i,i) is set
[i,i] is V15() set
{i,i} is set
{i} is set
{{i,i},{i}} is set
the Arrows of C . [i,i] is set

the carrier of C is non empty set
i is M2( the carrier of C)

<^i,i^> is non empty set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the Arrows of C . (i,i) is set
[i,i] is V15() set
{i,i} is set
{i} is set
{{i,i},{i}} is set
the Arrows of C . [i,i] is set
o1 is M2( the carrier of C)
<^i,o1^> is set
the Arrows of C . (i,o1) is set
[i,o1] is V15() set
{i,o1} is set
{{i,o1},{i}} is set
the Arrows of C . [i,o1] is set
<^o1,i^> is set
the Arrows of C . (o1,i) is set
[o1,i] is V15() set
{o1,i} is set
{o1} is set
{{o1,i},{o1}} is set
the Arrows of C . [o1,i] is set
idm o1 is retraction coretraction iso mono epi M2(<^o1,o1^>)
<^o1,o1^> is non empty set
the Arrows of C . (o1,o1) is set
[o1,o1] is V15() set
{o1,o1} is set
{{o1,o1},{o1}} is set
the Arrows of C . [o1,o1] is set
o2 is M2(<^i,o1^>)
o2 is M2(<^o1,i^>)
o2 * o2 is M2(<^i,i^>)
o1 is M2(<^o1,i^>)
o2 * o1 is M2(<^o1,o1^>)
(o2 * o2) * o1 is M2(<^o1,i^>)
o2 * (idm o1) is M2(<^o1,i^>)

the carrier of C is non empty set
i is M2( the carrier of C)
o1 is M2( the carrier of C)
<^i,o1^> is set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the Arrows of C . (i,o1) is set
[i,o1] is V15() set
{i,o1} is set
{i} is set
{{i,o1},{i}} is set
the Arrows of C . [i,o1] is set
<^o1,i^> is set
the Arrows of C . (o1,i) is set
[o1,i] is V15() set
{o1,i} is set
{o1} is set
{{o1,i},{o1}} is set
the Arrows of C . [o1,i] is set
o2 is M2(<^i,o1^>)
o1 is M2(<^o1,i^>)
o2 * o1 is M2(<^o1,o1^>)
<^o1,o1^> is non empty set
the Arrows of C . (o1,o1) is set
[o1,o1] is V15() set
{o1,o1} is set
{{o1,o1},{o1}} is set
the Arrows of C . [o1,o1] is set
o1 * (o2 * o1) is M2(<^o1,i^>)
o1 * o2 is M2(<^i,i^>)
<^i,i^> is non empty set
the Arrows of C . (i,i) is set
[i,i] is V15() set
{i,i} is set
{{i,i},{i}} is set
the Arrows of C . [i,i] is set
(o1 * o2) * o1 is M2(<^o1,i^>)

(idm i) * o1 is M2(<^o1,i^>)
idm o1 is retraction coretraction iso mono epi M2(<^o1,o1^>)
o1 * (idm o1) is M2(<^o1,i^>)

the carrier of C is non empty set
i is M2( the carrier of C)
o1 is M2( the carrier of C)
<^i,o1^> is set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the Arrows of C . (i,o1) is set
[i,o1] is V15() set
{i,o1} is set
{i} is set
{{i,o1},{i}} is set
the Arrows of C . [i,o1] is set
o2 is M2(<^i,o1^>)
o1 is M2(<^i,o1^>)
o2 is M2( the carrier of C)
<^o2,o2^> is non empty set
the Arrows of C . (o2,o2) is set
[o2,o2] is V15() set
{o2,o2} is set
{o2} is set
{{o2,o2},{o2}} is set
the Arrows of C . [o2,o2] is set
the M2(<^o2,o2^>) is M2(<^o2,o2^>)
<^o2,o1^> is set
the Arrows of C . (o2,o1) is set
[o2,o1] is V15() set
{o2,o1} is set
{{o2,o1},{o2}} is set
the Arrows of C . [o2,o1] is set
the M2(<^o2,o1^>) is M2(<^o2,o1^>)
<^i,o2^> is set
the Arrows of C . (i,o2) is set
[i,o2] is V15() set
{i,o2} is set
{{i,o2},{i}} is set
the Arrows of C . [i,o2] is set
the M2(<^i,o2^>) is M2(<^i,o2^>)
the M2(<^o2,o2^>) " is M2(<^o2,o2^>)
( the M2(<^o2,o2^>) ") * the M2(<^o2,o2^>) is M2(<^o2,o2^>)
the M2(<^o2,o1^>) * (( the M2(<^o2,o2^>) ") * the M2(<^o2,o2^>)) is M2(<^o2,o1^>)
( the M2(<^o2,o1^>) * (( the M2(<^o2,o2^>) ") * the M2(<^o2,o2^>))) * the M2(<^i,o2^>) is M2(<^i,o1^>)
C is non empty AltCatStr
the carrier of C is non empty set
i is M2( the carrier of C)
o1 is M2( the carrier of C)
<^i,o1^> is set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the Arrows of C . (i,o1) is set
[i,o1] is V15() set
{i,o1} is set
{i} is set
{{i,o1},{i}} is set
the Arrows of C . [i,o1] is set
o2 is M2(<^i,o1^>)
o1 is M2( the carrier of C)
<^o1,i^> is set
the Arrows of C . (o1,i) is set
[o1,i] is V15() set
{o1,i} is set
{o1} is set
{{o1,i},{o1}} is set
the Arrows of C . [o1,i] is set
o2 is M2(<^o1,i^>)
o2 * o2 is M2(<^o1,o1^>)
<^o1,o1^> is set
the Arrows of C . (o1,o1) is set
[o1,o1] is V15() set
{o1,o1} is set
{{o1,o1},{o1}} is set
the Arrows of C . [o1,o1] is set
p1 is M2(<^o1,i^>)
o2 * p1 is M2(<^o1,o1^>)
p2 is M2(<^o1,i^>)
C is non empty AltCatStr
the carrier of C is non empty set
o1 is M2( the carrier of C)
i is M2( the carrier of C)
<^o1,i^> is set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the Arrows of C . (o1,i) is set
[o1,i] is V15() set
{o1,i} is set
{o1} is set
{{o1,i},{o1}} is set
the Arrows of C . [o1,i] is set
o2 is M2(<^o1,i^>)
o1 is M2( the carrier of C)
<^i,o1^> is set
the Arrows of C . (i,o1) is set
[i,o1] is V15() set
{i,o1} is set
{i} is set
{{i,o1},{i}} is set
the Arrows of C . [i,o1] is set
o2 is M2(<^i,o1^>)
o2 * o2 is M2(<^o1,o1^>)
<^o1,o1^> is set
the Arrows of C . (o1,o1) is set
[o1,o1] is V15() set
{o1,o1} is set
{{o1,o1},{o1}} is set
the Arrows of C . [o1,o1] is set
p1 is M2(<^i,o1^>)
p1 * o2 is M2(<^o1,o1^>)
p2 is M2(<^i,o1^>)

the carrier of C is non empty set
i is M2( the carrier of C)
o1 is M2( the carrier of C)
<^o1,i^> is set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the Arrows of C . (o1,i) is set
[o1,i] is V15() set
{o1,i} is set
{o1} is set
{{o1,i},{o1}} is set
the Arrows of C . [o1,i] is set
o2 is M2(<^o1,i^>)
o2 " is M2(<^i,o1^>)
<^i,o1^> is set
the Arrows of C . (i,o1) is set
[i,o1] is V15() set
{i,o1} is set
{i} is set
{{i,o1},{i}} is set
the Arrows of C . [i,o1] is set
(o2 ") * o2 is M2(<^o1,o1^>)
<^o1,o1^> is non empty set
the Arrows of C . (o1,o1) is set
[o1,o1] is V15() set
{o1,o1} is set
{{o1,o1},{o1}} is set
the Arrows of C . [o1,o1] is set
idm o1 is retraction coretraction iso mono epi M2(<^o1,o1^>)
o1 is M2( the carrier of C)
<^o1,o1^> is set
the Arrows of C . (o1,o1) is set
[o1,o1] is V15() set
{o1,o1} is set
{o1} is set
{{o1,o1},{o1}} is set
the Arrows of C . [o1,o1] is set
<^o1,i^> is set
the Arrows of C . (o1,i) is set
[o1,i] is V15() set
{o1,i} is set
{{o1,i},{o1}} is set
the Arrows of C . [o1,i] is set
o2 is M2(<^o1,i^>)
(o2 ") * o2 is M2(<^o1,o1^>)
p1 is M2(<^o1,o1^>)
o2 * p1 is M2(<^o1,i^>)

the carrier of C is non empty set
i is M2( the carrier of C)
o1 is M2( the carrier of C)
<^i,o1^> is set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the Arrows of C . (i,o1) is set
[i,o1] is V15() set
{i,o1} is set
{i} is set
{{i,o1},{i}} is set
the Arrows of C . [i,o1] is set
o2 is M2(<^i,o1^>)
o2 " is M2(<^o1,i^>)
<^o1,i^> is set
the Arrows of C . (o1,i) is set
[o1,i] is V15() set
{o1,i} is set
{o1} is set
{{o1,i},{o1}} is set
the Arrows of C . [o1,i] is set
o2 * (o2 ") is M2(<^o1,o1^>)
<^o1,o1^> is non empty set
the Arrows of C . (o1,o1) is set
[o1,o1] is V15() set
{o1,o1} is set
{{o1,o1},{o1}} is set
the Arrows of C . [o1,o1] is set
idm o1 is retraction coretraction iso mono epi M2(<^o1,o1^>)
o1 is M2( the carrier of C)
<^o1,o1^> is set
the Arrows of C . (o1,o1) is set
[o1,o1] is V15() set
{o1,o1} is set
{{o1,o1},{o1}} is set
the Arrows of C . [o1,o1] is set
<^i,o1^> is set
the Arrows of C . (i,o1) is set
[i,o1] is V15() set
{i,o1} is set
{{i,o1},{i}} is set
the Arrows of C . [i,o1] is set
o2 is M2(<^i,o1^>)
o2 * (o2 ") is M2(<^o1,o1^>)
p1 is M2(<^o1,o1^>)
p1 * o2 is M2(<^i,o1^>)

the carrier of C is non empty set
i is M2( the carrier of C)
o1 is M2( the carrier of C)
<^o1,i^> is set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the Arrows of C . (o1,i) is set
[o1,i] is V15() set
{o1,i} is set
{o1} is set
{{o1,i},{o1}} is set
the Arrows of C . [o1,i] is set
<^i,o1^> is set
the Arrows of C . (i,o1) is set
[i,o1] is V15() set
{i,o1} is set
{i} is set
{{i,o1},{i}} is set
the Arrows of C . [i,o1] is set
o2 is M2(<^i,o1^>)
o1 is set
p1 is M2( the carrier of C)
<^o1,p1^> is set
the Arrows of C . (o1,p1) is set
[o1,p1] is V15() set
{o1,p1} is set
{{o1,p1},{o1}} is set
the Arrows of C . [o1,p1] is set
<^i,p1^> is set
the Arrows of C . (i,p1) is set
[i,p1] is V15() set
{i,p1} is set
{{i,p1},{i}} is set
the Arrows of C . [i,p1] is set
p2 is M2(<^i,p1^>)
o2 is M2(<^o1,i^>)
p2 * o2 is M2(<^o1,p1^>)
n is M2(<^o1,p1^>)
<^o1,o1^> is non empty set
the Arrows of C . (o1,o1) is set
[o1,o1] is V15() set
{o1,o1} is set
{{o1,o1},{o1}} is set
the Arrows of C . [o1,o1] is set
n2 is M2(<^o1,o1^>)
n * o2 is M2(<^i,p1^>)
(n * o2) * o2 is M2(<^o1,p1^>)
o2 * o2 is M2(<^o1,o1^>)
n * (o2 * o2) is M2(<^o1,p1^>)
n * n2 is M2(<^o1,p1^>)
idm o1 is retraction coretraction iso mono epi M2(<^o1,o1^>)
n * (idm o1) is M2(<^o1,p1^>)
p1 is M2( the carrier of C)
<^p1,i^> is set
the Arrows of C . (p1,i) is set
[p1,i] is V15() set
{p1,i} is set
{p1} is set
{{p1,i},{p1}} is set
the Arrows of C . [p1,i] is set
<^p1,o1^> is set
the Arrows of C . (p1,o1) is set
[p1,o1] is V15() set
{p1,o1} is set
{{p1,o1},{p1}} is set
the Arrows of C . [p1,o1] is set
p2 is M2(<^p1,o1^>)
o2 is M2(<^o1,i^>)
o2 * p2 is M2(<^p1,i^>)
n is M2(<^p1,i^>)
<^i,i^> is non empty set
the Arrows of C . (i,i) is set
[i,i] is V15() set
{i,i} is set
{{i,i},{i}} is set
the Arrows of C . [i,i] is set
n2 is M2(<^i,i^>)
o2 * n is M2(<^p1,o1^>)
o2 * (o2 * n) is M2(<^p1,i^>)
o2 * o2 is M2(<^i,i^>)
(o2 * o2) * n is M2(<^p1,i^>)
n2 * n is M2(<^p1,i^>)

(idm i) * n is M2(<^p1,i^>)

the carrier of C is non empty set

o2 is M2( the carrier of C)
idm o2 is retraction coretraction mono epi M2(<^o2,o2^>)
<^o2,o2^> is non empty set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the Arrows of C . (o2,o2) is set
[o2,o2] is V15() set
{o2,o2} is set
{o2} is set
{{o2,o2},{o2}} is set
the Arrows of C . [o2,o2] is set
o1 . (idm o2) is M2(<^(o1 . o2),(o1 . o2)^>)
o1 . o2 is M2( the carrier of i)
the carrier of i is non empty set
[: the carrier of i, the carrier of i:] is Relation-like non empty set
the ObjectMap of o1 is Relation-like [: the carrier of C, the carrier of C:] -defined [: the carrier of i, the carrier of i:] -valued Function-like quasi_total M2( bool [:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:])
[:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:] is Relation-like non empty set
bool [:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:] is non empty set
the ObjectMap of o1 . (o2,o2) is M2([: the carrier of i, the carrier of i:])
the ObjectMap of o1 . [o2,o2] is set
K40(( the ObjectMap of o1 . (o2,o2))) is set
<^(o1 . o2),(o1 . o2)^> is non empty set
the Arrows of i is Relation-like [: the carrier of i, the carrier of i:] -defined Function-like non empty V14([: the carrier of i, the carrier of i:]) set
the Arrows of i . ((o1 . o2),(o1 . o2)) is set
[(o1 . o2),(o1 . o2)] is V15() set
{(o1 . o2),(o1 . o2)} is set
{(o1 . o2)} is set
{{(o1 . o2),(o1 . o2)},{(o1 . o2)}} is set
the Arrows of i . [(o1 . o2),(o1 . o2)] is set
idm (o1 . o2) is retraction coretraction mono epi M2(<^(o1 . o2),(o1 . o2)^>)
Morph-Map (o1,o2,o2) is Relation-like <^o2,o2^> -defined <^(o1 . o2),(o1 . o2)^> -valued Function-like quasi_total M2( bool [:<^o2,o2^>,<^(o1 . o2),(o1 . o2)^>:])
[:<^o2,o2^>,<^(o1 . o2),(o1 . o2)^>:] is Relation-like non empty set
bool [:<^o2,o2^>,<^(o1 . o2),(o1 . o2)^>:] is non empty set
the MorphMap of o1 is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) V36() V37() MSUnTrans of the ObjectMap of o1, the Arrows of C, the Arrows of i
the MorphMap of o1 . (o2,o2) is set
the MorphMap of o1 . [o2,o2] is Relation-like Function-like set
(Morph-Map (o1,o2,o2)) . (idm o2) is M2(<^(o1 . o2),(o1 . o2)^>)
C is non empty AltCatStr
i is non empty AltCatStr
the carrier of C is non empty set
o1 is reflexive Contravariant FunctorStr over C,i
[: the carrier of C, the carrier of C:] is Relation-like non empty set
o1 is M2( the carrier of C)
o1 . o1 is M2( the carrier of i)
the carrier of i is non empty set
[: the carrier of i, the carrier of i:] is Relation-like non empty set
the ObjectMap of o1 is Relation-like [: the carrier of C, the carrier of C:] -defined [: the carrier of i, the carrier of i:] -valued Function-like quasi_total M2( bool [:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:])
[:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:] is Relation-like non empty set
bool [:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:] is non empty set
the ObjectMap of o1 . (o1,o1) is M2([: the carrier of i, the carrier of i:])
[o1,o1] is V15() set
{o1,o1} is set
{o1} is set
{{o1,o1},{o1}} is set
the ObjectMap of o1 . [o1,o1] is set
K40(( the ObjectMap of o1 . (o1,o1))) is set
o2 is M2( the carrier of C)
o1 . o2 is M2( the carrier of i)
the ObjectMap of o1 . (o2,o2) is M2([: the carrier of i, the carrier of i:])
[o2,o2] is V15() set
{o2,o2} is set
{o2} is set
{{o2,o2},{o2}} is set
the ObjectMap of o1 . [o2,o2] is set
K40(( the ObjectMap of o1 . (o2,o2))) is set
<^(o1 . o1),(o1 . o2)^> is set
the Arrows of i is Relation-like [: the carrier of i, the carrier of i:] -defined Function-like non empty V14([: the carrier of i, the carrier of i:]) set
the Arrows of i . ((o1 . o1),(o1 . o2)) is set
[(o1 . o1),(o1 . o2)] is V15() set
{(o1 . o1),(o1 . o2)} is set
{(o1 . o1)} is set
{{(o1 . o1),(o1 . o2)},{(o1 . o1)}} is set
the Arrows of i . [(o1 . o1),(o1 . o2)] is set
Morph-Map (o1,o2,o1) is Relation-like <^o2,o1^> -defined <^(o1 . o1),(o1 . o2)^> -valued Function-like quasi_total M2( bool [:<^o2,o1^>,<^(o1 . o1),(o1 . o2)^>:])
<^o2,o1^> is set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
the Arrows of C . (o2,o1) is set
[o2,o1] is V15() set
{o2,o1} is set
{{o2,o1},{o2}} is set
the Arrows of C . [o2,o1] is set
[:<^o2,o1^>,<^(o1 . o1),(o1 . o2)^>:] is Relation-like set
bool [:<^o2,o1^>,<^(o1 . o1),(o1 . o2)^>:] is non empty set
the MorphMap of o1 is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) V36() V37() MSUnTrans of the ObjectMap of o1, the Arrows of C, the Arrows of i
the MorphMap of o1 . (o2,o1) is set
the MorphMap of o1 . [o2,o1] is Relation-like Function-like set
proj1 the ObjectMap of o1 is Relation-like set
the ObjectMap of o1 * the Arrows of i is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
p1 is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) V36() V37() ManySortedFunction of the Arrows of C, the ObjectMap of o1 * the Arrows of i
p1 . [o2,o1] is Relation-like Function-like set
proj2 (p1 . [o2,o1]) is set
( the ObjectMap of o1 * the Arrows of i) . [o2,o1] is set
proj2 (Morph-Map (o1,o2,o1)) is set
the ObjectMap of o1 . (o2,o1) is M2([: the carrier of i, the carrier of i:])
the ObjectMap of o1 . [o2,o1] is set
the Arrows of i . ( the ObjectMap of o1 . (o2,o1)) is set
the ObjectMap of o1 * the Arrows of i is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
o2 is non empty set
[:[: the carrier of C, the carrier of C:],o2:] is Relation-like non empty set
bool [:[: the carrier of C, the carrier of C:],o2:] is non empty set
p2 is Relation-like [: the carrier of C, the carrier of C:] -defined o2 -valued Function-like quasi_total M2( bool [:[: the carrier of C, the carrier of C:],o2:])
p1 is Relation-like o2 -defined Function-like non empty V14(o2) set
p2 * p1 is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
o1 is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) V36() V37() ManySortedFunction of the Arrows of C, the ObjectMap of o1 * the Arrows of i
o2 is set

proj2 (o1 . o2) is set
( the ObjectMap of o1 * the Arrows of i) . o2 is set
p1 is set
p2 is set
[p1,p2] is V15() set
{p1,p2} is set
{p1} is set
{{p1,p2},{p1}} is set
n2 is M2( the carrier of C)
n is M2( the carrier of C)
[n2,n] is V15() set
{n2,n} is set
{n2} is set
{{n2,n},{n2}} is set
proj1 the ObjectMap of o1 is Relation-like set
o1 . n is M2( the carrier of i)
the ObjectMap of o1 . (n,n) is M2([: the carrier of i, the carrier of i:])
[n,n] is V15() set
{n,n} is set
{n} is set
{{n,n},{n}} is set
the ObjectMap of o1 . [n,n] is set
K40(( the ObjectMap of o1 . (n,n))) is set
o1 . n2 is M2( the carrier of i)
the ObjectMap of o1 . (n2,n2) is M2([: the carrier of i, the carrier of i:])
[n2,n2] is V15() set
{n2,n2} is set
{{n2,n2},{n2}} is set
the ObjectMap of o1 . [n2,n2] is set
K40(( the ObjectMap of o1 . (n2,n2))) is set
<^(o1 . n),(o1 . n2)^> is set
the Arrows of i . ((o1 . n),(o1 . n2)) is set
[(o1 . n),(o1 . n2)] is V15() set
{(o1 . n),(o1 . n2)} is set
{(o1 . n)} is set
{{(o1 . n),(o1 . n2)},{(o1 . n)}} is set
the Arrows of i . [(o1 . n),(o1 . n2)] is set
Morph-Map (o1,n2,n) is Relation-like <^n2,n^> -defined <^(o1 . n),(o1 . n2)^> -valued Function-like quasi_total M2( bool [:<^n2,n^>,<^(o1 . n),(o1 . n2)^>:])
<^n2,n^> is set
the Arrows of C . (n2,n) is set
the Arrows of C . [n2,n] is set
[:<^n2,n^>,<^(o1 . n),(o1 . n2)^>:] is Relation-like set
bool [:<^n2,n^>,<^(o1 . n),(o1 . n2)^>:] is non empty set
the MorphMap of o1 . (n2,n) is set
the MorphMap of o1 . [n2,n] is Relation-like Function-like set
proj2 (Morph-Map (o1,n2,n)) is set
the ObjectMap of o1 . (n2,n) is M2([: the carrier of i, the carrier of i:])
the ObjectMap of o1 . [n2,n] is set
the Arrows of i . ( the ObjectMap of o1 . (n2,n)) is set
( the ObjectMap of o1 * the Arrows of i) . [n2,n] is set
C is non empty AltCatStr
i is non empty AltCatStr
the carrier of C is non empty set
o1 is reflexive Contravariant FunctorStr over C,i
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the MorphMap of o1 is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) V36() V37() MSUnTrans of the ObjectMap of o1, the Arrows of C, the Arrows of i
the carrier of i is non empty set
[: the carrier of i, the carrier of i:] is Relation-like non empty set
the ObjectMap of o1 is Relation-like [: the carrier of C, the carrier of C:] -defined [: the carrier of i, the carrier of i:] -valued Function-like quasi_total M2( bool [:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:])
[:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:] is Relation-like non empty set
bool [:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:] is non empty set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
the Arrows of i is Relation-like [: the carrier of i, the carrier of i:] -defined Function-like non empty V14([: the carrier of i, the carrier of i:]) set
o2 is M2( the carrier of C)
o1 is M2( the carrier of C)
[o2,o1] is V15() set
{o2,o1} is set
{o2} is set
{{o2,o1},{o2}} is set
proj1 the MorphMap of o1 is non empty set
Morph-Map (o1,o2,o1) is Relation-like <^o2,o1^> -defined <^(o1 . o1),(o1 . o2)^> -valued Function-like quasi_total M2( bool [:<^o2,o1^>,<^(o1 . o1),(o1 . o2)^>:])
<^o2,o1^> is set
the Arrows of C . (o2,o1) is set
the Arrows of C . [o2,o1] is set
o1 . o1 is M2( the carrier of i)
the ObjectMap of o1 . (o1,o1) is M2([: the carrier of i, the carrier of i:])
[o1,o1] is V15() set
{o1,o1} is set
{o1} is set
{{o1,o1},{o1}} is set
the ObjectMap of o1 . [o1,o1] is set
K40(( the ObjectMap of o1 . (o1,o1))) is set
o1 . o2 is M2( the carrier of i)
the ObjectMap of o1 . (o2,o2) is M2([: the carrier of i, the carrier of i:])
[o2,o2] is V15() set
{o2,o2} is set
{{o2,o2},{o2}} is set
the ObjectMap of o1 . [o2,o2] is set
K40(( the ObjectMap of o1 . (o2,o2))) is set
<^(o1 . o1),(o1 . o2)^> is set
the Arrows of i . ((o1 . o1),(o1 . o2)) is set
[(o1 . o1),(o1 . o2)] is V15() set
{(o1 . o1),(o1 . o2)} is set
{(o1 . o1)} is set
{{(o1 . o1),(o1 . o2)},{(o1 . o1)}} is set
the Arrows of i . [(o1 . o1),(o1 . o2)] is set
[:<^o2,o1^>,<^(o1 . o1),(o1 . o2)^>:] is Relation-like set
bool [:<^o2,o1^>,<^(o1 . o1),(o1 . o2)^>:] is non empty set
the MorphMap of o1 . (o2,o1) is set
the MorphMap of o1 . [o2,o1] is Relation-like Function-like set
o1 is set
the MorphMap of o1 . o1 is Relation-like Function-like set

p1 is set
p2 is set
[p1,p2] is V15() set
{p1,p2} is set
{p1} is set
{{p1,p2},{p1}} is set
n is M2( the carrier of C)
n2 is M2( the carrier of C)
the MorphMap of o1 . (n,n2) is set
[n,n2] is V15() set
{n,n2} is set
{n} is set
{{n,n2},{n}} is set
the MorphMap of o1 . [n,n2] is Relation-like Function-like set
Morph-Map (o1,n,n2) is Relation-like <^n,n2^> -defined <^(o1 . n2),(o1 . n)^> -valued Function-like quasi_total M2( bool [:<^n,n2^>,<^(o1 . n2),(o1 . n)^>:])
<^n,n2^> is set
the Arrows of C . (n,n2) is set
the Arrows of C . [n,n2] is set
o1 . n2 is M2( the carrier of i)
the ObjectMap of o1 . (n2,n2) is M2([: the carrier of i, the carrier of i:])
[n2,n2] is V15() set
{n2,n2} is set
{n2} is set
{{n2,n2},{n2}} is set
the ObjectMap of o1 . [n2,n2] is set
K40(( the ObjectMap of o1 . (n2,n2))) is set
o1 . n is M2( the carrier of i)
the ObjectMap of o1 . (n,n) is M2([: the carrier of i, the carrier of i:])
[n,n] is V15() set
{n,n} is set
{{n,n},{n}} is set
the ObjectMap of o1 . [n,n] is set
K40(( the ObjectMap of o1 . (n,n))) is set
<^(o1 . n2),(o1 . n)^> is set
the Arrows of i . ((o1 . n2),(o1 . n)) is set
[(o1 . n2),(o1 . n)] is V15() set
{(o1 . n2),(o1 . n)} is set
{(o1 . n2)} is set
{{(o1 . n2),(o1 . n)},{(o1 . n2)}} is set
the Arrows of i . [(o1 . n2),(o1 . n)] is set
[:<^n,n2^>,<^(o1 . n2),(o1 . n)^>:] is Relation-like set
bool [:<^n,n2^>,<^(o1 . n2),(o1 . n)^>:] is non empty set
C is non empty AltCatStr
i is non empty AltCatStr
the carrier of C is non empty set
o1 is reflexive Covariant FunctorStr over C,i
o2 is M2( the carrier of C)
o1 . o2 is M2( the carrier of i)
the carrier of i is non empty set
[: the carrier of i, the carrier of i:] is Relation-like non empty set
the ObjectMap of o1 is Relation-like [: the carrier of C, the carrier of C:] -defined [: the carrier of i, the carrier of i:] -valued Function-like quasi_total M2( bool [:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:])
[: the carrier of C, the carrier of C:] is Relation-like non empty set
[:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:] is Relation-like non empty set
bool [:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:] is non empty set
the ObjectMap of o1 . (o2,o2) is M2([: the carrier of i, the carrier of i:])
[o2,o2] is V15() set
{o2,o2} is set
{o2} is set
{{o2,o2},{o2}} is set
the ObjectMap of o1 . [o2,o2] is set
K40(( the ObjectMap of o1 . (o2,o2))) is set
o1 is M2( the carrier of C)
o1 . o1 is M2( the carrier of i)
the ObjectMap of o1 . (o1,o1) is M2([: the carrier of i, the carrier of i:])
[o1,o1] is V15() set
{o1,o1} is set
{o1} is set
{{o1,o1},{o1}} is set
the ObjectMap of o1 . [o1,o1] is set
K40(( the ObjectMap of o1 . (o1,o1))) is set
<^(o1 . o2),(o1 . o1)^> is set
the Arrows of i is Relation-like [: the carrier of i, the carrier of i:] -defined Function-like non empty V14([: the carrier of i, the carrier of i:]) set
the Arrows of i . ((o1 . o2),(o1 . o1)) is set
[(o1 . o2),(o1 . o1)] is V15() set
{(o1 . o2),(o1 . o1)} is set
{(o1 . o2)} is set
{{(o1 . o2),(o1 . o1)},{(o1 . o2)}} is set
the Arrows of i . [(o1 . o2),(o1 . o1)] is set
<^o2,o1^> is set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
the Arrows of C . (o2,o1) is set
[o2,o1] is V15() set
{o2,o1} is set
{{o2,o1},{o2}} is set
the Arrows of C . [o2,o1] is set
o2 is M2(<^(o1 . o2),(o1 . o1)^>)
Morph-Map (o1,o2,o1) is Relation-like <^o2,o1^> -defined <^(o1 . o2),(o1 . o1)^> -valued Function-like quasi_total M2( bool [:<^o2,o1^>,<^(o1 . o2),(o1 . o1)^>:])
[:<^o2,o1^>,<^(o1 . o2),(o1 . o1)^>:] is Relation-like set
bool [:<^o2,o1^>,<^(o1 . o2),(o1 . o1)^>:] is non empty set
the MorphMap of o1 is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) V36() V37() MSUnTrans of the ObjectMap of o1, the Arrows of C, the Arrows of i
the MorphMap of o1 . (o2,o1) is set
the MorphMap of o1 . [o2,o1] is Relation-like Function-like set
proj2 (Morph-Map (o1,o2,o1)) is set
proj1 (Morph-Map (o1,o2,o1)) is set
p1 is set
(Morph-Map (o1,o2,o1)) . p1 is set
p2 is M2(<^o2,o1^>)
o1 . p2 is M2(<^(o1 . o2),(o1 . o1)^>)
C is non empty AltCatStr
i is non empty AltCatStr
the carrier of C is non empty set
o1 is reflexive Contravariant FunctorStr over C,i
o1 is M2( the carrier of C)
o1 . o1 is M2( the carrier of i)
the carrier of i is non empty set
[: the carrier of i, the carrier of i:] is Relation-like non empty set
the ObjectMap of o1 is Relation-like [: the carrier of C, the carrier of C:] -defined [: the carrier of i, the carrier of i:] -valued Function-like quasi_total M2( bool [:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:])
[: the carrier of C, the carrier of C:] is Relation-like non empty set
[:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:] is Relation-like non empty set
bool [:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:] is non empty set
the ObjectMap of o1 . (o1,o1) is M2([: the carrier of i, the carrier of i:])
[o1,o1] is V15() set
{o1,o1} is set
{o1} is set
{{o1,o1},{o1}} is set
the ObjectMap of o1 . [o1,o1] is set
K40(( the ObjectMap of o1 . (o1,o1))) is set
o2 is M2( the carrier of C)
o1 . o2 is M2( the carrier of i)
the ObjectMap of o1 . (o2,o2) is M2([: the carrier of i, the carrier of i:])
[o2,o2] is V15() set
{o2,o2} is set
{o2} is set
{{o2,o2},{o2}} is set
the ObjectMap of o1 . [o2,o2] is set
K40(( the ObjectMap of o1 . (o2,o2))) is set
<^(o1 . o1),(o1 . o2)^> is set
the Arrows of i is Relation-like [: the carrier of i, the carrier of i:] -defined Function-like non empty V14([: the carrier of i, the carrier of i:]) set
the Arrows of i . ((o1 . o1),(o1 . o2)) is set
[(o1 . o1),(o1 . o2)] is V15() set
{(o1 . o1),(o1 . o2)} is set
{(o1 . o1)} is set
{{(o1 . o1),(o1 . o2)},{(o1 . o1)}} is set
the Arrows of i . [(o1 . o1),(o1 . o2)] is set
<^o2,o1^> is set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
the Arrows of C . (o2,o1) is set
[o2,o1] is V15() set
{o2,o1} is set
{{o2,o1},{o2}} is set
the Arrows of C . [o2,o1] is set
o2 is M2(<^(o1 . o1),(o1 . o2)^>)
Morph-Map (o1,o2,o1) is Relation-like <^o2,o1^> -defined <^(o1 . o1),(o1 . o2)^> -valued Function-like quasi_total M2( bool [:<^o2,o1^>,<^(o1 . o1),(o1 . o2)^>:])
[:<^o2,o1^>,<^(o1 . o1),(o1 . o2)^>:] is Relation-like set
bool [:<^o2,o1^>,<^(o1 . o1),(o1 . o2)^>:] is non empty set
the MorphMap of o1 is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) V36() V37() MSUnTrans of the ObjectMap of o1, the Arrows of C, the Arrows of i
the MorphMap of o1 . (o2,o1) is set
the MorphMap of o1 . [o2,o1] is Relation-like Function-like set
proj2 (Morph-Map (o1,o2,o1)) is set
proj1 (Morph-Map (o1,o2,o1)) is set
p1 is set
(Morph-Map (o1,o2,o1)) . p1 is set
p2 is M2(<^o2,o1^>)
o1 . p2 is M2(<^(o1 . o1),(o1 . o2)^>)

the carrier of C is non empty set

o2 is M2( the carrier of C)
o1 is M2( the carrier of C)
<^o2,o1^> is set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the Arrows of C . (o2,o1) is set
[o2,o1] is V15() set
{o2,o1} is set
{o2} is set
{{o2,o1},{o2}} is set
the Arrows of C . [o2,o1] is set
<^o1,o2^> is set
the Arrows of C . (o1,o2) is set
[o1,o2] is V15() set
{o1,o2} is set
{o1} is set
{{o1,o2},{o1}} is set
the Arrows of C . [o1,o2] is set
o1 . o2 is M2( the carrier of i)
the carrier of i is non empty set
[: the carrier of i, the carrier of i:] is Relation-like non empty set
the ObjectMap of o1 is Relation-like [: the carrier of C, the carrier of C:] -defined [: the carrier of i, the carrier of i:] -valued Function-like quasi_total M2( bool [:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:])
[:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:] is Relation-like non empty set
bool [:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:] is non empty set
the ObjectMap of o1 . (o2,o2) is M2([: the carrier of i, the carrier of i:])
[o2,o2] is V15() set
{o2,o2} is set
{{o2,o2},{o2}} is set
the ObjectMap of o1 . [o2,o2] is set
K40(( the ObjectMap of o1 . (o2,o2))) is set
o1 . o1 is M2( the carrier of i)
the ObjectMap of o1 . (o1,o1) is M2([: the carrier of i, the carrier of i:])
[o1,o1] is V15() set
{o1,o1} is set
{{o1,o1},{o1}} is set
the ObjectMap of o1 . [o1,o1] is set
K40(( the ObjectMap of o1 . (o1,o1))) is set
o2 is M2(<^o2,o1^>)
o1 . o2 is M2(<^(o1 . o2),(o1 . o1)^>)
<^(o1 . o2),(o1 . o1)^> is set
the Arrows of i is Relation-like [: the carrier of i, the carrier of i:] -defined Function-like non empty V14([: the carrier of i, the carrier of i:]) set
the Arrows of i . ((o1 . o2),(o1 . o1)) is set
[(o1 . o2),(o1 . o1)] is V15() set
{(o1 . o2),(o1 . o1)} is set
{(o1 . o2)} is set
{{(o1 . o2),(o1 . o1)},{(o1 . o2)}} is set
the Arrows of i . [(o1 . o2),(o1 . o1)] is set
p1 is M2(<^o1,o2^>)
o1 . p1 is M2(<^(o1 . o1),(o1 . o2)^>)
<^(o1 . o1),(o1 . o2)^> is set
the Arrows of i . ((o1 . o1),(o1 . o2)) is set
[(o1 . o1),(o1 . o2)] is V15() set
{(o1 . o1),(o1 . o2)} is set
{(o1 . o1)} is set
{{(o1 . o1),(o1 . o2)},{(o1 . o1)}} is set
the Arrows of i . [(o1 . o1),(o1 . o2)] is set
o2 * p1 is M2(<^o1,o1^>)
<^o1,o1^> is non empty set
the Arrows of C . (o1,o1) is set
the Arrows of C . [o1,o1] is set
idm o1 is retraction coretraction mono epi M2(<^o1,o1^>)
(o1 . o2) * (o1 . p1) is M2(<^(o1 . o1),(o1 . o1)^>)
<^(o1 . o1),(o1 . o1)^> is non empty set
the Arrows of i . ((o1 . o1),(o1 . o1)) is set
[(o1 . o1),(o1 . o1)] is V15() set
{(o1 . o1),(o1 . o1)} is set
{{(o1 . o1),(o1 . o1)},{(o1 . o1)}} is set
the Arrows of i . [(o1 . o1),(o1 . o1)] is set
o1 . (idm o1) is M2(<^(o1 . o1),(o1 . o1)^>)
idm (o1 . o1) is retraction coretraction mono epi M2(<^(o1 . o1),(o1 . o1)^>)

the carrier of C is non empty set

o2 is M2( the carrier of C)
o1 is M2( the carrier of C)
<^o2,o1^> is set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the Arrows of C . (o2,o1) is set
[o2,o1] is V15() set
{o2,o1} is set
{o2} is set
{{o2,o1},{o2}} is set
the Arrows of C . [o2,o1] is set
<^o1,o2^> is set
the Arrows of C . (o1,o2) is set
[o1,o2] is V15() set
{o1,o2} is set
{o1} is set
{{o1,o2},{o1}} is set
the Arrows of C . [o1,o2] is set
o1 . o2 is M2( the carrier of i)
the carrier of i is non empty set
[: the carrier of i, the carrier of i:] is Relation-like non empty set
the ObjectMap of o1 is Relation-like [: the carrier of C, the carrier of C:] -defined [: the carrier of i, the carrier of i:] -valued Function-like quasi_total M2( bool [:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:])
[:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:] is Relation-like non empty set
bool [:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:] is non empty set
the ObjectMap of o1 . (o2,o2) is M2([: the carrier of i, the carrier of i:])
[o2,o2] is V15() set
{o2,o2} is set
{{o2,o2},{o2}} is set
the ObjectMap of o1 . [o2,o2] is set
K40(( the ObjectMap of o1 . (o2,o2))) is set
o1 . o1 is M2( the carrier of i)
the ObjectMap of o1 . (o1,o1) is M2([: the carrier of i, the carrier of i:])
[o1,o1] is V15() set
{o1,o1} is set
{{o1,o1},{o1}} is set
the ObjectMap of o1 . [o1,o1] is set
K40(( the ObjectMap of o1 . (o1,o1))) is set
o2 is M2(<^o2,o1^>)
o1 . o2 is M2(<^(o1 . o2),(o1 . o1)^>)
<^(o1 . o2),(o1 . o1)^> is set
the Arrows of i is Relation-like [: the carrier of i, the carrier of i:] -defined Function-like non empty V14([: the carrier of i, the carrier of i:]) set
the Arrows of i . ((o1 . o2),(o1 . o1)) is set
[(o1 . o2),(o1 . o1)] is V15() set
{(o1 . o2),(o1 . o1)} is set
{(o1 . o2)} is set
{{(o1 . o2),(o1 . o1)},{(o1 . o2)}} is set
the Arrows of i . [(o1 . o2),(o1 . o1)] is set
p1 is M2(<^o1,o2^>)
o1 . p1 is M2(<^(o1 . o1),(o1 . o2)^>)
<^(o1 . o1),(o1 . o2)^> is set
the Arrows of i . ((o1 . o1),(o1 . o2)) is set
[(o1 . o1),(o1 . o2)] is V15() set
{(o1 . o1),(o1 . o2)} is set
{(o1 . o1)} is set
{{(o1 . o1),(o1 . o2)},{(o1 . o1)}} is set
the Arrows of i . [(o1 . o1),(o1 . o2)] is set
p1 * o2 is M2(<^o2,o2^>)
<^o2,o2^> is non empty set
the Arrows of C . (o2,o2) is set
the Arrows of C . [o2,o2] is set
idm o2 is retraction coretraction mono epi M2(<^o2,o2^>)
(o1 . p1) * (o1 . o2) is M2(<^(o1 . o2),(o1 . o2)^>)
<^(o1 . o2),(o1 . o2)^> is non empty set
the Arrows of i . ((o1 . o2),(o1 . o2)) is set
[(o1 . o2),(o1 . o2)] is V15() set
{(o1 . o2),(o1 . o2)} is set
{{(o1 . o2),(o1 . o2)},{(o1 . o2)}} is set
the Arrows of i . [(o1 . o2),(o1 . o2)] is set
o1 . (idm o2) is M2(<^(o1 . o2),(o1 . o2)^>)
idm (o1 . o2) is retraction coretraction mono epi M2(<^(o1 . o2),(o1 . o2)^>)

the carrier of C is non empty set

o2 is M2( the carrier of C)
o1 is M2( the carrier of C)
<^o2,o1^> is set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the Arrows of C . (o2,o1) is set
[o2,o1] is V15() set
{o2,o1} is set
{o2} is set
{{o2,o1},{o2}} is set
the Arrows of C . [o2,o1] is set
<^o1,o2^> is set
the Arrows of C . (o1,o2) is set
[o1,o2] is V15() set
{o1,o2} is set
{o1} is set
{{o1,o2},{o1}} is set
the Arrows of C . [o1,o2] is set
o1 . o2 is M2( the carrier of i)
the carrier of i is non empty set
[: the carrier of i, the carrier of i:] is Relation-like non empty set
the ObjectMap of o1 is Relation-like [: the carrier of C, the carrier of C:] -defined [: the carrier of i, the carrier of i:] -valued Function-like quasi_total M2( bool [:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:])
[:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:] is Relation-like non empty set
bool [:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:] is non empty set
the ObjectMap of o1 . (o2,o2) is M2([: the carrier of i, the carrier of i:])
[o2,o2] is V15() set
{o2,o2} is set
{{o2,o2},{o2}} is set
the ObjectMap of o1 . [o2,o2] is set
K40(( the ObjectMap of o1 . (o2,o2))) is set
o1 . o1 is M2( the carrier of i)
the ObjectMap of o1 . (o1,o1) is M2([: the carrier of i, the carrier of i:])
[o1,o1] is V15() set
{o1,o1} is set
{{o1,o1},{o1}} is set
the ObjectMap of o1 . [o1,o1] is set
K40(( the ObjectMap of o1 . (o1,o1))) is set
o2 is M2(<^o2,o1^>)
o1 . o2 is M2(<^(o1 . o2),(o1 . o1)^>)
<^(o1 . o2),(o1 . o1)^> is set
the Arrows of i is Relation-like [: the carrier of i, the carrier of i:] -defined Function-like non empty V14([: the carrier of i, the carrier of i:]) set
the Arrows of i . ((o1 . o2),(o1 . o1)) is set
[(o1 . o2),(o1 . o1)] is V15() set
{(o1 . o2),(o1 . o1)} is set
{(o1 . o2)} is set
{{(o1 . o2),(o1 . o1)},{(o1 . o2)}} is set
the Arrows of i . [(o1 . o2),(o1 . o1)] is set
<^(o1 . o1),(o1 . o2)^> is set
the Arrows of i . ((o1 . o1),(o1 . o2)) is set
[(o1 . o1),(o1 . o2)] is V15() set
{(o1 . o1),(o1 . o2)} is set
{(o1 . o1)} is set
{{(o1 . o1),(o1 . o2)},{(o1 . o1)}} is set
the Arrows of i . [(o1 . o1),(o1 . o2)] is set

the carrier of C is non empty set

o2 is M2( the carrier of C)
o1 is M2( the carrier of C)
o1 . o2 is M2( the carrier of i)
the carrier of i is non empty set
[: the carrier of i, the carrier of i:] is Relation-like non empty set
the ObjectMap of o1 is Relation-like [: the carrier of C, the carrier of C:] -defined [: the carrier of i, the carrier of i:] -valued Function-like quasi_total M2( bool [:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:])
[: the carrier of C, the carrier of C:] is Relation-like non empty set
[:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:] is Relation-like non empty set
bool [:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:] is non empty set
the ObjectMap of o1 . (o2,o2) is M2([: the carrier of i, the carrier of i:])
[o2,o2] is V15() set
{o2,o2} is set
{o2