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