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