:: FUNCTOR1 semantic presentation

K156() is Element of bool K152()
K152() is set
bool K152() is non empty set
K118() is set
bool K118() is non empty set
bool K156() is non empty 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 non empty set
the non empty transitive V129() with_units reflexive AltCatStr is non empty transitive V129() with_units reflexive AltCatStr
A is non empty reflexive AltCatStr
B is SubCatStr of A
A is non empty reflexive AltCatStr
B is non empty reflexive AltCatStr
G is non empty reflexive SubCatStr of A
C is feasible FunctorStr over A,B
C | G is FunctorStr over G,B
incl G is reflexive feasible strict Covariant FunctorStr over G,A
C * (incl G) is feasible strict FunctorStr over G,B
A is set
id A is Relation-like A -defined A -valued Function-like one-to-one V14(A) quasi_total Element of bool [:A,A:]
[:A,A:] is Relation-like set
bool [:A,A:] is non empty set
B is Relation-like A -defined A -valued Function-like V14(A) quasi_total Element of bool [:A,A:]
rng B is set
A is non empty set
bool A is non empty set
B is non empty Element of bool A
bool B is non empty set
C is non empty Element of bool A
incl C is Relation-like C -defined A -valued C -valued Function-like one-to-one non empty V14(C) quasi_total onto Element of bool [:C,A:]
[:C,A:] is Relation-like non empty set
bool [:C,A:] is non empty set
incl B is Relation-like B -defined A -valued B -valued Function-like one-to-one non empty V14(B) quasi_total onto Element of bool [:B,A:]
[:B,A:] is Relation-like non empty set
bool [:B,A:] is non empty set
G is non empty Element of bool B
incl G is Relation-like G -defined B -valued G -valued Function-like one-to-one non empty V14(G) quasi_total onto Element of bool [:G,B:]
[:G,B:] is Relation-like non empty set
bool [:G,B:] is non empty set
(incl B) * (incl G) is Relation-like G -defined A -valued Function-like one-to-one non empty V14(G) quasi_total Element of bool [:G,A:]
[:G,A:] is Relation-like non empty set
bool [:G,A:] is non empty set
B /\ G is Element of bool B
id (B /\ G) is Relation-like B /\ G -defined B /\ G -valued Function-like one-to-one V14(B /\ G) quasi_total onto bijective Element of bool [:(B /\ G),(B /\ G):]
[:(B /\ G),(B /\ G):] is Relation-like set
bool [:(B /\ G),(B /\ G):] is non empty set
A is set
B is set
[:A,B:] is Relation-like set
bool [:A,B:] is non empty set
[:B,A:] is Relation-like set
bool [:B,A:] is non empty set
C is Relation-like A -defined B -valued Function-like quasi_total Element of bool [:A,B:]
C " is Relation-like Function-like set
rng C is set
A is set
B is set
[:A,B:] is Relation-like set
bool [:A,B:] is non empty set
C is non empty set
[:B,C:] is Relation-like set
bool [:B,C:] is non empty set
[:A,C:] is Relation-like set
bool [:A,C:] is non empty set
G is Relation-like A -defined B -valued Function-like quasi_total Element of bool [:A,B:]
F is Relation-like B -defined C -valued Function-like V14(B) quasi_total Element of bool [:B,C:]
F * G is Relation-like A -defined C -valued Function-like Element of bool [:A,C:]
rng F is set
GI is Relation-like A -defined C -valued Function-like V14(A) quasi_total Element of bool [:A,C:]
rng G is set
rng (F * G) is set
A is non empty reflexive AltCatStr
B is non empty reflexive SubCatStr of A
incl B is reflexive feasible strict Covariant FunctorStr over B,A
C is non empty SubCatStr of A
incl C is reflexive feasible strict Covariant FunctorStr over C,A
G is non empty SubCatStr of B
incl G is reflexive feasible strict Covariant FunctorStr over G,B
(incl B) * (incl G) is reflexive feasible strict Covariant FunctorStr over G,A
the carrier of B is non empty set
[: the carrier of B, the carrier of B:] is Relation-like non empty set
the carrier of G is non empty set
[: the carrier of G, the carrier of G:] is Relation-like non empty set
the MorphMap of (incl 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:]) V36() V37() MSUnTrans of the ObjectMap of (incl C), the Arrows of C, the Arrows of A
the carrier of C is non empty set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the carrier of A is non empty set
[: the carrier of A, the carrier of A:] is Relation-like non empty set
the ObjectMap of (incl C) is Relation-like [: the carrier of C, the carrier of C:] -defined [: the carrier of A, the carrier of A:] -valued Function-like non empty V14([: the carrier of C, the carrier of C:]) quasi_total Element of bool [:[: the carrier of C, the carrier of C:],[: the carrier of A, the carrier of A:]:]
[:[: the carrier of C, the carrier of C:],[: the carrier of A, the carrier of A:]:] is Relation-like non empty set
bool [:[: the carrier of C, the carrier of C:],[: the carrier of A, the carrier of A:]:] 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 A is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) set
the MorphMap of (incl G) is Relation-like [: the carrier of G, the carrier of G:] -defined Function-like non empty V14([: the carrier of G, the carrier of G:]) V36() V37() MSUnTrans of the ObjectMap of (incl G), the Arrows of G, the Arrows of B
the ObjectMap of (incl G) is Relation-like [: the carrier of G, the carrier of G:] -defined [: the carrier of B, the carrier of B:] -valued Function-like non empty V14([: the carrier of G, the carrier of G:]) quasi_total Element of bool [:[: the carrier of G, the carrier of G:],[: the carrier of B, the carrier of B:]:]
[:[: the carrier of G, the carrier of G:],[: the carrier of B, the carrier of B:]:] is Relation-like non empty set
bool [:[: the carrier of G, the carrier of G:],[: the carrier of B, the carrier of B:]:] is non empty set
the Arrows of G is Relation-like [: the carrier of G, the carrier of G:] -defined Function-like non empty V14([: the carrier of G, the carrier of G:]) set
the Arrows of B is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) set
the MorphMap of (incl B) is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) V36() V37() MSUnTrans of the ObjectMap of (incl B), the Arrows of B, the Arrows of A
the ObjectMap of (incl B) is Relation-like [: the carrier of B, the carrier of B:] -defined [: the carrier of A, the carrier of A:] -valued Function-like non empty V14([: the carrier of B, the carrier of B:]) quasi_total Element of bool [:[: the carrier of B, the carrier of B:],[: the carrier of A, the carrier of A:]:]
[:[: the carrier of B, the carrier of B:],[: the carrier of A, the carrier of A:]:] is Relation-like non empty set
bool [:[: the carrier of B, the carrier of B:],[: the carrier of A, the carrier of A:]:] is non empty set
the ObjectMap of (incl G) * the MorphMap of (incl B) is Relation-like [: the carrier of G, the carrier of G:] -defined Function-like non empty V14([: the carrier of G, the carrier of G:]) V36() V37() set
( the ObjectMap of (incl G) * the MorphMap of (incl B)) ** the MorphMap of (incl G) is Relation-like [: the carrier of G, the carrier of G:] -defined Function-like non empty V14([: the carrier of G, the carrier of G:]) V36() V37() set
dom the MorphMap of (incl G) is non empty set
dom ( the ObjectMap of (incl G) * the MorphMap of (incl B)) is non empty set
CA is set
the MorphMap of (incl C) . CA is Relation-like Function-like set
(( the ObjectMap of (incl G) * the MorphMap of (incl B)) ** the MorphMap of (incl G)) . CA is Relation-like Function-like set
id 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:]) V36() V37() ManySortedFunction of the Arrows of C, the Arrows of C
(id the Arrows of C) . CA is Relation-like Function-like set
dom (( the ObjectMap of (incl G) * the MorphMap of (incl B)) ** the MorphMap of (incl G)) is non empty set
(dom the MorphMap of (incl G)) /\ (dom ( the ObjectMap of (incl G) * the MorphMap of (incl B))) is set
id [: the carrier of G, the carrier of G:] is Relation-like [: the carrier of G, the carrier of G:] -defined [: the carrier of G, the carrier of G:] -valued Function-like one-to-one non empty V14([: the carrier of G, the carrier of G:]) quasi_total onto bijective Element of bool [:[: the carrier of G, the carrier of G:],[: the carrier of G, the carrier of G:]:]
[:[: the carrier of G, the carrier of G:],[: the carrier of G, the carrier of G:]:] is Relation-like non empty set
bool [:[: the carrier of G, the carrier of G:],[: the carrier of G, the carrier of G:]:] is non empty set
(id [: the carrier of G, the carrier of G:]) * the MorphMap of (incl B) is Relation-like [: the carrier of G, the carrier of G:] -defined Function-like V36() V37() set
dom ((id [: the carrier of G, the carrier of G:]) * the MorphMap of (incl B)) is set
dom the MorphMap of (incl B) is non empty set
(dom the MorphMap of (incl B)) /\ [: the carrier of G, the carrier of G:] is Relation-like set
[: the carrier of B, the carrier of B:] /\ [: the carrier of G, the carrier of G:] is Relation-like set
dom (id [: the carrier of G, the carrier of G:]) is Relation-like non empty set
the Arrows of G . CA is set
the Arrows of B . CA is set
( the ObjectMap of (incl G) * the MorphMap of (incl B)) . CA is Relation-like Function-like set
((id [: the carrier of G, the carrier of G:]) * the MorphMap of (incl B)) . CA is Relation-like Function-like set
(id [: the carrier of G, the carrier of G:]) . CA is set
the MorphMap of (incl B) . ((id [: the carrier of G, the carrier of G:]) . CA) is Relation-like Function-like set
the MorphMap of (incl B) . CA is Relation-like Function-like set
id the Arrows of B is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) V36() V37() ManySortedFunction of the Arrows of B, the Arrows of B
(id the Arrows of B) . CA is Relation-like Function-like set
the MorphMap of (incl G) . CA is Relation-like Function-like set
id the Arrows of G is Relation-like [: the carrier of G, the carrier of G:] -defined Function-like non empty V14([: the carrier of G, the carrier of G:]) V36() V37() ManySortedFunction of the Arrows of G, the Arrows of G
(id the Arrows of G) . CA is Relation-like Function-like set
( the MorphMap of (incl G) . CA) * ( the MorphMap of (incl B) . CA) is Relation-like Function-like set
id ( the Arrows of G . CA) is Relation-like the Arrows of G . CA -defined the Arrows of G . CA -valued Function-like one-to-one V14( the Arrows of G . CA) quasi_total onto bijective Element of bool [:( the Arrows of G . CA),( the Arrows of G . CA):]
[:( the Arrows of G . CA),( the Arrows of G . CA):] is Relation-like set
bool [:( the Arrows of G . CA),( the Arrows of G . CA):] is non empty set
(id ( the Arrows of G . CA)) * ((id the Arrows of B) . CA) is Relation-like the Arrows of G . CA -defined Function-like set
id ( the Arrows of B . CA) is Relation-like the Arrows of B . CA -defined the Arrows of B . CA -valued Function-like one-to-one V14( the Arrows of B . CA) quasi_total onto bijective Element of bool [:( the Arrows of B . CA),( the Arrows of B . CA):]
[:( the Arrows of B . CA),( the Arrows of B . CA):] is Relation-like set
bool [:( the Arrows of B . CA),( the Arrows of B . CA):] is non empty set
(id ( the Arrows of B . CA)) * (id ( the Arrows of G . CA)) is Relation-like the Arrows of G . CA -defined the Arrows of B . CA -valued Function-like one-to-one Element of bool [:( the Arrows of G . CA),( the Arrows of B . CA):]
[:( the Arrows of G . CA),( the Arrows of B . CA):] is Relation-like set
bool [:( the Arrows of G . CA),( the Arrows of B . CA):] is non empty set
( the Arrows of B . CA) /\ ( the Arrows of G . CA) is set
id (( the Arrows of B . CA) /\ ( the Arrows of G . CA)) is Relation-like ( the Arrows of B . CA) /\ ( the Arrows of G . CA) -defined ( the Arrows of B . CA) /\ ( the Arrows of G . CA) -valued Function-like one-to-one V14(( the Arrows of B . CA) /\ ( the Arrows of G . CA)) quasi_total onto bijective Element of bool [:(( the Arrows of B . CA) /\ ( the Arrows of G . CA)),(( the Arrows of B . CA) /\ ( the Arrows of G . CA)):]
[:(( the Arrows of B . CA) /\ ( the Arrows of G . CA)),(( the Arrows of B . CA) /\ ( the Arrows of G . CA)):] is Relation-like set
bool [:(( the Arrows of B . CA) /\ ( the Arrows of G . CA)),(( the Arrows of B . CA) /\ ( the Arrows of G . CA)):] is non empty set
id [: the carrier of G, the carrier of G:] is Relation-like [: the carrier of G, the carrier of G:] -defined [: the carrier of G, the carrier of G:] -valued Function-like one-to-one non empty V14([: the carrier of G, the carrier of G:]) quasi_total onto bijective Element of bool [:[: the carrier of G, the carrier of G:],[: the carrier of G, the carrier of G:]:]
[:[: the carrier of G, the carrier of G:],[: the carrier of G, the carrier of G:]:] is Relation-like non empty set
bool [:[: the carrier of G, the carrier of G:],[: the carrier of G, the carrier of G:]:] is non empty set
[: the carrier of B, the carrier of B:] /\ [: the carrier of G, the carrier of G:] is Relation-like set
id ([: the carrier of B, the carrier of B:] /\ [: the carrier of G, the carrier of G:]) is Relation-like [: the carrier of B, the carrier of B:] /\ [: the carrier of G, the carrier of G:] -defined [: the carrier of B, the carrier of B:] /\ [: the carrier of G, the carrier of G:] -valued Function-like one-to-one V14([: the carrier of B, the carrier of B:] /\ [: the carrier of G, the carrier of G:]) quasi_total onto bijective Element of bool [:([: the carrier of B, the carrier of B:] /\ [: the carrier of G, the carrier of G:]),([: the carrier of B, the carrier of B:] /\ [: the carrier of G, the carrier of G:]):]
[:([: the carrier of B, the carrier of B:] /\ [: the carrier of G, the carrier of G:]),([: the carrier of B, the carrier of B:] /\ [: the carrier of G, the carrier of G:]):] is Relation-like set
bool [:([: the carrier of B, the carrier of B:] /\ [: the carrier of G, the carrier of G:]),([: the carrier of B, the carrier of B:] /\ [: the carrier of G, the carrier of G:]):] is non empty set
id [: the carrier of B, the carrier of B:] is Relation-like [: the carrier of B, the carrier of B:] -defined [: the carrier of B, the carrier of B:] -valued Function-like one-to-one non empty V14([: the carrier of B, the carrier of B:]) quasi_total onto bijective Element of bool [:[: the carrier of B, the carrier of B:],[: the carrier of B, the carrier of B:]:]
[:[: the carrier of B, the carrier of B:],[: the carrier of B, the carrier of B:]:] is Relation-like non empty set
bool [:[: the carrier of B, the carrier of B:],[: the carrier of B, the carrier of B:]:] is non empty set
(id [: the carrier of B, the carrier of B:]) * (id [: the carrier of G, the carrier of G:]) is Relation-like [: the carrier of G, the carrier of G:] -defined [: the carrier of B, the carrier of B:] -valued Function-like one-to-one Element of bool [:[: the carrier of G, the carrier of G:],[: the carrier of B, the carrier of B:]:]
(id [: the carrier of B, the carrier of B:]) * the ObjectMap of (incl G) is Relation-like [: the carrier of G, the carrier of G:] -defined [: the carrier of B, the carrier of B:] -valued Function-like non empty V14([: the carrier of G, the carrier of G:]) quasi_total Element of bool [:[: the carrier of G, the carrier of G:],[: the carrier of B, the carrier of B:]:]
the ObjectMap of (incl B) * the ObjectMap of (incl G) is Relation-like [: the carrier of G, the carrier of G:] -defined [: the carrier of A, the carrier of A:] -valued Function-like non empty V14([: the carrier of G, the carrier of G:]) quasi_total Element of bool [:[: the carrier of G, the carrier of G:],[: the carrier of A, the carrier of A:]:]
[:[: the carrier of G, the carrier of G:],[: the carrier of A, the carrier of A:]:] is Relation-like non empty set
bool [:[: the carrier of G, the carrier of G:],[: the carrier of A, the carrier of A:]:] is non empty set
A is non empty AltCatStr
B is non empty AltCatStr
the carrier of A is non empty set
[: the carrier of A, the carrier of A:] is Relation-like non empty set
the carrier of B is non empty set
[: the carrier of B, the carrier of B:] is Relation-like non empty set
C is FunctorStr over A,B
the ObjectMap of C is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of B, the carrier of B:] -valued Function-like non empty V14([: the carrier of A, the carrier of A:]) quasi_total Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:]
[:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:] is Relation-like non empty set
bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:] is non empty set
the MorphMap of C is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() MSUnTrans of the ObjectMap of C, the Arrows of A, the Arrows of B
the Arrows of A is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) set
the Arrows of B is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) set
A is non empty AltGraph
B is non empty reflexive AltGraph
C is non empty reflexive AltGraph
G is feasible FunctorStr over A,B
F is FunctorStr over B,C
F * G is strict FunctorStr over A,C
the ObjectMap of G is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of B, the carrier of B:] -valued Function-like non empty V14([: the carrier of A, the carrier of A:]) quasi_total Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:]
the carrier of A is non empty set
[: the carrier of A, the carrier of A:] is Relation-like non empty set
the carrier of B is non empty set
[: the carrier of B, the carrier of B:] is Relation-like non empty set
[:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:] is Relation-like non empty set
bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:] is non empty set
the ObjectMap of F is Relation-like [: the carrier of B, the carrier of B:] -defined [: the carrier of C, the carrier of C:] -valued Function-like non empty V14([: the carrier of B, the carrier of B:]) quasi_total Element of bool [:[: the carrier of B, the carrier of B:],[: the carrier of C, the carrier of C:]:]
the carrier of C is non empty set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
[:[: the carrier of B, the carrier of B:],[: the carrier of C, the carrier of C:]:] is Relation-like non empty set
bool [:[: the carrier of B, the carrier of B:],[: the carrier of C, the carrier of C:]:] is non empty set
the ObjectMap of (F * G) is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of C, the carrier of C:] -valued Function-like non empty V14([: the carrier of A, the carrier of A:]) quasi_total Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of C, the carrier of C:]:]
[:[: the carrier of A, the carrier of A:],[: the carrier of C, the carrier of C:]:] is Relation-like non empty set
bool [:[: the carrier of A, the carrier of A:],[: the carrier of C, the carrier of C:]:] is non empty set
the ObjectMap of F * the ObjectMap of G is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of C, the carrier of C:] -valued Function-like non empty V14([: the carrier of A, the carrier of A:]) quasi_total Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of C, the carrier of C:]:]
A is non empty AltGraph
B is non empty reflexive AltGraph
C is non empty reflexive AltGraph
G is feasible FunctorStr over A,B
F is FunctorStr over B,C
F * G is strict FunctorStr over A,C
the MorphMap of F is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) V36() V37() MSUnTrans of the ObjectMap of F, the Arrows of B, the Arrows of C
the carrier of B is non empty set
[: the carrier of B, the carrier of B:] is Relation-like non empty set
the carrier of C is non empty set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the ObjectMap of F is Relation-like [: the carrier of B, the carrier of B:] -defined [: the carrier of C, the carrier of C:] -valued Function-like non empty V14([: the carrier of B, the carrier of B:]) quasi_total Element of bool [:[: the carrier of B, the carrier of B:],[: the carrier of C, the carrier of C:]:]
[:[: the carrier of B, the carrier of B:],[: the carrier of C, the carrier of C:]:] is Relation-like non empty set
bool [:[: the carrier of B, the carrier of B:],[: the carrier of C, the carrier of C:]:] is non empty set
the Arrows of B is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) 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 MorphMap of G is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() MSUnTrans of the ObjectMap of G, the Arrows of A, the Arrows of B
the carrier of A is non empty set
[: the carrier of A, the carrier of A:] is Relation-like non empty set
the ObjectMap of G is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of B, the carrier of B:] -valued Function-like non empty V14([: the carrier of A, the carrier of A:]) quasi_total Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:]
[:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:] is Relation-like non empty set
bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:] is non empty set
the Arrows of A is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) set
the MorphMap of (F * G) is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() MSUnTrans of the ObjectMap of (F * G), the Arrows of A, the Arrows of C
the ObjectMap of (F * G) is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of C, the carrier of C:] -valued Function-like non empty V14([: the carrier of A, the carrier of A:]) quasi_total Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of C, the carrier of C:]:]
[:[: the carrier of A, the carrier of A:],[: the carrier of C, the carrier of C:]:] is Relation-like non empty set
bool [:[: the carrier of A, the carrier of A:],[: the carrier of C, the carrier of C:]:] is non empty set
CB is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() set
CA is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of B, the carrier of B:] -valued Function-like non empty V14([: the carrier of A, the carrier of A:]) quasi_total Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:]
CA * the MorphMap of F is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() set
(CA * the MorphMap of F) ** the MorphMap of G is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() set
OGI is set
CB . OGI is Relation-like Function-like set
dom ((CA * the MorphMap of F) ** the MorphMap of G) is non empty set
the MorphMap of G . OGI is Relation-like Function-like set
(CA * the MorphMap of F) . OGI is Relation-like Function-like set
( the MorphMap of G . OGI) * ((CA * the MorphMap of F) . OGI) is Relation-like Function-like set
CA . OGI is set
the MorphMap of F . (CA . OGI) is Relation-like Function-like set
( the MorphMap of G . OGI) * ( the MorphMap of F . (CA . OGI)) is Relation-like Function-like set
A is non empty AltGraph
B is non empty reflexive AltGraph
C is non empty reflexive AltGraph
G is feasible FunctorStr over A,B
F is FunctorStr over B,C
F * G is strict FunctorStr over A,C
the carrier of C is non empty set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the carrier of B is non empty set
[: the carrier of B, the carrier of B:] is Relation-like non empty set
[:[: the carrier of B, the carrier of B:],[: the carrier of C, the carrier of C:]:] is Relation-like non empty set
bool [:[: the carrier of B, the carrier of B:],[: the carrier of C, the carrier of C:]:] is non empty set
the ObjectMap of F is Relation-like [: the carrier of B, the carrier of B:] -defined [: the carrier of C, the carrier of C:] -valued Function-like non empty V14([: the carrier of B, the carrier of B:]) quasi_total Element of bool [:[: the carrier of B, the carrier of B:],[: the carrier of C, the carrier of C:]:]
MF is Relation-like [: the carrier of B, the carrier of B:] -defined [: the carrier of C, the carrier of C:] -valued Function-like non empty V14([: the carrier of B, the carrier of B:]) quasi_total Element of bool [:[: the carrier of B, the carrier of B:],[: the carrier of C, the carrier of C:]:]
rng MF is Relation-like non empty set
the carrier of A is non empty set
[: the carrier of A, the carrier of A:] is Relation-like non empty set
[:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:] is Relation-like non empty set
bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:] is non empty set
the ObjectMap of G is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of B, the carrier of B:] -valued Function-like non empty V14([: the carrier of A, the carrier of A:]) quasi_total Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:]
CB is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of B, the carrier of B:] -valued Function-like non empty V14([: the carrier of A, the carrier of A:]) quasi_total Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:]
rng CB is Relation-like non empty set
MF * CB is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of C, the carrier of C:] -valued Function-like non empty V14([: the carrier of A, the carrier of A:]) quasi_total Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of C, the carrier of C:]:]
[:[: the carrier of A, the carrier of A:],[: the carrier of C, the carrier of C:]:] is Relation-like non empty set
bool [:[: the carrier of A, the carrier of A:],[: the carrier of C, the carrier of C:]:] is non empty set
rng (MF * CB) is Relation-like non empty set
the ObjectMap of (F * G) is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of C, the carrier of C:] -valued Function-like non empty V14([: the carrier of A, the carrier of A:]) quasi_total Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of C, the carrier of C:]:]
A is non empty AltGraph
B is non empty reflexive AltGraph
C is non empty reflexive AltGraph
G is feasible FunctorStr over A,B
F is FunctorStr over B,C
F * G is strict FunctorStr over A,C
the carrier of C is non empty set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the carrier of B is non empty set
[: the carrier of B, the carrier of B:] is Relation-like non empty set
the carrier of A is non empty set
[: the carrier of A, the carrier of A:] is Relation-like non empty set
[:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:] is Relation-like non empty set
bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:] is non empty set
the ObjectMap of G is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of B, the carrier of B:] -valued Function-like non empty V14([: the carrier of A, the carrier of A:]) quasi_total Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:]
[:[: the carrier of B, the carrier of B:],[: the carrier of C, the carrier of C:]:] is Relation-like non empty set
bool [:[: the carrier of B, the carrier of B:],[: the carrier of C, the carrier of C:]:] is non empty set
the ObjectMap of F is Relation-like [: the carrier of B, the carrier of B:] -defined [: the carrier of C, the carrier of C:] -valued Function-like non empty V14([: the carrier of B, the carrier of B:]) quasi_total Element of bool [:[: the carrier of B, the carrier of B:],[: the carrier of C, the carrier of C:]:]
the Arrows of A is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) set
the Arrows of B is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) set
the ObjectMap of G * the Arrows of B is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) set
the MorphMap of G is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() MSUnTrans of the ObjectMap of G, the Arrows of A, the Arrows of B
CA is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() ManySortedFunction of the Arrows of A, the ObjectMap of G * the Arrows of B
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 ObjectMap of F * the Arrows of C is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) set
the MorphMap of F is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) V36() V37() MSUnTrans of the ObjectMap of F, the Arrows of B, the Arrows of C
OGI is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) V36() V37() ManySortedFunction of the Arrows of B, the ObjectMap of F * the Arrows of C
the ObjectMap of (F * G) is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of C, the carrier of C:] -valued Function-like non empty V14([: the carrier of A, the carrier of A:]) quasi_total Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of C, the carrier of C:]:]
[:[: the carrier of A, the carrier of A:],[: the carrier of C, the carrier of C:]:] is Relation-like non empty set
bool [:[: the carrier of A, the carrier of A:],[: the carrier of C, the carrier of C:]:] is non empty set
the ObjectMap of (F * G) * the Arrows of C is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) set
the MorphMap of (F * G) is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() MSUnTrans of the ObjectMap of (F * G), the Arrows of A, the Arrows of C
CC is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() ManySortedFunction of the Arrows of A, the ObjectMap of (F * G) * the Arrows of C
OG is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of B, the carrier of B:] -valued Function-like non empty V14([: the carrier of A, the carrier of A:]) quasi_total Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:]
OG * OGI is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() set
(OG * OGI) ** CA is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() set
OF is set
CC . OF is Relation-like Function-like set
rng (CC . OF) is set
( the ObjectMap of (F * G) * the Arrows of C) . OF is set
OG . OF is set
the Arrows of B . (OG . OF) is set
( the ObjectMap of F * the Arrows of C) . (OG . OF) is set
[:( the Arrows of B . (OG . OF)),(( the ObjectMap of F * the Arrows of C) . (OG . OF)):] is Relation-like set
bool [:( the Arrows of B . (OG . OF)),(( the ObjectMap of F * the Arrows of C) . (OG . OF)):] is non empty set
OGI . (OG . OF) is Relation-like Function-like set
CA . OF is Relation-like Function-like set
(CA . OF) * (OGI . (OG . OF)) is Relation-like Function-like set
rng ((CA . OF) * (OGI . (OG . OF))) is set
rng (OGI . (OG . OF)) is set
OFI is Relation-like the Arrows of B . (OG . OF) -defined ( the ObjectMap of F * the Arrows of C) . (OG . OF) -valued Function-like quasi_total Element of bool [:( the Arrows of B . (OG . OF)),(( the ObjectMap of F * the Arrows of C) . (OG . OF)):]
rng OFI is set
(CA . OF) * {} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty V36() V37() set
rng ((CA . OF) * {}) is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty trivial V36() V37() set
OFI is Relation-like the Arrows of B . (OG . OF) -defined ( the ObjectMap of F * the Arrows of C) . (OG . OF) -valued Function-like quasi_total Element of bool [:( the Arrows of B . (OG . OF)),(( the ObjectMap of F * the Arrows of C) . (OG . OF)):]
rng OFI is set
dom OFI is set
OG * the Arrows of B is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) set
(OG * the Arrows of B) . OF is set
rng (CA . OF) is set
OFI is Relation-like the Arrows of B . (OG . OF) -defined ( the ObjectMap of F * the Arrows of C) . (OG . OF) -valued Function-like quasi_total Element of bool [:( the Arrows of B . (OG . OF)),(( the ObjectMap of F * the Arrows of C) . (OG . OF)):]
rng OFI is set
dom ((OG * OGI) ** CA) is non empty set
(OG * OGI) . OF is Relation-like Function-like set
(CA . OF) * ((OG * OGI) . OF) is Relation-like Function-like set
rng ((CA . OF) * ((OG * OGI) . OF)) is set
CB is Relation-like [: the carrier of B, the carrier of B:] -defined [: the carrier of C, the carrier of C:] -valued Function-like non empty V14([: the carrier of B, the carrier of B:]) quasi_total Element of bool [:[: the carrier of B, the carrier of B:],[: the carrier of C, the carrier of C:]:]
CB . (OG . OF) is set
the Arrows of C . (CB . (OG . OF)) is set
CB * OG is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of C, the carrier of C:] -valued Function-like non empty V14([: the carrier of A, the carrier of A:]) quasi_total Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of C, the carrier of C:]:]
(CB * OG) . OF is set
the Arrows of C . ((CB * OG) . OF) is set
the ObjectMap of (F * G) . OF is set
the Arrows of C . ( the ObjectMap of (F * G) . OF) is set
CC is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() ManySortedFunction of the Arrows of A, the ObjectMap of (F * G) * the Arrows of C
A is non empty AltGraph
B is non empty reflexive AltGraph
C is non empty reflexive AltGraph
G is feasible FunctorStr over A,B
F is FunctorStr over B,C
F * G is strict FunctorStr over A,C
A is non empty AltGraph
B is non empty reflexive AltGraph
C is non empty reflexive AltGraph
G is feasible FunctorStr over A,B
F is FunctorStr over B,C
F * G is strict FunctorStr over A,C
A is non empty AltGraph
B is non empty reflexive AltGraph
C is non empty reflexive AltGraph
G is feasible FunctorStr over A,B
F is FunctorStr over B,C
F * G is strict FunctorStr over A,C
A is non empty reflexive AltCatStr
B is non empty reflexive AltCatStr
C is non empty reflexive SubCatStr of A
G is non empty SubCatStr of A
F is non empty SubCatStr of C
GI is FunctorStr over A,B
GI | G is FunctorStr over G,B
incl G is reflexive feasible strict Covariant FunctorStr over G,A
GI * (incl G) is strict FunctorStr over G,B
GI | C is FunctorStr over C,B
incl C is reflexive feasible strict Covariant FunctorStr over C,A
GI * (incl C) is strict FunctorStr over C,B
(GI | C) | F is FunctorStr over F,B
incl F is reflexive feasible strict Covariant FunctorStr over F,C
(GI | C) * (incl F) is strict FunctorStr over F,B
(incl C) * (incl F) is reflexive feasible strict Covariant FunctorStr over F,A
GI * ((incl C) * (incl F)) is strict FunctorStr over F,B
A is non empty AltCatStr
B is non empty SubCatStr of A
incl B is reflexive feasible strict Covariant FunctorStr over B,A
the carrier of B is non empty set
[: the carrier of B, the carrier of B:] is Relation-like non empty set
the carrier of A is non empty set
[: the carrier of A, the carrier of A:] is Relation-like non empty set
the ObjectMap of (incl B) is Relation-like [: the carrier of B, the carrier of B:] -defined [: the carrier of A, the carrier of A:] -valued Function-like non empty V14([: the carrier of B, the carrier of B:]) quasi_total Element of bool [:[: the carrier of B, the carrier of B:],[: the carrier of A, the carrier of A:]:]
[:[: the carrier of B, the carrier of B:],[: the carrier of A, the carrier of A:]:] is Relation-like non empty set
bool [:[: the carrier of B, the carrier of B:],[: the carrier of A, the carrier of A:]:] is non empty set
the Arrows of A is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) set
the MorphMap of (incl B) is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) V36() V37() MSUnTrans of the ObjectMap of (incl B), the Arrows of B, the Arrows of A
the Arrows of B is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) set
the ObjectMap of (incl B) * the Arrows of A is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) set
G is non empty set
[:[: the carrier of B, the carrier of B:],G:] is Relation-like non empty set
bool [:[: the carrier of B, the carrier of B:],G:] is non empty set
GI is Relation-like [: the carrier of B, the carrier of B:] -defined G -valued Function-like non empty V14([: the carrier of B, the carrier of B:]) quasi_total Element of bool [:[: the carrier of B, the carrier of B:],G:]
F is Relation-like G -defined Function-like non empty V14(G) set
GI * F is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) set
dom the Arrows of A is non empty set
(dom the Arrows of A) /\ [: the carrier of B, the carrier of B:] is Relation-like set
C is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) V36() V37() ManySortedFunction of the Arrows of B, the ObjectMap of (incl B) * the Arrows of A
F is set
C . F is Relation-like Function-like set
rng (C . F) is set
( the ObjectMap of (incl B) * the Arrows of A) . F is set
the Arrows of A || the carrier of B is set
the Arrows of A | [: the carrier of B, the carrier of B:] is Relation-like [: the carrier of B, the carrier of B:] -defined [: the carrier of A, the carrier of A:] -defined Function-like set
the Arrows of B . F is set
the Arrows of A . F is set
id the Arrows of B is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) V36() V37() ManySortedFunction of the Arrows of B, the Arrows of B
(id the Arrows of B) . F is Relation-like Function-like set
rng ((id the Arrows of B) . F) is set
id ( the Arrows of B . F) is Relation-like the Arrows of B . F -defined the Arrows of B . F -valued Function-like one-to-one V14( the Arrows of B . F) quasi_total onto bijective Element of bool [:( the Arrows of B . F),( the Arrows of B . F):]
[:( the Arrows of B . F),( the Arrows of B . F):] is Relation-like set
bool [:( the Arrows of B . F),( the Arrows of B . F):] is non empty set
rng (id ( the Arrows of B . F)) is set
id [: the carrier of B, the carrier of B:] is Relation-like [: the carrier of B, the carrier of B:] -defined [: the carrier of B, the carrier of B:] -valued Function-like one-to-one non empty V14([: the carrier of B, the carrier of B:]) quasi_total onto bijective Element of bool [:[: the carrier of B, the carrier of B:],[: the carrier of B, the carrier of B:]:]
[:[: the carrier of B, the carrier of B:],[: the carrier of B, the carrier of B:]:] is Relation-like non empty set
bool [:[: the carrier of B, the carrier of B:],[: the carrier of B, the carrier of B:]:] is non empty set
(id [: the carrier of B, the carrier of B:]) * the Arrows of A is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like set
((id [: the carrier of B, the carrier of B:]) * the Arrows of A) . F is set
the Arrows of A | [: the carrier of B, the carrier of B:] is Relation-like [: the carrier of B, the carrier of B:] -defined [: the carrier of A, the carrier of A:] -defined Function-like set
dom ( the Arrows of A | [: the carrier of B, the carrier of B:]) is set
the Arrows of A || the carrier of B is set
G is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) set
F is set
G . F is set
the Arrows of B . F is set
GI is set
FI is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) V36() V37() ManySortedFunction of the Arrows of B, the ObjectMap of (incl B) * the Arrows of A
id the Arrows of B is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) V36() V37() ManySortedFunction of the Arrows of B, the Arrows of B
(id the Arrows of B) . F is Relation-like Function-like set
rng ((id the Arrows of B) . F) is set
( the ObjectMap of (incl B) * the Arrows of A) . F is set
id [: the carrier of B, the carrier of B:] is Relation-like [: the carrier of B, the carrier of B:] -defined [: the carrier of B, the carrier of B:] -valued Function-like one-to-one non empty V14([: the carrier of B, the carrier of B:]) quasi_total onto bijective Element of bool [:[: the carrier of B, the carrier of B:],[: the carrier of B, the carrier of B:]:]
[:[: the carrier of B, the carrier of B:],[: the carrier of B, the carrier of B:]:] is Relation-like non empty set
bool [:[: the carrier of B, the carrier of B:],[: the carrier of B, the carrier of B:]:] is non empty set
(id [: the carrier of B, the carrier of B:]) * the Arrows of A is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like set
((id [: the carrier of B, the carrier of B:]) * the Arrows of A) . F is set
the Arrows of A . F is set
MF is set
OG is set
[MF,OG] is set
{MF,OG} is non empty set
{MF} is non empty set
{{MF,OG},{MF}} is non empty set
G . (MF,OG) is set
G . [MF,OG] is set
the Arrows of A . (MF,OG) is set
the Arrows of A . [MF,OG] is set
id ( the Arrows of B . F) is Relation-like the Arrows of B . F -defined the Arrows of B . F -valued Function-like one-to-one V14( the Arrows of B . F) quasi_total onto bijective Element of bool [:( the Arrows of B . F),( the Arrows of B . F):]
[:( the Arrows of B . F),( the Arrows of B . F):] is Relation-like set
bool [:( the Arrows of B . F),( the Arrows of B . F):] is non empty set
rng (id ( the Arrows of B . F)) is set
F is set
the Arrows of B . F is set
G . F is set
GI is set
FI is set
[GI,FI] is set
{GI,FI} is non empty set
{GI} is non empty set
{{GI,FI},{GI}} is non empty set
G . (GI,FI) is set
G . [GI,FI] is set
the Arrows of A . (GI,FI) is set
the Arrows of A . [GI,FI] is set
MF is set
the Arrows of B . (GI,FI) is set
the Arrows of B . [GI,FI] is set
A is non empty AltCatStr
B is non empty AltCatStr
the carrier of A is non empty set
C is reflexive Covariant FunctorStr over A,B
[: the carrier of A, the carrier of A:] is Relation-like non empty set
the Arrows of A is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) set
the ObjectMap of C is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of B, the carrier of B:] -valued Function-like non empty V14([: the carrier of A, the carrier of A:]) quasi_total Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:]
the carrier of B is non empty set
[: the carrier of B, the carrier of B:] is Relation-like non empty set
[:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:] is Relation-like non empty set
bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:] is non empty set
the Arrows of B is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) set
the ObjectMap of C * the Arrows of B is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) set
the MorphMap of C is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() MSUnTrans of the ObjectMap of C, the Arrows of A, the Arrows of B
F is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() ManySortedFunction of the Arrows of A, the ObjectMap of C * the Arrows of B
GI is Element of the carrier of A
FI is Element of the carrier of A
[GI,FI] is set
{GI,FI} is non empty set
{GI} is non empty set
{{GI,FI},{GI}} is non empty set
dom the ObjectMap of C is Relation-like non empty set
F . [GI,FI] is Relation-like Function-like set
rng (F . [GI,FI]) is set
( the ObjectMap of C * the Arrows of B) . [GI,FI] is set
Morph-Map (C,GI,FI) is Relation-like <^GI,FI^> -defined <^(C . GI),(C . FI)^> -valued Function-like quasi_total Element of bool [:<^GI,FI^>,<^(C . GI),(C . FI)^>:]
<^GI,FI^> is set
C . GI is Element of the carrier of B
the ObjectMap of C . (GI,GI) is Element of [: the carrier of B, the carrier of B:]
[GI,GI] is set
{GI,GI} is non empty set
{{GI,GI},{GI}} is non empty set
the ObjectMap of C . [GI,GI] is set
K40(( the ObjectMap of C . (GI,GI))) is set
C . FI is Element of the carrier of B
the ObjectMap of C . (FI,FI) is Element of [: the carrier of B, the carrier of B:]
[FI,FI] is set
{FI,FI} is non empty set
{FI} is non empty set
{{FI,FI},{FI}} is non empty set
the ObjectMap of C . [FI,FI] is set
K40(( the ObjectMap of C . (FI,FI))) is set
<^(C . GI),(C . FI)^> is set
[:<^GI,FI^>,<^(C . GI),(C . FI)^>:] is Relation-like set
bool [:<^GI,FI^>,<^(C . GI),(C . FI)^>:] is non empty set
the MorphMap of C . (GI,FI) is set
the MorphMap of C . [GI,FI] is Relation-like Function-like set
rng (Morph-Map (C,GI,FI)) is set
the ObjectMap of C . (GI,FI) is Element of [: the carrier of B, the carrier of B:]
the ObjectMap of C . [GI,FI] is set
the Arrows of B . ( the ObjectMap of C . (GI,FI)) is set
the Arrows of B . ((C . GI),(C . FI)) is set
[(C . GI),(C . FI)] is set
{(C . GI),(C . FI)} is non empty set
{(C . GI)} is non empty set
{{(C . GI),(C . FI)},{(C . GI)}} is non empty set
the Arrows of B . [(C . GI),(C . FI)] is set
GI is non empty set
[:[: the carrier of A, the carrier of A:],GI:] is Relation-like non empty set
bool [:[: the carrier of A, the carrier of A:],GI:] is non empty set
MF is Relation-like [: the carrier of A, the carrier of A:] -defined GI -valued Function-like non empty V14([: the carrier of A, the carrier of A:]) quasi_total Element of bool [:[: the carrier of A, the carrier of A:],GI:]
FI is Relation-like GI -defined Function-like non empty V14(GI) set
MF * FI is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) set
F is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() ManySortedFunction of the Arrows of A, the ObjectMap of C * the Arrows of B
GI is set
F . GI is Relation-like Function-like set
rng (F . GI) is set
( the ObjectMap of C * the Arrows of B) . GI is set
FI is set
MF is set
[FI,MF] is set
{FI,MF} is non empty set
{FI} is non empty set
{{FI,MF},{FI}} is non empty set
OG is Element of the carrier of A
CB is Element of the carrier of A
[OG,CB] is set
{OG,CB} is non empty set
{OG} is non empty set
{{OG,CB},{OG}} is non empty set
C . OG is Element of the carrier of B
the ObjectMap of C . (OG,OG) is Element of [: the carrier of B, the carrier of B:]
[OG,OG] is set
{OG,OG} is non empty set
{{OG,OG},{OG}} is non empty set
the ObjectMap of C . [OG,OG] is set
K40(( the ObjectMap of C . (OG,OG))) is set
C . CB is Element of the carrier of B
the ObjectMap of C . (CB,CB) is Element of [: the carrier of B, the carrier of B:]
[CB,CB] is set
{CB,CB} is non empty set
{CB} is non empty set
{{CB,CB},{CB}} is non empty set
the ObjectMap of C . [CB,CB] is set
K40(( the ObjectMap of C . (CB,CB))) is set
<^(C . OG),(C . CB)^> is set
Morph-Map (C,OG,CB) is Relation-like <^OG,CB^> -defined <^(C . OG),(C . CB)^> -valued Function-like quasi_total Element of bool [:<^OG,CB^>,<^(C . OG),(C . CB)^>:]
<^OG,CB^> is set
[:<^OG,CB^>,<^(C . OG),(C . CB)^>:] is Relation-like set
bool [:<^OG,CB^>,<^(C . OG),(C . CB)^>:] is non empty set
the MorphMap of C . (OG,CB) is set
the MorphMap of C . [OG,CB] is Relation-like Function-like set
rng (Morph-Map (C,OG,CB)) is set
the Arrows of B . ((C . OG),(C . CB)) is set
[(C . OG),(C . CB)] is set
{(C . OG),(C . CB)} is non empty set
{(C . OG)} is non empty set
{{(C . OG),(C . CB)},{(C . OG)}} is non empty set
the Arrows of B . [(C . OG),(C . CB)] is set
the ObjectMap of C . (OG,CB) is Element of [: the carrier of B, the carrier of B:]
the ObjectMap of C . [OG,CB] is set
the Arrows of B . ( the ObjectMap of C . (OG,CB)) is set
( the ObjectMap of C * the Arrows of B) . (OG,CB) is set
( the ObjectMap of C * the Arrows of B) . [OG,CB] is set
A is non empty AltCatStr
B is non empty AltCatStr
the carrier of A is non empty set
C is reflexive Covariant FunctorStr over A,B
[: the carrier of A, the carrier of A:] is Relation-like non empty set
the MorphMap of C is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() MSUnTrans of the ObjectMap of C, the Arrows of A, the Arrows of B
the carrier of B is non empty set
[: the carrier of B, the carrier of B:] is Relation-like non empty set
the ObjectMap of C is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of B, the carrier of B:] -valued Function-like non empty V14([: the carrier of A, the carrier of A:]) quasi_total Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:]
[:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:] is Relation-like non empty set
bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:] is non empty set
the Arrows of A is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) set
the Arrows of B is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) set
F is Element of the carrier of A
GI is Element of the carrier of A
[F,GI] is set
{F,GI} is non empty set
{F} is non empty set
{{F,GI},{F}} is non empty set
dom the MorphMap of C is non empty set
Morph-Map (C,F,GI) is Relation-like <^F,GI^> -defined <^(C . F),(C . GI)^> -valued Function-like quasi_total Element of bool [:<^F,GI^>,<^(C . F),(C . GI)^>:]
<^F,GI^> is set
C . F is Element of the carrier of B
the ObjectMap of C . (F,F) is Element of [: the carrier of B, the carrier of B:]
[F,F] is set
{F,F} is non empty set
{{F,F},{F}} is non empty set
the ObjectMap of C . [F,F] is set
K40(( the ObjectMap of C . (F,F))) is set
C . GI is Element of the carrier of B
the ObjectMap of C . (GI,GI) is Element of [: the carrier of B, the carrier of B:]
[GI,GI] is set
{GI,GI} is non empty set
{GI} is non empty set
{{GI,GI},{GI}} is non empty set
the ObjectMap of C . [GI,GI] is set
K40(( the ObjectMap of C . (GI,GI))) is set
<^(C . F),(C . GI)^> is set
[:<^F,GI^>,<^(C . F),(C . GI)^>:] is Relation-like set
bool [:<^F,GI^>,<^(C . F),(C . GI)^>:] is non empty set
the MorphMap of C . (F,GI) is set
the MorphMap of C . [F,GI] is Relation-like Function-like set
F is set
the MorphMap of C . F is Relation-like Function-like set
GI is Relation-like Function-like set
FI is set
MF is set
[FI,MF] is set
{FI,MF} is non empty set
{FI} is non empty set
{{FI,MF},{FI}} is non empty set
OG is Element of the carrier of A
CB is Element of the carrier of A
the MorphMap of C . (OG,CB) is set
[OG,CB] is set
{OG,CB} is non empty set
{OG} is non empty set
{{OG,CB},{OG}} is non empty set
the MorphMap of C . [OG,CB] is Relation-like Function-like set
Morph-Map (C,OG,CB) is Relation-like <^OG,CB^> -defined <^(C . OG),(C . CB)^> -valued Function-like quasi_total Element of bool [:<^OG,CB^>,<^(C . OG),(C . CB)^>:]
<^OG,CB^> is set
C . OG is Element of the carrier of B
the ObjectMap of C . (OG,OG) is Element of [: the carrier of B, the carrier of B:]
[OG,OG] is set
{OG,OG} is non empty set
{{OG,OG},{OG}} is non empty set
the ObjectMap of C . [OG,OG] is set
K40(( the ObjectMap of C . (OG,OG))) is set
C . CB is Element of the carrier of B
the ObjectMap of C . (CB,CB) is Element of [: the carrier of B, the carrier of B:]
[CB,CB] is set
{CB,CB} is non empty set
{CB} is non empty set
{{CB,CB},{CB}} is non empty set
the ObjectMap of C . [CB,CB] is set
K40(( the ObjectMap of C . (CB,CB))) is set
<^(C . OG),(C . CB)^> is set
[:<^OG,CB^>,<^(C . OG),(C . CB)^>:] is Relation-like set
bool [:<^OG,CB^>,<^(C . OG),(C . CB)^>:] is non empty set
A is non empty transitive with_units reflexive AltCatStr
id A is reflexive feasible strict Covariant id-preserving comp-preserving covariant bijective Functor of A,A
(id A) " is strict FunctorStr over A,A
the carrier of A is non empty set
[: the carrier of A, the carrier of A:] is Relation-like non empty set
the Arrows of A is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) set
the ObjectMap of (id A) is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of A, the carrier of A:] -valued Function-like non empty V14([: the carrier of A, the carrier of A:]) quasi_total Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of A, the carrier of A:]:]
[:[: the carrier of A, the carrier of A:],[: the carrier of A, the carrier of A:]:] is Relation-like non empty set
bool [:[: the carrier of A, the carrier of A:],[: the carrier of A, the carrier of A:]:] is non empty set
the ObjectMap of (id A) * the Arrows of A is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) set
the MorphMap of (id A) is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() MSUnTrans of the ObjectMap of (id A), the Arrows of A, the Arrows of A
the MorphMap of ((id A) ") is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() MSUnTrans of the ObjectMap of ((id A) "), the Arrows of A, the Arrows of A
the ObjectMap of ((id A) ") is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of A, the carrier of A:] -valued Function-like non empty V14([: the carrier of A, the carrier of A:]) quasi_total Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of A, the carrier of A:]:]
the ObjectMap of (id A) " is Relation-like Function-like set
C is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() ManySortedFunction of the Arrows of A, the ObjectMap of (id A) * the Arrows of A
C "" is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() ManySortedFunction of the ObjectMap of (id A) * the Arrows of A, the Arrows of A
( the ObjectMap of (id A) ") * (C "") is Relation-like Function-like V36() V37() set
id the Arrows of A is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() ManySortedFunction of the Arrows of A, the Arrows of A
G is set
(id the Arrows of A) . G is Relation-like Function-like set
the Arrows of A . G is set
id ( the Arrows of A . G) is Relation-like the Arrows of A . G -defined the Arrows of A . G -valued Function-like one-to-one V14( the Arrows of A . G) quasi_total onto bijective Element of bool [:( the Arrows of A . G),( the Arrows of A . G):]
[:( the Arrows of A . G),( the Arrows of A . G):] is Relation-like set
bool [:( the Arrows of A . G),( the Arrows of A . G):] is non empty set
dom the Arrows of A is non empty set
(dom the Arrows of A) /\ [: the carrier of A, the carrier of A:] is Relation-like set
G is set
C . G is Relation-like Function-like set
rng (C . G) is set
( the ObjectMap of (id A) * the Arrows of A) . G is set
(id the Arrows of A) . G is Relation-like Function-like set
rng ((id the Arrows of A) . G) is set
the Arrows of A . G is set
id ( the Arrows of A . G) is Relation-like the Arrows of A . G -defined the Arrows of A . G -valued Function-like one-to-one V14( the Arrows of A . G) quasi_total onto bijective Element of bool [:( the Arrows of A . G),( the Arrows of A . G):]
[:( the Arrows of A . G),( the Arrows of A . G):] is Relation-like set
bool [:( the Arrows of A . G),( the Arrows of A . G):] is non empty set
rng (id ( the Arrows of A . G)) is set
id [: the carrier of A, the carrier of A:] is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of A, the carrier of A:] -valued Function-like one-to-one non empty V14([: the carrier of A, the carrier of A:]) quasi_total onto bijective Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of A, the carrier of A:]:]
(id [: the carrier of A, the carrier of A:]) * the Arrows of A is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) set
((id [: the carrier of A, the carrier of A:]) * the Arrows of A) . G is set
G is set
(C "") . G is Relation-like Function-like set
C . G is Relation-like Function-like set
the MorphMap of (id A) . G is Relation-like Function-like set
( the MorphMap of (id A) . G) " is Relation-like Function-like set
(id the Arrows of A) . G is Relation-like Function-like set
((id the Arrows of A) . G) " is Relation-like Function-like set
the Arrows of A . G is set
id ( the Arrows of A . G) is Relation-like the Arrows of A . G -defined the Arrows of A . G -valued Function-like one-to-one V14( the Arrows of A . G) quasi_total onto bijective Element of bool [:( the Arrows of A . G),( the Arrows of A . G):]
[:( the Arrows of A . G),( the Arrows of A . G):] is Relation-like set
bool [:( the Arrows of A . G),( the Arrows of A . G):] is non empty set
(id ( the Arrows of A . G)) " is Relation-like the Arrows of A . G -defined the Arrows of A . G -valued Function-like one-to-one V14( the Arrows of A . G) quasi_total onto bijective Element of bool [:( the Arrows of A . G),( the Arrows of A . G):]
id [: the carrier of A, the carrier of A:] is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of A, the carrier of A:] -valued Function-like one-to-one non empty V14([: the carrier of A, the carrier of A:]) quasi_total onto bijective Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of A, the carrier of A:]:]
(id [: the carrier of A, the carrier of A:]) * the MorphMap of (id A) is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() set
dom the MorphMap of (id A) is non empty set
(dom the MorphMap of (id A)) /\ [: the carrier of A, the carrier of A:] is Relation-like set
G is set
((id [: the carrier of A, the carrier of A:]) * the MorphMap of (id A)) . G is Relation-like Function-like set
the MorphMap of (id A) . G is Relation-like Function-like set
(id [: the carrier of A, the carrier of A:]) " is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of A, the carrier of A:] -valued Function-like one-to-one non empty V14([: the carrier of A, the carrier of A:]) quasi_total onto bijective Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of A, the carrier of A:]:]
A is non empty transitive with_units reflexive AltCatStr
B is non empty transitive with_units reflexive AltCatStr
id B is reflexive feasible strict Covariant id-preserving comp-preserving covariant bijective Functor of B,B
the carrier of A is non empty set
[: the carrier of A, the carrier of A:] is Relation-like non empty set
the carrier of B is non empty set
[: the carrier of B, the carrier of B:] is Relation-like non empty set
F is feasible FunctorStr over A,B
F " is strict FunctorStr over B,A
the Arrows of A is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) set
the ObjectMap of F is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of B, the carrier of B:] -valued Function-like non empty V14([: the carrier of A, the carrier of A:]) quasi_total Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:]
[:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:] is Relation-like non empty set
bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:] is non empty set
the Arrows of B is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) set
the ObjectMap of F * the Arrows of B is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) set
the MorphMap of F is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() MSUnTrans of the ObjectMap of F, the Arrows of A, the Arrows of B
the MorphMap of (F ") is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) V36() V37() MSUnTrans of the ObjectMap of (F "), the Arrows of B, the Arrows of A
the ObjectMap of (F ") is Relation-like [: the carrier of B, the carrier of B:] -defined [: the carrier of A, the carrier of A:] -valued Function-like non empty V14([: the carrier of B, the carrier of B:]) quasi_total Element of bool [:[: the carrier of B, the carrier of B:],[: the carrier of A, the carrier of A:]:]
[:[: the carrier of B, the carrier of B:],[: the carrier of A, the carrier of A:]:] is Relation-like non empty set
bool [:[: the carrier of B, the carrier of B:],[: the carrier of A, the carrier of A:]:] is non empty set
the ObjectMap of F " is Relation-like Function-like set
GI is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() ManySortedFunction of the Arrows of A, the ObjectMap of F * the Arrows of B
GI "" is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() ManySortedFunction of the ObjectMap of F * the Arrows of B, the Arrows of A
( the ObjectMap of F ") * (GI "") is Relation-like Function-like V36() V37() set
rng the ObjectMap of F is Relation-like non empty set
MF is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() ManySortedFunction of the Arrows of A, the ObjectMap of F * the Arrows of B
OG is feasible FunctorStr over B,A
the ObjectMap of OG is Relation-like [: the carrier of B, the carrier of B:] -defined [: the carrier of A, the carrier of A:] -valued Function-like non empty V14([: the carrier of B, the carrier of B:]) quasi_total Element of bool [:[: the carrier of B, the carrier of B:],[: the carrier of A, the carrier of A:]:]
the MorphMap of OG is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) V36() V37() MSUnTrans of the ObjectMap of OG, the Arrows of B, the Arrows of A
FunctorStr(# the ObjectMap of OG, the MorphMap of OG #) is strict FunctorStr over B,A
F * OG is feasible strict FunctorStr over B,B
dom the ObjectMap of F is Relation-like non empty set
the ObjectMap of OG * (GI "") is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) V36() V37() set
the ObjectMap of OG * MF is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) V36() V37() set
( the ObjectMap of OG * MF) ** ( the ObjectMap of OG * (GI "")) is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) V36() V37() set
dom (( the ObjectMap of OG * MF) ** ( the ObjectMap of OG * (GI ""))) is non empty set
id the Arrows of B is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) V36() V37() ManySortedFunction of the Arrows of B, the Arrows of B
OGI is set
(( the ObjectMap of OG * MF) ** ( the ObjectMap of OG * (GI ""))) . OGI is Relation-like Function-like set
(id the Arrows of B) . OGI is Relation-like Function-like set
dom the ObjectMap of OG is Relation-like non empty set
( the ObjectMap of OG * MF) . OGI is Relation-like Function-like set
the ObjectMap of OG . OGI is set
GI . ( the ObjectMap of OG . OGI) is Relation-like Function-like set
rng the ObjectMap of OG is Relation-like non empty set
MF . ( the ObjectMap of OG . OGI) is Relation-like Function-like set
rng (MF . ( the ObjectMap of OG . OGI)) is set
( the ObjectMap of F * the Arrows of B) . ( the ObjectMap of OG . OGI) is set
the ObjectMap of F . ( the ObjectMap of OG . OGI) is set
the Arrows of B . ( the ObjectMap of F . ( the ObjectMap of OG . OGI)) is set
CA is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of B, the carrier of B:] -valued Function-like non empty V14([: the carrier of A, the carrier of A:]) quasi_total Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:]
CA " is Relation-like Function-like set
(CA ") * CA is Relation-like [: the carrier of B, the carrier of B:] -valued Function-like set
((CA ") * CA) . OGI is set
id [: the carrier of B, the carrier of B:] is Relation-like [: the carrier of B, the carrier of B:] -defined [: the carrier of B, the carrier of B:] -valued Function-like one-to-one non empty V14([: the carrier of B, the carrier of B:]) quasi_total onto bijective Element of bool [:[: the carrier of B, the carrier of B:],[: the carrier of B, the carrier of B:]:]
[:[: the carrier of B, the carrier of B:],[: the carrier of B, the carrier of B:]:] is Relation-like non empty set
bool [:[: the carrier of B, the carrier of B:],[: the carrier of B, the carrier of B:]:] is non empty set
(id [: the carrier of B, the carrier of B:]) . OGI is set
dom MF is non empty set
( the ObjectMap of OG * (GI "")) . OGI is Relation-like Function-like set
(GI "") . ( the ObjectMap of OG . OGI) is Relation-like Function-like set
(GI . ( the ObjectMap of OG . OGI)) " is Relation-like Function-like set
(MF . ( the ObjectMap of OG . OGI)) " is Relation-like Function-like set
((MF . ( the ObjectMap of OG . OGI)) ") * (MF . ( the ObjectMap of OG . OGI)) is Relation-like Function-like set
the Arrows of B . OGI is set
id ( the Arrows of B . OGI) is Relation-like the Arrows of B . OGI -defined the Arrows of B . OGI -valued Function-like one-to-one V14( the Arrows of B . OGI) quasi_total onto bijective Element of bool [:( the Arrows of B . OGI),( the Arrows of B . OGI):]
[:( the Arrows of B . OGI),( the Arrows of B . OGI):] is Relation-like set
bool [:( the Arrows of B . OGI),( the Arrows of B . OGI):] is non empty set
the MorphMap of (F * OG) is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) V36() V37() MSUnTrans of the ObjectMap of (F * OG), the Arrows of B, the Arrows of B
the ObjectMap of (F * OG) is Relation-like [: the carrier of B, the carrier of B:] -defined [: the carrier of B, the carrier of B:] -valued Function-like non empty V14([: the carrier of B, the carrier of B:]) quasi_total Element of bool [:[: the carrier of B, the carrier of B:],[: the carrier of B, the carrier of B:]:]
[:[: the carrier of B, the carrier of B:],[: the carrier of B, the carrier of B:]:] is Relation-like non empty set
bool [:[: the carrier of B, the carrier of B:],[: the carrier of B, the carrier of B:]:] is non empty set
the ObjectMap of F * the ObjectMap of OG is Relation-like [: the carrier of B, the carrier of B:] -defined [: the carrier of B, the carrier of B:] -valued Function-like non empty V14([: the carrier of B, the carrier of B:]) quasi_total Element of bool [:[: the carrier of B, the carrier of B:],[: the carrier of B, the carrier of B:]:]
( the ObjectMap of F ") * the ObjectMap of F is Relation-like [: the carrier of B, the carrier of B:] -valued Function-like set
id [: the carrier of B, the carrier of B:] is Relation-like [: the carrier of B, the carrier of B:] -defined [: the carrier of B, the carrier of B:] -valued Function-like one-to-one non empty V14([: the carrier of B, the carrier of B:]) quasi_total onto bijective Element of bool [:[: the carrier of B, the carrier of B:],[: the carrier of B, the carrier of B:]:]
A is set
B is Relation-like A -defined Function-like V14(A) set
C is Relation-like A -defined Function-like V14(A) set
id C is Relation-like A -defined Function-like V14(A) V36() V37() ManySortedFunction of C,C
id B is Relation-like A -defined Function-like V14(A) V36() V37() ManySortedFunction of B,B
G is Relation-like A -defined Function-like V14(A) V36() V37() ManySortedFunction of B,C
G "" is Relation-like A -defined Function-like V14(A) V36() V37() ManySortedFunction of C,B
F is Relation-like A -defined Function-like V14(A) V36() V37() ManySortedFunction of C,B
G ** F is Relation-like A -defined Function-like V14(A) V36() V37() set
F ** G is Relation-like A -defined Function-like V14(A) V36() V37() set
FI is set
B . FI is set
C . FI is set
[:(B . FI),(C . FI):] is Relation-like set
bool [:(B . FI),(C . FI):] is non empty set
G . FI is Relation-like Function-like set
[:(C . FI),(B . FI):] is Relation-like set
bool [:(C . FI),(B . FI):] is non empty set
F . FI is Relation-like Function-like set
dom G is set
MF is Relation-like B . FI -defined C . FI -valued Function-like quasi_total Element of bool [:(B . FI),(C . FI):]
OG is Relation-like C . FI -defined B . FI -valued Function-like quasi_total Element of bool [:(C . FI),(B . FI):]
MF " is Relation-like Function-like set
MF * OG is Relation-like C . FI -defined C . FI -valued Function-like Element of bool [:(C . FI),(C . FI):]
[:(C . FI),(C . FI):] is Relation-like set
bool [:(C . FI),(C . FI):] is non empty set
rng MF is set
id (rng MF) is Relation-like rng MF -defined rng MF -valued Function-like one-to-one V14( rng MF) quasi_total onto bijective Element of bool [:(rng MF),(rng MF):]
[:(rng MF),(rng MF):] is Relation-like set
bool [:(rng MF),(rng MF):] is non empty set
id (C . FI) is Relation-like C . FI -defined C . FI -valued Function-like one-to-one V14(C . FI) quasi_total onto bijective Element of bool [:(C . FI),(C . FI):]
(G ** F) . FI is Relation-like Function-like set
FI is set
GI is Relation-like A -defined Function-like V14(A) V36() V37() set
GI . FI is Relation-like Function-like set
C . FI is set
id (C . FI) is Relation-like C . FI -defined C . FI -valued Function-like one-to-one V14(C . FI) quasi_total onto bijective Element of bool [:(C . FI),(C . FI):]
[:(C . FI),(C . FI):] is Relation-like set
bool [:(C . FI),(C . FI):] is non empty set
MF is set
(F ** G) . MF is Relation-like Function-like set
B . MF is set
id (B . MF) is Relation-like B . MF -defined B . MF -valued Function-like one-to-one V14(B . MF) quasi_total onto bijective Element of bool [:(B . MF),(B . MF):]
[:(B . MF),(B . MF):] is Relation-like set
bool [:(B . MF),(B . MF):] is non empty set
C . MF is set
[:(B . MF),(C . MF):] is Relation-like set
bool [:(B . MF),(C . MF):] is non empty set
G . MF is Relation-like Function-like set
[:(C . MF),(B . MF):] is Relation-like set
bool [:(C . MF),(B . MF):] is non empty set
F . MF is Relation-like Function-like set
OG is Relation-like B . MF -defined C . MF -valued Function-like quasi_total Element of bool [:(B . MF),(C . MF):]
dom OG is set
CB is Relation-like C . MF -defined B . MF -valued Function-like quasi_total Element of bool [:(C . MF),(B . MF):]
OG " is Relation-like Function-like set
CB * OG is Relation-like B . MF -defined B . MF -valued Function-like Element of bool [:(B . MF),(B . MF):]
MF is set
(F ** G) . MF is Relation-like Function-like set
B . MF is set
id (B . MF) is Relation-like B . MF -defined B . MF -valued Function-like one-to-one V14(B . MF) quasi_total onto bijective Element of bool [:(B . MF),(B . MF):]
[:(B . MF),(B . MF):] is Relation-like set
bool [:(B . MF),(B . MF):] is non empty set
FI is Relation-like A -defined Function-like V14(A) V36() V37() set
MF is Relation-like A -defined Function-like V14(A) V36() V37() ManySortedFunction of B,B
A is non empty transitive with_units reflexive AltCatStr
B is non empty transitive with_units reflexive AltCatStr
id A is reflexive feasible strict Covariant id-preserving comp-preserving covariant bijective Functor of A,A
the carrier of A is non empty set
[: the carrier of A, the carrier of A:] is Relation-like non empty set
G is feasible FunctorStr over A,B
G " is strict FunctorStr over B,A
(G ") * G is strict FunctorStr over A,A
the Arrows of A is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) set
the ObjectMap of G is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of B, the carrier of B:] -valued Function-like non empty V14([: the carrier of A, the carrier of A:]) quasi_total Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:]
the carrier of B is non empty set
[: the carrier of B, the carrier of B:] is Relation-like non empty set
[:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:] is Relation-like non empty set
bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:] is non empty set
the Arrows of B is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) set
the ObjectMap of G * the Arrows of B is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) set
the MorphMap of G is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() MSUnTrans of the ObjectMap of G, the Arrows of A, the Arrows of B
the MorphMap of (G ") is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) V36() V37() MSUnTrans of the ObjectMap of (G "), the Arrows of B, the Arrows of A
the ObjectMap of (G ") is Relation-like [: the carrier of B, the carrier of B:] -defined [: the carrier of A, the carrier of A:] -valued Function-like non empty V14([: the carrier of B, the carrier of B:]) quasi_total Element of bool [:[: the carrier of B, the carrier of B:],[: the carrier of A, the carrier of A:]:]
[:[: the carrier of B, the carrier of B:],[: the carrier of A, the carrier of A:]:] is Relation-like non empty set
bool [:[: the carrier of B, the carrier of B:],[: the carrier of A, the carrier of A:]:] is non empty set
the ObjectMap of G " is Relation-like Function-like set
F is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() ManySortedFunction of the Arrows of A, the ObjectMap of G * the Arrows of B
F "" is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() ManySortedFunction of the ObjectMap of G * the Arrows of B, the Arrows of A
( the ObjectMap of G ") * (F "") is Relation-like Function-like V36() V37() set
dom the ObjectMap of G is Relation-like non empty set
FI is set
( the ObjectMap of G * the Arrows of B) . FI is set
the Arrows of A . FI is set
MF is set
OG is set
[MF,OG] is set
{MF,OG} is non empty set
{MF} is non empty set
{{MF,OG},{MF}} is non empty set
CB is Element of the carrier of A
CA is Element of the carrier of A
the Arrows of A . (CB,CA) is set
[CB,CA] is set
{CB,CA} is non empty set
{CB} is non empty set
{{CB,CA},{CB}} is non empty set
the Arrows of A . [CB,CA] is set
<^CB,CA^> is set
the ObjectMap of G . (CB,CA) is Element of [: the carrier of B, the carrier of B:]
the ObjectMap of G . [CB,CA] is set
the Arrows of B . ( the ObjectMap of G . (CB,CA)) is set
id [: the carrier of A, the carrier of A:] is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of A, the carrier of A:] -valued Function-like one-to-one non empty V14([: the carrier of A, the carrier of A:]) quasi_total onto bijective Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of A, the carrier of A:]:]
[:[: the carrier of A, the carrier of A:],[: the carrier of A, the carrier of A:]:] is Relation-like non empty set
bool [:[: the carrier of A, the carrier of A:],[: the carrier of A, the carrier of A:]:] is non empty set
(id [: the carrier of A, the carrier of A:]) * (F "") is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() set
FI is set
((id [: the carrier of A, the carrier of A:]) * (F "")) . FI is Relation-like Function-like set
(F "") . FI is Relation-like Function-like set
(id [: the carrier of A, the carrier of A:]) . FI is set
(F "") . ((id [: the carrier of A, the carrier of A:]) . FI) is Relation-like Function-like set
the ObjectMap of ((G ") * G) is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of A, the carrier of A:] -valued Function-like non empty V14([: the carrier of A, the carrier of A:]) quasi_total Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of A, the carrier of A:]:]
the ObjectMap of (G ") * the ObjectMap of G is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of A, the carrier of A:] -valued Function-like non empty V14([: the carrier of A, the carrier of A:]) quasi_total Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of A, the carrier of A:]:]
the ObjectMap of G * ( the ObjectMap of G ") is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like set
the MorphMap of ((G ") * G) is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() MSUnTrans of the ObjectMap of ((G ") * G), the Arrows of A, the Arrows of A
the ObjectMap of G * (( the ObjectMap of G ") * (F "")) is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like V36() V37() set
( the ObjectMap of G * (( the ObjectMap of G ") * (F ""))) ** F is Relation-like Function-like V36() V37() set
( the ObjectMap of G * ( the ObjectMap of G ")) * (F "") is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like V36() V37() set
(( the ObjectMap of G * ( the ObjectMap of G ")) * (F "")) ** F is Relation-like Function-like V36() V37() set
((id [: the carrier of A, the carrier of A:]) * (F "")) ** F is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() set
id the Arrows of A is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() ManySortedFunction of the Arrows of A, the Arrows of A
FI is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() ManySortedFunction of the Arrows of A, the ObjectMap of G * the Arrows of B
A is non empty transitive with_units reflexive AltCatStr
B is non empty transitive with_units reflexive AltCatStr
the carrier of A is non empty set
[: the carrier of A, the carrier of A:] is Relation-like non empty set
the carrier of B is non empty set
[: the carrier of B, the carrier of B:] is Relation-like non empty set
F is feasible FunctorStr over A,B
F " is strict FunctorStr over B,A
(F ") " is strict FunctorStr over A,B
the ObjectMap of F is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of B, the carrier of B:] -valued Function-like non empty V14([: the carrier of A, the carrier of A:]) quasi_total Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:]
[:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:] is Relation-like non empty set
bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:] is non empty set
the MorphMap of F is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() MSUnTrans of the ObjectMap of F, the Arrows of A, the Arrows of B
the Arrows of A is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) set
the Arrows of B is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) set
FunctorStr(# the ObjectMap of F, the MorphMap of F #) is strict FunctorStr over A,B
the ObjectMap of (F ") is Relation-like [: the carrier of B, the carrier of B:] -defined [: the carrier of A, the carrier of A:] -valued Function-like non empty V14([: the carrier of B, the carrier of B:]) quasi_total Element of bool [:[: the carrier of B, the carrier of B:],[: the carrier of A, the carrier of A:]:]
[:[: the carrier of B, the carrier of B:],[: the carrier of A, the carrier of A:]:] is Relation-like non empty set
bool [:[: the carrier of B, the carrier of B:],[: the carrier of A, the carrier of A:]:] is non empty set
the ObjectMap of (F ") " is Relation-like Function-like set
the ObjectMap of F " is Relation-like Function-like set
( the ObjectMap of F ") " is Relation-like Function-like set
rng the ObjectMap of F is Relation-like non empty set
the MorphMap of ((F ") ") is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() MSUnTrans of the ObjectMap of ((F ") "), the Arrows of A, the Arrows of B
the ObjectMap of ((F ") ") is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of B, the carrier of B:] -valued Function-like non empty V14([: the carrier of A, the carrier of A:]) quasi_total Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:]
the ObjectMap of (F ") * the Arrows of A is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) set
the MorphMap of (F ") is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) V36() V37() MSUnTrans of the ObjectMap of (F "), the Arrows of B, the Arrows of A
the ObjectMap of F * the Arrows of B is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) set
GI is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) V36() V37() ManySortedFunction of the Arrows of B, the ObjectMap of (F ") * the Arrows of A
GI "" is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) V36() V37() ManySortedFunction of the ObjectMap of (F ") * the Arrows of A, the Arrows of B
( the ObjectMap of (F ") ") * (GI "") is Relation-like Function-like V36() V37() set
FI is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() ManySortedFunction of the Arrows of A, the ObjectMap of F * the Arrows of B
FI "" is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() ManySortedFunction of the ObjectMap of F * the Arrows of B, the Arrows of A
( the ObjectMap of F ") * (FI "") is Relation-like Function-like V36() V37() set
MF is set
(( the ObjectMap of (F ") ") * (GI "")) . MF is Relation-like Function-like set
the MorphMap of F . MF is Relation-like Function-like set
the ObjectMap of F . MF is set
( the ObjectMap of F ") . ( the ObjectMap of F . MF) is set
FI . MF is Relation-like Function-like set
(GI "") . ( the ObjectMap of F . MF) is Relation-like Function-like set
the MorphMap of (F ") . ( the ObjectMap of F . MF) is Relation-like Function-like set
( the MorphMap of (F ") . ( the ObjectMap of F . MF)) " is Relation-like Function-like set
(FI "") . (( the ObjectMap of F ") . ( the ObjectMap of F . MF)) is Relation-like Function-like set
((FI "") . (( the ObjectMap of F ") . ( the ObjectMap of F . MF))) " is Relation-like Function-like set
FI . (( the ObjectMap of F ") . ( the ObjectMap of F . MF)) is Relation-like Function-like set
(FI . (( the ObjectMap of F ") . ( the ObjectMap of F . MF))) " is Relation-like Function-like set
((FI . (( the ObjectMap of F ") . ( the ObjectMap of F . MF))) ") " is Relation-like Function-like set
(FI . MF) " is Relation-like Function-like set
((FI . MF) ") " is Relation-like Function-like set
OG is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) V36() V37() ManySortedFunction of the Arrows of B, the ObjectMap of (F ") * the Arrows of A
OG is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() ManySortedFunction of the Arrows of A, the ObjectMap of F * the Arrows of B
A is non empty transitive with_units reflexive AltCatStr
B is non empty transitive with_units reflexive AltCatStr
C is non empty transitive with_units reflexive AltCatStr
G is feasible FunctorStr over A,B
G " is strict FunctorStr over B,A
F is feasible FunctorStr over B,C
F " is strict FunctorStr over C,B
F * G is feasible strict FunctorStr over A,C
(F * G) " is strict FunctorStr over C,A
GI is feasible FunctorStr over B,A
the ObjectMap of GI is Relation-like [: the carrier of B, the carrier of B:] -defined [: the carrier of A, the carrier of A:] -valued Function-like non empty V14([: the carrier of B, the carrier of B:]) quasi_total Element of bool [:[: the carrier of B, the carrier of B:],[: the carrier of A, the carrier of A:]:]
the carrier of B is non empty set
[: the carrier of B, the carrier of B:] is Relation-like non empty set
the carrier of A is non empty set
[: the carrier of A, the carrier of A:] is Relation-like non empty set
[:[: the carrier of B, the carrier of B:],[: the carrier of A, the carrier of A:]:] is Relation-like non empty set
bool [:[: the carrier of B, the carrier of B:],[: the carrier of A, the carrier of A:]:] is non empty set
the MorphMap of GI is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) V36() V37() MSUnTrans of the ObjectMap of GI, the Arrows of B, the Arrows of A
the Arrows of B is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) set
the Arrows of A is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) set
FunctorStr(# the ObjectMap of GI, the MorphMap of GI #) is strict FunctorStr over B,A
FI is feasible FunctorStr over C,B
the ObjectMap of FI is Relation-like [: the carrier of C, the carrier of C:] -defined [: the carrier of B, the carrier of B:] -valued Function-like non empty V14([: the carrier of C, the carrier of C:]) quasi_total Element of bool [:[: the carrier of C, the carrier of C:],[: the carrier of B, the carrier of B:]:]
the carrier of C is non empty set
[: 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 B, the carrier of B:]:] is Relation-like non empty set
bool [:[: the carrier of C, the carrier of C:],[: the carrier of B, the carrier of B:]:] is non empty set
the MorphMap of FI 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 FI, the Arrows of C, the Arrows of B
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
FunctorStr(# the ObjectMap of FI, the MorphMap of FI #) is strict FunctorStr over C,B
GI * FI is feasible strict FunctorStr over C,A
the ObjectMap of F is Relation-like [: the carrier of B, the carrier of B:] -defined [: the carrier of C, the carrier of C:] -valued Function-like non empty V14([: the carrier of B, the carrier of B:]) quasi_total Element of bool [:[: the carrier of B, the carrier of B:],[: the carrier of C, the carrier of C:]:]
[:[: the carrier of B, the carrier of B:],[: the carrier of C, the carrier of C:]:] is Relation-like non empty set
bool [:[: the carrier of B, the carrier of B:],[: the carrier of C, the carrier of C:]:] is non empty set
the ObjectMap of F * the Arrows of C is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) set
the MorphMap of F is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) V36() V37() MSUnTrans of the ObjectMap of F, the Arrows of B, the Arrows of C
MF is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) V36() V37() ManySortedFunction of the Arrows of B, the ObjectMap of F * the Arrows of C
the ObjectMap of G is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of B, the carrier of B:] -valued Function-like non empty V14([: the carrier of A, the carrier of A:]) quasi_total Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:]
[:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:] is Relation-like non empty set
bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:] is non empty set
the ObjectMap of G " is Relation-like Function-like set
the ObjectMap of F " is Relation-like Function-like set
the ObjectMap of (F * G) is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of C, the carrier of C:] -valued Function-like non empty V14([: the carrier of A, the carrier of A:]) quasi_total Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of C, the carrier of C:]:]
[:[: the carrier of A, the carrier of A:],[: the carrier of C, the carrier of C:]:] is Relation-like non empty set
bool [:[: the carrier of A, the carrier of A:],[: the carrier of C, the carrier of C:]:] is non empty set
the ObjectMap of (F * G) * the Arrows of C is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) set
the MorphMap of (F * G) is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() MSUnTrans of the ObjectMap of (F * G), the Arrows of A, the Arrows of C
the ObjectMap of G * the Arrows of B is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) set
the MorphMap of G is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() MSUnTrans of the ObjectMap of G, the Arrows of A, the Arrows of B
MG is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() ManySortedFunction of the Arrows of A, the ObjectMap of G * the Arrows of B
MFG is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() ManySortedFunction of the Arrows of A, the ObjectMap of (F * G) * the Arrows of C
the MorphMap of ((F * G) ") 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 ((F * G) "), the Arrows of C, the Arrows of A
the ObjectMap of ((F * G) ") is Relation-like [: the carrier of C, the carrier of C:] -defined [: the carrier of A, the carrier of A:] -valued Function-like non empty V14([: the carrier of C, the carrier of C:]) quasi_total Element of bool [:[: the carrier of C, the carrier of C:],[: the carrier of A, the carrier of A:]:]
[:[: the carrier of C, the carrier of C:],[: the carrier of A, the carrier of A:]:] is Relation-like non empty set
bool [:[: the carrier of C, the carrier of C:],[: the carrier of A, the carrier of A:]:] is non empty set
the MorphMap of (GI * FI) 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 (GI * FI), the Arrows of C, the Arrows of A
the ObjectMap of (GI * FI) is Relation-like [: the carrier of C, the carrier of C:] -defined [: the carrier of A, the carrier of A:] -valued Function-like non empty V14([: the carrier of C, the carrier of C:]) quasi_total Element of bool [:[: the carrier of C, the carrier of C:],[: the carrier of A, the carrier of A:]:]
the ObjectMap of (F * G) " is Relation-like Function-like set
f is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() ManySortedFunction of the Arrows of A, the ObjectMap of (F * G) * the Arrows of C
f "" is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() ManySortedFunction of the ObjectMap of (F * G) * the Arrows of C, the Arrows of A
( the ObjectMap of (F * G) ") * (f "") is Relation-like Function-like V36() V37() set
rng the ObjectMap of G is Relation-like non empty set
the MorphMap of (F ") 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 (F "), the Arrows of C, the Arrows of B
the ObjectMap of (F ") is Relation-like [: the carrier of C, the carrier of C:] -defined [: the carrier of B, the carrier of B:] -valued Function-like non empty V14([: the carrier of C, the carrier of C:]) quasi_total Element of bool [:[: the carrier of C, the carrier of C:],[: the carrier of B, the carrier of B:]:]
the MorphMap of (G ") is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) V36() V37() MSUnTrans of the ObjectMap of (G "), the Arrows of B, the Arrows of A
the ObjectMap of (G ") is Relation-like [: the carrier of B, the carrier of B:] -defined [: the carrier of A, the carrier of A:] -valued Function-like non empty V14([: the carrier of B, the carrier of B:]) quasi_total Element of bool [:[: the carrier of B, the carrier of B:],[: the carrier of A, the carrier of A:]:]
the ObjectMap of (F ") * the MorphMap of (G ") 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() set
( the ObjectMap of (F ") * the MorphMap of (G ")) ** the MorphMap of (F ") 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() set
OFI is Relation-like [: the carrier of C, the carrier of C:] -defined [: the carrier of B, the carrier of B:] -valued Function-like non empty V14([: the carrier of C, the carrier of C:]) quasi_total Element of bool [:[: the carrier of C, the carrier of C:],[: the carrier of B, the carrier of B:]:]
MF "" is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) V36() V37() ManySortedFunction of the ObjectMap of F * the Arrows of C, the Arrows of B
OFI * (MF "") 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() set
OGI is Relation-like [: the carrier of B, the carrier of B:] -defined [: the carrier of A, the carrier of A:] -valued Function-like non empty V14([: the carrier of B, the carrier of B:]) quasi_total Element of bool [:[: the carrier of B, the carrier of B:],[: the carrier of A, the carrier of A:]:]
MG "" is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() ManySortedFunction of the ObjectMap of G * the Arrows of B, the Arrows of A
OGI * (MG "") is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) V36() V37() set
OFI * (OGI * (MG "")) 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() set
(OFI * (OGI * (MG ""))) ** (OFI * (MF "")) 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() set
dom ((OFI * (OGI * (MG ""))) ** (OFI * (MF ""))) is non empty set
OG is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of B, the carrier of B:] -valued Function-like non empty V14([: the carrier of A, the carrier of A:]) quasi_total Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:]
OG " is Relation-like Function-like set
(OG ") * OG is Relation-like [: the carrier of B, the carrier of B:] -valued Function-like set
id [: the carrier of B, the carrier of B:] is Relation-like [: the carrier of B, the carrier of B:] -defined [: the carrier of B, the carrier of B:] -valued Function-like one-to-one non empty V14([: the carrier of B, the carrier of B:]) quasi_total onto bijective Element of bool [:[: the carrier of B, the carrier of B:],[: the carrier of B, the carrier of B:]:]
[:[: the carrier of B, the carrier of B:],[: the carrier of B, the carrier of B:]:] is Relation-like non empty set
bool [:[: the carrier of B, the carrier of B:],[: the carrier of B, the carrier of B:]:] is non empty set
OFG is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of C, the carrier of C:] -valued Function-like non empty V14([: the carrier of A, the carrier of A:]) quasi_total Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of C, the carrier of C:]:]
OFG " is Relation-like Function-like set
the ObjectMap of F * OG is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of C, the carrier of C:] -valued Function-like non empty V14([: the carrier of A, the carrier of A:]) quasi_total Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of C, the carrier of C:]:]
( the ObjectMap of F * OG) " is Relation-like Function-like set
( the ObjectMap of F ") * (OG ") is Relation-like Function-like set
i is set
(( the ObjectMap of (F * G) ") * (f "")) . i is Relation-like Function-like set
(( the ObjectMap of (F ") * the MorphMap of (G ")) ** the MorphMap of (F ")) . i is Relation-like Function-like set
(OFG ") . i is set
MG . ((OFG ") . i) is Relation-like Function-like set
(( the ObjectMap of F ") * (OG ")) . i is set
OG . ((( the ObjectMap of F ") * (OG ")) . i) is set
MF . (OG . ((( the ObjectMap of F ") * (OG ")) . i)) is Relation-like Function-like set
(MG . ((OFG ") . i)) * (MF . (OG . ((( the ObjectMap of F ") * (OG ")) . i))) is Relation-like Function-like set
((MG . ((OFG ") . i)) * (MF . (OG . ((( the ObjectMap of F ") * (OG ")) . i)))) " is Relation-like Function-like set
OFI . i is set
OGI . (OFI . i) is set
OG . (OGI . (OFI . i)) is set
MF . (OG . (OGI . (OFI . i))) is Relation-like Function-like set
(MG . ((OFG ") . i)) * (MF . (OG . (OGI . (OFI . i)))) is Relation-like Function-like set
((MG . ((OFG ") . i)) * (MF . (OG . (OGI . (OFI . i))))) " is Relation-like Function-like set
OG * OGI is Relation-like [: the carrier of B, the carrier of B:] -defined [: the carrier of B, the carrier of B:] -valued Function-like non empty V14([: the carrier of B, the carrier of B:]) quasi_total Element of bool [:[: the carrier of B, the carrier of B:],[: the carrier of B, the carrier of B:]:]
(OG * OGI) . (OFI . i) is set
MF . ((OG * OGI) . (OFI . i)) is Relation-like Function-like set
(MG . ((OFG ") . i)) * (MF . ((OG * OGI) . (OFI . i))) is Relation-like Function-like set
((MG . ((OFG ") . i)) * (MF . ((OG * OGI) . (OFI . i)))) " is Relation-like Function-like set
(id [: the carrier of B, the carrier of B:]) * OFI is Relation-like [: the carrier of C, the carrier of C:] -defined [: the carrier of B, the carrier of B:] -valued Function-like non empty V14([: the carrier of C, the carrier of C:]) quasi_total Element of bool [:[: the carrier of C, the carrier of C:],[: the carrier of B, the carrier of B:]:]
((id [: the carrier of B, the carrier of B:]) * OFI) . i is set
MF . (((id [: the carrier of B, the carrier of B:]) * OFI) . i) is Relation-like Function-like set
(MG . ((OFG ") . i)) * (MF . (((id [: the carrier of B, the carrier of B:]) * OFI) . i)) is Relation-like Function-like set
((MG . ((OFG ") . i)) * (MF . (((id [: the carrier of B, the carrier of B:]) * OFI) . i))) " is Relation-like Function-like set
OGI * OFI is Relation-like [: the carrier of C, the carrier of C:] -defined [: the carrier of A, the carrier of A:] -valued Function-like non empty V14([: the carrier of C, the carrier of C:]) quasi_total Element of bool [:[: the carrier of C, the carrier of C:],[: the carrier of A, the carrier of A:]:]
(OGI * OFI) . i is set
MG . ((OGI * OFI) . i) is Relation-like Function-like set
( the ObjectMap of F ") . i is set
MF . (( the ObjectMap of F ") . i) is Relation-like Function-like set
(MG . ((OGI * OFI) . i)) * (MF . (( the ObjectMap of F ") . i)) is Relation-like Function-like set
((MG . ((OGI * OFI) . i)) * (MF . (( the ObjectMap of F ") . i))) " is Relation-like Function-like set
OG * MF is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() set
(OG * MF) ** MG is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() set
dom ((OG * MF) ** MG) is non empty set
( the ObjectMap of (F * G) ") . i is set
dom ( the ObjectMap of (F * G) ") is set
MFG "" is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() ManySortedFunction of the ObjectMap of (F * G) * the Arrows of C, the Arrows of A
(MFG "") . (( the ObjectMap of (F * G) ") . i) is Relation-like Function-like set
MFG . (( the ObjectMap of (F * G) ") . i) is Relation-like Function-like set
(MFG . (( the ObjectMap of (F * G) ") . i)) " is Relation-like Function-like set
((OG * MF) ** MG) . ((OFG ") . i) is Relation-like Function-like set
(((OG * MF) ** MG) . ((OFG ") . i)) " is Relation-like Function-like set
(OG * MF) . ((OFG ") . i) is Relation-like Function-like set
(MG . ((OFG ") . i)) * ((OG * MF) . ((OFG ") . i)) is Relation-like Function-like set
((MG . ((OFG ") . i)) * ((OG * MF) . ((OFG ") . i))) " is Relation-like Function-like set
c₂₂ is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() ManySortedFunction of the Arrows of A, the ObjectMap of (F * G) * the Arrows of C
MF . (OFI . i) is Relation-like Function-like set
MG . (OGI . (OFI . i)) is Relation-like Function-like set
(MG . (OGI . (OFI . i))) * (MF . (( the ObjectMap of F ") . i)) is Relation-like Function-like set
((MG . (OGI . (OFI . i))) * (MF . (( the ObjectMap of F ") . i))) " is Relation-like Function-like set
(MF . (OFI . i)) " is Relation-like Function-like set
(MG . (OGI . (OFI . i))) " is Relation-like Function-like set
((MF . (OFI . i)) ") * ((MG . (OGI . (OFI . i))) ") is Relation-like Function-like set
(MF . (( the ObjectMap of F ") . i)) " is Relation-like Function-like set
(MG "") . (OGI . (OFI . i)) is Relation-like Function-like set
((MF . (( the ObjectMap of F ") . i)) ") * ((MG "") . (OGI . (OFI . i))) is Relation-like Function-like set
(OGI * (MG "")) . (OFI . i) is Relation-like Function-like set
((MF . (( the ObjectMap of F ") . i)) ") * ((OGI * (MG "")) . (OFI . i)) is Relation-like Function-like set
(OFI * (OGI * (MG ""))) . i is Relation-like Function-like set
((MF . (OFI . i)) ") * ((OFI * (OGI * (MG ""))) . i) is Relation-like Function-like set
(MF "") . (OFI . i) is Relation-like Function-like set
((MF "") . (OFI . i)) * ((OFI * (OGI * (MG ""))) . i) is Relation-like Function-like set
(OFI * (MF "")) . i is Relation-like Function-like set
((OFI * (MF "")) . i) * ((OFI * (OGI * (MG ""))) . i) is Relation-like Function-like set
c₂₂ is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() ManySortedFunction of the Arrows of A, the ObjectMap of G * the Arrows of B
c₂₂ is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) V36() V37() ManySortedFunction of the Arrows of B, the ObjectMap of F * the Arrows of C
c₂₂ is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) V36() V37() ManySortedFunction of the Arrows of B, the ObjectMap of F * the Arrows of C
c₂₂ "" is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) V36() V37() ManySortedFunction of the ObjectMap of F * the Arrows of C, the Arrows of B
( the ObjectMap of F ") * (c₂₂ "") is Relation-like Function-like V36() V37() set
c₂₃ is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() ManySortedFunction of the Arrows of A, the ObjectMap of G * the Arrows of B
c₂₃ "" is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) V36() V37() ManySortedFunction of the ObjectMap of G * the Arrows of B, the Arrows of A
( the ObjectMap of G ") * (c₂₃ "") is Relation-like Function-like V36() V37() set
the ObjectMap of FI * the MorphMap of GI 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() set
( the ObjectMap of FI * the MorphMap of GI) ** the MorphMap of FI 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() set
the ObjectMap of (F * G) " is Relation-like Function-like set
the ObjectMap of F * the ObjectMap of G is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of C, the carrier of C:] -valued Function-like non empty V14([: the carrier of A, the carrier of A:]) quasi_total Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of C, the carrier of C:]:]
( the ObjectMap of F * the ObjectMap of G) " is Relation-like Function-like set
( the ObjectMap of F ") * ( the ObjectMap of G ") is Relation-like Function-like set
( the ObjectMap of F ") * the ObjectMap of GI is Relation-like [: the carrier of A, the carrier of A:] -valued Function-like set
the ObjectMap of GI * the ObjectMap of FI is Relation-like [: the carrier of C, the carrier of C:] -defined [: the carrier of A, the carrier of A:] -valued Function-like non empty V14([: the carrier of C, the carrier of C:]) quasi_total Element of bool [:[: the carrier of C, the carrier of C:],[: the carrier of A, the carrier of A:]:]