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

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

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

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

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

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

(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

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

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 . k is 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 . k is 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 . k is 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)