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

the Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty V36() V37() set is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty V36() V37() 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

C is non empty transitive V129() with_units reflexive 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

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^>)

C is non empty transitive V129() 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( 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^>)

C is non empty transitive V129() with_units reflexive 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

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

C is non empty transitive V129() with_units reflexive AltCatStr

the carrier of C is non empty set

i is M2( the carrier of C)

idm i is retraction coretraction mono epi 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

C is non empty transitive V129() with_units reflexive AltCatStr

the carrier of C is non empty set

i is M2( the carrier of C)

idm i is retraction coretraction iso mono epi 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

<^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^>)

C is non empty transitive V129() with_units reflexive 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

<^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 is retraction coretraction iso mono epi M2(<^i,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^>)

C is non empty transitive V129() with_units reflexive 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(<^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^>)

C is non empty transitive V129() with_units reflexive AltCatStr

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^>)

C is non empty transitive V129() with_units reflexive 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^>)

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^>)

C is non empty transitive V129() with_units reflexive AltCatStr

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 is retraction coretraction iso mono epi M2(<^i,i^>)

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

C is non empty transitive with_units reflexive AltCatStr

i is non empty transitive with_units reflexive AltCatStr

the carrier of C is non empty set

o1 is reflexive feasible Contravariant id-preserving comp-reversing contravariant Functor of C,i

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

o1 . o2 is Relation-like Function-like 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

o2 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)^>)

C is non empty transitive with_units reflexive AltCatStr

i is non empty transitive with_units reflexive AltCatStr

the carrier of C is non empty set

o1 is reflexive feasible Covariant id-preserving comp-preserving covariant Functor of C,i

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)^>)

C is non empty transitive with_units reflexive AltCatStr

i is non empty transitive with_units reflexive AltCatStr

the carrier of C is non empty set

o1 is reflexive feasible Covariant id-preserving comp-preserving covariant Functor of C,i

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)^>)

C is non empty transitive V129() with_units reflexive AltCatStr

i is non empty transitive V129() with_units reflexive AltCatStr

the carrier of C is non empty set

o1 is reflexive feasible Covariant id-preserving comp-preserving covariant Functor of C,i

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

C is non empty transitive V129() with_units reflexive AltCatStr

i is non empty transitive V129() with_units reflexive AltCatStr

the carrier of C is non empty set

o1 is reflexive feasible Covariant id-preserving comp-preserving covariant Functor of C,i

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