:: YELLOW20 semantic presentation

K154() is M2( bool K150())

K150() is set

bool K150() is non empty set

K116() is set

bool K116() is non empty set

bool K154() is non empty set

{} is set

the Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty Function-yielding V37() set is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty Function-yielding V37() set

1 is non empty set

{{},1} is set

proj1 {} is set

proj2 {} is set

A1 is non empty transitive with_units reflexive AltCatStr

A2 is non empty transitive with_units reflexive AltCatStr

the carrier of A1 is non empty set

the carrier of A2 is non empty set

F is reflexive feasible FunctorStr over A1,A2

F " is strict FunctorStr over A2,A1

B2 is M2( the carrier of A1)

F . B2 is M2( the carrier of A2)

[: the carrier of A2, the carrier of A2:] is Relation-like non empty set

the ObjectMap of F is Relation-like [: the carrier of A1, the carrier of A1:] -defined [: the carrier of A2, the carrier of A2:] -valued Function-like quasi_total M2( bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A2, the carrier of A2:]:])

[: the carrier of A1, the carrier of A1:] is Relation-like non empty set

[:[: the carrier of A1, the carrier of A1:],[: the carrier of A2, the carrier of A2:]:] is Relation-like non empty set

bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A2, the carrier of A2:]:] is non empty set

the ObjectMap of F . (B2,B2) is M2([: the carrier of A2, the carrier of A2:])

[B2,B2] is V15() set

{B2,B2} is set

{B2} is set

{{B2,B2},{B2}} is set

the ObjectMap of F . [B2,B2] is set

( the ObjectMap of F . (B2,B2)) `1 is set

G is M2( the carrier of A2)

(F ") . G is M2( the carrier of A1)

the ObjectMap of (F ") is Relation-like [: the carrier of A2, the carrier of A2:] -defined [: the carrier of A1, the carrier of A1:] -valued Function-like quasi_total M2( bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:])

[:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:] is Relation-like non empty set

bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:] is non empty set

the ObjectMap of (F ") . (G,G) is M2([: the carrier of A1, the carrier of A1:])

[G,G] is V15() set

{G,G} is set

{G} is set

{{G,G},{G}} is set

the ObjectMap of (F ") . [G,G] is set

( the ObjectMap of (F ") . (G,G)) `1 is set

(F ") * F is strict FunctorStr over A1,A1

id A1 is reflexive feasible strict Covariant id-preserving comp-preserving covariant bijective Functor of A1,A1

((F ") * F) . B2 is M2( the carrier of A1)

the ObjectMap of ((F ") * F) is Relation-like [: the carrier of A1, the carrier of A1:] -defined [: the carrier of A1, the carrier of A1:] -valued Function-like quasi_total M2( bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A1, the carrier of A1:]:])

[:[: the carrier of A1, the carrier of A1:],[: the carrier of A1, the carrier of A1:]:] is Relation-like non empty set

bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A1, the carrier of A1:]:] is non empty set

the ObjectMap of ((F ") * F) . (B2,B2) is M2([: the carrier of A1, the carrier of A1:])

the ObjectMap of ((F ") * F) . [B2,B2] is set

( the ObjectMap of ((F ") * F) . (B2,B2)) `1 is set

B1 is reflexive feasible FunctorStr over A2,A1

F * B1 is feasible strict FunctorStr over A2,A2

id A2 is reflexive feasible strict Covariant id-preserving comp-preserving covariant bijective Functor of A2,A2

(F * B1) . G is M2( the carrier of A2)

the ObjectMap of (F * B1) is Relation-like [: the carrier of A2, the carrier of A2:] -defined [: the carrier of A2, the carrier of A2:] -valued Function-like quasi_total M2( bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A2, the carrier of A2:]:])

[:[: the carrier of A2, the carrier of A2:],[: the carrier of A2, the carrier of A2:]:] is Relation-like non empty set

bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A2, the carrier of A2:]:] is non empty set

the ObjectMap of (F * B1) . (G,G) is M2([: the carrier of A2, the carrier of A2:])

the ObjectMap of (F * B1) . [G,G] is set

( the ObjectMap of (F * B1) . (G,G)) `1 is set

A1 is non empty transitive with_units reflexive AltCatStr

A2 is non empty transitive with_units reflexive AltCatStr

the carrier of A1 is non empty set

F is reflexive feasible Covariant FunctorStr over A1,A2

F " is strict FunctorStr over A2,A1

B1 is reflexive feasible Covariant FunctorStr over A2,A1

B2 is M2( the carrier of A1)

G is M2( the carrier of A1)

<^B2,G^> is set

the Arrows of A1 is Relation-like [: the carrier of A1, the carrier of A1:] -defined Function-like non empty total set

[: the carrier of A1, the carrier of A1:] is Relation-like non empty set

the Arrows of A1 . (B2,G) is set

[B2,G] is V15() set

{B2,G} is set

{B2} is set

{{B2,G},{B2}} is set

the Arrows of A1 . [B2,G] is set

F . B2 is M2( the carrier of A2)

the carrier of A2 is non empty set

[: the carrier of A2, the carrier of A2:] is Relation-like non empty set

the ObjectMap of F is Relation-like [: the carrier of A1, the carrier of A1:] -defined [: the carrier of A2, the carrier of A2:] -valued Function-like quasi_total M2( bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A2, the carrier of A2:]:])

[:[: the carrier of A1, the carrier of A1:],[: the carrier of A2, the carrier of A2:]:] is Relation-like non empty set

bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A2, the carrier of A2:]:] is non empty set

the ObjectMap of F . (B2,B2) is M2([: the carrier of A2, the carrier of A2:])

[B2,B2] is V15() set

{B2,B2} is set

{{B2,B2},{B2}} is set

the ObjectMap of F . [B2,B2] is set

( the ObjectMap of F . (B2,B2)) `1 is set

F . G is M2( the carrier of A2)

the ObjectMap of F . (G,G) is M2([: the carrier of A2, the carrier of A2:])

[G,G] is V15() set

{G,G} is set

{G} is set

{{G,G},{G}} is set

the ObjectMap of F . [G,G] is set

( the ObjectMap of F . (G,G)) `1 is set

<^(F . B2),(F . G)^> is set

the Arrows of A2 is Relation-like [: the carrier of A2, the carrier of A2:] -defined Function-like non empty total set

the Arrows of A2 . ((F . B2),(F . G)) is set

[(F . B2),(F . G)] is V15() set

{(F . B2),(F . G)} is set

{(F . B2)} is set

{{(F . B2),(F . G)},{(F . B2)}} is set

the Arrows of A2 . [(F . B2),(F . G)] is set

B1 . (F . B2) is M2( the carrier of A1)

the ObjectMap of B1 is Relation-like [: the carrier of A2, the carrier of A2:] -defined [: the carrier of A1, the carrier of A1:] -valued Function-like quasi_total M2( bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:])

[:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:] is Relation-like non empty set

bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:] is non empty set

the ObjectMap of B1 . ((F . B2),(F . B2)) is M2([: the carrier of A1, the carrier of A1:])

[(F . B2),(F . B2)] is V15() set

{(F . B2),(F . B2)} is set

{{(F . B2),(F . B2)},{(F . B2)}} is set

the ObjectMap of B1 . [(F . B2),(F . B2)] is set

( the ObjectMap of B1 . ((F . B2),(F . B2))) `1 is set

B1 . (F . G) is M2( the carrier of A1)

the ObjectMap of B1 . ((F . G),(F . G)) is M2([: the carrier of A1, the carrier of A1:])

[(F . G),(F . G)] is V15() set

{(F . G),(F . G)} is set

{(F . G)} is set

{{(F . G),(F . G)},{(F . G)}} is set

the ObjectMap of B1 . [(F . G),(F . G)] is set

( the ObjectMap of B1 . ((F . G),(F . G))) `1 is set

b is M2(<^B2,G^>)

F . b is M2(<^(F . B2),(F . G)^>)

c is M2(<^(F . B2),(F . G)^>)

B1 . c is M2(<^(B1 . (F . B2)),(B1 . (F . G))^>)

<^(B1 . (F . B2)),(B1 . (F . G))^> is set

the Arrows of A1 . ((B1 . (F . B2)),(B1 . (F . G))) is set

[(B1 . (F . B2)),(B1 . (F . G))] is V15() set

{(B1 . (F . B2)),(B1 . (F . G))} is set

{(B1 . (F . B2))} is set

{{(B1 . (F . B2)),(B1 . (F . G))},{(B1 . (F . B2))}} is set

the Arrows of A1 . [(B1 . (F . B2)),(B1 . (F . G))] is set

(F ") * F is strict FunctorStr over A1,A1

id A1 is reflexive feasible strict Covariant id-preserving comp-preserving covariant bijective Functor of A1,A1

B1 * F is reflexive feasible strict Covariant FunctorStr over A1,A1

(B1 * F) . b is M2(<^((B1 * F) . B2),((B1 * F) . G)^>)

(B1 * F) . B2 is M2( the carrier of A1)

the ObjectMap of (B1 * F) is Relation-like [: the carrier of A1, the carrier of A1:] -defined [: the carrier of A1, the carrier of A1:] -valued Function-like quasi_total M2( bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A1, the carrier of A1:]:])

[:[: the carrier of A1, the carrier of A1:],[: the carrier of A1, the carrier of A1:]:] is Relation-like non empty set

bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A1, the carrier of A1:]:] is non empty set

the ObjectMap of (B1 * F) . (B2,B2) is M2([: the carrier of A1, the carrier of A1:])

the ObjectMap of (B1 * F) . [B2,B2] is set

( the ObjectMap of (B1 * F) . (B2,B2)) `1 is set

(B1 * F) . G is M2( the carrier of A1)

the ObjectMap of (B1 * F) . (G,G) is M2([: the carrier of A1, the carrier of A1:])

the ObjectMap of (B1 * F) . [G,G] is set

( the ObjectMap of (B1 * F) . (G,G)) `1 is set

<^((B1 * F) . B2),((B1 * F) . G)^> is set

the Arrows of A1 . (((B1 * F) . B2),((B1 * F) . G)) is set

[((B1 * F) . B2),((B1 * F) . G)] is V15() set

{((B1 * F) . B2),((B1 * F) . G)} is set

{((B1 * F) . B2)} is set

{{((B1 * F) . B2),((B1 * F) . G)},{((B1 * F) . B2)}} is set

the Arrows of A1 . [((B1 * F) . B2),((B1 * F) . G)] is set

F * B1 is reflexive feasible strict Covariant FunctorStr over A2,A2

id A2 is reflexive feasible strict Covariant id-preserving comp-preserving covariant bijective Functor of A2,A2

(F * B1) . c is M2(<^((F * B1) . (F . B2)),((F * B1) . (F . G))^>)

(F * B1) . (F . B2) is M2( the carrier of A2)

the ObjectMap of (F * B1) is Relation-like [: the carrier of A2, the carrier of A2:] -defined [: the carrier of A2, the carrier of A2:] -valued Function-like quasi_total M2( bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A2, the carrier of A2:]:])

[:[: the carrier of A2, the carrier of A2:],[: the carrier of A2, the carrier of A2:]:] is Relation-like non empty set

bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A2, the carrier of A2:]:] is non empty set

the ObjectMap of (F * B1) . ((F . B2),(F . B2)) is M2([: the carrier of A2, the carrier of A2:])

the ObjectMap of (F * B1) . [(F . B2),(F . B2)] is set

( the ObjectMap of (F * B1) . ((F . B2),(F . B2))) `1 is set

(F * B1) . (F . G) is M2( the carrier of A2)

the ObjectMap of (F * B1) . ((F . G),(F . G)) is M2([: the carrier of A2, the carrier of A2:])

the ObjectMap of (F * B1) . [(F . G),(F . G)] is set

( the ObjectMap of (F * B1) . ((F . G),(F . G))) `1 is set

<^((F * B1) . (F . B2)),((F * B1) . (F . G))^> is set

the Arrows of A2 . (((F * B1) . (F . B2)),((F * B1) . (F . G))) is set

[((F * B1) . (F . B2)),((F * B1) . (F . G))] is V15() set

{((F * B1) . (F . B2)),((F * B1) . (F . G))} is set

{((F * B1) . (F . B2))} is set

{{((F * B1) . (F . B2)),((F * B1) . (F . G))},{((F * B1) . (F . B2))}} is set

the Arrows of A2 . [((F * B1) . (F . B2)),((F * B1) . (F . G))] is set

A1 is non empty transitive with_units reflexive AltCatStr

A2 is non empty transitive with_units reflexive AltCatStr

the carrier of A1 is non empty set

F is reflexive feasible Contravariant FunctorStr over A1,A2

F " is strict FunctorStr over A2,A1

B1 is reflexive feasible Contravariant FunctorStr over A2,A1

B2 is M2( the carrier of A1)

G is M2( the carrier of A1)

<^B2,G^> is set

the Arrows of A1 is Relation-like [: the carrier of A1, the carrier of A1:] -defined Function-like non empty total set

[: the carrier of A1, the carrier of A1:] is Relation-like non empty set

the Arrows of A1 . (B2,G) is set

[B2,G] is V15() set

{B2,G} is set

{B2} is set

{{B2,G},{B2}} is set

the Arrows of A1 . [B2,G] is set

F . G is M2( the carrier of A2)

the carrier of A2 is non empty set

[: the carrier of A2, the carrier of A2:] is Relation-like non empty set

the ObjectMap of F is Relation-like [: the carrier of A1, the carrier of A1:] -defined [: the carrier of A2, the carrier of A2:] -valued Function-like quasi_total M2( bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A2, the carrier of A2:]:])

[:[: the carrier of A1, the carrier of A1:],[: the carrier of A2, the carrier of A2:]:] is Relation-like non empty set

bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A2, the carrier of A2:]:] is non empty set

the ObjectMap of F . (G,G) is M2([: the carrier of A2, the carrier of A2:])

[G,G] is V15() set

{G,G} is set

{G} is set

{{G,G},{G}} is set

the ObjectMap of F . [G,G] is set

( the ObjectMap of F . (G,G)) `1 is set

F . B2 is M2( the carrier of A2)

the ObjectMap of F . (B2,B2) is M2([: the carrier of A2, the carrier of A2:])

[B2,B2] is V15() set

{B2,B2} is set

{{B2,B2},{B2}} is set

the ObjectMap of F . [B2,B2] is set

( the ObjectMap of F . (B2,B2)) `1 is set

<^(F . G),(F . B2)^> is set

the Arrows of A2 is Relation-like [: the carrier of A2, the carrier of A2:] -defined Function-like non empty total set

the Arrows of A2 . ((F . G),(F . B2)) is set

[(F . G),(F . B2)] is V15() set

{(F . G),(F . B2)} is set

{(F . G)} is set

{{(F . G),(F . B2)},{(F . G)}} is set

the Arrows of A2 . [(F . G),(F . B2)] is set

B1 . (F . B2) is M2( the carrier of A1)

the ObjectMap of B1 is Relation-like [: the carrier of A2, the carrier of A2:] -defined [: the carrier of A1, the carrier of A1:] -valued Function-like quasi_total M2( bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:])

[:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:] is Relation-like non empty set

bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:] is non empty set

the ObjectMap of B1 . ((F . B2),(F . B2)) is M2([: the carrier of A1, the carrier of A1:])

[(F . B2),(F . B2)] is V15() set

{(F . B2),(F . B2)} is set

{(F . B2)} is set

{{(F . B2),(F . B2)},{(F . B2)}} is set

the ObjectMap of B1 . [(F . B2),(F . B2)] is set

( the ObjectMap of B1 . ((F . B2),(F . B2))) `1 is set

B1 . (F . G) is M2( the carrier of A1)

the ObjectMap of B1 . ((F . G),(F . G)) is M2([: the carrier of A1, the carrier of A1:])

[(F . G),(F . G)] is V15() set

{(F . G),(F . G)} is set

{{(F . G),(F . G)},{(F . G)}} is set

the ObjectMap of B1 . [(F . G),(F . G)] is set

( the ObjectMap of B1 . ((F . G),(F . G))) `1 is set

b is M2(<^B2,G^>)

F . b is M2(<^(F . G),(F . B2)^>)

c is M2(<^(F . G),(F . B2)^>)

B1 . c is M2(<^(B1 . (F . B2)),(B1 . (F . G))^>)

<^(B1 . (F . B2)),(B1 . (F . G))^> is set

the Arrows of A1 . ((B1 . (F . B2)),(B1 . (F . G))) is set

[(B1 . (F . B2)),(B1 . (F . G))] is V15() set

{(B1 . (F . B2)),(B1 . (F . G))} is set

{(B1 . (F . B2))} is set

{{(B1 . (F . B2)),(B1 . (F . G))},{(B1 . (F . B2))}} is set

the Arrows of A1 . [(B1 . (F . B2)),(B1 . (F . G))] is set

(F ") * F is strict FunctorStr over A1,A1

id A1 is reflexive feasible strict Covariant id-preserving comp-preserving covariant bijective Functor of A1,A1

B1 * F is reflexive feasible strict Covariant FunctorStr over A1,A1

(B1 * F) . b is M2(<^((B1 * F) . B2),((B1 * F) . G)^>)

(B1 * F) . B2 is M2( the carrier of A1)

the ObjectMap of (B1 * F) is Relation-like [: the carrier of A1, the carrier of A1:] -defined [: the carrier of A1, the carrier of A1:] -valued Function-like quasi_total M2( bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A1, the carrier of A1:]:])

[:[: the carrier of A1, the carrier of A1:],[: the carrier of A1, the carrier of A1:]:] is Relation-like non empty set

bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A1, the carrier of A1:]:] is non empty set

the ObjectMap of (B1 * F) . (B2,B2) is M2([: the carrier of A1, the carrier of A1:])

the ObjectMap of (B1 * F) . [B2,B2] is set

( the ObjectMap of (B1 * F) . (B2,B2)) `1 is set

(B1 * F) . G is M2( the carrier of A1)

the ObjectMap of (B1 * F) . (G,G) is M2([: the carrier of A1, the carrier of A1:])

the ObjectMap of (B1 * F) . [G,G] is set

( the ObjectMap of (B1 * F) . (G,G)) `1 is set

<^((B1 * F) . B2),((B1 * F) . G)^> is set

the Arrows of A1 . (((B1 * F) . B2),((B1 * F) . G)) is set

[((B1 * F) . B2),((B1 * F) . G)] is V15() set

{((B1 * F) . B2),((B1 * F) . G)} is set

{((B1 * F) . B2)} is set

{{((B1 * F) . B2),((B1 * F) . G)},{((B1 * F) . B2)}} is set

the Arrows of A1 . [((B1 * F) . B2),((B1 * F) . G)] is set

F * B1 is reflexive feasible strict Covariant FunctorStr over A2,A2

id A2 is reflexive feasible strict Covariant id-preserving comp-preserving covariant bijective Functor of A2,A2

(F * B1) . c is M2(<^((F * B1) . (F . G)),((F * B1) . (F . B2))^>)

(F * B1) . (F . G) is M2( the carrier of A2)

the ObjectMap of (F * B1) is Relation-like [: the carrier of A2, the carrier of A2:] -defined [: the carrier of A2, the carrier of A2:] -valued Function-like quasi_total M2( bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A2, the carrier of A2:]:])

[:[: the carrier of A2, the carrier of A2:],[: the carrier of A2, the carrier of A2:]:] is Relation-like non empty set

bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A2, the carrier of A2:]:] is non empty set

the ObjectMap of (F * B1) . ((F . G),(F . G)) is M2([: the carrier of A2, the carrier of A2:])

the ObjectMap of (F * B1) . [(F . G),(F . G)] is set

( the ObjectMap of (F * B1) . ((F . G),(F . G))) `1 is set

(F * B1) . (F . B2) is M2( the carrier of A2)

the ObjectMap of (F * B1) . ((F . B2),(F . B2)) is M2([: the carrier of A2, the carrier of A2:])

the ObjectMap of (F * B1) . [(F . B2),(F . B2)] is set

( the ObjectMap of (F * B1) . ((F . B2),(F . B2))) `1 is set

<^((F * B1) . (F . G)),((F * B1) . (F . B2))^> is set

the Arrows of A2 . (((F * B1) . (F . G)),((F * B1) . (F . B2))) is set

[((F * B1) . (F . G)),((F * B1) . (F . B2))] is V15() set

{((F * B1) . (F . G)),((F * B1) . (F . B2))} is set

{((F * B1) . (F . G))} is set

{{((F * B1) . (F . G)),((F * B1) . (F . B2))},{((F * B1) . (F . G))}} is set

the Arrows of A2 . [((F * B1) . (F . G)),((F * B1) . (F . B2))] is set

A1 is non empty transitive V106() with_units reflexive AltCatStr

A2 is non empty transitive V106() with_units reflexive AltCatStr

id A2 is reflexive feasible strict Covariant id-preserving comp-preserving covariant bijective Functor of A2,A2

F is feasible id-preserving Functor of A1,A2

F " is strict FunctorStr over A2,A1

(F ") * F is strict FunctorStr over A1,A1

id A1 is reflexive feasible strict Covariant id-preserving comp-preserving covariant bijective Functor of A1,A1

B2 is feasible id-preserving Functor of A2,A1

F * B2 is feasible strict FunctorStr over A2,A2

the ObjectMap of B2 is Relation-like [: the carrier of A2, the carrier of A2:] -defined [: the carrier of A1, the carrier of A1:] -valued Function-like quasi_total M2( bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:])

the carrier of A2 is non empty set

[: the carrier of A2, the carrier of A2:] is Relation-like non empty set

the carrier of A1 is non empty set

[: the carrier of A1, the carrier of A1:] is Relation-like non empty set

[:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:] is Relation-like non empty set

bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:] is non empty set

the MorphMap of B2 is Relation-like [: the carrier of A2, the carrier of A2:] -defined Function-like non empty total Function-yielding V37() MSUnTrans of the ObjectMap of B2, the Arrows of A2, the Arrows of A1

the Arrows of A2 is Relation-like [: the carrier of A2, the carrier of A2:] -defined Function-like non empty total set

the Arrows of A1 is Relation-like [: the carrier of A1, the carrier of A1:] -defined Function-like non empty total set

FunctorStr(# the ObjectMap of B2, the MorphMap of B2 #) is strict FunctorStr over A2,A1

(id A1) * B2 is feasible strict FunctorStr over A2,A1

B1 is feasible FunctorStr over A2,A1

B1 * (id A2) is feasible strict FunctorStr over A2,A1

A1 is non empty transitive V106() with_units reflexive AltCatStr

A2 is non empty transitive V106() with_units reflexive AltCatStr

id A1 is reflexive feasible strict Covariant id-preserving comp-preserving covariant bijective Functor of A1,A1

F is feasible id-preserving Functor of A1,A2

F " is strict FunctorStr over A2,A1

B1 is feasible FunctorStr over A2,A1

F * B1 is feasible strict FunctorStr over A2,A2

id A2 is reflexive feasible strict Covariant id-preserving comp-preserving covariant bijective Functor of A2,A2

B2 is feasible id-preserving Functor of A2,A1

B2 * F is feasible strict FunctorStr over A1,A1

the ObjectMap of B2 is Relation-like [: the carrier of A2, the carrier of A2:] -defined [: the carrier of A1, the carrier of A1:] -valued Function-like quasi_total M2( bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:])

the carrier of A2 is non empty set

[: the carrier of A2, the carrier of A2:] is Relation-like non empty set

the carrier of A1 is non empty set

[: the carrier of A1, the carrier of A1:] is Relation-like non empty set

[:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:] is Relation-like non empty set

bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:] is non empty set

the MorphMap of B2 is Relation-like [: the carrier of A2, the carrier of A2:] -defined Function-like non empty total Function-yielding V37() MSUnTrans of the ObjectMap of B2, the Arrows of A2, the Arrows of A1

the Arrows of A2 is Relation-like [: the carrier of A2, the carrier of A2:] -defined Function-like non empty total set

the Arrows of A1 is Relation-like [: the carrier of A1, the carrier of A1:] -defined Function-like non empty total set

FunctorStr(# the ObjectMap of B2, the MorphMap of B2 #) is strict FunctorStr over A2,A1

(id A1) * B1 is feasible strict FunctorStr over A2,A1

B2 * (id A2) is feasible strict id-preserving FunctorStr over A2,A1

A1 is non empty transitive V106() with_units reflexive AltCatStr

A2 is non empty transitive V106() with_units reflexive AltCatStr

the carrier of A2 is non empty set

F is reflexive feasible Covariant id-preserving comp-preserving covariant Functor of A1,A2

F " is strict FunctorStr over A2,A1

B1 is reflexive feasible Covariant id-preserving comp-preserving covariant Functor of A2,A1

the ObjectMap of B1 is Relation-like [: the carrier of A2, the carrier of A2:] -defined [: the carrier of A1, the carrier of A1:] -valued Function-like quasi_total M2( bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:])

[: the carrier of A2, the carrier of A2:] is Relation-like non empty set

the carrier of A1 is non empty set

[: the carrier of A1, the carrier of A1:] is Relation-like non empty set

[:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:] is Relation-like non empty set

bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:] is non empty set

the MorphMap of B1 is Relation-like [: the carrier of A2, the carrier of A2:] -defined Function-like non empty total Function-yielding V37() MSUnTrans of the ObjectMap of B1, the Arrows of A2, the Arrows of A1

the Arrows of A2 is Relation-like [: the carrier of A2, the carrier of A2:] -defined Function-like non empty total set

the Arrows of A1 is Relation-like [: the carrier of A1, the carrier of A1:] -defined Function-like non empty total set

FunctorStr(# the ObjectMap of B1, the MorphMap of B1 #) is strict FunctorStr over A2,A1

B2 is M2( the carrier of A2)

G is M2( the carrier of A2)

<^B2,G^> is set

the Arrows of A2 . (B2,G) is set

[B2,G] is V15() set

{B2,G} is set

{B2} is set

{{B2,G},{B2}} is set

the Arrows of A2 . [B2,G] is set

F * B1 is reflexive feasible strict Covariant id-preserving comp-preserving covariant Functor of A2,A2

b is M2(<^B2,G^>)

(F * B1) . b is M2(<^((F * B1) . B2),((F * B1) . G)^>)

(F * B1) . B2 is M2( the carrier of A2)

the ObjectMap of (F * B1) is Relation-like [: the carrier of A2, the carrier of A2:] -defined [: the carrier of A2, the carrier of A2:] -valued Function-like quasi_total M2( bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A2, the carrier of A2:]:])

[:[: the carrier of A2, the carrier of A2:],[: the carrier of A2, the carrier of A2:]:] is Relation-like non empty set

bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A2, the carrier of A2:]:] is non empty set

the ObjectMap of (F * B1) . (B2,B2) is M2([: the carrier of A2, the carrier of A2:])

[B2,B2] is V15() set

{B2,B2} is set

{{B2,B2},{B2}} is set

the ObjectMap of (F * B1) . [B2,B2] is set

( the ObjectMap of (F * B1) . (B2,B2)) `1 is set

(F * B1) . G is M2( the carrier of A2)

the ObjectMap of (F * B1) . (G,G) is M2([: the carrier of A2, the carrier of A2:])

[G,G] is V15() set

{G,G} is set

{G} is set

{{G,G},{G}} is set

the ObjectMap of (F * B1) . [G,G] is set

( the ObjectMap of (F * B1) . (G,G)) `1 is set

<^((F * B1) . B2),((F * B1) . G)^> is set

the Arrows of A2 . (((F * B1) . B2),((F * B1) . G)) is set

[((F * B1) . B2),((F * B1) . G)] is V15() set

{((F * B1) . B2),((F * B1) . G)} is set

{((F * B1) . B2)} is set

{{((F * B1) . B2),((F * B1) . G)},{((F * B1) . B2)}} is set

the Arrows of A2 . [((F * B1) . B2),((F * B1) . G)] is set

B1 . B2 is M2( the carrier of A1)

the ObjectMap of B1 . (B2,B2) is M2([: the carrier of A1, the carrier of A1:])

the ObjectMap of B1 . [B2,B2] is set

( the ObjectMap of B1 . (B2,B2)) `1 is set

B1 . G is M2( the carrier of A1)

the ObjectMap of B1 . (G,G) is M2([: the carrier of A1, the carrier of A1:])

the ObjectMap of B1 . [G,G] is set

( the ObjectMap of B1 . (G,G)) `1 is set

B1 . b is M2(<^(B1 . B2),(B1 . G)^>)

<^(B1 . B2),(B1 . G)^> is set

the Arrows of A1 . ((B1 . B2),(B1 . G)) is set

[(B1 . B2),(B1 . G)] is V15() set

{(B1 . B2),(B1 . G)} is set

{(B1 . B2)} is set

{{(B1 . B2),(B1 . G)},{(B1 . B2)}} is set

the Arrows of A1 . [(B1 . B2),(B1 . G)] is set

F . (B1 . b) is M2(<^(F . (B1 . B2)),(F . (B1 . G))^>)

F . (B1 . B2) is M2( the carrier of A2)

the ObjectMap of F is Relation-like [: the carrier of A1, the carrier of A1:] -defined [: the carrier of A2, the carrier of A2:] -valued Function-like quasi_total M2( bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A2, the carrier of A2:]:])

[:[: the carrier of A1, the carrier of A1:],[: the carrier of A2, the carrier of A2:]:] is Relation-like non empty set

bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A2, the carrier of A2:]:] is non empty set

the ObjectMap of F . ((B1 . B2),(B1 . B2)) is M2([: the carrier of A2, the carrier of A2:])

[(B1 . B2),(B1 . B2)] is V15() set

{(B1 . B2),(B1 . B2)} is set

{{(B1 . B2),(B1 . B2)},{(B1 . B2)}} is set

the ObjectMap of F . [(B1 . B2),(B1 . B2)] is set

( the ObjectMap of F . ((B1 . B2),(B1 . B2))) `1 is set

F . (B1 . G) is M2( the carrier of A2)

the ObjectMap of F . ((B1 . G),(B1 . G)) is M2([: the carrier of A2, the carrier of A2:])

[(B1 . G),(B1 . G)] is V15() set

{(B1 . G),(B1 . G)} is set

{(B1 . G)} is set

{{(B1 . G),(B1 . G)},{(B1 . G)}} is set

the ObjectMap of F . [(B1 . G),(B1 . G)] is set

( the ObjectMap of F . ((B1 . G),(B1 . G))) `1 is set

<^(F . (B1 . B2)),(F . (B1 . G))^> is set

the Arrows of A2 . ((F . (B1 . B2)),(F . (B1 . G))) is set

[(F . (B1 . B2)),(F . (B1 . G))] is V15() set

{(F . (B1 . B2)),(F . (B1 . G))} is set

{(F . (B1 . B2))} is set

{{(F . (B1 . B2)),(F . (B1 . G))},{(F . (B1 . B2))}} is set

the Arrows of A2 . [(F . (B1 . B2)),(F . (B1 . G))] is set

id A2 is reflexive feasible strict Covariant id-preserving comp-preserving covariant bijective Functor of A2,A2

(id A2) . b is M2(<^((id A2) . B2),((id A2) . G)^>)

(id A2) . B2 is M2( the carrier of A2)

the ObjectMap of (id A2) is Relation-like [: the carrier of A2, the carrier of A2:] -defined [: the carrier of A2, the carrier of A2:] -valued Function-like quasi_total M2( bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A2, the carrier of A2:]:])

the ObjectMap of (id A2) . (B2,B2) is M2([: the carrier of A2, the carrier of A2:])

the ObjectMap of (id A2) . [B2,B2] is set

( the ObjectMap of (id A2) . (B2,B2)) `1 is set

(id A2) . G is M2( the carrier of A2)

the ObjectMap of (id A2) . (G,G) is M2([: the carrier of A2, the carrier of A2:])

the ObjectMap of (id A2) . [G,G] is set

( the ObjectMap of (id A2) . (G,G)) `1 is set

<^((id A2) . B2),((id A2) . G)^> is set

the Arrows of A2 . (((id A2) . B2),((id A2) . G)) is set

[((id A2) . B2),((id A2) . G)] is V15() set

{((id A2) . B2),((id A2) . G)} is set

{((id A2) . B2)} is set

{{((id A2) . B2),((id A2) . G)},{((id A2) . B2)}} is set

the Arrows of A2 . [((id A2) . B2),((id A2) . G)] is set

B2 is M2( the carrier of A2)

(F * B1) . B2 is M2( the carrier of A2)

the ObjectMap of (F * B1) . (B2,B2) is M2([: the carrier of A2, the carrier of A2:])

[B2,B2] is V15() set

{B2,B2} is set

{B2} is set

{{B2,B2},{B2}} is set

the ObjectMap of (F * B1) . [B2,B2] is set

( the ObjectMap of (F * B1) . (B2,B2)) `1 is set

B1 . B2 is M2( the carrier of A1)

the ObjectMap of B1 . (B2,B2) is M2([: the carrier of A1, the carrier of A1:])

the ObjectMap of B1 . [B2,B2] is set

( the ObjectMap of B1 . (B2,B2)) `1 is set

F . (B1 . B2) is M2( the carrier of A2)

the ObjectMap of F . ((B1 . B2),(B1 . B2)) is M2([: the carrier of A2, the carrier of A2:])

[(B1 . B2),(B1 . B2)] is V15() set

{(B1 . B2),(B1 . B2)} is set

{(B1 . B2)} is set

{{(B1 . B2),(B1 . B2)},{(B1 . B2)}} is set

the ObjectMap of F . [(B1 . B2),(B1 . B2)] is set

( the ObjectMap of F . ((B1 . B2),(B1 . B2))) `1 is set

(id A2) . B2 is M2( the carrier of A2)

the ObjectMap of (id A2) . (B2,B2) is M2([: the carrier of A2, the carrier of A2:])

the ObjectMap of (id A2) . [B2,B2] is set

( the ObjectMap of (id A2) . (B2,B2)) `1 is set

A1 is non empty transitive V106() with_units reflexive AltCatStr

A2 is non empty transitive V106() with_units reflexive AltCatStr

the carrier of A2 is non empty set

F is reflexive feasible Contravariant id-preserving comp-reversing contravariant Functor of A1,A2

F " is strict FunctorStr over A2,A1

B1 is reflexive feasible Contravariant id-preserving comp-reversing contravariant Functor of A2,A1

the ObjectMap of B1 is Relation-like [: the carrier of A2, the carrier of A2:] -defined [: the carrier of A1, the carrier of A1:] -valued Function-like quasi_total M2( bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:])

[: the carrier of A2, the carrier of A2:] is Relation-like non empty set

the carrier of A1 is non empty set

[: the carrier of A1, the carrier of A1:] is Relation-like non empty set

[:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:] is Relation-like non empty set

bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:] is non empty set

the MorphMap of B1 is Relation-like [: the carrier of A2, the carrier of A2:] -defined Function-like non empty total Function-yielding V37() MSUnTrans of the ObjectMap of B1, the Arrows of A2, the Arrows of A1

the Arrows of A2 is Relation-like [: the carrier of A2, the carrier of A2:] -defined Function-like non empty total set

the Arrows of A1 is Relation-like [: the carrier of A1, the carrier of A1:] -defined Function-like non empty total set

FunctorStr(# the ObjectMap of B1, the MorphMap of B1 #) is strict FunctorStr over A2,A1

B2 is M2( the carrier of A2)

G is M2( the carrier of A2)

<^B2,G^> is set

the Arrows of A2 . (B2,G) is set

[B2,G] is V15() set

{B2,G} is set

{B2} is set

{{B2,G},{B2}} is set

the Arrows of A2 . [B2,G] is set

F * B1 is reflexive feasible strict Covariant id-preserving comp-preserving covariant Functor of A2,A2

b is M2(<^B2,G^>)

(F * B1) . b is M2(<^((F * B1) . B2),((F * B1) . G)^>)

(F * B1) . B2 is M2( the carrier of A2)

the ObjectMap of (F * B1) is Relation-like [: the carrier of A2, the carrier of A2:] -defined [: the carrier of A2, the carrier of A2:] -valued Function-like quasi_total M2( bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A2, the carrier of A2:]:])

[:[: the carrier of A2, the carrier of A2:],[: the carrier of A2, the carrier of A2:]:] is Relation-like non empty set

bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A2, the carrier of A2:]:] is non empty set

the ObjectMap of (F * B1) . (B2,B2) is M2([: the carrier of A2, the carrier of A2:])

[B2,B2] is V15() set

{B2,B2} is set

{{B2,B2},{B2}} is set

the ObjectMap of (F * B1) . [B2,B2] is set

( the ObjectMap of (F * B1) . (B2,B2)) `1 is set

(F * B1) . G is M2( the carrier of A2)

the ObjectMap of (F * B1) . (G,G) is M2([: the carrier of A2, the carrier of A2:])

[G,G] is V15() set

{G,G} is set

{G} is set

{{G,G},{G}} is set

the ObjectMap of (F * B1) . [G,G] is set

( the ObjectMap of (F * B1) . (G,G)) `1 is set

<^((F * B1) . B2),((F * B1) . G)^> is set

the Arrows of A2 . (((F * B1) . B2),((F * B1) . G)) is set

[((F * B1) . B2),((F * B1) . G)] is V15() set

{((F * B1) . B2),((F * B1) . G)} is set

{((F * B1) . B2)} is set

{{((F * B1) . B2),((F * B1) . G)},{((F * B1) . B2)}} is set

the Arrows of A2 . [((F * B1) . B2),((F * B1) . G)] is set

B1 . G is M2( the carrier of A1)

the ObjectMap of B1 . (G,G) is M2([: the carrier of A1, the carrier of A1:])

the ObjectMap of B1 . [G,G] is set

( the ObjectMap of B1 . (G,G)) `1 is set

B1 . B2 is M2( the carrier of A1)

the ObjectMap of B1 . (B2,B2) is M2([: the carrier of A1, the carrier of A1:])

the ObjectMap of B1 . [B2,B2] is set

( the ObjectMap of B1 . (B2,B2)) `1 is set

B1 . b is M2(<^(B1 . G),(B1 . B2)^>)

<^(B1 . G),(B1 . B2)^> is set

the Arrows of A1 . ((B1 . G),(B1 . B2)) is set

[(B1 . G),(B1 . B2)] is V15() set

{(B1 . G),(B1 . B2)} is set

{(B1 . G)} is set

{{(B1 . G),(B1 . B2)},{(B1 . G)}} is set

the Arrows of A1 . [(B1 . G),(B1 . B2)] is set

F . (B1 . b) is M2(<^(F . (B1 . B2)),(F . (B1 . G))^>)

F . (B1 . B2) is M2( the carrier of A2)

the ObjectMap of F is Relation-like [: the carrier of A1, the carrier of A1:] -defined [: the carrier of A2, the carrier of A2:] -valued Function-like quasi_total M2( bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A2, the carrier of A2:]:])

[:[: the carrier of A1, the carrier of A1:],[: the carrier of A2, the carrier of A2:]:] is Relation-like non empty set

bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A2, the carrier of A2:]:] is non empty set

the ObjectMap of F . ((B1 . B2),(B1 . B2)) is M2([: the carrier of A2, the carrier of A2:])

[(B1 . B2),(B1 . B2)] is V15() set

{(B1 . B2),(B1 . B2)} is set

{(B1 . B2)} is set

{{(B1 . B2),(B1 . B2)},{(B1 . B2)}} is set

the ObjectMap of F . [(B1 . B2),(B1 . B2)] is set

( the ObjectMap of F . ((B1 . B2),(B1 . B2))) `1 is set

F . (B1 . G) is M2( the carrier of A2)

the ObjectMap of F . ((B1 . G),(B1 . G)) is M2([: the carrier of A2, the carrier of A2:])

[(B1 . G),(B1 . G)] is V15() set

{(B1 . G),(B1 . G)} is set

{{(B1 . G),(B1 . G)},{(B1 . G)}} is set

the ObjectMap of F . [(B1 . G),(B1 . G)] is set

( the ObjectMap of F . ((B1 . G),(B1 . G))) `1 is set

<^(F . (B1 . B2)),(F . (B1 . G))^> is set

the Arrows of A2 . ((F . (B1 . B2)),(F . (B1 . G))) is set

[(F . (B1 . B2)),(F . (B1 . G))] is V15() set

{(F . (B1 . B2)),(F . (B1 . G))} is set

{(F . (B1 . B2))} is set

{{(F . (B1 . B2)),(F . (B1 . G))},{(F . (B1 . B2))}} is set

the Arrows of A2 . [(F . (B1 . B2)),(F . (B1 . G))] is set

id A2 is reflexive feasible strict Covariant id-preserving comp-preserving covariant bijective Functor of A2,A2

(id A2) . b is M2(<^((id A2) . B2),((id A2) . G)^>)

(id A2) . B2 is M2( the carrier of A2)

the ObjectMap of (id A2) is Relation-like [: the carrier of A2, the carrier of A2:] -defined [: the carrier of A2, the carrier of A2:] -valued Function-like quasi_total M2( bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A2, the carrier of A2:]:])

the ObjectMap of (id A2) . (B2,B2) is M2([: the carrier of A2, the carrier of A2:])

the ObjectMap of (id A2) . [B2,B2] is set

( the ObjectMap of (id A2) . (B2,B2)) `1 is set

(id A2) . G is M2( the carrier of A2)

the ObjectMap of (id A2) . (G,G) is M2([: the carrier of A2, the carrier of A2:])

the ObjectMap of (id A2) . [G,G] is set

( the ObjectMap of (id A2) . (G,G)) `1 is set

<^((id A2) . B2),((id A2) . G)^> is set

the Arrows of A2 . (((id A2) . B2),((id A2) . G)) is set

[((id A2) . B2),((id A2) . G)] is V15() set

{((id A2) . B2),((id A2) . G)} is set

{((id A2) . B2)} is set

{{((id A2) . B2),((id A2) . G)},{((id A2) . B2)}} is set

the Arrows of A2 . [((id A2) . B2),((id A2) . G)] is set

B2 is M2( the carrier of A2)

(F * B1) . B2 is M2( the carrier of A2)

the ObjectMap of (F * B1) . (B2,B2) is M2([: the carrier of A2, the carrier of A2:])

[B2,B2] is V15() set

{B2,B2} is set

{B2} is set

{{B2,B2},{B2}} is set

the ObjectMap of (F * B1) . [B2,B2] is set

( the ObjectMap of (F * B1) . (B2,B2)) `1 is set

B1 . B2 is M2( the carrier of A1)

the ObjectMap of B1 . (B2,B2) is M2([: the carrier of A1, the carrier of A1:])

the ObjectMap of B1 . [B2,B2] is set

( the ObjectMap of B1 . (B2,B2)) `1 is set

F . (B1 . B2) is M2( the carrier of A2)

the ObjectMap of F . ((B1 . B2),(B1 . B2)) is M2([: the carrier of A2, the carrier of A2:])

[(B1 . B2),(B1 . B2)] is V15() set

{(B1 . B2),(B1 . B2)} is set

{(B1 . B2)} is set

{{(B1 . B2),(B1 . B2)},{(B1 . B2)}} is set

the ObjectMap of F . [(B1 . B2),(B1 . B2)] is set

( the ObjectMap of F . ((B1 . B2),(B1 . B2))) `1 is set

(id A2) . B2 is M2( the carrier of A2)

the ObjectMap of (id A2) . (B2,B2) is M2([: the carrier of A2, the carrier of A2:])

the ObjectMap of (id A2) . [B2,B2] is set

( the ObjectMap of (id A2) . (B2,B2)) `1 is set

A1 is non empty transitive V106() with_units reflexive AltCatStr

A2 is non empty transitive V106() with_units reflexive AltCatStr

the carrier of A1 is non empty set

F is reflexive feasible Covariant id-preserving comp-preserving covariant Functor of A1,A2

F " is strict FunctorStr over A2,A1

B1 is reflexive feasible Covariant id-preserving comp-preserving covariant Functor of A2,A1

the ObjectMap of B1 is Relation-like [: the carrier of A2, the carrier of A2:] -defined [: the carrier of A1, the carrier of A1:] -valued Function-like quasi_total M2( bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:])

the carrier of A2 is non empty set

[: the carrier of A2, the carrier of A2:] is Relation-like non empty set

[: the carrier of A1, the carrier of A1:] is Relation-like non empty set

[:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:] is Relation-like non empty set

bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:] is non empty set

the MorphMap of B1 is Relation-like [: the carrier of A2, the carrier of A2:] -defined Function-like non empty total Function-yielding V37() MSUnTrans of the ObjectMap of B1, the Arrows of A2, the Arrows of A1

the Arrows of A2 is Relation-like [: the carrier of A2, the carrier of A2:] -defined Function-like non empty total set

the Arrows of A1 is Relation-like [: the carrier of A1, the carrier of A1:] -defined Function-like non empty total set

FunctorStr(# the ObjectMap of B1, the MorphMap of B1 #) is strict FunctorStr over A2,A1

B2 is M2( the carrier of A1)

G is M2( the carrier of A1)

<^B2,G^> is set

the Arrows of A1 . (B2,G) is set

[B2,G] is V15() set

{B2,G} is set

{B2} is set

{{B2,G},{B2}} is set

the Arrows of A1 . [B2,G] is set

B1 * F is reflexive feasible strict Covariant id-preserving comp-preserving covariant Functor of A1,A1

b is M2(<^B2,G^>)

(B1 * F) . b is M2(<^((B1 * F) . B2),((B1 * F) . G)^>)

(B1 * F) . B2 is M2( the carrier of A1)

the ObjectMap of (B1 * F) is Relation-like [: the carrier of A1, the carrier of A1:] -defined [: the carrier of A1, the carrier of A1:] -valued Function-like quasi_total M2( bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A1, the carrier of A1:]:])

[:[: the carrier of A1, the carrier of A1:],[: the carrier of A1, the carrier of A1:]:] is Relation-like non empty set

bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A1, the carrier of A1:]:] is non empty set

the ObjectMap of (B1 * F) . (B2,B2) is M2([: the carrier of A1, the carrier of A1:])

[B2,B2] is V15() set

{B2,B2} is set

{{B2,B2},{B2}} is set

the ObjectMap of (B1 * F) . [B2,B2] is set

( the ObjectMap of (B1 * F) . (B2,B2)) `1 is set

(B1 * F) . G is M2( the carrier of A1)

the ObjectMap of (B1 * F) . (G,G) is M2([: the carrier of A1, the carrier of A1:])

[G,G] is V15() set

{G,G} is set

{G} is set

{{G,G},{G}} is set

the ObjectMap of (B1 * F) . [G,G] is set

( the ObjectMap of (B1 * F) . (G,G)) `1 is set

<^((B1 * F) . B2),((B1 * F) . G)^> is set

the Arrows of A1 . (((B1 * F) . B2),((B1 * F) . G)) is set

[((B1 * F) . B2),((B1 * F) . G)] is V15() set

{((B1 * F) . B2),((B1 * F) . G)} is set

{((B1 * F) . B2)} is set

{{((B1 * F) . B2),((B1 * F) . G)},{((B1 * F) . B2)}} is set

the Arrows of A1 . [((B1 * F) . B2),((B1 * F) . G)] is set

F . B2 is M2( the carrier of A2)

the ObjectMap of F is Relation-like [: the carrier of A1, the carrier of A1:] -defined [: the carrier of A2, the carrier of A2:] -valued Function-like quasi_total M2( bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A2, the carrier of A2:]:])

[:[: the carrier of A1, the carrier of A1:],[: the carrier of A2, the carrier of A2:]:] is Relation-like non empty set

bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A2, the carrier of A2:]:] is non empty set

the ObjectMap of F . (B2,B2) is M2([: the carrier of A2, the carrier of A2:])

the ObjectMap of F . [B2,B2] is set

( the ObjectMap of F . (B2,B2)) `1 is set

F . G is M2( the carrier of A2)

the ObjectMap of F . (G,G) is M2([: the carrier of A2, the carrier of A2:])

the ObjectMap of F . [G,G] is set

( the ObjectMap of F . (G,G)) `1 is set

F . b is M2(<^(F . B2),(F . G)^>)

<^(F . B2),(F . G)^> is set

the Arrows of A2 . ((F . B2),(F . G)) is set

[(F . B2),(F . G)] is V15() set

{(F . B2),(F . G)} is set

{(F . B2)} is set

{{(F . B2),(F . G)},{(F . B2)}} is set

the Arrows of A2 . [(F . B2),(F . G)] is set

B1 . (F . b) is M2(<^(B1 . (F . B2)),(B1 . (F . G))^>)

B1 . (F . B2) is M2( the carrier of A1)

the ObjectMap of B1 . ((F . B2),(F . B2)) is M2([: the carrier of A1, the carrier of A1:])

[(F . B2),(F . B2)] is V15() set

{(F . B2),(F . B2)} is set

{{(F . B2),(F . B2)},{(F . B2)}} is set

the ObjectMap of B1 . [(F . B2),(F . B2)] is set

( the ObjectMap of B1 . ((F . B2),(F . B2))) `1 is set

B1 . (F . G) is M2( the carrier of A1)

the ObjectMap of B1 . ((F . G),(F . G)) is M2([: the carrier of A1, the carrier of A1:])

[(F . G),(F . G)] is V15() set

{(F . G),(F . G)} is set

{(F . G)} is set

{{(F . G),(F . G)},{(F . G)}} is set

the ObjectMap of B1 . [(F . G),(F . G)] is set

( the ObjectMap of B1 . ((F . G),(F . G))) `1 is set

<^(B1 . (F . B2)),(B1 . (F . G))^> is set

the Arrows of A1 . ((B1 . (F . B2)),(B1 . (F . G))) is set

[(B1 . (F . B2)),(B1 . (F . G))] is V15() set

{(B1 . (F . B2)),(B1 . (F . G))} is set

{(B1 . (F . B2))} is set

{{(B1 . (F . B2)),(B1 . (F . G))},{(B1 . (F . B2))}} is set

the Arrows of A1 . [(B1 . (F . B2)),(B1 . (F . G))] is set

id A1 is reflexive feasible strict Covariant id-preserving comp-preserving covariant bijective Functor of A1,A1

(id A1) . b is M2(<^((id A1) . B2),((id A1) . G)^>)

(id A1) . B2 is M2( the carrier of A1)

the ObjectMap of (id A1) is Relation-like [: the carrier of A1, the carrier of A1:] -defined [: the carrier of A1, the carrier of A1:] -valued Function-like quasi_total M2( bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A1, the carrier of A1:]:])

the ObjectMap of (id A1) . (B2,B2) is M2([: the carrier of A1, the carrier of A1:])

the ObjectMap of (id A1) . [B2,B2] is set

( the ObjectMap of (id A1) . (B2,B2)) `1 is set

(id A1) . G is M2( the carrier of A1)

the ObjectMap of (id A1) . (G,G) is M2([: the carrier of A1, the carrier of A1:])

the ObjectMap of (id A1) . [G,G] is set

( the ObjectMap of (id A1) . (G,G)) `1 is set

<^((id A1) . B2),((id A1) . G)^> is set

the Arrows of A1 . (((id A1) . B2),((id A1) . G)) is set

[((id A1) . B2),((id A1) . G)] is V15() set

{((id A1) . B2),((id A1) . G)} is set

{((id A1) . B2)} is set

{{((id A1) . B2),((id A1) . G)},{((id A1) . B2)}} is set

the Arrows of A1 . [((id A1) . B2),((id A1) . G)] is set

B2 is M2( the carrier of A1)

(B1 * F) . B2 is M2( the carrier of A1)

the ObjectMap of (B1 * F) . (B2,B2) is M2([: the carrier of A1, the carrier of A1:])

[B2,B2] is V15() set

{B2,B2} is set

{B2} is set

{{B2,B2},{B2}} is set

the ObjectMap of (B1 * F) . [B2,B2] is set

( the ObjectMap of (B1 * F) . (B2,B2)) `1 is set

F . B2 is M2( the carrier of A2)

the ObjectMap of F . (B2,B2) is M2([: the carrier of A2, the carrier of A2:])

the ObjectMap of F . [B2,B2] is set

( the ObjectMap of F . (B2,B2)) `1 is set

B1 . (F . B2) is M2( the carrier of A1)

the ObjectMap of B1 . ((F . B2),(F . B2)) is M2([: the carrier of A1, the carrier of A1:])

[(F . B2),(F . B2)] is V15() set

{(F . B2),(F . B2)} is set

{(F . B2)} is set

{{(F . B2),(F . B2)},{(F . B2)}} is set

the ObjectMap of B1 . [(F . B2),(F . B2)] is set

( the ObjectMap of B1 . ((F . B2),(F . B2))) `1 is set

(id A1) . B2 is M2( the carrier of A1)

the ObjectMap of (id A1) . (B2,B2) is M2([: the carrier of A1, the carrier of A1:])

the ObjectMap of (id A1) . [B2,B2] is set

( the ObjectMap of (id A1) . (B2,B2)) `1 is set

A1 is non empty transitive V106() with_units reflexive AltCatStr

A2 is non empty transitive V106() with_units reflexive AltCatStr

the carrier of A1 is non empty set

F is reflexive feasible Contravariant id-preserving comp-reversing contravariant Functor of A1,A2

F " is strict FunctorStr over A2,A1

B1 is reflexive feasible Contravariant id-preserving comp-reversing contravariant Functor of A2,A1

the ObjectMap of B1 is Relation-like [: the carrier of A2, the carrier of A2:] -defined [: the carrier of A1, the carrier of A1:] -valued Function-like quasi_total M2( bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:])

the carrier of A2 is non empty set

[: the carrier of A2, the carrier of A2:] is Relation-like non empty set

[: the carrier of A1, the carrier of A1:] is Relation-like non empty set

[:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:] is Relation-like non empty set

bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:] is non empty set

the MorphMap of B1 is Relation-like [: the carrier of A2, the carrier of A2:] -defined Function-like non empty total Function-yielding V37() MSUnTrans of the ObjectMap of B1, the Arrows of A2, the Arrows of A1

the Arrows of A2 is Relation-like [: the carrier of A2, the carrier of A2:] -defined Function-like non empty total set

the Arrows of A1 is Relation-like [: the carrier of A1, the carrier of A1:] -defined Function-like non empty total set

FunctorStr(# the ObjectMap of B1, the MorphMap of B1 #) is strict FunctorStr over A2,A1

B2 is M2( the carrier of A1)

G is M2( the carrier of A1)

<^B2,G^> is set

the Arrows of A1 . (B2,G) is set

[B2,G] is V15() set

{B2,G} is set

{B2} is set

{{B2,G},{B2}} is set

the Arrows of A1 . [B2,G] is set

B1 * F is reflexive feasible strict Covariant id-preserving comp-preserving covariant Functor of A1,A1

b is M2(<^B2,G^>)

(B1 * F) . b is M2(<^((B1 * F) . B2),((B1 * F) . G)^>)

(B1 * F) . B2 is M2( the carrier of A1)

the ObjectMap of (B1 * F) is Relation-like [: the carrier of A1, the carrier of A1:] -defined [: the carrier of A1, the carrier of A1:] -valued Function-like quasi_total M2( bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A1, the carrier of A1:]:])

[:[: the carrier of A1, the carrier of A1:],[: the carrier of A1, the carrier of A1:]:] is Relation-like non empty set

bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A1, the carrier of A1:]:] is non empty set

the ObjectMap of (B1 * F) . (B2,B2) is M2([: the carrier of A1, the carrier of A1:])

[B2,B2] is V15() set

{B2,B2} is set

{{B2,B2},{B2}} is set

the ObjectMap of (B1 * F) . [B2,B2] is set

( the ObjectMap of (B1 * F) . (B2,B2)) `1 is set

(B1 * F) . G is M2( the carrier of A1)

the ObjectMap of (B1 * F) . (G,G) is M2([: the carrier of A1, the carrier of A1:])

[G,G] is V15() set

{G,G} is set

{G} is set

{{G,G},{G}} is set

the ObjectMap of (B1 * F) . [G,G] is set

( the ObjectMap of (B1 * F) . (G,G)) `1 is set

<^((B1 * F) . B2),((B1 * F) . G)^> is set

the Arrows of A1 . (((B1 * F) . B2),((B1 * F) . G)) is set

[((B1 * F) . B2),((B1 * F) . G)] is V15() set

{((B1 * F) . B2),((B1 * F) . G)} is set

{((B1 * F) . B2)} is set

{{((B1 * F) . B2),((B1 * F) . G)},{((B1 * F) . B2)}} is set

the Arrows of A1 . [((B1 * F) . B2),((B1 * F) . G)] is set

F . G is M2( the carrier of A2)

the ObjectMap of F is Relation-like [: the carrier of A1, the carrier of A1:] -defined [: the carrier of A2, the carrier of A2:] -valued Function-like quasi_total M2( bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A2, the carrier of A2:]:])

[:[: the carrier of A1, the carrier of A1:],[: the carrier of A2, the carrier of A2:]:] is Relation-like non empty set

bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A2, the carrier of A2:]:] is non empty set

the ObjectMap of F . (G,G) is M2([: the carrier of A2, the carrier of A2:])

the ObjectMap of F . [G,G] is set

( the ObjectMap of F . (G,G)) `1 is set

F . B2 is M2( the carrier of A2)

the ObjectMap of F . (B2,B2) is M2([: the carrier of A2, the carrier of A2:])

the ObjectMap of F . [B2,B2] is set

( the ObjectMap of F . (B2,B2)) `1 is set

F . b is M2(<^(F . G),(F . B2)^>)

<^(F . G),(F . B2)^> is set

the Arrows of A2 . ((F . G),(F . B2)) is set

[(F . G),(F . B2)] is V15() set

{(F . G),(F . B2)} is set

{(F . G)} is set

{{(F . G),(F . B2)},{(F . G)}} is set

the Arrows of A2 . [(F . G),(F . B2)] is set

B1 . (F . b) is M2(<^(B1 . (F . B2)),(B1 . (F . G))^>)

B1 . (F . B2) is M2( the carrier of A1)

the ObjectMap of B1 . ((F . B2),(F . B2)) is M2([: the carrier of A1, the carrier of A1:])

[(F . B2),(F . B2)] is V15() set

{(F . B2),(F . B2)} is set

{(F . B2)} is set

{{(F . B2),(F . B2)},{(F . B2)}} is set

the ObjectMap of B1 . [(F . B2),(F . B2)] is set

( the ObjectMap of B1 . ((F . B2),(F . B2))) `1 is set

B1 . (F . G) is M2( the carrier of A1)

the ObjectMap of B1 . ((F . G),(F . G)) is M2([: the carrier of A1, the carrier of A1:])

[(F . G),(F . G)] is V15() set

{(F . G),(F . G)} is set

{{(F . G),(F . G)},{(F . G)}} is set

the ObjectMap of B1 . [(F . G),(F . G)] is set

( the ObjectMap of B1 . ((F . G),(F . G))) `1 is set

<^(B1 . (F . B2)),(B1 . (F . G))^> is set

the Arrows of A1 . ((B1 . (F . B2)),(B1 . (F . G))) is set

[(B1 . (F . B2)),(B1 . (F . G))] is V15() set

{(B1 . (F . B2)),(B1 . (F . G))} is set

{(B1 . (F . B2))} is set

{{(B1 . (F . B2)),(B1 . (F . G))},{(B1 . (F . B2))}} is set

the Arrows of A1 . [(B1 . (F . B2)),(B1 . (F . G))] is set

id A1 is reflexive feasible strict Covariant id-preserving comp-preserving covariant bijective Functor of A1,A1

(id A1) . b is M2(<^((id A1) . B2),((id A1) . G)^>)

(id A1) . B2 is M2( the carrier of A1)

the ObjectMap of (id A1) is Relation-like [: the