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

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

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

(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

(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

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

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

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

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

(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

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

(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

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

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

product C2 is set
R is set
proj1 C2 is 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 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
{ (b1 * the Arrows of B) where b1 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:])),():] 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

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,