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