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

1 is non empty set
{{},1} is non empty set

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

C * (incl G) is feasible strict FunctorStr over G,B
A is set

[:A,A:] is Relation-like set
bool [:A,A:] is non empty set

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

[:C,A:] is Relation-like non empty set
bool [:C,A:] is non empty set

[:B,A:] is Relation-like non empty set
bool [:B,A:] is non empty set
G is non empty Element of bool B

[:G,B:] is Relation-like non empty set
bool [:G,B:] is non empty set

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

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

rng F is set

rng G is set
rng (F * G) is set
A is non empty reflexive AltCatStr
B is non empty reflexive SubCatStr of A

C is non empty SubCatStr of A

G is non empty SubCatStr of 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

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

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) * (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

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

GI * (incl G) is strict FunctorStr over G,B
GI | C is FunctorStr over C,B

GI * (incl C) is strict FunctorStr over C,B
(GI | C) | F is FunctorStr over F,B

(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

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

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

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

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

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

(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

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

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

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