:: FUNCTOR3 semantic presentation

K125() is M2( bool K121())

K121() is set

bool K121() is non empty set

K87() is set

bool K87() is non empty set

bool K125() is non empty 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 non empty set

the non empty transitive strict associative with_units reflexive AltCatStr is non empty transitive strict associative with_units reflexive AltCatStr

A is non empty transitive AltCatStr

B is non empty with_units reflexive AltCatStr

the carrier of B is non empty set

the M2( the carrier of B) is M2( the carrier of B)

idm the M2( the carrier of B) is retraction coretraction mono epi M2(<^ the M2( the carrier of B), the M2( the carrier of B)^>)

<^ the M2( the carrier of B), the M2( the carrier of B)^> is non empty set

A --> (idm the M2( the carrier of B)) is reflexive feasible strict Covariant Contravariant comp-preserving comp-reversing FunctorStr over A,B

A is non empty transitive with_units reflexive AltCatStr

B is non empty with_units reflexive AltCatStr

the carrier of B is non empty set

the M2( the carrier of B) is M2( the carrier of B)

idm the M2( the carrier of B) is retraction coretraction mono epi M2(<^ the M2( the carrier of B), the M2( the carrier of B)^>)

<^ the M2( the carrier of B), the M2( the carrier of B)^> is non empty set

A --> (idm the M2( the carrier of B)) is reflexive feasible strict Covariant Contravariant id-preserving comp-preserving comp-reversing FunctorStr over A,B

A is non empty transitive with_units reflexive AltCatStr

B is non empty with_units reflexive AltCatStr

the carrier of B is non empty set

the M2( the carrier of B) is M2( the carrier of B)

idm the M2( the carrier of B) is retraction coretraction mono epi M2(<^ the M2( the carrier of B), the M2( the carrier of B)^>)

<^ the M2( the carrier of B), the M2( the carrier of B)^> is non empty set

A --> (idm the M2( the carrier of B)) is reflexive feasible strict Covariant Contravariant id-preserving comp-preserving comp-reversing FunctorStr over A,B

F2 is feasible id-preserving Functor of A,B

A is non empty transitive associative with_units reflexive AltCatStr

the carrier of A is non empty set

B is M2( the carrier of A)

F1 is M2( the carrier of A)

<^B,F1^> is set

a is M2( the carrier of A)

<^F1,a^> is set

F2 is M2( the carrier of A)

<^B,F2^> is set

<^F2,a^> is set

idm F1 is retraction coretraction iso mono epi M2(<^F1,F1^>)

<^F1,F1^> is non empty set

idm F2 is retraction coretraction iso mono epi M2(<^F2,F2^>)

<^F2,F2^> is non empty set

<^F1,B^> is set

<^a,F2^> is set

e is M2(<^B,F1^>)

e " is M2(<^F1,B^>)

e * (e ") is M2(<^F1,F1^>)

e1 is M2(<^F1,a^>)

e1 * e is M2(<^B,a^>)

<^B,a^> is set

k is M2(<^B,F2^>)

k * (e ") is M2(<^F1,F2^>)

<^F1,F2^> is set

a is M2(<^F2,a^>)

a * k is M2(<^B,a^>)

a " is M2(<^a,F2^>)

(a ") * a is M2(<^F2,F2^>)

(a ") * e1 is M2(<^F1,F2^>)

e1 * (idm F1) is M2(<^F1,a^>)

(e1 * e) * (e ") is M2(<^F1,a^>)

a * (k * (e ")) is M2(<^F1,a^>)

(a ") * (a * (k * (e "))) is M2(<^F1,F2^>)

((a ") * a) * (k * (e ")) is M2(<^F1,F2^>)

A is non empty transitive AltCatStr

the carrier of A is non empty set

B is non empty with_units reflexive AltCatStr

F1 is non empty with_units reflexive AltCatStr

a is reflexive feasible Covariant FunctorStr over A,B

F2 is FunctorStr over B,F1

F2 * a is strict FunctorStr over A,F1

e is M2( the carrier of A)

e1 is M2( the carrier of A)

Morph-Map ((F2 * a),e,e1) is Relation-like Function-like set

the MorphMap of (F2 * 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:]) Function-yielding V37() MSUnTrans of the ObjectMap of (F2 * a), the Arrows of A, the Arrows of F1

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

the carrier of F1 is non empty set

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

the ObjectMap of (F2 * a) is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of F1, the carrier of F1:] -valued Function-like non empty V14([: the carrier of A, the carrier of A:]) V18([: the carrier of A, the carrier of A:],[: the carrier of F1, the carrier of F1:]) M2( bool [:[: the carrier of A, the carrier of A:],[: the carrier of F1, the carrier of F1:]:])

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

bool [:[: the carrier of A, the carrier of A:],[: the carrier of F1, the carrier of F1:]:] 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 F1 is Relation-like [: the carrier of F1, the carrier of F1:] -defined Function-like non empty V14([: the carrier of F1, the carrier of F1:]) set

the MorphMap of (F2 * a) . (e,e1) is set

[e,e1] is set

the MorphMap of (F2 * a) . [e,e1] is Relation-like Function-like set

Morph-Map (a,e,e1) is Relation-like <^e,e1^> -defined <^(a . e),(a . e1)^> -valued Function-like V18(<^e,e1^>,<^(a . e),(a . e1)^>) M2( bool [:<^e,e1^>,<^(a . e),(a . e1)^>:])

<^e,e1^> is set

a . e is M2( 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 ObjectMap of a 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:]) V18([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]) M2( bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:])

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

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

the ObjectMap of a . (e,e) is M2([: the carrier of B, the carrier of B:])

[e,e] is set

the ObjectMap of a . [e,e] is set

K40(( the ObjectMap of a . (e,e))) is set

a . e1 is M2( the carrier of B)

the ObjectMap of a . (e1,e1) is M2([: the carrier of B, the carrier of B:])

[e1,e1] is set

the ObjectMap of a . [e1,e1] is set

K40(( the ObjectMap of a . (e1,e1))) is set

<^(a . e),(a . e1)^> is set

[:<^e,e1^>,<^(a . e),(a . e1)^>:] is Relation-like set

bool [:<^e,e1^>,<^(a . e),(a . e1)^>:] is non empty set

the MorphMap 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:]) Function-yielding V37() MSUnTrans of the ObjectMap of a, the Arrows of A, the Arrows of B

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 a . (e,e1) is set

the MorphMap of a . [e,e1] is Relation-like Function-like set

Morph-Map (F2,(a . e),(a . e1)) is Relation-like Function-like set

the MorphMap of F2 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:]) Function-yielding V37() MSUnTrans of the ObjectMap of F2, the Arrows of B, the Arrows of F1

the ObjectMap of F2 is Relation-like [: the carrier of B, the carrier of B:] -defined [: the carrier of F1, the carrier of F1:] -valued Function-like non empty V14([: the carrier of B, the carrier of B:]) V18([: the carrier of B, the carrier of B:],[: the carrier of F1, the carrier of F1:]) M2( bool [:[: the carrier of B, the carrier of B:],[: the carrier of F1, the carrier of F1:]:])

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

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

the MorphMap of F2 . ((a . e),(a . e1)) is set

[(a . e),(a . e1)] is set

the MorphMap of F2 . [(a . e),(a . e1)] is Relation-like Function-like set

(Morph-Map (a,e,e1)) (#) (Morph-Map (F2,(a . e),(a . e1))) is Relation-like <^e,e1^> -defined Function-like set

dom the MorphMap of F2 is non empty set

rng the ObjectMap of a is Relation-like the carrier of B -defined the carrier of B -valued non empty M2( bool [: the carrier of B, the carrier of B:])

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

the ObjectMap of a (#) the MorphMap of F2 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:]) Function-yielding V37() set

dom ( the ObjectMap of a (#) the MorphMap of F2) is non empty set

dom the ObjectMap of a is Relation-like non empty set

( the ObjectMap of a (#) the MorphMap of F2) . [e,e1] is Relation-like Function-like set

the ObjectMap of a . (e,e1) is M2([: the carrier of B, the carrier of B:])

the ObjectMap of a . [e,e1] is set

the MorphMap of F2 . ( the ObjectMap of a . (e,e1)) is Relation-like Function-like set

dom the MorphMap of a is non empty set

(dom ( the ObjectMap of a (#) the MorphMap of F2)) /\ (dom the MorphMap of a) is set

( the ObjectMap of a (#) the MorphMap of F2) ** the MorphMap 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:]) Function-yielding V37() set

dom (( the ObjectMap of a (#) the MorphMap of F2) ** the MorphMap of a) is non empty set

(( the ObjectMap of a (#) the MorphMap of F2) ** the MorphMap of a) . (e,e1) is set

(( the ObjectMap of a (#) the MorphMap of F2) ** the MorphMap of a) . [e,e1] is Relation-like Function-like set

A is non empty transitive AltCatStr

the carrier of A is non empty set

B is non empty with_units reflexive AltCatStr

F1 is non empty with_units reflexive AltCatStr

a is reflexive feasible Contravariant FunctorStr over A,B

F2 is FunctorStr over B,F1

F2 * a is strict FunctorStr over A,F1

e is M2( the carrier of A)

e1 is M2( the carrier of A)

Morph-Map ((F2 * a),e,e1) is Relation-like Function-like set

the MorphMap of (F2 * 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:]) Function-yielding V37() MSUnTrans of the ObjectMap of (F2 * a), the Arrows of A, the Arrows of F1

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

the carrier of F1 is non empty set

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

the ObjectMap of (F2 * a) is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of F1, the carrier of F1:] -valued Function-like non empty V14([: the carrier of A, the carrier of A:]) V18([: the carrier of A, the carrier of A:],[: the carrier of F1, the carrier of F1:]) M2( bool [:[: the carrier of A, the carrier of A:],[: the carrier of F1, the carrier of F1:]:])

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

bool [:[: the carrier of A, the carrier of A:],[: the carrier of F1, the carrier of F1:]:] 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 F1 is Relation-like [: the carrier of F1, the carrier of F1:] -defined Function-like non empty V14([: the carrier of F1, the carrier of F1:]) set

the MorphMap of (F2 * a) . (e,e1) is set

[e,e1] is set

the MorphMap of (F2 * a) . [e,e1] is Relation-like Function-like set

Morph-Map (a,e,e1) is Relation-like <^e,e1^> -defined <^(a . e1),(a . e)^> -valued Function-like V18(<^e,e1^>,<^(a . e1),(a . e)^>) M2( bool [:<^e,e1^>,<^(a . e1),(a . e)^>:])

<^e,e1^> is set

a . e1 is M2( 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 ObjectMap of a 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:]) V18([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]) M2( bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:])

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

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

the ObjectMap of a . (e1,e1) is M2([: the carrier of B, the carrier of B:])

[e1,e1] is set

the ObjectMap of a . [e1,e1] is set

K40(( the ObjectMap of a . (e1,e1))) is set

a . e is M2( the carrier of B)

the ObjectMap of a . (e,e) is M2([: the carrier of B, the carrier of B:])

[e,e] is set

the ObjectMap of a . [e,e] is set

K40(( the ObjectMap of a . (e,e))) is set

<^(a . e1),(a . e)^> is set

[:<^e,e1^>,<^(a . e1),(a . e)^>:] is Relation-like set

bool [:<^e,e1^>,<^(a . e1),(a . e)^>:] is non empty set

the MorphMap 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:]) Function-yielding V37() MSUnTrans of the ObjectMap of a, the Arrows of A, the Arrows of B

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 a . (e,e1) is set

the MorphMap of a . [e,e1] is Relation-like Function-like set

Morph-Map (F2,(a . e1),(a . e)) is Relation-like Function-like set

the MorphMap of F2 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:]) Function-yielding V37() MSUnTrans of the ObjectMap of F2, the Arrows of B, the Arrows of F1

the ObjectMap of F2 is Relation-like [: the carrier of B, the carrier of B:] -defined [: the carrier of F1, the carrier of F1:] -valued Function-like non empty V14([: the carrier of B, the carrier of B:]) V18([: the carrier of B, the carrier of B:],[: the carrier of F1, the carrier of F1:]) M2( bool [:[: the carrier of B, the carrier of B:],[: the carrier of F1, the carrier of F1:]:])

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

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

the MorphMap of F2 . ((a . e1),(a . e)) is set

[(a . e1),(a . e)] is set

the MorphMap of F2 . [(a . e1),(a . e)] is Relation-like Function-like set

(Morph-Map (a,e,e1)) (#) (Morph-Map (F2,(a . e1),(a . e))) is Relation-like <^e,e1^> -defined Function-like set

dom the MorphMap of F2 is non empty set

rng the ObjectMap of a is Relation-like the carrier of B -defined the carrier of B -valued non empty M2( bool [: the carrier of B, the carrier of B:])

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

the ObjectMap of a (#) the MorphMap of F2 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:]) Function-yielding V37() set

dom ( the ObjectMap of a (#) the MorphMap of F2) is non empty set

dom the ObjectMap of a is Relation-like non empty set

( the ObjectMap of a (#) the MorphMap of F2) . [e,e1] is Relation-like Function-like set

the ObjectMap of a . (e,e1) is M2([: the carrier of B, the carrier of B:])

the ObjectMap of a . [e,e1] is set

the MorphMap of F2 . ( the ObjectMap of a . (e,e1)) is Relation-like Function-like set

dom the MorphMap of a is non empty set

(dom ( the ObjectMap of a (#) the MorphMap of F2)) /\ (dom the MorphMap of a) is set

( the ObjectMap of a (#) the MorphMap of F2) ** the MorphMap 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:]) Function-yielding V37() set

dom (( the ObjectMap of a (#) the MorphMap of F2) ** the MorphMap of a) is non empty set

(( the ObjectMap of a (#) the MorphMap of F2) ** the MorphMap of a) . (e,e1) is set

(( the ObjectMap of a (#) the MorphMap of F2) ** the MorphMap of a) . [e,e1] is Relation-like Function-like set

A is set

B is non empty set

[:A,B:] is Relation-like set

bool [:A,B:] is non empty set

F1 is Relation-like A -defined B -valued Function-like V14(A) V18(A,B) M2( bool [:A,B:])

a is Relation-like A -defined Function-like V14(A) set

F2 is Relation-like B -defined Function-like non empty V14(B) set

F1 (#) F2 is Relation-like A -defined Function-like V14(A) set

id F2 is Relation-like B -defined Function-like non empty V14(B) Function-yielding V37() ManySortedFunction of F2,F2

F1 (#) (id F2) is Relation-like A -defined Function-like V14(A) Function-yielding V37() set

e is Relation-like A -defined Function-like V14(A) Function-yielding V37() ManySortedFunction of a,F1 (#) F2

(F1 (#) (id F2)) ** e is Relation-like A -defined Function-like V14(A) Function-yielding V37() set

e1 is set

(F1 (#) F2) . e1 is set

F1 . e1 is set

F2 . (F1 . e1) is set

(F1 (#) (id F2)) . e1 is Relation-like Function-like set

(id F2) . (F1 . e1) is Relation-like Function-like set

id ((F1 (#) F2) . e1) is Relation-like (F1 (#) F2) . e1 -defined (F1 (#) F2) . e1 -valued Function-like one-to-one V14((F1 (#) F2) . e1) V18((F1 (#) F2) . e1,(F1 (#) F2) . e1) M2( bool [:((F1 (#) F2) . e1),((F1 (#) F2) . e1):])

[:((F1 (#) F2) . e1),((F1 (#) F2) . e1):] is Relation-like set

bool [:((F1 (#) F2) . e1),((F1 (#) F2) . e1):] is non empty set

e1 is set

(F1 (#) (id F2)) . e1 is Relation-like Function-like set

(F1 (#) F2) . e1 is set

[:((F1 (#) F2) . e1),((F1 (#) F2) . e1):] is Relation-like set

bool [:((F1 (#) F2) . e1),((F1 (#) F2) . e1):] is non empty set

id ((F1 (#) F2) . e1) is Relation-like (F1 (#) F2) . e1 -defined (F1 (#) F2) . e1 -valued Function-like one-to-one V14((F1 (#) F2) . e1) V18((F1 (#) F2) . e1,(F1 (#) F2) . e1) M2( bool [:((F1 (#) F2) . e1),((F1 (#) F2) . e1):])

e1 is set

e . e1 is Relation-like Function-like set

a . e1 is set

(F1 (#) F2) . e1 is set

[:(a . e1),((F1 (#) F2) . e1):] is Relation-like set

bool [:(a . e1),((F1 (#) F2) . e1):] is non empty set

(F1 (#) (id F2)) . e1 is Relation-like Function-like set

F1 . e1 is set

(id F2) . (F1 . e1) is Relation-like Function-like set

F2 . (F1 . e1) is set

id (F2 . (F1 . e1)) is Relation-like F2 . (F1 . e1) -defined F2 . (F1 . e1) -valued Function-like one-to-one V14(F2 . (F1 . e1)) V18(F2 . (F1 . e1),F2 . (F1 . e1)) M2( bool [:(F2 . (F1 . e1)),(F2 . (F1 . e1)):])

[:(F2 . (F1 . e1)),(F2 . (F1 . e1)):] is Relation-like set

bool [:(F2 . (F1 . e1)),(F2 . (F1 . e1)):] is non empty set

((F1 (#) (id F2)) ** e) . e1 is Relation-like Function-like set

id ((F1 (#) F2) . e1) is Relation-like (F1 (#) F2) . e1 -defined (F1 (#) F2) . e1 -valued Function-like one-to-one V14((F1 (#) F2) . e1) V18((F1 (#) F2) . e1,(F1 (#) F2) . e1) M2( bool [:((F1 (#) F2) . e1),((F1 (#) F2) . e1):])

[:((F1 (#) F2) . e1),((F1 (#) F2) . e1):] is Relation-like set

bool [:((F1 (#) F2) . e1),((F1 (#) F2) . e1):] is non empty set

(e . e1) (#) (id ((F1 (#) F2) . e1)) is Relation-like (F1 (#) F2) . e1 -valued Function-like set

A is non empty transitive AltCatStr

B is non empty with_units reflexive AltCatStr

id B is reflexive feasible strict Covariant V165(B,B) FunctorStr over B,B

F1 is feasible FunctorStr over A,B

(id B) * F1 is feasible strict FunctorStr over A,B

the ObjectMap of F1 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:]) V18([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]) M2( 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 MorphMap of F1 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:]) Function-yielding V37() MSUnTrans of the ObjectMap of F1, the Arrows of A, the Arrows of B

the Arrows of A is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) set

the Arrows of B is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) set

FunctorStr(# the ObjectMap of F1, the MorphMap of F1 #) is strict FunctorStr over A,B

the ObjectMap of ((id B) * F1) 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:]) V18([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]) M2( bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:])

the ObjectMap of (id B) is Relation-like [: the carrier of B, the carrier of B:] -defined [: the carrier of B, the carrier of B:] -valued Function-like non empty V14([: the carrier of B, the carrier of B:]) V18([: the carrier of B, the carrier of B:],[: the carrier of B, the carrier of B:]) M2( bool [:[: the carrier of B, the carrier of B:],[: the carrier of B, the carrier of B:]:])

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

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

the ObjectMap of (id B) * the ObjectMap of F1 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:]) V18([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]) M2( bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:])

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:]) V18([: the carrier of B, the carrier of B:],[: the carrier of B, the carrier of B:]) M2( bool [:[: the carrier of B, the carrier of B:],[: the carrier of B, the carrier of B:]:])

(id [: the carrier of B, the carrier of B:]) * the ObjectMap of F1 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:]) V18([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]) M2( bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:])

the ObjectMap of F1 (#) 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 ((id B) * F1) 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:]) Function-yielding V37() MSUnTrans of the ObjectMap of ((id B) * F1), the Arrows of A, the Arrows of B

the MorphMap of (id 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:]) Function-yielding V37() MSUnTrans of the ObjectMap of (id B), the Arrows of B, the Arrows of B

the ObjectMap of F1 (#) the MorphMap of (id 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:]) Function-yielding V37() set

( the ObjectMap of F1 (#) the MorphMap of (id B)) ** the MorphMap of F1 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:]) Function-yielding V37() 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:]) Function-yielding V37() ManySortedFunction of the Arrows of B, the Arrows of B

the ObjectMap of F1 (#) (id 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:]) Function-yielding V37() set

( the ObjectMap of F1 (#) (id the Arrows of B)) ** the MorphMap of F1 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:]) Function-yielding V37() set

A is non empty transitive with_units reflexive AltCatStr

id A is reflexive feasible strict Covariant id-preserving comp-preserving covariant V165(A,A) Functor of A,A

B is non empty with_units reflexive AltCatStr

F1 is feasible FunctorStr over A,B

F1 * (id A) is feasible strict FunctorStr over A,B

the ObjectMap of F1 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:]) V18([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]) M2( 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 MorphMap of F1 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:]) Function-yielding V37() MSUnTrans of the ObjectMap of F1, the Arrows of A, the Arrows of B

the Arrows of A is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) set

the Arrows of B is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like non empty V14([: the carrier of B, the carrier of B:]) set

FunctorStr(# the ObjectMap of F1, the MorphMap of F1 #) is strict FunctorStr over A,B

the ObjectMap of (F1 * (id A)) 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:]) V18([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]) M2( bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:])

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:]) V18([: the carrier of A, the carrier of A:],[: the carrier of A, the carrier of A:]) M2( 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 F1 * the ObjectMap of (id A) 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:]) V18([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]) M2( bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:])

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:]) V18([: the carrier of A, the carrier of A:],[: the carrier of A, the carrier of A:]) M2( bool [:[: the carrier of A, the carrier of A:],[: the carrier of A, the carrier of A:]:])

the ObjectMap of F1 * (id [: the carrier of A, the carrier of A:]) 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:]) V18([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]) M2( bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:])

the ObjectMap of F1 (#) 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 (F1 * (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:]) Function-yielding V37() MSUnTrans of the ObjectMap of (F1 * (id A)), the Arrows of A, the Arrows of B

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:]) Function-yielding V37() MSUnTrans of the ObjectMap of (id A), the Arrows of A, the Arrows of A

the ObjectMap of (id A) (#) the MorphMap of F1 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:]) Function-yielding V37() set

( the ObjectMap of (id A) (#) the MorphMap of F1) ** 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:]) Function-yielding V37() set

(id [: the carrier of A, the carrier of A:]) (#) the MorphMap of F1 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:]) Function-yielding V37() set

((id [: the carrier of A, the carrier of A:]) (#) the MorphMap of F1) ** 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:]) Function-yielding V37() set

the MorphMap of F1 ** 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:]) Function-yielding 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:]) Function-yielding V37() ManySortedFunction of the Arrows of A, the Arrows of A

the MorphMap of F1 ** (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:]) Function-yielding V37() set

A is non empty AltCatStr

the carrier of A is non empty set

B is non empty reflexive AltCatStr

F1 is non empty reflexive AltCatStr

a is reflexive feasible Covariant FunctorStr over A,B

F2 is reflexive feasible Covariant FunctorStr over B,F1

F2 * a is reflexive feasible strict Covariant FunctorStr over A,F1

e is M2( the carrier of A)

a . e is M2( 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 ObjectMap of a 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:]) V18([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]) M2( 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:] 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 a . (e,e) is M2([: the carrier of B, the carrier of B:])

[e,e] is set

the ObjectMap of a . [e,e] is set

K40(( the ObjectMap of a . (e,e))) is set

e1 is M2( the carrier of A)

<^e,e1^> is set

a . e1 is M2( the carrier of B)

the ObjectMap of a . (e1,e1) is M2([: the carrier of B, the carrier of B:])

[e1,e1] is set

the ObjectMap of a . [e1,e1] is set

K40(( the ObjectMap of a . (e1,e1))) is set

k is M2(<^e,e1^>)

(F2 * a) . k is M2(<^((F2 * a) . e),((F2 * a) . e1)^>)

(F2 * a) . e is M2( the carrier of F1)

the carrier of F1 is non empty set

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

the ObjectMap of (F2 * a) is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of F1, the carrier of F1:] -valued Function-like non empty V14([: the carrier of A, the carrier of A:]) V18([: the carrier of A, the carrier of A:],[: the carrier of F1, the carrier of F1:]) M2( bool [:[: the carrier of A, the carrier of A:],[: the carrier of F1, the carrier of F1:]:])

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

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

the ObjectMap of (F2 * a) . (e,e) is M2([: the carrier of F1, the carrier of F1:])

the ObjectMap of (F2 * a) . [e,e] is set

K40(( the ObjectMap of (F2 * a) . (e,e))) is set

(F2 * a) . e1 is M2( the carrier of F1)

the ObjectMap of (F2 * a) . (e1,e1) is M2([: the carrier of F1, the carrier of F1:])

the ObjectMap of (F2 * a) . [e1,e1] is set

K40(( the ObjectMap of (F2 * a) . (e1,e1))) is set

<^((F2 * a) . e),((F2 * a) . e1)^> is set

a . k is M2(<^(a . e),(a . e1)^>)

<^(a . e),(a . e1)^> is set

F2 . (a . k) is M2(<^(F2 . (a . e)),(F2 . (a . e1))^>)

F2 . (a . e) is M2( the carrier of F1)

the ObjectMap of F2 is Relation-like [: the carrier of B, the carrier of B:] -defined [: the carrier of F1, the carrier of F1:] -valued Function-like non empty V14([: the carrier of B, the carrier of B:]) V18([: the carrier of B, the carrier of B:],[: the carrier of F1, the carrier of F1:]) M2( bool [:[: the carrier of B, the carrier of B:],[: the carrier of F1, the carrier of F1:]:])

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

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

the ObjectMap of F2 . ((a . e),(a . e)) is M2([: the carrier of F1, the carrier of F1:])

[(a . e),(a . e)] is set

the ObjectMap of F2 . [(a . e),(a . e)] is set

K40(( the ObjectMap of F2 . ((a . e),(a . e)))) is set

F2 . (a . e1) is M2( the carrier of F1)

the ObjectMap of F2 . ((a . e1),(a . e1)) is M2([: the carrier of F1, the carrier of F1:])

[(a . e1),(a . e1)] is set

the ObjectMap of F2 . [(a . e1),(a . e1)] is set

K40(( the ObjectMap of F2 . ((a . e1),(a . e1)))) is set

<^(F2 . (a . e)),(F2 . (a . e1))^> is set

the MorphMap 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:]) Function-yielding V37() MSUnTrans of the ObjectMap of a, 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

the MorphMap of a . (e,e1) is set

[e,e1] is set

the MorphMap of a . [e,e1] is Relation-like Function-like set

the MorphMap of F2 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:]) Function-yielding V37() MSUnTrans of the ObjectMap of F2, the Arrows of B, the Arrows of F1

the Arrows of F1 is Relation-like [: the carrier of F1, the carrier of F1:] -defined Function-like non empty V14([: the carrier of F1, the carrier of F1:]) set

the ObjectMap of a (#) the MorphMap of F2 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:]) Function-yielding V37() set

( the ObjectMap of a (#) the MorphMap of F2) ** the MorphMap 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:]) Function-yielding V37() set

(( the ObjectMap of a (#) the MorphMap of F2) ** the MorphMap of a) . (e,e1) is set

(( the ObjectMap of a (#) the MorphMap of F2) ** the MorphMap of a) . [e,e1] is Relation-like Function-like set

( the ObjectMap of a (#) the MorphMap of F2) . (e,e1) is set

( the ObjectMap of a (#) the MorphMap of F2) . [e,e1] is Relation-like Function-like set

dom (( the ObjectMap of a (#) the MorphMap of F2) ** the MorphMap of a) is non empty set

dom ( the ObjectMap of a (#) the MorphMap of F2) is non empty set

dom the MorphMap of a is non empty set

(dom ( the ObjectMap of a (#) the MorphMap of F2)) /\ (dom the MorphMap of a) is set

[: the carrier of A, the carrier of A:] /\ (dom the MorphMap of a) is Relation-like set

[: the carrier of A, the carrier of A:] /\ [: the carrier of A, the carrier of A:] is Relation-like set

dom the ObjectMap of a is Relation-like non empty set

Morph-Map (a,e,e1) is Relation-like <^e,e1^> -defined <^(a . e),(a . e1)^> -valued Function-like V18(<^e,e1^>,<^(a . e),(a . e1)^>) M2( bool [:<^e,e1^>,<^(a . e),(a . e1)^>:])

[:<^e,e1^>,<^(a . e),(a . e1)^>:] is Relation-like set

bool [:<^e,e1^>,<^(a . e),(a . e1)^>:] is non empty set

dom (Morph-Map (a,e,e1)) is set

Morph-Map ((F2 * a),e,e1) is Relation-like <^e,e1^> -defined <^((F2 * a) . e),((F2 * a) . e1)^> -valued Function-like V18(<^e,e1^>,<^((F2 * a) . e),((F2 * a) . e1)^>) M2( bool [:<^e,e1^>,<^((F2 * a) . e),((F2 * a) . e1)^>:])

[:<^e,e1^>,<^((F2 * a) . e),((F2 * a) . e1)^>:] is Relation-like set

bool [:<^e,e1^>,<^((F2 * a) . e),((F2 * a) . e1)^>:] is non empty set

the MorphMap of (F2 * 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:]) Function-yielding V37() MSUnTrans of the ObjectMap of (F2 * a), the Arrows of A, the Arrows of F1

the MorphMap of (F2 * a) . (e,e1) is set

the MorphMap of (F2 * a) . [e,e1] is Relation-like Function-like set

(Morph-Map ((F2 * a),e,e1)) . k is set

G1t is Relation-like Function-like set

G1t . k is set

sF2 is Relation-like Function-like set

fa is Relation-like Function-like set

sF2 (#) fa is Relation-like Function-like set

(sF2 (#) fa) . k is set

(Morph-Map (a,e,e1)) . k is set

fa . ((Morph-Map (a,e,e1)) . k) is set

fa . (a . k) is set

the ObjectMap of a . (e,e1) is M2([: the carrier of B, the carrier of B:])

the ObjectMap of a . [e,e1] is set

the MorphMap of F2 . ( the ObjectMap of a . (e,e1)) is Relation-like Function-like set

( the MorphMap of F2 . ( the ObjectMap of a . (e,e1))) . (a . k) is set

Morph-Map (F2,(a . e),(a . e1)) is Relation-like <^(a . e),(a . e1)^> -defined <^(F2 . (a . e)),(F2 . (a . e1))^> -valued Function-like V18(<^(a . e),(a . e1)^>,<^(F2 . (a . e)),(F2 . (a . e1))^>) M2( bool [:<^(a . e),(a . e1)^>,<^(F2 . (a . e)),(F2 . (a . e1))^>:])

[:<^(a . e),(a . e1)^>,<^(F2 . (a . e)),(F2 . (a . e1))^>:] is Relation-like set

bool [:<^(a . e),(a . e1)^>,<^(F2 . (a . e)),(F2 . (a . e1))^>:] is non empty set

the MorphMap of F2 . ((a . e),(a . e1)) is set

[(a . e),(a . e1)] is set

the MorphMap of F2 . [(a . e),(a . e1)] is Relation-like Function-like set

(Morph-Map (F2,(a . e),(a . e1))) . (a . k) is set

A is non empty AltCatStr

the carrier of A is non empty set

B is non empty reflexive AltCatStr

F1 is non empty reflexive AltCatStr

a is reflexive feasible Contravariant FunctorStr over A,B

F2 is reflexive feasible Contravariant FunctorStr over B,F1

F2 * a is reflexive feasible strict Covariant FunctorStr over A,F1

e is M2( the carrier of A)

a . e is M2( 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 ObjectMap of a 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:]) V18([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]) M2( 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:] 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 a . (e,e) is M2([: the carrier of B, the carrier of B:])

[e,e] is set

the ObjectMap of a . [e,e] is set

K40(( the ObjectMap of a . (e,e))) is set

e1 is M2( the carrier of A)

<^e,e1^> is set

a . e1 is M2( the carrier of B)

the ObjectMap of a . (e1,e1) is M2([: the carrier of B, the carrier of B:])

[e1,e1] is set

the ObjectMap of a . [e1,e1] is set

K40(( the ObjectMap of a . (e1,e1))) is set

k is M2(<^e,e1^>)

(F2 * a) . k is M2(<^((F2 * a) . e),((F2 * a) . e1)^>)

(F2 * a) . e is M2( the carrier of F1)

the carrier of F1 is non empty set

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

the ObjectMap of (F2 * a) is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of F1, the carrier of F1:] -valued Function-like non empty V14([: the carrier of A, the carrier of A:]) V18([: the carrier of A, the carrier of A:],[: the carrier of F1, the carrier of F1:]) M2( bool [:[: the carrier of A, the carrier of A:],[: the carrier of F1, the carrier of F1:]:])

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

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

the ObjectMap of (F2 * a) . (e,e) is M2([: the carrier of F1, the carrier of F1:])

the ObjectMap of (F2 * a) . [e,e] is set

K40(( the ObjectMap of (F2 * a) . (e,e))) is set

(F2 * a) . e1 is M2( the carrier of F1)

the ObjectMap of (F2 * a) . (e1,e1) is M2([: the carrier of F1, the carrier of F1:])

the ObjectMap of (F2 * a) . [e1,e1] is set

K40(( the ObjectMap of (F2 * a) . (e1,e1))) is set

<^((F2 * a) . e),((F2 * a) . e1)^> is set

a . k is M2(<^(a . e1),(a . e)^>)

<^(a . e1),(a . e)^> is set

F2 . (a . k) is M2(<^(F2 . (a . e)),(F2 . (a . e1))^>)

F2 . (a . e) is M2( the carrier of F1)

the ObjectMap of F2 is Relation-like [: the carrier of B, the carrier of B:] -defined [: the carrier of F1, the carrier of F1:] -valued Function-like non empty V14([: the carrier of B, the carrier of B:]) V18([: the carrier of B, the carrier of B:],[: the carrier of F1, the carrier of F1:]) M2( bool [:[: the carrier of B, the carrier of B:],[: the carrier of F1, the carrier of F1:]:])

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

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

the ObjectMap of F2 . ((a . e),(a . e)) is M2([: the carrier of F1, the carrier of F1:])

[(a . e),(a . e)] is set

the ObjectMap of F2 . [(a . e),(a . e)] is set

K40(( the ObjectMap of F2 . ((a . e),(a . e)))) is set

F2 . (a . e1) is M2( the carrier of F1)

the ObjectMap of F2 . ((a . e1),(a . e1)) is M2([: the carrier of F1, the carrier of F1:])

[(a . e1),(a . e1)] is set

the ObjectMap of F2 . [(a . e1),(a . e1)] is set

K40(( the ObjectMap of F2 . ((a . e1),(a . e1)))) is set

<^(F2 . (a . e)),(F2 . (a . e1))^> is set

the MorphMap 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:]) Function-yielding V37() MSUnTrans of the ObjectMap of a, 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

the MorphMap of a . (e,e1) is set

[e,e1] is set

the MorphMap of a . [e,e1] is Relation-like Function-like set

the MorphMap of F2 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:]) Function-yielding V37() MSUnTrans of the ObjectMap of F2, the Arrows of B, the Arrows of F1

the Arrows of F1 is Relation-like [: the carrier of F1, the carrier of F1:] -defined Function-like non empty V14([: the carrier of F1, the carrier of F1:]) set

the ObjectMap of a (#) the MorphMap of F2 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:]) Function-yielding V37() set

( the ObjectMap of a (#) the MorphMap of F2) ** the MorphMap 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:]) Function-yielding V37() set

(( the ObjectMap of a (#) the MorphMap of F2) ** the MorphMap of a) . (e,e1) is set

(( the ObjectMap of a (#) the MorphMap of F2) ** the MorphMap of a) . [e,e1] is Relation-like Function-like set

( the ObjectMap of a (#) the MorphMap of F2) . (e,e1) is set

( the ObjectMap of a (#) the MorphMap of F2) . [e,e1] is Relation-like Function-like set

dom (( the ObjectMap of a (#) the MorphMap of F2) ** the MorphMap of a) is non empty set

dom ( the ObjectMap of a (#) the MorphMap of F2) is non empty set

dom the MorphMap of a is non empty set

(dom ( the ObjectMap of a (#) the MorphMap of F2)) /\ (dom the MorphMap of a) is set

[: the carrier of A, the carrier of A:] /\ (dom the MorphMap of a) is Relation-like set

[: the carrier of A, the carrier of A:] /\ [: the carrier of A, the carrier of A:] is Relation-like set

dom the ObjectMap of a is Relation-like non empty set

Morph-Map (a,e,e1) is Relation-like <^e,e1^> -defined <^(a . e1),(a . e)^> -valued Function-like V18(<^e,e1^>,<^(a . e1),(a . e)^>) M2( bool [:<^e,e1^>,<^(a . e1),(a . e)^>:])

[:<^e,e1^>,<^(a . e1),(a . e)^>:] is Relation-like set

bool [:<^e,e1^>,<^(a . e1),(a . e)^>:] is non empty set

dom (Morph-Map (a,e,e1)) is set

Morph-Map ((F2 * a),e,e1) is Relation-like <^e,e1^> -defined <^((F2 * a) . e),((F2 * a) . e1)^> -valued Function-like V18(<^e,e1^>,<^((F2 * a) . e),((F2 * a) . e1)^>) M2( bool [:<^e,e1^>,<^((F2 * a) . e),((F2 * a) . e1)^>:])

[:<^e,e1^>,<^((F2 * a) . e),((F2 * a) . e1)^>:] is Relation-like set

bool [:<^e,e1^>,<^((F2 * a) . e),((F2 * a) . e1)^>:] is non empty set

the MorphMap of (F2 * 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:]) Function-yielding V37() MSUnTrans of the ObjectMap of (F2 * a), the Arrows of A, the Arrows of F1

the MorphMap of (F2 * a) . (e,e1) is set

the MorphMap of (F2 * a) . [e,e1] is Relation-like Function-like set

(Morph-Map ((F2 * a),e,e1)) . k is set

G1t is Relation-like Function-like set

G1t . k is set

sF2 is Relation-like Function-like set

fa is Relation-like Function-like set

sF2 (#) fa is Relation-like Function-like set

(sF2 (#) fa) . k is set

(Morph-Map (a,e,e1)) . k is set

fa . ((Morph-Map (a,e,e1)) . k) is set

fa . (a . k) is set

the ObjectMap of a . (e,e1) is M2([: the carrier of B, the carrier of B:])

the ObjectMap of a . [e,e1] is set

the MorphMap of F2 . ( the ObjectMap of a . (e,e1)) is Relation-like Function-like set

( the MorphMap of F2 . ( the ObjectMap of a . (e,e1))) . (a . k) is set

Morph-Map (F2,(a . e1),(a . e)) is Relation-like <^(a . e1),(a . e)^> -defined <^(F2 . (a . e)),(F2 . (a . e1))^> -valued Function-like V18(<^(a . e1),(a . e)^>,<^(F2 . (a . e)),(F2 . (a . e1))^>) M2( bool [:<^(a . e1),(a . e)^>,<^(F2 . (a . e)),(F2 . (a . e1))^>:])

[:<^(a . e1),(a . e)^>,<^(F2 . (a . e)),(F2 . (a . e1))^>:] is Relation-like set

bool [:<^(a . e1),(a . e)^>,<^(F2 . (a . e)),(F2 . (a . e1))^>:] is non empty set

the MorphMap of F2 . ((a . e1),(a . e)) is set

[(a . e1),(a . e)] is set

the MorphMap of F2 . [(a . e1),(a . e)] is Relation-like Function-like set

(Morph-Map (F2,(a . e1),(a . e))) . (a . k) is set

A is non empty AltCatStr

the carrier of A is non empty set

B is non empty reflexive AltCatStr

F1 is non empty reflexive AltCatStr

a is reflexive feasible Covariant FunctorStr over A,B

F2 is reflexive feasible Contravariant FunctorStr over B,F1

F2 * a is reflexive feasible strict Contravariant FunctorStr over A,F1

e is M2( the carrier of A)

a . e is M2( 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 ObjectMap of a 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:]) V18([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]) M2( 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:] 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 a . (e,e) is M2([: the carrier of B, the carrier of B:])

[e,e] is set

the ObjectMap of a . [e,e] is set

K40(( the ObjectMap of a . (e,e))) is set

e1 is M2( the carrier of A)

<^e,e1^> is set

a . e1 is M2( the carrier of B)

the ObjectMap of a . (e1,e1) is M2([: the carrier of B, the carrier of B:])

[e1,e1] is set

the ObjectMap of a . [e1,e1] is set

K40(( the ObjectMap of a . (e1,e1))) is set

k is M2(<^e,e1^>)

(F2 * a) . k is M2(<^((F2 * a) . e1),((F2 * a) . e)^>)

(F2 * a) . e1 is M2( the carrier of F1)

the carrier of F1 is non empty set

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

the ObjectMap of (F2 * a) is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of F1, the carrier of F1:] -valued Function-like non empty V14([: the carrier of A, the carrier of A:]) V18([: the carrier of A, the carrier of A:],[: the carrier of F1, the carrier of F1:]) M2( bool [:[: the carrier of A, the carrier of A:],[: the carrier of F1, the carrier of F1:]:])

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

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

the ObjectMap of (F2 * a) . (e1,e1) is M2([: the carrier of F1, the carrier of F1:])

the ObjectMap of (F2 * a) . [e1,e1] is set

K40(( the ObjectMap of (F2 * a) . (e1,e1))) is set

(F2 * a) . e is M2( the carrier of F1)

the ObjectMap of (F2 * a) . (e,e) is M2([: the carrier of F1, the carrier of F1:])

the ObjectMap of (F2 * a) . [e,e] is set

K40(( the ObjectMap of (F2 * a) . (e,e))) is set

<^((F2 * a) . e1),((F2 * a) . e)^> is set

a . k is M2(<^(a . e),(a . e1)^>)

<^(a . e),(a . e1)^> is set

F2 . (a . k) is M2(<^(F2 . (a . e1)),(F2 . (a . e))^>)

F2 . (a . e1) is M2( the carrier of F1)

the ObjectMap of F2 is Relation-like [: the carrier of B, the carrier of B:] -defined [: the carrier of F1, the carrier of F1:] -valued Function-like non empty V14([: the carrier of B, the carrier of B:]) V18([: the carrier of B, the carrier of B:],[: the carrier of F1, the carrier of F1:]) M2( bool [:[: the carrier of B, the carrier of B:],[: the carrier of F1, the carrier of F1:]:])

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

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

the ObjectMap of F2 . ((a . e1),(a . e1)) is M2([: the carrier of F1, the carrier of F1:])

[(a . e1),(a . e1)] is set

the ObjectMap of F2 . [(a . e1),(a . e1)] is set

K40(( the ObjectMap of F2 . ((a . e1),(a . e1)))) is set

F2 . (a . e) is M2( the carrier of F1)

the ObjectMap of F2 . ((a . e),(a . e)) is M2([: the carrier of F1, the carrier of F1:])

[(a . e),(a . e)] is set

the ObjectMap of F2 . [(a . e),(a . e)] is set

K40(( the ObjectMap of F2 . ((a . e),(a . e)))) is set

<^(F2 . (a . e1)),(F2 . (a . e))^> is set

the MorphMap 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:]) Function-yielding V37() MSUnTrans of the ObjectMap of a, 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

the MorphMap of a . (e,e1) is set

[e,e1] is set

the MorphMap of a . [e,e1] is Relation-like Function-like set

the MorphMap of F2 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:]) Function-yielding V37() MSUnTrans of the ObjectMap of F2, the Arrows of B, the Arrows of F1

the Arrows of F1 is Relation-like [: the carrier of F1, the carrier of F1:] -defined Function-like non empty V14([: the carrier of F1, the carrier of F1:]) set

the ObjectMap of a (#) the MorphMap of F2 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:]) Function-yielding V37() set

( the ObjectMap of a (#) the MorphMap of F2) ** the MorphMap 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:]) Function-yielding V37() set

(( the ObjectMap of a (#) the MorphMap of F2) ** the MorphMap of a) . (e,e1) is set

(( the ObjectMap of a (#) the MorphMap of F2) ** the MorphMap of a) . [e,e1] is Relation-like Function-like set

( the ObjectMap of a (#) the MorphMap of F2) . (e,e1) is set

( the ObjectMap of a (#) the MorphMap of F2) . [e,e1] is Relation-like Function-like set

dom (( the ObjectMap of a (#) the MorphMap of F2) ** the MorphMap of a) is non empty set

dom ( the ObjectMap of a (#) the MorphMap of F2) is non empty set

dom the MorphMap of a is non empty set

(dom ( the ObjectMap of a (#) the MorphMap of F2)) /\ (dom the MorphMap of a) is set

[: the carrier of A, the carrier of A:] /\ (dom the MorphMap of a) is Relation-like set

[: the carrier of A, the carrier of A:] /\ [: the carrier of A, the carrier of A:] is Relation-like set

dom the ObjectMap of a is Relation-like non empty set

Morph-Map (a,e,e1) is Relation-like <^e,e1^> -defined <^(a . e),(a . e1)^> -valued Function-like V18(<^e,e1^>,<^(a . e),(a . e1)^>) M2( bool [:<^e,e1^>,<^(a . e),(a . e1)^>:])

[:<^e,e1^>,<^(a . e),(a . e1)^>:] is Relation-like set

bool [:<^e,e1^>,<^(a . e),(a . e1)^>:] is non empty set

dom (Morph-Map (a,e,e1)) is set

Morph-Map ((F2 * a),e,e1) is Relation-like <^e,e1^> -defined <^((F2 * a) . e1),((F2 * a) . e)^> -valued Function-like V18(<^e,e1^>,<^((F2 * a) . e1),((F2 * a) . e)^>) M2( bool [:<^e,e1^>,<^((F2 * a) . e1),((F2 * a) . e)^>:])

[:<^e,e1^>,<^((F2 * a) . e1),((F2 * a) . e)^>:] is Relation-like set

bool [:<^e,e1^>,<^((F2 * a) . e1),((F2 * a) . e)^>:] is non empty set

the MorphMap of (F2 * 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:]) Function-yielding V37() MSUnTrans of the ObjectMap of (F2 * a), the Arrows of A, the Arrows of F1

the MorphMap of (F2 * a) . (e,e1) is set

the MorphMap of (F2 * a) . [e,e1] is Relation-like Function-like set

(Morph-Map ((F2 * a),e,e1)) . k is set

G1t is Relation-like Function-like set

G1t . k is set

sF2 is Relation-like Function-like set

fa is Relation-like Function-like set

sF2 (#) fa is Relation-like Function-like set

(sF2 (#) fa) . k is set

(Morph-Map (a,e,e1)) . k is set

fa . ((Morph-Map (a,e,e1)) . k) is set

fa . (a . k) is set

the ObjectMap of a . (e,e1) is M2([: the carrier of B, the carrier of B:])

the ObjectMap of a . [e,e1] is set

the MorphMap of F2 . ( the ObjectMap of a . (e,e1)) is Relation-like Function-like set

( the MorphMap of F2 . ( the ObjectMap of a . (e,e1))) . (a . k) is set

Morph-Map (F2,(a . e),(a . e1)) is Relation-like <^(a . e),(a . e1)^> -defined <^(F2 . (a . e1)),(F2 . (a . e))^> -valued Function-like V18(<^(a . e),(a . e1)^>,<^(F2 . (a . e1)),(F2 . (a . e))^>) M2( bool [:<^(a . e),(a . e1)^>,<^(F2 . (a . e1)),(F2 . (a . e))^>:])

[:<^(a . e),(a . e1)^>,<^(F2 . (a . e1)),(F2 . (a . e))^>:] is Relation-like set

bool [:<^(a . e),(a . e1)^>,<^(F2 . (a . e1)),(F2 . (a . e))^>:] is non empty set

the MorphMap of F2 . ((a . e),(a . e1)) is set

[(a . e),(a . e1)] is set

the MorphMap of F2 . [(a . e),(a . e1)] is Relation-like Function-like set

(Morph-Map (F2,(a . e),(a . e1))) . (a . k) is set

A is non empty AltCatStr

the carrier of A is non empty set

B is non empty reflexive AltCatStr

F1 is non empty reflexive AltCatStr

a is reflexive feasible Covariant FunctorStr over F1,B

F2 is reflexive feasible Contravariant FunctorStr over A,F1

a * F2 is reflexive feasible strict Contravariant FunctorStr over A,B

e is M2( the carrier of A)

F2 . e is M2( the carrier of F1)

the carrier of F1 is non empty set

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

the ObjectMap of F2 is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of F1, the carrier of F1:] -valued Function-like non empty V14([: the carrier of A, the carrier of A:]) V18([: the carrier of A, the carrier of A:],[: the carrier of F1, the carrier of F1:]) M2( bool [:[: the carrier of A, the carrier of A:],[: the carrier of F1, the carrier of F1:]:])

[: 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 F1, the carrier of F1:]:] is Relation-like non empty set

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

the ObjectMap of F2 . (e,e) is M2([: the carrier of F1, the carrier of F1:])

[e,e] is set

the ObjectMap of F2 . [e,e] is set

K40(( the ObjectMap of F2 . (e,e))) is set

e1 is M2( the carrier of A)

<^e,e1^> is set

F2 . e1 is M2( the carrier of F1)

the ObjectMap of F2 . (e1,e1) is M2([: the carrier of F1, the carrier of F1:])

[e1,e1] is set

the ObjectMap of F2 . [e1,e1] is set

K40(( the ObjectMap of F2 . (e1,e1))) is set

k is M2(<^e,e1^>)

(a * F2) . k is M2(<^((a * F2) . e1),((a * F2) . e)^>)

(a * F2) . e1 is M2( 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 ObjectMap of (a * F2) 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:]) V18([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]) M2( bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:])

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

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

the ObjectMap of (a * F2) . (e1,e1) is M2([: the carrier of B, the carrier of B:])

the ObjectMap of (a * F2) . [e1,e1] is set

K40(( the ObjectMap of (a * F2) . (e1,e1))) is set

(a * F2) . e is M2( the carrier of B)

the ObjectMap of (a * F2) . (e,e) is M2([: the carrier of B, the carrier of B:])

the ObjectMap of (a * F2) . [e,e] is set

K40(( the ObjectMap of (a * F2) . (e,e))) is set

<^((a * F2) . e1),((a * F2) . e)