:: FUNCTOR2 semantic presentation

K179() is Element of bool K175()
K175() is set
bool K175() is non empty set
K102() is set
bool K102() is non empty set
{} is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional set
1 is non empty set
{{},1} is non empty set
bool K179() is non empty set
A is non empty transitive with_units V103() AltCatStr
B is non empty with_units V103() AltCatStr
C1 is Functor of A,B
C2 is Functor of A,B
A is non empty transitive with_units V103() AltCatStr
B is non empty with_units V103() AltCatStr
C1 is feasible id-preserving Functor of A,B
C1 is feasible id-preserving Functor of A,B
C1 is feasible id-preserving Functor of A,B
C1 is feasible id-preserving Functor of A,B
A is non empty transitive with_units V103() AltCatStr
B is non empty transitive with_units V103() AltCatStr
the carrier of A is non empty set
C1 is reflexive feasible Covariant id-preserving comp-preserving covariant Functor of A,B
C2 is Element of the carrier of A
idm C2 is Element of <^C2,C2^>
<^C2,C2^> is set
the Arrows of A is non empty Relation-like [: the carrier of A, the carrier of A:] -defined Function-like V17([: the carrier of A, the carrier of A:]) set
[: the carrier of A, the carrier of A:] is non empty Relation-like set
the Arrows of A . (C2,C2) is set
[C2,C2] is V1() set
the Arrows of A . [C2,C2] is set
C1 . (idm C2) is Element of <^(C1 . C2),(C1 . C2)^>
C1 . C2 is Element of the carrier of B
the carrier of B is non empty set
<^(C1 . C2),(C1 . C2)^> is set
the Arrows of B is non empty Relation-like [: the carrier of B, the carrier of B:] -defined Function-like V17([: the carrier of B, the carrier of B:]) set
[: the carrier of B, the carrier of B:] is non empty Relation-like set
the Arrows of B . ((C1 . C2),(C1 . C2)) is set
[(C1 . C2),(C1 . C2)] is V1() set
the Arrows of B . [(C1 . C2),(C1 . C2)] is set
idm (C1 . C2) is Element of <^(C1 . C2),(C1 . C2)^>
Morph-Map (C1,C2,C2) is Relation-like <^C2,C2^> -defined <^(C1 . C2),(C1 . C2)^> -valued Function-like quasi_total Element of bool [:<^C2,C2^>,<^(C1 . C2),(C1 . C2)^>:]
[:<^C2,C2^>,<^(C1 . C2),(C1 . C2)^>:] is Relation-like set
bool [:<^C2,C2^>,<^(C1 . C2),(C1 . C2)^>:] is non empty set
(Morph-Map (C1,C2,C2)) . (idm C2) is set
A is non empty transitive with_units V103() AltCatStr
B is non empty transitive with_units V103() AltCatStr
the carrier of A is non empty set
R is feasible id-preserving Functor of A,B
T is Element of the carrier of A
R . T is Element of the carrier of B
the carrier of B is non empty set
<^(R . T),(R . T)^> is set
the Arrows of B is non empty Relation-like [: the carrier of B, the carrier of B:] -defined Function-like V17([: the carrier of B, the carrier of B:]) set
[: the carrier of B, the carrier of B:] is non empty Relation-like set
the Arrows of B . ((R . T),(R . T)) is set
[(R . T),(R . T)] is V1() set
the Arrows of B . [(R . T),(R . T)] is set
A is non empty transitive with_units V103() AltCatStr
B is non empty transitive with_units V103() AltCatStr
C1 is feasible id-preserving Functor of A,B
C2 is feasible id-preserving Functor of A,B
R is feasible id-preserving Functor of A,B
the carrier of A is non empty set
T is Element of the carrier of A
C1 . T is Element of the carrier of B
the carrier of B is non empty set
R . T is Element of the carrier of B
<^(C1 . T),(R . T)^> is set
the Arrows of B is non empty Relation-like [: the carrier of B, the carrier of B:] -defined Function-like V17([: the carrier of B, the carrier of B:]) set
[: the carrier of B, the carrier of B:] is non empty Relation-like set
the Arrows of B . ((C1 . T),(R . T)) is set
[(C1 . T),(R . T)] is V1() set
the Arrows of B . [(C1 . T),(R . T)] is set
C2 . T is Element of the carrier of B
<^(C1 . T),(C2 . T)^> is set
the Arrows of B . ((C1 . T),(C2 . T)) is set
[(C1 . T),(C2 . T)] is V1() set
the Arrows of B . [(C1 . T),(C2 . T)] is set
<^(C2 . T),(R . T)^> is set
the Arrows of B . ((C2 . T),(R . T)) is set
[(C2 . T),(R . T)] is V1() set
the Arrows of B . [(C2 . T),(R . T)] is set
A is non empty transitive with_units V103() AltCatStr
B is non empty transitive with_units V103() AltCatStr
C1 is feasible id-preserving Functor of A,B
C2 is feasible id-preserving Functor of A,B
the carrier of A is non empty set
R is Element of the carrier of A
C1 . R is Element of the carrier of B
the carrier of B is non empty set
C2 . R is Element of the carrier of B
<^(C1 . R),(C2 . R)^> is set
the Arrows of B is non empty Relation-like [: the carrier of B, the carrier of B:] -defined Function-like V17([: the carrier of B, the carrier of B:]) set
[: the carrier of B, the carrier of B:] is non empty Relation-like set
the Arrows of B . ((C1 . R),(C2 . R)) is set
[(C1 . R),(C2 . R)] is V1() set
the Arrows of B . [(C1 . R),(C2 . R)] is set
T is Element of the carrier of A
C1 . T is Element of the carrier of B
C2 . T is Element of the carrier of B
<^(C1 . T),(C2 . T)^> is set
the Arrows of B . ((C1 . T),(C2 . T)) is set
[(C1 . T),(C2 . T)] is V1() set
the Arrows of B . [(C1 . T),(C2 . T)] is set
R is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) set
T is Element of the carrier of A
R . T is set
C1 . T is Element of the carrier of B
the carrier of B is non empty set
C2 . T is Element of the carrier of B
<^(C1 . T),(C2 . T)^> is set
the Arrows of B is non empty Relation-like [: the carrier of B, the carrier of B:] -defined Function-like V17([: the carrier of B, the carrier of B:]) set
[: the carrier of B, the carrier of B:] is non empty Relation-like set
the Arrows of B . ((C1 . T),(C2 . T)) is set
[(C1 . T),(C2 . T)] is V1() set
the Arrows of B . [(C1 . T),(C2 . T)] is set
A is non empty transitive with_units V103() AltCatStr
B is non empty transitive with_units V103() AltCatStr
the carrier of A is non empty set
C1 is feasible id-preserving Functor of A,B
C2 is Element of the carrier of A
C1 . C2 is Element of the carrier of B
the carrier of B is non empty set
idm (C1 . C2) is Element of <^(C1 . C2),(C1 . C2)^>
<^(C1 . C2),(C1 . C2)^> is set
the Arrows of B is non empty Relation-like [: the carrier of B, the carrier of B:] -defined Function-like V17([: the carrier of B, the carrier of B:]) set
[: the carrier of B, the carrier of B:] is non empty Relation-like set
the Arrows of B . ((C1 . C2),(C1 . C2)) is set
[(C1 . C2),(C1 . C2)] is V1() set
the Arrows of B . [(C1 . C2),(C1 . C2)] is set
C2 is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) set
R is Element of the carrier of A
C2 . R is set
C1 . R is Element of the carrier of B
the carrier of B is non empty set
<^(C1 . R),(C1 . R)^> is set
the Arrows of B is non empty Relation-like [: the carrier of B, the carrier of B:] -defined Function-like V17([: the carrier of B, the carrier of B:]) set
[: the carrier of B, the carrier of B:] is non empty Relation-like set
the Arrows of B . ((C1 . R),(C1 . R)) is set
[(C1 . R),(C1 . R)] is V1() set
the Arrows of B . [(C1 . R),(C1 . R)] is set
idm (C1 . R) is Element of <^(C1 . R),(C1 . R)^>
C2 is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,C1)
R is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,C1)
T is set
C2 . T is set
N is Element of the carrier of A
C1 . N is Element of the carrier of B
the carrier of B is non empty set
idm (C1 . N) is Element of <^(C1 . N),(C1 . N)^>
<^(C1 . N),(C1 . N)^> is set
the Arrows of B is non empty Relation-like [: the carrier of B, the carrier of B:] -defined Function-like V17([: the carrier of B, the carrier of B:]) set
[: the carrier of B, the carrier of B:] is non empty Relation-like set
the Arrows of B . ((C1 . N),(C1 . N)) is set
[(C1 . N),(C1 . N)] is V1() set
the Arrows of B . [(C1 . N),(C1 . N)] is set
R . T is set
A is non empty transitive with_units V103() AltCatStr
B is non empty transitive with_units V103() AltCatStr
C1 is feasible id-preserving Functor of A,B
C2 is feasible id-preserving Functor of A,B
the carrier of A is non empty set
T is Element of the carrier of A
C1 . T is Element of the carrier of B
the carrier of B is non empty set
C2 . T is Element of the carrier of B
<^(C1 . T),(C2 . T)^> is set
the Arrows of B is non empty Relation-like [: the carrier of B, the carrier of B:] -defined Function-like V17([: the carrier of B, the carrier of B:]) set
[: the carrier of B, the carrier of B:] is non empty Relation-like set
the Arrows of B . ((C1 . T),(C2 . T)) is set
[(C1 . T),(C2 . T)] is V1() set
the Arrows of B . [(C1 . T),(C2 . T)] is set
R is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,C2)
R . T is set
N is Element of <^(C1 . T),(C2 . T)^>
M is Element of <^(C1 . T),(C2 . T)^>
A is non empty transitive with_units V103() AltCatStr
B is non empty transitive with_units V103() AltCatStr
C1 is feasible id-preserving Functor of A,B
C2 is feasible id-preserving Functor of A,B
R is feasible id-preserving Functor of A,B
the carrier of A is non empty set
T is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,C2)
N is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C2,R)
M is Element of the carrier of A
C1 . M is Element of the carrier of B
the carrier of B is non empty set
C2 . M is Element of the carrier of B
R . M is Element of the carrier of B
(A,B,C1,C2,T,M) is Element of <^(C1 . M),(C2 . M)^>
<^(C1 . M),(C2 . M)^> is set
the Arrows of B is non empty Relation-like [: the carrier of B, the carrier of B:] -defined Function-like V17([: the carrier of B, the carrier of B:]) set
[: the carrier of B, the carrier of B:] is non empty Relation-like set
the Arrows of B . ((C1 . M),(C2 . M)) is set
[(C1 . M),(C2 . M)] is V1() set
the Arrows of B . [(C1 . M),(C2 . M)] is set
(A,B,C2,R,N,M) is Element of <^(C2 . M),(R . M)^>
<^(C2 . M),(R . M)^> is set
the Arrows of B . ((C2 . M),(R . M)) is set
[(C2 . M),(R . M)] is V1() set
the Arrows of B . [(C2 . M),(R . M)] is set
(A,B,C2,R,N,M) * (A,B,C1,C2,T,M) is Element of <^(C1 . M),(R . M)^>
<^(C1 . M),(R . M)^> is set
the Arrows of B . ((C1 . M),(R . M)) is set
[(C1 . M),(R . M)] is V1() set
the Arrows of B . [(C1 . M),(R . M)] is set
M is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) set
O is Element of the carrier of A
M . O is set
C1 . O is Element of the carrier of B
the carrier of B is non empty set
R . O is Element of the carrier of B
<^(C1 . O),(R . O)^> is set
the Arrows of B is non empty Relation-like [: the carrier of B, the carrier of B:] -defined Function-like V17([: the carrier of B, the carrier of B:]) set
[: the carrier of B, the carrier of B:] is non empty Relation-like set
the Arrows of B . ((C1 . O),(R . O)) is set
[(C1 . O),(R . O)] is V1() set
the Arrows of B . [(C1 . O),(R . O)] is set
C2 . O is Element of the carrier of B
(A,B,C1,C2,T,O) is Element of <^(C1 . O),(C2 . O)^>
<^(C1 . O),(C2 . O)^> is set
the Arrows of B . ((C1 . O),(C2 . O)) is set
[(C1 . O),(C2 . O)] is V1() set
the Arrows of B . [(C1 . O),(C2 . O)] is set
(A,B,C2,R,N,O) is Element of <^(C2 . O),(R . O)^>
<^(C2 . O),(R . O)^> is set
the Arrows of B . ((C2 . O),(R . O)) is set
[(C2 . O),(R . O)] is V1() set
the Arrows of B . [(C2 . O),(R . O)] is set
(A,B,C2,R,N,O) * (A,B,C1,C2,T,O) is Element of <^(C1 . O),(R . O)^>
O is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,R)
P is Element of the carrier of A
(A,B,C1,R,O,P) is Element of <^(C1 . P),(R . P)^>
C1 . P is Element of the carrier of B
the carrier of B is non empty set
R . P is Element of the carrier of B
<^(C1 . P),(R . P)^> is set
the Arrows of B is non empty Relation-like [: the carrier of B, the carrier of B:] -defined Function-like V17([: the carrier of B, the carrier of B:]) set
[: the carrier of B, the carrier of B:] is non empty Relation-like set
the Arrows of B . ((C1 . P),(R . P)) is set
[(C1 . P),(R . P)] is V1() set
the Arrows of B . [(C1 . P),(R . P)] is set
C2 . P is Element of the carrier of B
(A,B,C1,C2,T,P) is Element of <^(C1 . P),(C2 . P)^>
<^(C1 . P),(C2 . P)^> is set
the Arrows of B . ((C1 . P),(C2 . P)) is set
[(C1 . P),(C2 . P)] is V1() set
the Arrows of B . [(C1 . P),(C2 . P)] is set
(A,B,C2,R,N,P) is Element of <^(C2 . P),(R . P)^>
<^(C2 . P),(R . P)^> is set
the Arrows of B . ((C2 . P),(R . P)) is set
[(C2 . P),(R . P)] is V1() set
the Arrows of B . [(C2 . P),(R . P)] is set
(A,B,C2,R,N,P) * (A,B,C1,C2,T,P) is Element of <^(C1 . P),(R . P)^>
M . P is set
M is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,R)
O is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,R)
P is set
M . P is set
i is Element of the carrier of A
(A,B,C1,R,M,i) is Element of <^(C1 . i),(R . i)^>
C1 . i is Element of the carrier of B
the carrier of B is non empty set
R . i is Element of the carrier of B
<^(C1 . i),(R . i)^> is set
the Arrows of B is non empty Relation-like [: the carrier of B, the carrier of B:] -defined Function-like V17([: the carrier of B, the carrier of B:]) set
[: the carrier of B, the carrier of B:] is non empty Relation-like set
the Arrows of B . ((C1 . i),(R . i)) is set
[(C1 . i),(R . i)] is V1() set
the Arrows of B . [(C1 . i),(R . i)] is set
C2 . i is Element of the carrier of B
(A,B,C1,C2,T,i) is Element of <^(C1 . i),(C2 . i)^>
<^(C1 . i),(C2 . i)^> is set
the Arrows of B . ((C1 . i),(C2 . i)) is set
[(C1 . i),(C2 . i)] is V1() set
the Arrows of B . [(C1 . i),(C2 . i)] is set
(A,B,C2,R,N,i) is Element of <^(C2 . i),(R . i)^>
<^(C2 . i),(R . i)^> is set
the Arrows of B . ((C2 . i),(R . i)) is set
[(C2 . i),(R . i)] is V1() set
the Arrows of B . [(C2 . i),(R . i)] is set
(A,B,C2,R,N,i) * (A,B,C1,C2,T,i) is Element of <^(C1 . i),(R . i)^>
(A,B,C1,R,O,i) is Element of <^(C1 . i),(R . i)^>
O . P is set
A is non empty transitive with_units V103() AltCatStr
B is non empty transitive with_units V103() AltCatStr
the carrier of A is non empty set
C1 is feasible id-preserving Functor of A,B
C2 is feasible id-preserving Functor of A,B
R is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,C2)
T is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,C2)
N is set
R . N is set
M is Element of the carrier of A
(A,B,C1,C2,R,M) is Element of <^(C1 . M),(C2 . M)^>
C1 . M is Element of the carrier of B
the carrier of B is non empty set
C2 . M is Element of the carrier of B
<^(C1 . M),(C2 . M)^> is set
the Arrows of B is non empty Relation-like [: the carrier of B, the carrier of B:] -defined Function-like V17([: the carrier of B, the carrier of B:]) set
[: the carrier of B, the carrier of B:] is non empty Relation-like set
the Arrows of B . ((C1 . M),(C2 . M)) is set
[(C1 . M),(C2 . M)] is V1() set
the Arrows of B . [(C1 . M),(C2 . M)] is set
(A,B,C1,C2,T,M) is Element of <^(C1 . M),(C2 . M)^>
T . N is set
A is non empty transitive with_units V103() AltCatStr
B is non empty transitive with_units V103() AltCatStr
the carrier of A is non empty set
C1 is feasible id-preserving Functor of A,B
(A,B,C1) is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,C1)
C2 is Element of the carrier of A
(A,B,C1,C1,(A,B,C1),C2) is Element of <^(C1 . C2),(C1 . C2)^>
C1 . C2 is Element of the carrier of B
the carrier of B is non empty set
<^(C1 . C2),(C1 . C2)^> is set
the Arrows of B is non empty Relation-like [: the carrier of B, the carrier of B:] -defined Function-like V17([: the carrier of B, the carrier of B:]) set
[: the carrier of B, the carrier of B:] is non empty Relation-like set
the Arrows of B . ((C1 . C2),(C1 . C2)) is set
[(C1 . C2),(C1 . C2)] is V1() set
the Arrows of B . [(C1 . C2),(C1 . C2)] is set
idm (C1 . C2) is Element of <^(C1 . C2),(C1 . C2)^>
(A,B,C1) . C2 is set
A is non empty transitive with_units V103() AltCatStr
B is non empty transitive with_units V103() AltCatStr
the carrier of A is non empty set
C1 is feasible id-preserving Functor of A,B
C2 is feasible id-preserving Functor of A,B
(A,B,C2) is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C2,C2)
(A,B,C1) is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,C1)
R is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,C2)
(A,B,C1,C2,C2,R,(A,B,C2)) is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,C2)
(A,B,C1,C1,C2,(A,B,C1),R) is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,C2)
T is Element of the carrier of A
C1 . T is Element of the carrier of B
the carrier of B is non empty set
C2 . T is Element of the carrier of B
<^(C1 . T),(C2 . T)^> is set
the Arrows of B is non empty Relation-like [: the carrier of B, the carrier of B:] -defined Function-like V17([: the carrier of B, the carrier of B:]) set
[: the carrier of B, the carrier of B:] is non empty Relation-like set
the Arrows of B . ((C1 . T),(C2 . T)) is set
[(C1 . T),(C2 . T)] is V1() set
the Arrows of B . [(C1 . T),(C2 . T)] is set
(A,B,C1,C2,(A,B,C1,C2,C2,R,(A,B,C2)),T) is Element of <^(C1 . T),(C2 . T)^>
(A,B,C1,C2,R,T) is Element of <^(C1 . T),(C2 . T)^>
(A,B,C2,C2,(A,B,C2),T) is Element of <^(C2 . T),(C2 . T)^>
<^(C2 . T),(C2 . T)^> is set
the Arrows of B . ((C2 . T),(C2 . T)) is set
[(C2 . T),(C2 . T)] is V1() set
the Arrows of B . [(C2 . T),(C2 . T)] is set
(A,B,C2,C2,(A,B,C2),T) * (A,B,C1,C2,R,T) is Element of <^(C1 . T),(C2 . T)^>
idm (C2 . T) is Element of <^(C2 . T),(C2 . T)^>
(idm (C2 . T)) * (A,B,C1,C2,R,T) is Element of <^(C1 . T),(C2 . T)^>
T is Element of the carrier of A
C1 . T is Element of the carrier of B
C2 . T is Element of the carrier of B
<^(C1 . T),(C2 . T)^> is set
the Arrows of B . ((C1 . T),(C2 . T)) is set
[(C1 . T),(C2 . T)] is V1() set
the Arrows of B . [(C1 . T),(C2 . T)] is set
(A,B,C1,C2,(A,B,C1,C1,C2,(A,B,C1),R),T) is Element of <^(C1 . T),(C2 . T)^>
(A,B,C1,C1,(A,B,C1),T) is Element of <^(C1 . T),(C1 . T)^>
<^(C1 . T),(C1 . T)^> is set
the Arrows of B . ((C1 . T),(C1 . T)) is set
[(C1 . T),(C1 . T)] is V1() set
the Arrows of B . [(C1 . T),(C1 . T)] is set
(A,B,C1,C2,R,T) is Element of <^(C1 . T),(C2 . T)^>
(A,B,C1,C2,R,T) * (A,B,C1,C1,(A,B,C1),T) is Element of <^(C1 . T),(C2 . T)^>
idm (C1 . T) is Element of <^(C1 . T),(C1 . T)^>
(A,B,C1,C2,R,T) * (idm (C1 . T)) is Element of <^(C1 . T),(C2 . T)^>
A is non empty transitive V99() with_units V103() AltCatStr
B is non empty transitive V99() with_units V103() AltCatStr
the carrier of A is non empty set
C1 is feasible id-preserving Functor of A,B
C2 is feasible id-preserving Functor of A,B
R is feasible id-preserving Functor of A,B
T is feasible id-preserving Functor of A,B
N is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,C2)
M is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C2,R)
(A,B,C1,C2,R,N,M) is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,R)
O is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,R,T)
(A,B,C2,R,T,M,O) is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C2,T)
(A,B,C1,C2,T,N,(A,B,C2,R,T,M,O)) is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,T)
(A,B,C1,R,T,(A,B,C1,C2,R,N,M),O) is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,T)
P is Element of the carrier of A
R . P is Element of the carrier of B
the carrier of B is non empty set
T . P is Element of the carrier of B
<^(R . P),(T . P)^> is set
the Arrows of B is non empty Relation-like [: the carrier of B, the carrier of B:] -defined Function-like V17([: the carrier of B, the carrier of B:]) set
[: the carrier of B, the carrier of B:] is non empty Relation-like set
the Arrows of B . ((R . P),(T . P)) is set
[(R . P),(T . P)] is V1() set
the Arrows of B . [(R . P),(T . P)] is set
C1 . P is Element of the carrier of B
C2 . P is Element of the carrier of B
<^(C1 . P),(C2 . P)^> is set
the Arrows of B . ((C1 . P),(C2 . P)) is set
[(C1 . P),(C2 . P)] is V1() set
the Arrows of B . [(C1 . P),(C2 . P)] is set
<^(C2 . P),(R . P)^> is set
the Arrows of B . ((C2 . P),(R . P)) is set
[(C2 . P),(R . P)] is V1() set
the Arrows of B . [(C2 . P),(R . P)] is set
(A,B,C1,T,(A,B,C1,C2,T,N,(A,B,C2,R,T,M,O)),P) is Element of <^(C1 . P),(T . P)^>
<^(C1 . P),(T . P)^> is set
the Arrows of B . ((C1 . P),(T . P)) is set
[(C1 . P),(T . P)] is V1() set
the Arrows of B . [(C1 . P),(T . P)] is set
(A,B,C1,C2,N,P) is Element of <^(C1 . P),(C2 . P)^>
(A,B,C2,T,(A,B,C2,R,T,M,O),P) is Element of <^(C2 . P),(T . P)^>
<^(C2 . P),(T . P)^> is set
the Arrows of B . ((C2 . P),(T . P)) is set
[(C2 . P),(T . P)] is V1() set
the Arrows of B . [(C2 . P),(T . P)] is set
(A,B,C2,T,(A,B,C2,R,T,M,O),P) * (A,B,C1,C2,N,P) is Element of <^(C1 . P),(T . P)^>
(A,B,C2,R,M,P) is Element of <^(C2 . P),(R . P)^>
(A,B,R,T,O,P) is Element of <^(R . P),(T . P)^>
(A,B,R,T,O,P) * (A,B,C2,R,M,P) is Element of <^(C2 . P),(T . P)^>
((A,B,R,T,O,P) * (A,B,C2,R,M,P)) * (A,B,C1,C2,N,P) is Element of <^(C1 . P),(T . P)^>
(A,B,C2,R,M,P) * (A,B,C1,C2,N,P) is Element of <^(C1 . P),(R . P)^>
<^(C1 . P),(R . P)^> is set
the Arrows of B . ((C1 . P),(R . P)) is set
[(C1 . P),(R . P)] is V1() set
the Arrows of B . [(C1 . P),(R . P)] is set
(A,B,R,T,O,P) * ((A,B,C2,R,M,P) * (A,B,C1,C2,N,P)) is Element of <^(C1 . P),(T . P)^>
(A,B,C1,R,(A,B,C1,C2,R,N,M),P) is Element of <^(C1 . P),(R . P)^>
(A,B,R,T,O,P) * (A,B,C1,R,(A,B,C1,C2,R,N,M),P) is Element of <^(C1 . P),(T . P)^>
(A,B,C1,T,(A,B,C1,R,T,(A,B,C1,C2,R,N,M),O),P) is Element of <^(C1 . P),(T . P)^>
A is non empty transitive with_units V103() AltCatStr
B is non empty transitive with_units V103() AltCatStr
the carrier of A is non empty set
C1 is reflexive feasible Covariant id-preserving comp-preserving covariant Functor of A,B
(A,B,C1) is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,C1)
R is Element of the carrier of A
T is Element of the carrier of A
<^R,T^> is set
the Arrows of A is non empty Relation-like [: the carrier of A, the carrier of A:] -defined Function-like V17([: the carrier of A, the carrier of A:]) set
[: the carrier of A, the carrier of A:] is non empty Relation-like set
the Arrows of A . (R,T) is set
[R,T] is V1() set
the Arrows of A . [R,T] is set
C1 . R is Element of the carrier of B
the carrier of B is non empty set
C1 . T is Element of the carrier of B
(A,B,C1,C1,(A,B,C1),T) is Element of <^(C1 . T),(C1 . T)^>
<^(C1 . T),(C1 . T)^> is set
the Arrows of B is non empty Relation-like [: the carrier of B, the carrier of B:] -defined Function-like V17([: the carrier of B, the carrier of B:]) set
[: the carrier of B, the carrier of B:] is non empty Relation-like set
the Arrows of B . ((C1 . T),(C1 . T)) is set
[(C1 . T),(C1 . T)] is V1() set
the Arrows of B . [(C1 . T),(C1 . T)] is set
(A,B,C1,C1,(A,B,C1),R) is Element of <^(C1 . R),(C1 . R)^>
<^(C1 . R),(C1 . R)^> is set
the Arrows of B . ((C1 . R),(C1 . R)) is set
[(C1 . R),(C1 . R)] is V1() set
the Arrows of B . [(C1 . R),(C1 . R)] is set
N is Element of <^R,T^>
C1 . N is Element of <^(C1 . R),(C1 . T)^>
<^(C1 . R),(C1 . T)^> is set
the Arrows of B . ((C1 . R),(C1 . T)) is set
[(C1 . R),(C1 . T)] is V1() set
the Arrows of B . [(C1 . R),(C1 . T)] is set
(A,B,C1,C1,(A,B,C1),T) * (C1 . N) is Element of <^(C1 . R),(C1 . T)^>
(C1 . N) * (A,B,C1,C1,(A,B,C1),R) is Element of <^(C1 . R),(C1 . T)^>
<^R,R^> is set
the Arrows of A . (R,R) is set
[R,R] is V1() set
the Arrows of A . [R,R] is set
<^T,T^> is set
the Arrows of A . (T,T) is set
[T,T] is V1() set
the Arrows of A . [T,T] is set
idm (C1 . T) is Element of <^(C1 . T),(C1 . T)^>
(idm (C1 . T)) * (C1 . N) is Element of <^(C1 . R),(C1 . T)^>
idm T is Element of <^T,T^>
C1 . (idm T) is Element of <^(C1 . T),(C1 . T)^>
(C1 . (idm T)) * (C1 . N) is Element of <^(C1 . R),(C1 . T)^>
(idm T) * N is Element of <^R,T^>
C1 . ((idm T) * N) is Element of <^(C1 . R),(C1 . T)^>
idm R is Element of <^R,R^>
N * (idm R) is Element of <^R,T^>
C1 . (N * (idm R)) is Element of <^(C1 . R),(C1 . T)^>
C1 . (idm R) is Element of <^(C1 . R),(C1 . R)^>
(C1 . N) * (C1 . (idm R)) is Element of <^(C1 . R),(C1 . T)^>
idm (C1 . R) is Element of <^(C1 . R),(C1 . R)^>
(C1 . N) * (idm (C1 . R)) is Element of <^(C1 . R),(C1 . T)^>
A is non empty transitive with_units V103() AltCatStr
B is non empty transitive with_units V103() AltCatStr
the carrier of A is non empty set
R is reflexive feasible Covariant id-preserving comp-preserving covariant Functor of A,B
(A,B,R) is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,R,R)
T is Element of the carrier of A
N is Element of the carrier of A
<^T,N^> is set
the Arrows of A is non empty Relation-like [: the carrier of A, the carrier of A:] -defined Function-like V17([: the carrier of A, the carrier of A:]) set
[: the carrier of A, the carrier of A:] is non empty Relation-like set
the Arrows of A . (T,N) is set
[T,N] is V1() set
the Arrows of A . [T,N] is set
R . T is Element of the carrier of B
the carrier of B is non empty set
R . N is Element of the carrier of B
M is Element of <^T,N^>
R . M is Element of <^(R . T),(R . N)^>
<^(R . T),(R . N)^> is set
the Arrows of B is non empty Relation-like [: the carrier of B, the carrier of B:] -defined Function-like V17([: the carrier of B, the carrier of B:]) set
[: the carrier of B, the carrier of B:] is non empty Relation-like set
the Arrows of B . ((R . T),(R . N)) is set
[(R . T),(R . N)] is V1() set
the Arrows of B . [(R . T),(R . N)] is set
(A,B,R,R,(A,B,R),N) is Element of <^(R . N),(R . N)^>
<^(R . N),(R . N)^> is set
the Arrows of B . ((R . N),(R . N)) is set
[(R . N),(R . N)] is V1() set
the Arrows of B . [(R . N),(R . N)] is set
(A,B,R,R,(A,B,R),N) * (R . M) is Element of <^(R . T),(R . N)^>
(A,B,R,R,(A,B,R),T) is Element of <^(R . T),(R . T)^>
<^(R . T),(R . T)^> is set
the Arrows of B . ((R . T),(R . T)) is set
[(R . T),(R . T)] is V1() set
the Arrows of B . [(R . T),(R . T)] is set
(R . M) * (A,B,R,R,(A,B,R),T) is Element of <^(R . T),(R . N)^>
A is non empty transitive with_units V103() AltCatStr
B is non empty transitive with_units V103() AltCatStr
C1 is reflexive feasible Covariant id-preserving comp-preserving covariant Functor of A,B
A is non empty transitive V99() with_units V103() AltCatStr
B is non empty transitive V99() with_units V103() AltCatStr
the carrier of A is non empty set
C1 is reflexive feasible Covariant id-preserving comp-preserving covariant Functor of A,B
C2 is reflexive feasible Covariant id-preserving comp-preserving covariant Functor of A,B
R is reflexive feasible Covariant id-preserving comp-preserving covariant Functor of A,B
T is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,C2)
N is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C2,R)
(A,B,C1,C2,R,T,N) is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,R)
M is Element of the carrier of A
O is Element of the carrier of A
<^M,O^> is set
the Arrows of A is non empty Relation-like [: the carrier of A, the carrier of A:] -defined Function-like V17([: the carrier of A, the carrier of A:]) set
[: the carrier of A, the carrier of A:] is non empty Relation-like set
the Arrows of A . (M,O) is set
[M,O] is V1() set
the Arrows of A . [M,O] is set
C1 . M is Element of the carrier of B
the carrier of B is non empty set
C1 . O is Element of the carrier of B
R . O is Element of the carrier of B
(A,B,C1,R,(A,B,C1,C2,R,T,N),O) is Element of <^(C1 . O),(R . O)^>
<^(C1 . O),(R . O)^> is set
the Arrows of B is non empty Relation-like [: the carrier of B, the carrier of B:] -defined Function-like V17([: the carrier of B, the carrier of B:]) set
[: the carrier of B, the carrier of B:] is non empty Relation-like set
the Arrows of B . ((C1 . O),(R . O)) is set
[(C1 . O),(R . O)] is V1() set
the Arrows of B . [(C1 . O),(R . O)] is set
R . M is Element of the carrier of B
(A,B,C1,R,(A,B,C1,C2,R,T,N),M) is Element of <^(C1 . M),(R . M)^>
<^(C1 . M),(R . M)^> is set
the Arrows of B . ((C1 . M),(R . M)) is set
[(C1 . M),(R . M)] is V1() set
the Arrows of B . [(C1 . M),(R . M)] is set
C2 . O is Element of the carrier of B
<^(C1 . O),(C2 . O)^> is set
the Arrows of B . ((C1 . O),(C2 . O)) is set
[(C1 . O),(C2 . O)] is V1() set
the Arrows of B . [(C1 . O),(C2 . O)] is set
C2 . M is Element of the carrier of B
<^(C1 . M),(C2 . M)^> is set
the Arrows of B . ((C1 . M),(C2 . M)) is set
[(C1 . M),(C2 . M)] is V1() set
the Arrows of B . [(C1 . M),(C2 . M)] is set
<^(C2 . O),(R . O)^> is set
the Arrows of B . ((C2 . O),(R . O)) is set
[(C2 . O),(R . O)] is V1() set
the Arrows of B . [(C2 . O),(R . O)] is set
<^(C2 . M),(R . M)^> is set
the Arrows of B . ((C2 . M),(R . M)) is set
[(C2 . M),(R . M)] is V1() set
the Arrows of B . [(C2 . M),(R . M)] is set
<^(C1 . M),(C1 . O)^> is set
the Arrows of B . ((C1 . M),(C1 . O)) is set
[(C1 . M),(C1 . O)] is V1() set
the Arrows of B . [(C1 . M),(C1 . O)] is set
P is Element of <^M,O^>
C1 . P is Element of <^(C1 . M),(C1 . O)^>
(A,B,C1,R,(A,B,C1,C2,R,T,N),O) * (C1 . P) is Element of <^(C1 . M),(R . O)^>
<^(C1 . M),(R . O)^> is set
the Arrows of B . ((C1 . M),(R . O)) is set
[(C1 . M),(R . O)] is V1() set
the Arrows of B . [(C1 . M),(R . O)] is set
R . P is Element of <^(R . M),(R . O)^>
<^(R . M),(R . O)^> is set
the Arrows of B . ((R . M),(R . O)) is set
[(R . M),(R . O)] is V1() set
the Arrows of B . [(R . M),(R . O)] is set
(R . P) * (A,B,C1,R,(A,B,C1,C2,R,T,N),M) is Element of <^(C1 . M),(R . O)^>
<^(C2 . M),(C2 . O)^> is set
the Arrows of B . ((C2 . M),(C2 . O)) is set
[(C2 . M),(C2 . O)] is V1() set
the Arrows of B . [(C2 . M),(C2 . O)] is set
(A,B,C1,C2,T,O) is Element of <^(C1 . O),(C2 . O)^>
(A,B,C2,R,N,O) is Element of <^(C2 . O),(R . O)^>
(A,B,C2,R,N,O) * (A,B,C1,C2,T,O) is Element of <^(C1 . O),(R . O)^>
((A,B,C2,R,N,O) * (A,B,C1,C2,T,O)) * (C1 . P) is Element of <^(C1 . M),(R . O)^>
(A,B,C1,C2,T,O) * (C1 . P) is Element of <^(C1 . M),(C2 . O)^>
<^(C1 . M),(C2 . O)^> is set
the Arrows of B . ((C1 . M),(C2 . O)) is set
[(C1 . M),(C2 . O)] is V1() set
the Arrows of B . [(C1 . M),(C2 . O)] is set
(A,B,C2,R,N,O) * ((A,B,C1,C2,T,O) * (C1 . P)) is Element of <^(C1 . M),(R . O)^>
(A,B,C1,C2,T,M) is Element of <^(C1 . M),(C2 . M)^>
C2 . P is Element of <^(C2 . M),(C2 . O)^>
(C2 . P) * (A,B,C1,C2,T,M) is Element of <^(C1 . M),(C2 . O)^>
(A,B,C2,R,N,O) * ((C2 . P) * (A,B,C1,C2,T,M)) is Element of <^(C1 . M),(R . O)^>
(A,B,C2,R,N,O) * (C2 . P) is Element of <^(C2 . M),(R . O)^>
<^(C2 . M),(R . O)^> is set
the Arrows of B . ((C2 . M),(R . O)) is set
[(C2 . M),(R . O)] is V1() set
the Arrows of B . [(C2 . M),(R . O)] is set
((A,B,C2,R,N,O) * (C2 . P)) * (A,B,C1,C2,T,M) is Element of <^(C1 . M),(R . O)^>
(A,B,C2,R,N,M) is Element of <^(C2 . M),(R . M)^>
(R . P) * (A,B,C2,R,N,M) is Element of <^(C2 . M),(R . O)^>
((R . P) * (A,B,C2,R,N,M)) * (A,B,C1,C2,T,M) is Element of <^(C1 . M),(R . O)^>
(A,B,C2,R,N,M) * (A,B,C1,C2,T,M) is Element of <^(C1 . M),(R . M)^>
(R . P) * ((A,B,C2,R,N,M) * (A,B,C1,C2,T,M)) is Element of <^(C1 . M),(R . O)^>
A is non empty transitive V99() with_units V103() AltCatStr
B is non empty transitive V99() with_units V103() AltCatStr
C1 is reflexive feasible Covariant id-preserving comp-preserving covariant Functor of A,B
C2 is reflexive feasible Covariant id-preserving comp-preserving covariant Functor of A,B
R is reflexive feasible Covariant id-preserving comp-preserving covariant Functor of A,B
the carrier of A is non empty set
T is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,C2)
N is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C2,R)
(A,B,C1,C2,R,T,N) is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,R)
M is Element of the carrier of A
O is Element of the carrier of A
<^M,O^> is set
the Arrows of A is non empty Relation-like [: the carrier of A, the carrier of A:] -defined Function-like V17([: the carrier of A, the carrier of A:]) set
[: the carrier of A, the carrier of A:] is non empty Relation-like set
the Arrows of A . (M,O) is set
[M,O] is V1() set
the Arrows of A . [M,O] is set
C1 . M is Element of the carrier of B
the carrier of B is non empty set
C1 . O is Element of the carrier of B
R . O is Element of the carrier of B
P is Element of <^M,O^>
C1 . P is Element of <^(C1 . M),(C1 . O)^>
<^(C1 . M),(C1 . O)^> is set
the Arrows of B is non empty Relation-like [: the carrier of B, the carrier of B:] -defined Function-like V17([: the carrier of B, the carrier of B:]) set
[: the carrier of B, the carrier of B:] is non empty Relation-like set
the Arrows of B . ((C1 . M),(C1 . O)) is set
[(C1 . M),(C1 . O)] is V1() set
the Arrows of B . [(C1 . M),(C1 . O)] is set
(A,B,C1,R,(A,B,C1,C2,R,T,N),O) is Element of <^(C1 . O),(R . O)^>
<^(C1 . O),(R . O)^> is set
the Arrows of B . ((C1 . O),(R . O)) is set
[(C1 . O),(R . O)] is V1() set
the Arrows of B . [(C1 . O),(R . O)] is set
(A,B,C1,R,(A,B,C1,C2,R,T,N),O) * (C1 . P) is Element of <^(C1 . M),(R . O)^>
<^(C1 . M),(R . O)^> is set
the Arrows of B . ((C1 . M),(R . O)) is set
[(C1 . M),(R . O)] is V1() set
the Arrows of B . [(C1 . M),(R . O)] is set
R . M is Element of the carrier of B
(A,B,C1,R,(A,B,C1,C2,R,T,N),M) is Element of <^(C1 . M),(R . M)^>
<^(C1 . M),(R . M)^> is set
the Arrows of B . ((C1 . M),(R . M)) is set
[(C1 . M),(R . M)] is V1() set
the Arrows of B . [(C1 . M),(R . M)] is set
R . P is Element of <^(R . M),(R . O)^>
<^(R . M),(R . O)^> is set
the Arrows of B . ((R . M),(R . O)) is set
[(R . M),(R . O)] is V1() set
the Arrows of B . [(R . M),(R . O)] is set
(R . P) * (A,B,C1,R,(A,B,C1,C2,R,T,N),M) is Element of <^(C1 . M),(R . O)^>
A is non empty transitive with_units V103() AltCatStr
B is non empty transitive with_units V103() AltCatStr
C1 is reflexive feasible Covariant id-preserving comp-preserving covariant Functor of A,B
C2 is reflexive feasible Covariant id-preserving comp-preserving covariant Functor of A,B
the carrier of A is non empty set
A is non empty transitive with_units V103() AltCatStr
B is non empty transitive with_units V103() AltCatStr
C1 is reflexive feasible Covariant id-preserving comp-preserving covariant Functor of A,B
(A,B,C1) is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,C1)
the carrier of A is non empty set
C2 is Element of the carrier of A
R is Element of the carrier of A
<^C2,R^> is set
the Arrows of A is non empty Relation-like [: the carrier of A, the carrier of A:] -defined Function-like V17([: the carrier of A, the carrier of A:]) set
[: the carrier of A, the carrier of A:] is non empty Relation-like set
the Arrows of A . (C2,R) is set
[C2,R] is V1() set
the Arrows of A . [C2,R] is set
C1 . C2 is Element of the carrier of B
the carrier of B is non empty set
C1 . R is Element of the carrier of B
T is Element of <^C2,R^>
C1 . T is Element of <^(C1 . C2),(C1 . R)^>
<^(C1 . C2),(C1 . R)^> is set
the Arrows of B is non empty Relation-like [: the carrier of B, the carrier of B:] -defined Function-like V17([: the carrier of B, the carrier of B:]) set
[: the carrier of B, the carrier of B:] is non empty Relation-like set
the Arrows of B . ((C1 . C2),(C1 . R)) is set
[(C1 . C2),(C1 . R)] is V1() set
the Arrows of B . [(C1 . C2),(C1 . R)] is set
(A,B,C1,C1,(A,B,C1),R) is Element of <^(C1 . R),(C1 . R)^>
<^(C1 . R),(C1 . R)^> is set
the Arrows of B . ((C1 . R),(C1 . R)) is set
[(C1 . R),(C1 . R)] is V1() set
the Arrows of B . [(C1 . R),(C1 . R)] is set
(A,B,C1,C1,(A,B,C1),R) * (C1 . T) is Element of <^(C1 . C2),(C1 . R)^>
(A,B,C1,C1,(A,B,C1),C2) is Element of <^(C1 . C2),(C1 . C2)^>
<^(C1 . C2),(C1 . C2)^> is set
the Arrows of B . ((C1 . C2),(C1 . C2)) is set
[(C1 . C2),(C1 . C2)] is V1() set
the Arrows of B . [(C1 . C2),(C1 . C2)] is set
(C1 . T) * (A,B,C1,C1,(A,B,C1),C2) is Element of <^(C1 . C2),(C1 . R)^>
A is non empty transitive V99() with_units V103() AltCatStr
B is non empty transitive V99() with_units V103() AltCatStr
C1 is reflexive feasible Covariant id-preserving comp-preserving covariant Functor of A,B
C2 is reflexive feasible Covariant id-preserving comp-preserving covariant Functor of A,B
R is reflexive feasible Covariant id-preserving comp-preserving covariant Functor of A,B
the carrier of A is non empty set
T is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,C2)
N is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C2,R)
(A,B,C1,C2,R,T,N) is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,R)
M is Element of the carrier of A
O is Element of the carrier of A
<^M,O^> is set
the Arrows of A is non empty Relation-like [: the carrier of A, the carrier of A:] -defined Function-like V17([: the carrier of A, the carrier of A:]) set
[: the carrier of A, the carrier of A:] is non empty Relation-like set
the Arrows of A . (M,O) is set
[M,O] is V1() set
the Arrows of A . [M,O] is set
i is Element of the carrier of A
j is Element of the carrier of A
<^i,j^> is set
the Arrows of A . (i,j) is set
[i,j] is V1() set
the Arrows of A . [i,j] is set
C1 . M is Element of the carrier of B
the carrier of B is non empty set
C1 . O is Element of the carrier of B
C2 . O is Element of the carrier of B
P is Element of <^M,O^>
C1 . P is Element of <^(C1 . M),(C1 . O)^>
<^(C1 . M),(C1 . O)^> is set
the Arrows of B is non empty Relation-like [: the carrier of B, the carrier of B:] -defined Function-like V17([: the carrier of B, the carrier of B:]) set
[: the carrier of B, the carrier of B:] is non empty Relation-like set
the Arrows of B . ((C1 . M),(C1 . O)) is set
[(C1 . M),(C1 . O)] is V1() set
the Arrows of B . [(C1 . M),(C1 . O)] is set
(A,B,C1,C2,T,O) is Element of <^(C1 . O),(C2 . O)^>
<^(C1 . O),(C2 . O)^> is set
the Arrows of B . ((C1 . O),(C2 . O)) is set
[(C1 . O),(C2 . O)] is V1() set
the Arrows of B . [(C1 . O),(C2 . O)] is set
(A,B,C1,C2,T,O) * (C1 . P) is Element of <^(C1 . M),(C2 . O)^>
<^(C1 . M),(C2 . O)^> is set
the Arrows of B . ((C1 . M),(C2 . O)) is set
[(C1 . M),(C2 . O)] is V1() set
the Arrows of B . [(C1 . M),(C2 . O)] is set
C2 . M is Element of the carrier of B
(A,B,C1,C2,T,M) is Element of <^(C1 . M),(C2 . M)^>
<^(C1 . M),(C2 . M)^> is set
the Arrows of B . ((C1 . M),(C2 . M)) is set
[(C1 . M),(C2 . M)] is V1() set
the Arrows of B . [(C1 . M),(C2 . M)] is set
C2 . P is Element of <^(C2 . M),(C2 . O)^>
<^(C2 . M),(C2 . O)^> is set
the Arrows of B . ((C2 . M),(C2 . O)) is set
[(C2 . M),(C2 . O)] is V1() set
the Arrows of B . [(C2 . M),(C2 . O)] is set
(C2 . P) * (A,B,C1,C2,T,M) is Element of <^(C1 . M),(C2 . O)^>
C2 . i is Element of the carrier of B
C2 . j is Element of the carrier of B
R . j is Element of the carrier of B
k is Element of <^i,j^>
C2 . k is Element of <^(C2 . i),(C2 . j)^>
<^(C2 . i),(C2 . j)^> is set
the Arrows of B . ((C2 . i),(C2 . j)) is set
[(C2 . i),(C2 . j)] is V1() set
the Arrows of B . [(C2 . i),(C2 . j)] is set
(A,B,C2,R,N,j) is Element of <^(C2 . j),(R . j)^>
<^(C2 . j),(R . j)^> is set
the Arrows of B . ((C2 . j),(R . j)) is set
[(C2 . j),(R . j)] is V1() set
the Arrows of B . [(C2 . j),(R . j)] is set
(A,B,C2,R,N,j) * (C2 . k) is Element of <^(C2 . i),(R . j)^>
<^(C2 . i),(R . j)^> is set
the Arrows of B . ((C2 . i),(R . j)) is set
[(C2 . i),(R . j)] is V1() set
the Arrows of B . [(C2 . i),(R . j)] is set
R . i is Element of the carrier of B
(A,B,C2,R,N,i) is Element of <^(C2 . i),(R . i)^>
<^(C2 . i),(R . i)^> is set
the Arrows of B . ((C2 . i),(R . i)) is set
[(C2 . i),(R . i)] is V1() set
the Arrows of B . [(C2 . i),(R . i)] is set
R . k is Element of <^(R . i),(R . j)^>
<^(R . i),(R . j)^> is set
the Arrows of B . ((R . i),(R . j)) is set
[(R . i),(R . j)] is V1() set
the Arrows of B . [(R . i),(R . j)] is set
(R . k) * (A,B,C2,R,N,i) is Element of <^(C2 . i),(R . j)^>
M is Element of the carrier of A
O is Element of the carrier of A
<^M,O^> is set
the Arrows of A is non empty Relation-like [: the carrier of A, the carrier of A:] -defined Function-like V17([: the carrier of A, the carrier of A:]) set
[: the carrier of A, the carrier of A:] is non empty Relation-like set
the Arrows of A . (M,O) is set
[M,O] is V1() set
the Arrows of A . [M,O] is set
C1 . M is Element of the carrier of B
the carrier of B is non empty set
C1 . O is Element of the carrier of B
R . O is Element of the carrier of B
P is Element of <^M,O^>
C1 . P is Element of <^(C1 . M),(C1 . O)^>
<^(C1 . M),(C1 . O)^> is set
the Arrows of B is non empty Relation-like [: the carrier of B, the carrier of B:] -defined Function-like V17([: the carrier of B, the carrier of B:]) set
[: the carrier of B, the carrier of B:] is non empty Relation-like set
the Arrows of B . ((C1 . M),(C1 . O)) is set
[(C1 . M),(C1 . O)] is V1() set
the Arrows of B . [(C1 . M),(C1 . O)] is set
(A,B,C1,R,(A,B,C1,C2,R,T,N),O) is Element of <^(C1 . O),(R . O)^>
<^(C1 . O),(R . O)^> is set
the Arrows of B . ((C1 . O),(R . O)) is set
[(C1 . O),(R . O)] is V1() set
the Arrows of B . [(C1 . O),(R . O)] is set
(A,B,C1,R,(A,B,C1,C2,R,T,N),O) * (C1 . P) is Element of <^(C1 . M),(R . O)^>
<^(C1 . M),(R . O)^> is set
the Arrows of B . ((C1 . M),(R . O)) is set
[(C1 . M),(R . O)] is V1() set
the Arrows of B . [(C1 . M),(R . O)] is set
R . M is Element of the carrier of B
(A,B,C1,R,(A,B,C1,C2,R,T,N),M) is Element of <^(C1 . M),(R . M)^>
<^(C1 . M),(R . M)^> is set
the Arrows of B . ((C1 . M),(R . M)) is set
[(C1 . M),(R . M)] is V1() set
the Arrows of B . [(C1 . M),(R . M)] is set
R . P is Element of <^(R . M),(R . O)^>
<^(R . M),(R . O)^> is set
the Arrows of B . ((R . M),(R . O)) is set
[(R . M),(R . O)] is V1() set
the Arrows of B . [(R . M),(R . O)] is set
(R . P) * (A,B,C1,R,(A,B,C1,C2,R,T,N),M) is Element of <^(C1 . M),(R . O)^>
M is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,R)
O is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,R)
A is non empty transitive with_units V103() AltCatStr
B is non empty transitive with_units V103() AltCatStr
the carrier of A is non empty set
C1 is reflexive feasible Covariant id-preserving comp-preserving covariant Functor of A,B
C2 is reflexive feasible Covariant id-preserving comp-preserving covariant Functor of A,B
(A,B,C2) is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C2,C2)
(A,B,C1) is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,C1)
R is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,C2)
(A,B,C1,C2,C2,R,(A,B,C2)) is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,C2)
(A,B,C1,C1,C2,(A,B,C1),R) is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,C2)
A is non empty transitive with_units V103() AltCatStr
B is non empty transitive with_units V103() AltCatStr
the carrier of A is non empty set
C1 is reflexive feasible Covariant id-preserving comp-preserving covariant Functor of A,B
C2 is reflexive feasible Covariant id-preserving comp-preserving covariant Functor of A,B
R is reflexive feasible Covariant id-preserving comp-preserving covariant Functor of A,B
T is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,C2)
N is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C2,R)
(A,B,C1,C2,R,T,N) is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,R)
M is Element of the carrier of A
(A,B,C1,R,(A,B,C1,C2,R,T,N),M) is Element of <^(C1 . M),(R . M)^>
C1 . M is Element of the carrier of B
the carrier of B is non empty set
R . M is Element of the carrier of B
<^(C1 . M),(R . M)^> is set
the Arrows of B is non empty Relation-like [: the carrier of B, the carrier of B:] -defined Function-like V17([: the carrier of B, the carrier of B:]) set
[: the carrier of B, the carrier of B:] is non empty Relation-like set
the Arrows of B . ((C1 . M),(R . M)) is set
[(C1 . M),(R . M)] is V1() set
the Arrows of B . [(C1 . M),(R . M)] is set
C2 . M is Element of the carrier of B
(A,B,C1,C2,T,M) is Element of <^(C1 . M),(C2 . M)^>
<^(C1 . M),(C2 . M)^> is set
the Arrows of B . ((C1 . M),(C2 . M)) is set
[(C1 . M),(C2 . M)] is V1() set
the Arrows of B . [(C1 . M),(C2 . M)] is set
(A,B,C2,R,N,M) is Element of <^(C2 . M),(R . M)^>
<^(C2 . M),(R . M)^> is set
the Arrows of B . ((C2 . M),(R . M)) is set
[(C2 . M),(R . M)] is V1() set
the Arrows of B . [(C2 . M),(R . M)] is set
(A,B,C2,R,N,M) * (A,B,C1,C2,T,M) is Element of <^(C1 . M),(R . M)^>
A is non empty transitive V99() with_units V103() AltCatStr
B is non empty transitive V99() with_units V103() AltCatStr
the carrier of A is non empty set
C1 is reflexive feasible Covariant id-preserving comp-preserving covariant Functor of A,B
C2 is reflexive feasible Covariant id-preserving comp-preserving covariant Functor of A,B
R is reflexive feasible Covariant id-preserving comp-preserving covariant Functor of A,B
T is reflexive feasible Covariant id-preserving comp-preserving covariant Functor of A,B
N is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,C2)
M is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C2,R)
(A,B,C1,C2,R,N,M) is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,R)
O is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,R,T)
(A,B,C2,R,T,M,O) is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C2,T)
(A,B,C1,C2,T,N,(A,B,C2,R,T,M,O)) is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,T)
(A,B,C1,R,T,(A,B,C1,C2,R,N,M),O) is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,T)
(A,B,C1,C2,T,N,(A,B,C2,R,T,M,O)) is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,T)
(A,B,C2,R,T,M,O) is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C2,T)
(A,B,C1,C2,T,N,(A,B,C2,R,T,M,O)) is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,T)
(A,B,C1,C2,R,N,M) is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,R)
(A,B,C1,R,T,(A,B,C1,C2,R,N,M),O) is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,T)
(A,B,C1,R,T,(A,B,C1,C2,R,N,M),O) is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,C1,T)
A is set
C1 is Relation-like A -defined Function-like V17(A) set
B is Relation-like A -defined Function-like V17(A) set
C2 is Relation-like A -defined Function-like V17(A) set
product C2 is set
R is set
proj1 C2 is set
T is Relation-like Function-like set
proj1 T is set
N is set
T . N is set
B . N is set
C1 . N is set
[:(B . N),(C1 . N):] is Relation-like set
bool [:(B . N),(C1 . N):] is non empty set
C2 . N is set
Funcs ((B . N),(C1 . N)) is set
N is Relation-like A -defined Function-like V17(A) set
T is Relation-like A -defined Function-like V17(A) set
N is set
T . N is set
B . N is set
C1 . N is set
Funcs ((B . N),(C1 . N)) is set
[:(B . N),(C1 . N):] is Relation-like set
bool [:(B . N),(C1 . N):] is non empty set
N is set
T . N is set
C2 . N is set
B . N is set
C1 . N is set
Funcs ((B . N),(C1 . N)) is set
proj1 C2 is set
N is set
T . N is set
C2 . N is set
proj1 T is set
C2 is set
C1 . C2 is set
B . C2 is set
C2 is set
R is set
T is set
T is set
C1 . T is set
B . T is set
A is non empty transitive with_units V103() AltCatStr
B is non empty transitive with_units V103() AltCatStr
the carrier of A is non empty set
[: the carrier of A, the carrier of A:] is non empty Relation-like set
the carrier of B is non empty set
[: the carrier of B, the carrier of B:] is non empty Relation-like set
Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]) is non empty FUNCTION_DOMAIN of [: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]
the Arrows of B is non empty Relation-like [: the carrier of B, the carrier of B:] -defined Function-like V17([: the carrier of B, the carrier of B:]) set
{ (b₁ * the Arrows of B) where b₁ is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of B, the carrier of B:] -valued Function-like quasi_total Element of Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]) : verum } is set
the Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of B, the carrier of B:] -valued Function-like quasi_total Element of Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]) is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of B, the carrier of B:] -valued Function-like quasi_total Element of Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:])
the Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of B, the carrier of B:] -valued Function-like quasi_total Element of Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]) * the Arrows of B is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like set
[:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:] is non empty Relation-like set
bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:] is non empty set
the Arrows of A is non empty Relation-like [: the carrier of A, the carrier of A:] -defined Function-like V17([: the carrier of A, the carrier of A:]) set
N is set
P is non empty Relation-like [: the carrier of A, the carrier of A:] -defined Function-like V17([: the carrier of A, the carrier of A:]) set
M is set
([: the carrier of A, the carrier of A:], the Arrows of A,P) is set
i is non empty Relation-like [: the carrier of A, the carrier of A:] -defined Function-like V17([: the carrier of A, the carrier of A:]) set
O is set
([: the carrier of A, the carrier of A:], the Arrows of A,i) is set
T is non empty set
N is set
M is set
O is set
P is set
i is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of B, the carrier of B:] -valued Function-like quasi_total Covariant Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:]
j is non empty Relation-like [: the carrier of A, the carrier of A:] -defined Function-like V17([: the carrier of A, the carrier of A:]) V41() MSUnTrans of i, the Arrows of A, the Arrows of B
[i,j] is V1() set
FunctorStr(# i,j #) is strict FunctorStr over A,B
k is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of B, the carrier of B:] -valued Function-like quasi_total Covariant Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:]
h is non empty Relation-like [: the carrier of A, the carrier of A:] -defined Function-like V17([: the carrier of A, the carrier of A:]) V41() MSUnTrans of k, the Arrows of A, the Arrows of B
[k,h] is V1() set
FunctorStr(# k,h #) is strict FunctorStr over A,B
union N is set
[:(Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:])),(union N):] is Relation-like set
M is set
O is set
i is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of B, the carrier of B:] -valued Function-like quasi_total Covariant Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:]
P is set
j is non empty Relation-like [: the carrier of A, the carrier of A:] -defined Function-like V17([: the carrier of A, the carrier of A:]) V41() MSUnTrans of i, the Arrows of A, the Arrows of B
[i,j] is V1() set
FunctorStr(# i,j #) is strict FunctorStr over A,B
P is reflexive feasible strict Covariant id-preserving comp-preserving covariant Functor of A,B
the ObjectMap of P is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of B, the carrier of B:] -valued Function-like quasi_total Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:]
i is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of B, the carrier of B:] -valued Function-like quasi_total Covariant Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:]
the MorphMap of P is non empty Relation-like [: the carrier of A, the carrier of A:] -defined Function-like V17([: the carrier of A, the carrier of A:]) V41() MSUnTrans of the ObjectMap of P, the Arrows of A, the Arrows of B
j is non empty Relation-like [: the carrier of A, the carrier of A:] -defined Function-like V17([: the carrier of A, the carrier of A:]) V41() MSUnTrans of i, the Arrows of A, the Arrows of B
[i,j] is V1() set
h is Element of the carrier of A
g is Element of the carrier of A
the Arrows of A . (h,g) is set
[h,g] is V1() set
the Arrows of A . [h,g] is set
i . (h,g) is Element of [: the carrier of B, the carrier of B:]
i . [h,g] is set
the Arrows of B . (i . (h,g)) is set
<^h,g^> is set
h is Element of the carrier of A
g is Element of the carrier of A
the Arrows of A . (h,g) is set
[h,g] is V1() set
the Arrows of A . [h,g] is set
P . h is Element of the carrier of B
P . g is Element of the carrier of B
[(P . h),(P . g)] is V1() Element of [: the carrier of B, the carrier of B:]
the Arrows of B . [(P . h),(P . g)] is set
i . (h,g) is Element of [: the carrier of B, the carrier of B:]
i . [h,g] is set
k is set
i * the Arrows of B is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like set
f is set
the Arrows of A . f is set
i . f is set
the Arrows of B . (i . f) is set
T is set
i9 is set
[T,i9] is V1() set
i . (T,i9) is set
i . [T,i9] is set
the Arrows of B . (i . (T,i9)) is set
j9 is Element of the carrier of A
P . j9 is Element of the carrier of B
k9 is Element of the carrier of A
P . k9 is Element of the carrier of B
[(P . j9),(P . k9)] is V1() Element of [: the carrier of B, the carrier of B:]
the Arrows of B . [(P . j9),(P . k9)] is set
the Arrows of A . (T,i9) is set
the Arrows of A . [T,i9] is set
g is non empty Relation-like [: the carrier of A, the carrier of A:] -defined Function-like V17([: the carrier of A, the carrier of A:]) set
f is set
the Arrows of A . f is set
g . f is set
i . f is set
the Arrows of B . (i . f) is set
f is set
g . f is set
the Arrows of A . f is set
([: the carrier of A, the carrier of A:], the Arrows of A,g) is set
C1 is set
C2 is set
R is set
A is non empty transitive V99() with_units V103() AltCatStr
B is non empty transitive V99() with_units V103() AltCatStr
(A,B) is set
the carrier of A is non empty set
[:(A,B),(A,B):] is Relation-like set
C1 is set
C2 is set
R is set
[C2,R] is V1() set
T is reflexive feasible strict Covariant id-preserving comp-preserving covariant Functor of A,B
N is reflexive feasible strict Covariant id-preserving comp-preserving covariant Functor of A,B
M is Element of the carrier of A
T . M is Element of the carrier of B
the carrier of B is non empty set
N . M is Element of the carrier of B
<^(T . M),(N . M)^> is set
the Arrows of B is non empty Relation-like [: the carrier of B, the carrier of B:] -defined Function-like V17([: the carrier of B, the carrier of B:]) set
[: the carrier of B, the carrier of B:] is non empty Relation-like set
the Arrows of B . ((T . M),(N . M)) is set
[(T . M),(N . M)] is V1() set
the Arrows of B . [(T . M),(N . M)] is set
M is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) set
product M is set
O is set
P is reflexive feasible strict Covariant id-preserving comp-preserving covariant Functor of A,B
i is reflexive feasible strict Covariant id-preserving comp-preserving covariant Functor of A,B
[P,i] is V1() set
j is set
h is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) set
g is set
h . g is set
M . g is set
f is Element of the carrier of A
M . f is set
T . f is Element of the carrier of B
the carrier of B is non empty set
N . f is Element of the carrier of B
<^(T . f),(N . f)^> is set
the Arrows of B is non empty Relation-like [: the carrier of B, the carrier of B:] -defined Function-like V17([: the carrier of B, the carrier of B:]) set
[: the carrier of B, the carrier of B:] is non empty Relation-like set
the Arrows of B . ((T . f),(N . f)) is set
[(T . f),(N . f)] is V1() set
the Arrows of B . [(T . f),(N . f)] is set
h . f is set
proj1 M is non empty set
g is set
h . g is set
M . g is set
proj1 h is non empty set
C1 is Relation-like [:(A,B),(A,B):] -defined Function-like V17([:(A,B),(A,B):]) set
[:(A,B),(A,B),(A,B):] is set
{|C1,C1|} is Relation-like [:(A,B),(A,B),(A,B):] -defined Function-like V17([:(A,B),(A,B),(A,B):]) set
{|C1|} is Relation-like [:(A,B),(A,B),(A,B):] -defined Function-like V17([:(A,B),(A,B),(A,B):]) set
C2 is set
{|C1,C1|} . C2 is set
{|C1|} . C2 is set
[:[:(A,B),(A,B):],(A,B):] is Relation-like set
R is set
T is set
[R,T] is V1() set
N is set
M is set
[N,M] is V1() set
[N,M,T] is V1() V2() set
[[N,M],T] is V1() set
O is non empty set
P is Element of O
i is Element of O
j is Element of O
[P,i,j] is V1() V2() Element of [:O,O,O:]
[:O,O,O:] is non empty set
[P,i] is V1() set
[[P,i],j] is V1() set
{|C1|} . [P,i,j] is set
{|C1|} . (P,i,j) is set
C1 . (P,j) is set
[P,j] is V1() set
C1 . [P,j] is set
{|C1,C1|} . [P,i,j] is set
{|C1,C1|} . (P,i,j) is set
C1 . (i,j) is set
[i,j] is V1() set
C1 . [i,j] is set
C1 . (P,i) is set
C1 . [P,i] is set
[:(C1 . (i,j)),(C1 . (P,i)):] is Relation-like set
f is set
k is reflexive feasible strict Covariant id-preserving comp-preserving covariant Functor of A,B
g is reflexive feasible strict Covariant id-preserving comp-preserving covariant Functor of A,B
[k,g] is V1() set
T is set
i9 is set
[T,i9] is V1() set
[i,j] is V1() Element of [:O,O:]
[:O,O:] is non empty Relation-like set
C1 . [i,j] is set
h is reflexive feasible strict Covariant id-preserving comp-preserving covariant Functor of A,B
[P,i] is V1() Element of [:O,O:]
C1 . [P,i] is set
k9 is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,k,h)
j9 is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,h,g)
(A,B,k,h,g,k9,j9) is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,k,g)
t2 is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,k,g)
t1 is reflexive feasible strict Covariant id-preserving comp-preserving covariant Functor of A,B
a is reflexive feasible strict Covariant id-preserving comp-preserving covariant Functor of A,B
b is reflexive feasible strict Covariant id-preserving comp-preserving covariant Functor of A,B
[t1,a,b] is V1() V2() set
[t1,a] is V1() set
[[t1,a],b] is V1() set
b is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,t1,a)
t2 is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,a,b)
[t2,b] is V1() set
(A,B,t1,a,b,b,t2) is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,t1,b)
a is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,a,b)
C1 . [k,g] is set
k is set
C2 is Relation-like [:(A,B),(A,B),(A,B):] -defined Function-like V17([:(A,B),(A,B),(A,B):]) V41() ManySortedFunction of {|C1,C1|},{|C1|}
AltCatStr(# (A,B),C1,C2 #) is strict AltCatStr
the reflexive feasible strict Covariant id-preserving comp-preserving covariant Functor of A,B is reflexive feasible strict Covariant id-preserving comp-preserving covariant Functor of A,B
the carrier of AltCatStr(# (A,B),C1,C2 #) is set
T is Element of the carrier of AltCatStr(# (A,B),C1,C2 #)
N is Element of the carrier of AltCatStr(# (A,B),C1,C2 #)
<^T,N^> is set
the Arrows of AltCatStr(# (A,B),C1,C2 #) is Relation-like [: the carrier of AltCatStr(# (A,B),C1,C2 #), the carrier of AltCatStr(# (A,B),C1,C2 #):] -defined Function-like V17([: the carrier of AltCatStr(# (A,B),C1,C2 #), the carrier of AltCatStr(# (A,B),C1,C2 #):]) set
[: the carrier of AltCatStr(# (A,B),C1,C2 #), the carrier of AltCatStr(# (A,B),C1,C2 #):] is Relation-like set
the Arrows of AltCatStr(# (A,B),C1,C2 #) . (T,N) is set
[T,N] is V1() set
the Arrows of AltCatStr(# (A,B),C1,C2 #) . [T,N] is set
M is Element of the carrier of AltCatStr(# (A,B),C1,C2 #)
<^N,M^> is set
the Arrows of AltCatStr(# (A,B),C1,C2 #) . (N,M) is set
[N,M] is V1() set
the Arrows of AltCatStr(# (A,B),C1,C2 #) . [N,M] is set
<^T,M^> is set
the Arrows of AltCatStr(# (A,B),C1,C2 #) . (T,M) is set
[T,M] is V1() set
the Arrows of AltCatStr(# (A,B),C1,C2 #) . [T,M] is set
C1 . [N,M] is set
j is set
P is reflexive feasible strict Covariant id-preserving comp-preserving covariant Functor of A,B
i is reflexive feasible strict Covariant id-preserving comp-preserving covariant Functor of A,B
C1 . [T,N] is set
h is set
O is reflexive feasible strict Covariant id-preserving comp-preserving covariant Functor of A,B
g is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,O,P)
k is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,P,i)
(A,B,O,P,i,g,k) is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,O,i)
T is non empty transitive strict AltCatStr
the carrier of T is non empty set
the Arrows of T is non empty Relation-like [: the carrier of T, the carrier of T:] -defined Function-like V17([: the carrier of T, the carrier of T:]) set
[: the carrier of T, the carrier of T:] is non empty Relation-like set
the Comp of T is non empty Relation-like [: the carrier of T, the carrier of T, the carrier of T:] -defined Function-like V17([: the carrier of T, the carrier of T, the carrier of T:]) V41() ManySortedFunction of {| the Arrows of T, the Arrows of T|},{| the Arrows of T|}
[: the carrier of T, the carrier of T, the carrier of T:] is non empty set
{| the Arrows of T, the Arrows of T|} is non empty Relation-like [: the carrier of T, the carrier of T, the carrier of T:] -defined Function-like V17([: the carrier of T, the carrier of T, the carrier of T:]) set
{| the Arrows of T|} is non empty Relation-like [: the carrier of T, the carrier of T, the carrier of T:] -defined Function-like V17([: the carrier of T, the carrier of T, the carrier of T:]) set
N is reflexive feasible strict Covariant id-preserving comp-preserving covariant Functor of A,B
M is reflexive feasible strict Covariant id-preserving comp-preserving covariant Functor of A,B
the Arrows of T . (N,M) is set
[N,M] is V1() set
the Arrows of T . [N,M] is set
O is set
N is reflexive feasible strict Covariant id-preserving comp-preserving covariant Functor of A,B
M is reflexive feasible strict Covariant id-preserving comp-preserving covariant Functor of A,B
O is reflexive feasible strict Covariant id-preserving comp-preserving covariant Functor of A,B
the Comp of T . (N,M,O) is set
P is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,N,M)
i is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,M,O)
(A,B,N,M,O,P,i) is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,N,O)
[N,M] is V1() set
[M,O] is V1() set
C1 . [M,O] is set
j is non empty set
k is Element of j
h is Element of j
g is Element of j
[k,h,g] is V1() V2() Element of [:j,j,j:]
[:j,j,j:] is non empty set
[k,h] is V1() set
[[k,h],g] is V1() set
{|C1,C1|} . [k,h,g] is set
{|C1,C1|} . (k,h,g) is set
C1 . (h,g) is set
[h,g] is V1() set
C1 . [h,g] is set
C1 . (k,h) is set
C1 . [k,h] is set
[:(C1 . (h,g)),(C1 . (k,h)):] is Relation-like set
[:[:(A,B),(A,B):],(A,B):] is Relation-like set
[N,M,O] is V1() V2() set
[[N,M],O] is V1() set
{|C1,C1|} . [N,M,O] is set
{|C1|} . [N,M,O] is set
[:({|C1,C1|} . [N,M,O]),({|C1|} . [N,M,O]):] is Relation-like set
bool [:({|C1,C1|} . [N,M,O]),({|C1|} . [N,M,O]):] is non empty set
C2 . [N,M,O] is set
f is Relation-like {|C1,C1|} . [N,M,O] -defined {|C1|} . [N,M,O] -valued Function-like quasi_total Element of bool [:({|C1,C1|} . [N,M,O]),({|C1|} . [N,M,O]):]
C1 . [N,M] is set
[i,P] is V1() set
f . (i,P) is set
f . [i,P] is set
C2 . (N,M,O) is set
C1 is non empty transitive strict AltCatStr
the carrier of C1 is non empty set
the Arrows of C1 is non empty Relation-like [: the carrier of C1, the carrier of C1:] -defined Function-like V17([: the carrier of C1, the carrier of C1:]) set
[: the carrier of C1, the carrier of C1:] is non empty Relation-like set
the Comp of C1 is non empty Relation-like [: the carrier of C1, the carrier of C1, the carrier of C1:] -defined Function-like V17([: the carrier of C1, the carrier of C1, the carrier of C1:]) V41() ManySortedFunction of {| the Arrows of C1, the Arrows of C1|},{| the Arrows of C1|}
[: the carrier of C1, the carrier of C1, the carrier of C1:] is non empty set
{| the Arrows of C1, the Arrows of C1|} is non empty Relation-like [: the carrier of C1, the carrier of C1, the carrier of C1:] -defined Function-like V17([: the carrier of C1, the carrier of C1, the carrier of C1:]) set
{| the Arrows of C1|} is non empty Relation-like [: the carrier of C1, the carrier of C1, the carrier of C1:] -defined Function-like V17([: the carrier of C1, the carrier of C1, the carrier of C1:]) set
C2 is non empty transitive strict AltCatStr
the carrier of C2 is non empty set
the Arrows of C2 is non empty Relation-like [: the carrier of C2, the carrier of C2:] -defined Function-like V17([: the carrier of C2, the carrier of C2:]) set
[: the carrier of C2, the carrier of C2:] is non empty Relation-like set
the Comp of C2 is non empty Relation-like [: the carrier of C2, the carrier of C2, the carrier of C2:] -defined Function-like V17([: the carrier of C2, the carrier of C2, the carrier of C2:]) V41() ManySortedFunction of {| the Arrows of C2, the Arrows of C2|},{| the Arrows of C2|}
[: the carrier of C2, the carrier of C2, the carrier of C2:] is non empty set
{| the Arrows of C2, the Arrows of C2|} is non empty Relation-like [: the carrier of C2, the carrier of C2, the carrier of C2:] -defined Function-like V17([: the carrier of C2, the carrier of C2, the carrier of C2:]) set
{| the Arrows of C2|} is non empty Relation-like [: the carrier of C2, the carrier of C2, the carrier of C2:] -defined Function-like V17([: the carrier of C2, the carrier of C2, the carrier of C2:]) set
i is set
j is set
the Arrows of C1 . (i,j) is set
[i,j] is V1() set
the Arrows of C1 . [i,j] is set
the Arrows of C2 . (i,j) is set
the Arrows of C2 . [i,j] is set
g is set
h is reflexive feasible strict Covariant id-preserving comp-preserving covariant Functor of A,B
k is reflexive feasible strict Covariant id-preserving comp-preserving covariant Functor of A,B
i is set
j is set
k is set
the Comp of C1 . (i,j,k) is set
the Comp of C2 . (i,j,k) is set
the Arrows of C1 . (i,j) is set
[i,j] is V1() set
the Arrows of C1 . [i,j] is set
the Arrows of C1 . (j,k) is set
[j,k] is V1() set
the Arrows of C1 . [j,k] is set
T is non empty set
the Arrows of C2 . (i,j) is set
the Arrows of C2 . [i,j] is set
j9 is Element of T
k9 is Element of T
the Arrows of C2 . (j9,k9) is set
[j9,k9] is V1() set
the Arrows of C2 . [j9,k9] is set
i9 is Element of T
the Arrows of C2 . (i9,j9) is set
[i9,j9] is V1() set
the Arrows of C2 . [i9,j9] is set
[:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):] is Relation-like set
[i9,j9,k9] is V1() V2() Element of [:T,T,T:]
[:T,T,T:] is non empty set
[[i9,j9],k9] is V1() set
{| the Arrows of C2, the Arrows of C2|} . [i9,j9,k9] is set
{| the Arrows of C2, the Arrows of C2|} . (i9,j9,k9) is set
{| the Arrows of C2|} . [i9,j9,k9] is set
{| the Arrows of C2|} . (i9,j9,k9) is set
the Arrows of C2 . (i9,k9) is set
[i9,k9] is V1() set
the Arrows of C2 . [i9,k9] is set
the Comp of C2 . [i9,j9,k9] is set
the Comp of C2 . (i9,j9,k9) is set
[:[:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):],( the Arrows of C2 . (i9,k9)):] is Relation-like set
bool [:[:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):],( the Arrows of C2 . (i9,k9)):] is non empty set
the Comp of C1 . [i9,j9,k9] is set
the Comp of C1 . (i9,j9,k9) is set
T is non empty set
the Arrows of C2 . (j,k) is set
the Arrows of C2 . [j,k] is set
j9 is Element of T
k9 is Element of T
the Arrows of C2 . (j9,k9) is set
[j9,k9] is V1() set
the Arrows of C2 . [j9,k9] is set
i9 is Element of T
the Arrows of C2 . (i9,j9) is set
[i9,j9] is V1() set
the Arrows of C2 . [i9,j9] is set
[:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):] is Relation-like set
[i9,j9,k9] is V1() V2() Element of [:T,T,T:]
[:T,T,T:] is non empty set
[[i9,j9],k9] is V1() set
{| the Arrows of C2, the Arrows of C2|} . [i9,j9,k9] is set
{| the Arrows of C2, the Arrows of C2|} . (i9,j9,k9) is set
{| the Arrows of C2|} . [i9,j9,k9] is set
{| the Arrows of C2|} . (i9,j9,k9) is set
the Arrows of C2 . (i9,k9) is set
[i9,k9] is V1() set
the Arrows of C2 . [i9,k9] is set
the Comp of C2 . [i9,j9,k9] is set
the Comp of C2 . (i9,j9,k9) is set
[:[:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):],( the Arrows of C2 . (i9,k9)):] is Relation-like set
bool [:[:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):],( the Arrows of C2 . (i9,k9)):] is non empty set
the Comp of C1 . [i9,j9,k9] is set
the Comp of C1 . (i9,j9,k9) is set
the Arrows of C1 . (i,j) is set
[i,j] is V1() set
the Arrows of C1 . [i,j] is set
the Arrows of C1 . (j,k) is set
[j,k] is V1() set
the Arrows of C1 . [j,k] is set
T is non empty set
i9 is Element of T
j9 is Element of T
k9 is Element of T
[i9,j9,k9] is V1() V2() Element of [:T,T,T:]
[:T,T,T:] is non empty set
[i9,j9] is V1() set
[[i9,j9],k9] is V1() set
{| the Arrows of C2, the Arrows of C2|} . [i9,j9,k9] is set
{| the Arrows of C2, the Arrows of C2|} . (i9,j9,k9) is set
the Arrows of C2 . (j9,k9) is set
[j9,k9] is V1() set
the Arrows of C2 . [j9,k9] is set
the Arrows of C2 . (i9,j9) is set
the Arrows of C2 . [i9,j9] is set
[:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):] is Relation-like set
{| the Arrows of C2|} . [i9,j9,k9] is set
{| the Arrows of C2|} . (i9,j9,k9) is set
the Arrows of C2 . (i9,k9) is set
[i9,k9] is V1() set
the Arrows of C2 . [i9,k9] is set
the Comp of C2 . [i9,j9,k9] is set
the Comp of C2 . (i9,j9,k9) is set
the Arrows of C2 . (j,k) is set
the Arrows of C2 . [j,k] is set
the Arrows of C2 . (i,j) is set
the Arrows of C2 . [i,j] is set
[:( the Arrows of C2 . (j,k)),( the Arrows of C2 . (i,j)):] is Relation-like set
the Arrows of C2 . (i,k) is set
[i,k] is V1() set
the Arrows of C2 . [i,k] is set
[:[:( the Arrows of C2 . (j,k)),( the Arrows of C2 . (i,j)):],( the Arrows of C2 . (i,k)):] is Relation-like set
bool [:[:( the Arrows of C2 . (j,k)),( the Arrows of C2 . (i,j)):],( the Arrows of C2 . (i,k)):] is non empty set
the Comp of C1 . [i9,j9,k9] is set
the Comp of C1 . (i9,j9,k9) is set
t1 is Relation-like [:( the Arrows of C2 . (j,k)),( the Arrows of C2 . (i,j)):] -defined the Arrows of C2 . (i,k) -valued Function-like quasi_total Element of bool [:[:( the Arrows of C2 . (j,k)),( the Arrows of C2 . (i,j)):],( the Arrows of C2 . (i,k)):]
t2 is Relation-like [:( the Arrows of C2 . (j,k)),( the Arrows of C2 . (i,j)):] -defined the Arrows of C2 . (i,k) -valued Function-like quasi_total Element of bool [:[:( the Arrows of C2 . (j,k)),( the Arrows of C2 . (i,j)):],( the Arrows of C2 . (i,k)):]
a is Element of the Arrows of C2 . (j,k)
b is Element of the Arrows of C2 . (i,j)
t1 . (a,b) is set
[a,b] is V1() set
t1 . [a,b] is set
t2 . (a,b) is set
t2 . [a,b] is set
g is reflexive feasible strict Covariant id-preserving comp-preserving covariant Functor of A,B
h is reflexive feasible strict Covariant id-preserving comp-preserving covariant Functor of A,B
f is reflexive feasible strict Covariant id-preserving comp-preserving covariant Functor of A,B
the Comp of C1 . (f,g,h) is set
a is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,g,h)
b is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,f,g)
(A,B,f,g,h,b,a) is non empty Relation-like the carrier of A -defined Function-like V17( the carrier of A) (A,B,f,h)
the Comp of C2 . (f,g,h) is set
t2 is Relation-like Function-like set
t2 . (a,b) is set
[a,b] is V1() set
t2 . [a,b] is set
c₂₈ is Relation-like Function-like set
c₂₈ . (a,b) is set
c₂₈ . [a,b] is set
the Arrows of C1 . (i,j) is set
[i,j] is V1() set
the Arrows of C1 . [i,j] is set
the Arrows of C1 . (j,k) is set
[j,k] is V1() set
the Arrows of C1 . [j,k] is set