:: INDEX_1 semantic presentation

K124() is Element of bool K120()

K120() is set

bool K120() is set

K119() is set

bool K119() is set

bool K124() is set

{} is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V86() set

1 is non empty set

{{},1} is non empty set

C is non empty set

the non empty Relation-like non-empty non empty-yielding C -defined Function-like total set is non empty Relation-like non-empty non empty-yielding C -defined Function-like total set

the Element of C is Element of C

the non empty Relation-like non-empty non empty-yielding C -defined Function-like total set . the Element of C is non empty set

C is non empty non void V52() Category-like V65() V66() V67() with_identities with_triple-like_morphisms Categorial CatStr

the carrier' of C is non empty set

I is Element of the carrier' of C

I `2 is set

I `11 is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of (I `11) is non empty set

I `12 is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of (I `12) is non empty set

dom I is Element of the carrier of C

the carrier of C is non empty set

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like V18( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is Relation-like set

bool [: the carrier' of C, the carrier of C:] is set

the Source of C . I is Element of the carrier of C

cat (I `11) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

cat (I `12) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

I `2 is Relation-like the carrier' of (cat (dom I)) -defined the carrier' of (cat (cod I)) -valued Function-like V18( the carrier' of (cat (dom I)), the carrier' of (cat (cod I))) Functor of cat (dom I), cat (cod I)

cat (dom I) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of (cat (dom I)) is non empty set

cod I is Element of the carrier of C

the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like V18( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

the Target of C . I is Element of the carrier of C

cat (cod I) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of (cat (cod I)) is non empty set

C is non empty non void V52() Category-like V65() V66() V67() with_identities with_triple-like_morphisms Categorial CatStr

the carrier' of C is non empty set

D is Element of the carrier' of C

dom D is Element of the carrier of C

the carrier of C is non empty set

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like V18( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is Relation-like set

bool [: the carrier' of C, the carrier of C:] is set

the Source of C . D is Element of the carrier of C

I is Element of the carrier' of C

cod I is Element of the carrier of C

the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like V18( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

the Target of C . I is Element of the carrier of C

D (*) I is Element of the carrier' of C

dom I is Element of the carrier of C

the Source of C . I is Element of the carrier of C

cod D is Element of the carrier of C

the Target of C . D is Element of the carrier of C

[(dom I),(cod D)] is V1() Element of the carrier of [:C,C:]

[:C,C:] is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier of [:C,C:] is non empty set

{(dom I),(cod D)} is non empty set

{(dom I)} is non empty set

{{(dom I),(cod D)},{(dom I)}} is non empty set

I `11 is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of (I `11) is non empty set

I `12 is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of (I `12) is non empty set

D `11 is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of (D `11) is non empty set

D `12 is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of (D `12) is non empty set

(C,I) is Relation-like the carrier' of (I `11) -defined the carrier' of (I `12) -valued Function-like V18( the carrier' of (I `11), the carrier' of (I `12)) Functor of I `11 ,I `12

(C,D) is Relation-like the carrier' of (D `11) -defined the carrier' of (D `12) -valued Function-like V18( the carrier' of (D `11), the carrier' of (D `12)) Functor of D `11 ,D `12

(C,D) * (C,I) is Relation-like the carrier' of (I `11) -defined the carrier' of (D `12) -valued Function-like Element of bool [: the carrier' of (I `11), the carrier' of (D `12):]

[: the carrier' of (I `11), the carrier' of (D `12):] is Relation-like set

bool [: the carrier' of (I `11), the carrier' of (D `12):] is set

[[(dom I),(cod D)],((C,D) * (C,I))] is V1() set

{[(dom I),(cod D)],((C,D) * (C,I))} is non empty set

{[(dom I),(cod D)]} is non empty Relation-like Function-like set

{{[(dom I),(cod D)],((C,D) * (C,I))},{[(dom I),(cod D)]}} is non empty set

[(dom I),(cod I)] is V1() Element of the carrier of [:C,C:]

{(dom I),(cod I)} is non empty set

{{(dom I),(cod I)},{(dom I)}} is non empty set

J is Relation-like the carrier' of (I `11) -defined the carrier' of (D `11) -valued Function-like V18( the carrier' of (I `11), the carrier' of (D `11)) Functor of I `11 ,D `11

[[(dom I),(cod I)],J] is V1() set

{[(dom I),(cod I)],J} is non empty set

{[(dom I),(cod I)]} is non empty Relation-like Function-like set

{{[(dom I),(cod I)],J},{[(dom I),(cod I)]}} is non empty set

[(dom D),(cod D)] is V1() Element of the carrier of [:C,C:]

{(dom D),(cod D)} is non empty set

{(dom D)} is non empty set

{{(dom D),(cod D)},{(dom D)}} is non empty set

E is Relation-like the carrier' of (D `11) -defined the carrier' of (D `12) -valued Function-like V18( the carrier' of (D `11), the carrier' of (D `12)) Functor of D `11 ,D `12

[[(dom D),(cod D)],E] is V1() set

{[(dom D),(cod D)],E} is non empty set

{[(dom D),(cod D)]} is non empty Relation-like Function-like set

{{[(dom D),(cod D)],E},{[(dom D),(cod D)]}} is non empty set

E * J is Relation-like the carrier' of (I `11) -defined the carrier' of (I `11) -defined the carrier' of (D `12) -valued the carrier' of (D `12) -valued Function-like V18( the carrier' of (I `11), the carrier' of (D `12)) Functor of I `11 ,D `12

[[(dom I),(cod D)],(E * J)] is V1() set

{[(dom I),(cod D)],(E * J)} is non empty set

{{[(dom I),(cod D)],(E * J)},{[(dom I),(cod D)]}} is non empty set

E * (C,I) is Relation-like the carrier' of (I `11) -defined the carrier' of (D `12) -valued Function-like Element of bool [: the carrier' of (I `11), the carrier' of (D `12):]

[[(dom I),(cod D)],(E * (C,I))] is V1() set

{[(dom I),(cod D)],(E * (C,I))} is non empty set

{{[(dom I),(cod D)],(E * (C,I))},{[(dom I),(cod D)]}} is non empty set

C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of C is non empty set

the carrier of C is non empty set

I is non empty non void V52() Category-like V65() V66() V67() with_identities with_triple-like_morphisms Categorial CatStr

the carrier' of I is non empty set

D is non empty non void V52() Category-like V65() V66() V67() with_identities with_triple-like_morphisms Categorial CatStr

the carrier' of D is non empty set

the carrier of I is non empty set

the carrier of D is non empty set

J is Relation-like the carrier' of C -defined the carrier' of I -valued Function-like V18( the carrier' of C, the carrier' of I) Functor of C,I

Obj J is Relation-like the carrier of C -defined the carrier of I -valued Function-like V18( the carrier of C, the carrier of I) Element of bool [: the carrier of C, the carrier of I:]

[: the carrier of C, the carrier of I:] is Relation-like set

bool [: the carrier of C, the carrier of I:] is set

E is Relation-like the carrier' of C -defined the carrier' of D -valued Function-like V18( the carrier' of C, the carrier' of D) Functor of C,D

Obj E is Relation-like the carrier of C -defined the carrier of D -valued Function-like V18( the carrier of C, the carrier of D) Element of bool [: the carrier of C, the carrier of D:]

[: the carrier of C, the carrier of D:] is Relation-like set

bool [: the carrier of C, the carrier of D:] is set

K is set

F is Element of the carrier of C

id F is Morphism of F,F

dom (id F) is Element of the carrier of C

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like V18( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is Relation-like set

bool [: the carrier' of C, the carrier of C:] is set

the Source of C . (id F) is Element of the carrier of C

(Obj J) . K is set

J . (id F) is Element of the carrier' of I

dom (J . (id F)) is Element of the carrier of I

the Source of I is Relation-like the carrier' of I -defined the carrier of I -valued Function-like V18( the carrier' of I, the carrier of I) Element of bool [: the carrier' of I, the carrier of I:]

[: the carrier' of I, the carrier of I:] is Relation-like set

bool [: the carrier' of I, the carrier of I:] is set

the Source of I . (J . (id F)) is Element of the carrier of I

(J . (id F)) `11 is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

E . (id F) is Element of the carrier' of D

dom (E . (id F)) is Element of the carrier of D

the Source of D is Relation-like the carrier' of D -defined the carrier of D -valued Function-like V18( the carrier' of D, the carrier of D) Element of bool [: the carrier' of D, the carrier of D:]

[: the carrier' of D, the carrier of D:] is Relation-like set

bool [: the carrier' of D, the carrier of D:] is set

the Source of D . (E . (id F)) is Element of the carrier of D

(Obj E) . K is set

proj1 (Obj J) is set

proj1 (Obj E) is set

1Cat ({},1) is non empty trivial V46() non void V51(1) V52() trivial' strict Category-like V65() V66() V67() with_identities CatStr

{{}} is non empty functional set

{1} is non empty set

1 :-> {} is Relation-like {1} -defined {{}} -valued Function-like one-to-one V18({1},{{}}) Function-yielding V86() Element of bool [:{1},{{}}:]

[:{1},{{}}:] is Relation-like set

bool [:{1},{{}}:] is set

{1} --> {} is non empty Relation-like {1} -defined {{}} -valued Function-like constant total V18({1},{{}}) Function-yielding V86() Element of bool [:{1},{{}}:]

(1,1) :-> 1 is Relation-like [:{1},{1}:] -defined {1} -valued Function-like V18([:{1},{1}:],{1}) Element of bool [:[:{1},{1}:],{1}:]

[:{1},{1}:] is Relation-like set

[:[:{1},{1}:],{1}:] is Relation-like set

bool [:[:{1},{1}:],{1}:] is set

[1,1] is V1() set

{1,1} is non empty set

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

{[1,1]} is non empty Relation-like Function-like set

{[1,1]} --> 1 is non empty Relation-like non-empty non empty-yielding {[1,1]} -defined {1} -valued Function-like constant total V18({[1,1]},{1}) Element of bool [:{[1,1]},{1}:]

[:{[1,1]},{1}:] is Relation-like set

bool [:{[1,1]},{1}:] is set

CatStr(# {{}},{1},(1 :-> {}),(1 :-> {}),((1,1) :-> 1) #) is non empty non void V52() strict CatStr

{(1Cat ({},1))} is non empty set

[:{},{(1Cat ({},1))}:] is Relation-like set

bool [:{},{(1Cat ({},1))}:] is set

{} --> (1Cat ({},1)) is empty Relation-like non-empty empty-yielding {} -defined {(1Cat ({},1))} -valued Function-like one-to-one constant functional total V18( {} ,{(1Cat ({},1))}) Function-yielding V86() Element of bool [:{},{(1Cat ({},1))}:]

C is empty Relation-like non-empty empty-yielding {} -defined {(1Cat ({},1))} -valued Function-like one-to-one constant functional total V18( {} ,{(1Cat ({},1))}) Function-yielding V86() Element of bool [:{},{(1Cat ({},1))}:]

I is set

proj1 C is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V86() set

C . I is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V86() set

C is set

1Cat ({},1) is non empty trivial V46() non void V51(1) V52() trivial' strict Category-like V65() V66() V67() with_identities CatStr

{{}} is non empty functional set

{1} is non empty set

1 :-> {} is Relation-like {1} -defined {{}} -valued Function-like one-to-one V18({1},{{}}) Function-yielding V86() Element of bool [:{1},{{}}:]

[:{1},{{}}:] is Relation-like set

bool [:{1},{{}}:] is set

{1} --> {} is non empty Relation-like {1} -defined {{}} -valued Function-like constant total V18({1},{{}}) Function-yielding V86() Element of bool [:{1},{{}}:]

(1,1) :-> 1 is Relation-like [:{1},{1}:] -defined {1} -valued Function-like V18([:{1},{1}:],{1}) Element of bool [:[:{1},{1}:],{1}:]

[:{1},{1}:] is Relation-like set

[:[:{1},{1}:],{1}:] is Relation-like set

bool [:[:{1},{1}:],{1}:] is set

[1,1] is V1() set

{1,1} is non empty set

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

{[1,1]} is non empty Relation-like Function-like set

{[1,1]} --> 1 is non empty Relation-like non-empty non empty-yielding {[1,1]} -defined {1} -valued Function-like constant total V18({[1,1]},{1}) Element of bool [:{[1,1]},{1}:]

[:{[1,1]},{1}:] is Relation-like set

bool [:{[1,1]},{1}:] is set

CatStr(# {{}},{1},(1 :-> {}),(1 :-> {}),((1,1) :-> 1) #) is non empty non void V52() strict CatStr

{(1Cat ({},1))} is non empty set

[:C,{(1Cat ({},1))}:] is Relation-like set

bool [:C,{(1Cat ({},1))}:] is set

C --> (1Cat ({},1)) is Relation-like C -defined {(1Cat ({},1))} -valued Function-like constant total V18(C,{(1Cat ({},1))}) Element of bool [:C,{(1Cat ({},1))}:]

I is Relation-like C -defined {(1Cat ({},1))} -valued Function-like constant total V18(C,{(1Cat ({},1))}) Element of bool [:C,{(1Cat ({},1))}:]

D is set

proj1 I is set

I . D is set

C is set

I is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

C --> I is Relation-like C -defined {I} -valued Function-like constant total V18(C,{I}) Element of bool [:C,{I}:]

{I} is non empty set

[:C,{I}:] is Relation-like set

bool [:C,{I}:] is set

D is set

proj1 (C --> I) is set

(C --> I) . D is set

C is non empty set

I is non empty Relation-like C -defined Function-like total set

C is Relation-like Function-like () set

proj2 C is set

I is set

proj1 C is set

D is set

C . D is set

C is non empty set

I is non empty Relation-like C -defined Function-like total () set

D is Element of C

I . D is set

proj1 I is non empty set

C is Relation-like Function-like set

I is Relation-like Function-like () set

C * I is Relation-like Function-like set

D is set

proj1 (C * I) is set

(C * I) . D is set

C . D is set

I . (C . D) is set

proj1 I is set

C is Relation-like Function-like () set

proj1 C is set

I is set

C . I is set

D is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier of D is non empty set

J is set

E is set

K is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier of K is non empty set

I is Relation-like Function-like set

proj1 I is set

D is set

I . D is set

C . D is set

J is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier of J is non empty set

I is Relation-like non-empty Function-like set

proj1 I is set

D is Relation-like non-empty Function-like set

proj1 D is set

J is set

C . J is set

I . J is set

E is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier of E is non empty set

D . J is set

I is set

C . I is set

D is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of D is non empty set

J is set

E is set

K is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of K is non empty set

I is Relation-like Function-like set

proj1 I is set

D is set

I . D is set

C . D is set

J is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of J is non empty set

I is Relation-like non-empty Function-like set

proj1 I is set

D is Relation-like non-empty Function-like set

proj1 D is set

J is set

C . J is set

I . J is set

E is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of E is non empty set

D . J is set

C is non empty set

I is non empty Relation-like C -defined Function-like total () set

(I) is Relation-like non-empty Function-like set

proj1 (I) is set

proj1 I is non empty set

(I) is Relation-like non-empty Function-like set

proj1 (I) is set

proj1 I is non empty set

C is non empty set

I is non empty Relation-like C -defined Function-like total () set

(I) is Relation-like non-empty C -defined Function-like set

proj1 (I) is set

proj1 I is non empty set

(I) is Relation-like non-empty C -defined Function-like set

proj1 (I) is set

proj1 I is non empty set

C is set

I is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

C --> I is Relation-like C -defined {I} -valued Function-like constant total V18(C,{I}) () Element of bool [:C,{I}:]

{I} is non empty set

[:C,{I}:] is Relation-like set

bool [:C,{I}:] is set

((C --> I)) is Relation-like non-empty Function-like set

the carrier of I is non empty set

C --> the carrier of I is Relation-like non-empty C -defined { the carrier of I} -valued Function-like constant total V18(C,{ the carrier of I}) Element of bool [:C,{ the carrier of I}:]

{ the carrier of I} is non empty set

[:C,{ the carrier of I}:] is Relation-like set

bool [:C,{ the carrier of I}:] is set

((C --> I)) is Relation-like non-empty Function-like set

the carrier' of I is non empty set

C --> the carrier' of I is Relation-like non-empty C -defined { the carrier' of I} -valued Function-like constant total V18(C,{ the carrier' of I}) Element of bool [:C,{ the carrier' of I}:]

{ the carrier' of I} is non empty set

[:C,{ the carrier' of I}:] is Relation-like set

bool [:C,{ the carrier' of I}:] is set

proj1 (C --> I) is set

proj1 ((C --> I)) is set

D is set

(C --> I) . D is set

((C --> I)) . D is set

proj1 ((C --> I)) is set

D is set

(C --> I) . D is set

((C --> I)) . D is set

C is set

I is set

the Relation-like C -defined Function-like total set is Relation-like C -defined Function-like total set

the Relation-like I -defined Function-like total set is Relation-like I -defined Function-like total set

[ the Relation-like C -defined Function-like total set , the Relation-like I -defined Function-like total set ] is V1() set

{ the Relation-like C -defined Function-like total set , the Relation-like I -defined Function-like total set } is non empty functional set

{ the Relation-like C -defined Function-like total set } is non empty functional set

{{ the Relation-like C -defined Function-like total set , the Relation-like I -defined Function-like total set },{ the Relation-like C -defined Function-like total set }} is non empty set

C is set

I is set

D is Relation-like C -defined Function-like total set

J is Relation-like I -defined Function-like total set

[D,J] is V1() set

{D,J} is non empty functional set

{D} is non empty functional set

{{D,J},{D}} is non empty set

C is set

I is set

D is (C,I)

D `1 is set

J is Relation-like C -defined Function-like total set

E is Relation-like I -defined Function-like total set

(C,I,J,E) is V1() (C,I)

{J,E} is non empty functional set

{J} is non empty functional set

{{J,E},{J}} is non empty set

D `2 is set

J is Relation-like C -defined Function-like total set

E is Relation-like I -defined Function-like total set

(C,I,J,E) is V1() (C,I)

{J,E} is non empty functional set

{J} is non empty functional set

{{J,E},{J}} is non empty set

C is set

I is set

D is (C,I)

D `1 is Relation-like Function-like set

J is Relation-like C -defined Function-like total set

E is Relation-like I -defined Function-like total set

(C,I,J,E) is V1() (C,I)

{J,E} is non empty functional set

{J} is non empty functional set

{{J,E},{J}} is non empty set

D `2 is Relation-like Function-like set

J is Relation-like C -defined Function-like total set

E is Relation-like I -defined Function-like total set

(C,I,J,E) is V1() (C,I)

{J,E} is non empty functional set

{J} is non empty functional set

{{J,E},{J}} is non empty set

C is set

I is set

D is (C,I)

D `1 is Relation-like C -defined Function-like set

J is Relation-like C -defined Function-like set

E is Relation-like C -defined Function-like total set

K is Relation-like I -defined Function-like total set

(C,I,E,K) is V1() (C,I)

{E,K} is non empty functional set

{E} is non empty functional set

{{E,K},{E}} is non empty set

D `2 is Relation-like I -defined Function-like set

J is Relation-like I -defined Function-like set

E is Relation-like C -defined Function-like total set

K is Relation-like I -defined Function-like total set

(C,I,E,K) is V1() (C,I)

{E,K} is non empty functional set

{E} is non empty functional set

{{E,K},{E}} is non empty set

C is set

I is set

C is set

I is set

the Relation-like I -defined Function-like total Function-yielding V86() set is Relation-like I -defined Function-like total Function-yielding V86() set

the Relation-like C -defined Function-like total () set is Relation-like C -defined Function-like total () set

(C,I, the Relation-like C -defined Function-like total () set , the Relation-like I -defined Function-like total Function-yielding V86() set ) is V1() (C,I)

{ the Relation-like C -defined Function-like total () set , the Relation-like I -defined Function-like total Function-yielding V86() set } is non empty functional set

{ the Relation-like C -defined Function-like total () set } is non empty functional set

{{ the Relation-like C -defined Function-like total () set , the Relation-like I -defined Function-like total Function-yielding V86() set },{ the Relation-like C -defined Function-like total () set }} is non empty set

E is (C,I)

E `1 is Relation-like C -defined Function-like total set

E `2 is Relation-like I -defined Function-like total set

C is set

I is set

D is (C,I) (C,I)

D `1 is Relation-like C -defined Function-like total set

C is set

I is set

D is (C,I) (C,I)

D `2 is Relation-like I -defined Function-like total set

C is Relation-like Function-like Function-yielding V86() set

proj2 C is set

I is set

proj1 C is set

D is set

C . D is Relation-like Function-like set

C is set

I is set

D is Relation-like C -defined Function-like total () set

J is Relation-like I -defined Function-like total Function-yielding V86() set

[D,J] is V1() set

{D,J} is non empty functional set

{D} is non empty functional set

{{D,J},{D}} is non empty set

(C,I,D,J) is V1() (C,I)

(C,I,D,J) `1 is Relation-like C -defined Function-like total set

(C,I,D,J) `2 is Relation-like I -defined Function-like total set

C is non empty set

I is non empty Relation-like C -defined Function-like total () set

D is non empty Relation-like C -defined Function-like total () set

J is set

E is Element of C

(C,I,E) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of (C,I,E) is non empty set

(C,D,E) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of (C,D,E) is non empty set

the Relation-like the carrier' of (C,I,E) -defined the carrier' of (C,D,E) -valued Function-like V18( the carrier' of (C,I,E), the carrier' of (C,D,E)) Functor of (C,I,E),(C,D,E) is Relation-like the carrier' of (C,I,E) -defined the carrier' of (C,D,E) -valued Function-like V18( the carrier' of (C,I,E), the carrier' of (C,D,E)) Functor of (C,I,E),(C,D,E)

F is set

G is set

J is Relation-like Function-like set

proj1 J is set

E is set

J . E is set

K is Element of C

(C,I,K) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of (C,I,K) is non empty set

(C,D,K) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of (C,D,K) is non empty set

F is Relation-like the carrier' of (C,I,K) -defined the carrier' of (C,D,K) -valued Function-like V18( the carrier' of (C,I,K), the carrier' of (C,D,K)) Functor of (C,I,K),(C,D,K)

E is non empty Relation-like C -defined Function-like total Function-yielding V86() set

K is Element of C

E . K is Relation-like Function-like set

(C,I,K) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of (C,I,K) is non empty set

(C,D,K) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of (C,D,K) is non empty set

F is Element of C

(C,I,F) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of (C,I,F) is non empty set

(C,D,F) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of (C,D,F) is non empty set

G is Relation-like the carrier' of (C,I,F) -defined the carrier' of (C,D,F) -valued Function-like V18( the carrier' of (C,I,F), the carrier' of (C,D,F)) Functor of (C,I,F),(C,D,F)

F

F

F

C is non empty Relation-like F

I is set

proj1 C is non empty set

C . I is set

D is Element of F

C . D is set

F

I is non empty Relation-like F

D is Element of F

I . D is Relation-like Function-like set

(F

the carrier' of (F

(F

the carrier' of (F

F

D is non empty Relation-like F

J is Element of F

D . J is Relation-like Function-like set

F

C is non empty set

I is non empty Relation-like C -defined Function-like total () set

D is non empty Relation-like C -defined Function-like total () set

J is non empty Relation-like C -defined Function-like total Function-yielding V86() (C,I,D)

E is Element of C

J . E is Relation-like Function-like set

(C,I,E) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of (C,I,E) is non empty set

(C,D,E) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of (C,D,E) is non empty set

I is non empty set

C is non empty set

[:I,C:] is Relation-like set

bool [:I,C:] is set

D is Relation-like I -defined C -valued Function-like V18(I,C) Element of bool [:I,C:]

J is Relation-like I -defined C -valued Function-like V18(I,C) Element of bool [:I,C:]

the non empty Relation-like C -defined Function-like total () set is non empty Relation-like C -defined Function-like total () set

D * the non empty Relation-like C -defined Function-like total () set is non empty Relation-like I -defined Function-like total () set

J * the non empty Relation-like C -defined Function-like total () set is non empty Relation-like I -defined Function-like total () set

the non empty Relation-like I -defined Function-like total Function-yielding V86() (I,D * the non empty Relation-like C -defined Function-like total () set ,J * the non empty Relation-like C -defined Function-like total () set ) is non empty Relation-like I -defined Function-like total Function-yielding V86() (I,D * the non empty Relation-like C -defined Function-like total () set ,J * the non empty Relation-like C -defined Function-like total () set )

(C,I, the non empty Relation-like C -defined Function-like total () set , the non empty Relation-like I -defined Function-like total Function-yielding V86() (I,D * the non empty Relation-like C -defined Function-like total () set ,J * the non empty Relation-like C -defined Function-like total () set )) is V1() (C,I) (C,I) (C,I)

{ the non empty Relation-like C -defined Function-like total () set , the non empty Relation-like I -defined Function-like total Function-yielding V86() (I,D * the non empty Relation-like C -defined Function-like total () set ,J * the non empty Relation-like C -defined Function-like total () set )} is non empty functional set

{ the non empty Relation-like C -defined Function-like total () set } is non empty functional set

{{ the non empty Relation-like C -defined Function-like total () set , the non empty Relation-like I -defined Function-like total Function-yielding V86() (I,D * the non empty Relation-like C -defined Function-like total () set ,J * the non empty Relation-like C -defined Function-like total () set )},{ the non empty Relation-like C -defined Function-like total () set }} is non empty set

F is V1() (C,I) (C,I) (C,I)

F `2 is non empty Relation-like I -defined Function-like total Function-yielding V86() set

F `1 is non empty Relation-like C -defined Function-like total () set

D * (F `1) is non empty Relation-like I -defined Function-like total () set

J * (F `1) is non empty Relation-like I -defined Function-like total () set

I is non empty set

C is non empty set

[:I,C:] is Relation-like set

bool [:I,C:] is set

D is Relation-like I -defined C -valued Function-like V18(I,C) Element of bool [:I,C:]

J is Relation-like I -defined C -valued Function-like V18(I,C) Element of bool [:I,C:]

E is (C,I) (C,I,D,J)

E `2 is non empty Relation-like I -defined Function-like total set

E `1 is non empty Relation-like C -defined Function-like total () set

D * (E `1) is non empty Relation-like I -defined Function-like total () set

J * (E `1) is non empty Relation-like I -defined Function-like total () set

F is Element of I

(E `2) . F is set

D . F is Element of C

(C,(E `1),(D . F)) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of (C,(E `1),(D . F)) is non empty set

J . F is Element of C

(C,(E `1),(J . F)) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of (C,(E `1),(J . F)) is non empty set

proj1 (D * (E `1)) is non empty set

(I,(D * (E `1)),F) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

K is non empty Relation-like I -defined Function-like total Function-yielding V86() (I,D * (E `1),J * (E `1))

(I,(D * (E `1)),(J * (E `1)),K,F) is Relation-like the carrier' of (I,(D * (E `1)),F) -defined the carrier' of (I,(J * (E `1)),F) -valued Function-like V18( the carrier' of (I,(D * (E `1)),F), the carrier' of (I,(J * (E `1)),F)) Functor of (I,(D * (E `1)),F),(I,(J * (E `1)),F)

the carrier' of (I,(D * (E `1)),F) is non empty set

(I,(J * (E `1)),F) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of (I,(J * (E `1)),F) is non empty set

proj1 (J * (E `1)) is non empty set

C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier of C is non empty set

the carrier' of C is non empty set

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like V18( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is Relation-like set

bool [: the carrier' of C, the carrier of C:] is set

the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like V18( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

I is ( the carrier of C, the carrier' of C) ( the carrier of C, the carrier' of C, the Source of C, the Target of C)

I `2 is non empty Relation-like the carrier' of C -defined Function-like total set

D is Element of the carrier' of C

(I `2) . D is set

I `1 is non empty Relation-like the carrier of C -defined Function-like total () set

dom D is Element of the carrier of C

the Source of C . D is Element of the carrier of C

( the carrier of C,(I `1),(dom D)) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of ( the carrier of C,(I `1),(dom D)) is non empty set

cod D is Element of the carrier of C

the Target of C . D is Element of the carrier of C

( the carrier of C,(I `1),(cod D)) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of ( the carrier of C,(I `1),(cod D)) is non empty set

I is non empty set

C is non empty set

[:I,C:] is Relation-like set

bool [:I,C:] is set

D is Relation-like I -defined C -valued Function-like V18(I,C) Element of bool [:I,C:]

J is Relation-like I -defined C -valued Function-like V18(I,C) Element of bool [:I,C:]

E is (C,I) (C,I,D,J)

E `2 is non empty Relation-like I -defined Function-like total set

E `1 is non empty Relation-like C -defined Function-like total () set

D * (E `1) is non empty Relation-like I -defined Function-like total () set

J * (E `1) is non empty Relation-like I -defined Function-like total () set

I is non empty set

C is non empty set

[:I,C:] is Relation-like set

bool [:I,C:] is set

D is Relation-like I -defined C -valued Function-like V18(I,C) Element of bool [:I,C:]

J is Relation-like I -defined C -valued Function-like V18(I,C) Element of bool [:I,C:]

E is (C,I) (C,I,D,J)

E `1 is non empty Relation-like C -defined Function-like total () set

proj2 (E `1) is non empty categorial set

K is non empty non void V52() strict Category-like V65() V66() V67() with_identities with_triple-like_morphisms Categorial full CatStr

the carrier of K is non empty set

proj1 (E `1) is non empty set

F is non empty non void V52() strict Category-like V65() V66() V67() with_identities with_triple-like_morphisms Categorial full CatStr

the carrier of F is non empty set

G is Element of C

(C,(E `1),G) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

D * (E `1) is non empty Relation-like I -defined Function-like total () set

J * (E `1) is non empty Relation-like I -defined Function-like total () set

(C,I,D,J,E) is non empty Relation-like I -defined Function-like total Function-yielding V86() (I,D * (E `1),J * (E `1))

G is Element of I

(I,(D * (E `1)),(J * (E `1)),(C,I,D,J,E),G) is Relation-like the carrier' of (I,(D * (E `1)),G) -defined the carrier' of (I,(J * (E `1)),G) -valued Function-like V18( the carrier' of (I,(D * (E `1)),G), the carrier' of (I,(J * (E `1)),G)) Functor of (I,(D * (E `1)),G),(I,(J * (E `1)),G)

(I,(D * (E `1)),G) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of (I,(D * (E `1)),G) is non empty set

(I,(J * (E `1)),G) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of (I,(J * (E `1)),G) is non empty set

D . G is Element of C

(C,(E `1),(D . G)) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of (C,(E `1),(D . G)) is non empty set

J . G is Element of C

(C,(E `1),(J . G)) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of (C,(E `1),(J . G)) is non empty set

[(C,(E `1),(D . G)),(C,(E `1),(J . G))] is V1() set

{(C,(E `1),(D . G)),(C,(E `1),(J . G))} is non empty set

{(C,(E `1),(D . G))} is non empty set

{{(C,(E `1),(D . G)),(C,(E `1),(J . G))},{(C,(E `1),(D . G))}} is non empty set

[[(C,(E `1),(D . G)),(C,(E `1),(J . G))],(I,(D * (E `1)),(J * (E `1)),(C,I,D,J,E),G)] is V1() set

{[(C,(E `1),(D . G)),(C,(E `1),(J . G))],(I,(D * (E `1)),(J * (E `1)),(C,I,D,J,E),G)} is non empty set

{[(C,(E `1),(D . G)),(C,(E `1),(J . G))]} is non empty Relation-like Function-like set

{{[(C,(E `1),(D . G)),(C,(E `1),(J . G))],(I,(D * (E `1)),(J * (E `1)),(C,I,D,J,E),G)},{[(C,(E `1),(D . G)),(C,(E `1),(J . G))]}} is non empty set

the carrier' of F is non empty set

I is non empty set

C is non empty set

[:I,C:] is Relation-like set

bool [:I,C:] is set

D is Relation-like I -defined C -valued Function-like V18(I,C) Element of bool [:I,C:]

J is Relation-like I -defined C -valued Function-like V18(I,C) Element of bool [:I,C:]

E is (C,I) (C,I,D,J)

E `1 is non empty Relation-like C -defined Function-like total () set

D * (E `1) is non empty Relation-like I -defined Function-like total () set

J * (E `1) is non empty Relation-like I -defined Function-like total () set

(C,I,D,J,E) is non empty Relation-like I -defined Function-like total Function-yielding V86() (I,D * (E `1),J * (E `1))

K is non empty non void V52() strict Category-like V65() V66() V67() with_identities with_triple-like_morphisms Categorial full CatStr

the carrier of K is non empty set

the carrier' of K is non empty set

I is non empty set

C is non empty set

[:I,C:] is Relation-like set

bool [:I,C:] is set

D is Relation-like I -defined C -valued Function-like V18(I,C) Element of bool [:I,C:]

J is Relation-like I -defined C -valued Function-like V18(I,C) Element of bool [:I,C:]

E is (C,I) (C,I,D,J)

E `1 is non empty Relation-like C -defined Function-like total () set

D * (E `1) is non empty Relation-like I -defined Function-like total () set

J * (E `1) is non empty Relation-like I -defined Function-like total () set

(C,I,D,J,E) is non empty Relation-like I -defined Function-like total Function-yielding V86() (I,D * (E `1),J * (E `1))

K is non empty non void V52() strict Category-like V65() V66() V67() with_identities with_triple-like_morphisms Categorial full CatStr

the carrier of K is non empty set

the carrier' of K is non empty set

I is non empty set

C is non empty set

[:I,C:] is Relation-like set

bool [:I,C:] is set

[:I,I:] is Relation-like set

[:[:I,I:],I:] is Relation-like set

bool [:[:I,I:],I:] is set

[:C,I:] is Relation-like set

bool [:C,I:] is set

D is Relation-like I -defined C -valued Function-like V18(I,C) Element of bool [:I,C:]

J is Relation-like I -defined C -valued Function-like V18(I,C) Element of bool [:I,C:]

E is Relation-like [:I,I:] -defined I -valued Function-like Element of bool [:[:I,I:],I:]

CatStr(# C,I,D,J,E #) is non empty non void V52() strict CatStr

F is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

K is Relation-like C -defined I -valued Function-like V18(C,I) Element of bool [:C,I:]

id F is Relation-like the carrier' of F -defined the carrier' of F -valued Function-like V18( the carrier' of F, the carrier' of F) Functor of F,F

the carrier' of F is non empty set

id the carrier' of F is non empty Relation-like the carrier' of F -defined the carrier' of F -valued Function-like one-to-one total Element of bool [: the carrier' of F, the carrier' of F:]

[: the carrier' of F, the carrier' of F:] is Relation-like set

bool [: the carrier' of F, the carrier' of F:] is set

I --> (id F) is non empty Relation-like I -defined {(id F)} -valued Function-like constant total V18(I,{(id F)}) Function-yielding V86() Element of bool [:I,{(id F)}:]

{(id F)} is non empty functional set

[:I,{(id F)}:] is Relation-like set

bool [:I,{(id F)}:] is set

C --> F is non empty Relation-like C -defined {F} -valued Function-like constant total V18(C,{F}) () Element of bool [:C,{F}:]

{F} is non empty set

[:C,{F}:] is Relation-like set

bool [:C,{F}:] is set

(C,I,(C --> F),(I --> (id F))) is V1() (C,I) (C,I) (C,I)

{(C --> F),(I --> (id F))} is non empty functional set

{(C --> F)} is non empty functional set

{{(C --> F),(I --> (id F))},{(C --> F)}} is non empty set

(C,I,(C --> F),(I --> (id F))) `1 is non empty Relation-like C -defined Function-like total () set

(C,I,(C --> F),(I --> (id F))) `2 is non empty Relation-like I -defined Function-like total Function-yielding V86() set

(C --> F) * D is non empty Relation-like I -defined {F} -valued Function-like total () Element of bool [:I,{F}:]

[:I,{F}:] is Relation-like set

bool [:I,{F}:] is set

(C --> F) * J is non empty Relation-like I -defined {F} -valued Function-like total () Element of bool [:I,{F}:]

GI is Element of I

(I --> (id F)) . GI is Relation-like Function-like set

(I,((C --> F) * D),GI) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of (I,((C --> F) * D),GI) is non empty set

(I,((C --> F) * J),GI) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of (I,((C --> F) * J),GI) is non empty set

D . GI is Element of C

(C,(C --> F),(D . GI)) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

proj1 ((C --> F) * D) is non empty set

(I --> (id F)) . GI is Relation-like Function-like Element of {(id F)}

J . GI is Element of C

(C,(C --> F),(J . GI)) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

proj1 ((C --> F) * J) is non empty set

GI is (C,I) (C,I,D,J)

GI `1 is non empty Relation-like C -defined Function-like total () set

D * (GI `1) is non empty Relation-like I -defined Function-like total () set

J * (GI `1) is non empty Relation-like I -defined Function-like total () set

(C,I,D,J,GI) is non empty Relation-like I -defined Function-like total Function-yielding V86() (I,D * (GI `1),J * (GI `1))

h1 is Element of C

K . h1 is Element of I

(I,(D * (GI `1)),(J * (GI `1)),(C,I,D,J,GI),(K . h1)) is Relation-like the carrier' of (I,(D * (GI `1)),(K . h1)) -defined the carrier' of (I,(J * (GI `1)),(K . h1)) -valued Function-like V18( the carrier' of (I,(D * (GI `1)),(K . h1)), the carrier' of (I,(J * (GI `1)),(K . h1))) Functor of (I,(D * (GI `1)),(K . h1)),(I,(J * (GI `1)),(K . h1))

(I,(D * (GI `1)),(K . h1)) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of (I,(D * (GI `1)),(K . h1)) is non empty set

(I,(J * (GI `1)),(K . h1)) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of (I,(J * (GI `1)),(K . h1)) is non empty set

(C,(GI `1),h1) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

id (C,(GI `1),h1) is Relation-like the carrier' of (C,(GI `1),h1) -defined the carrier' of (C,(GI `1),h1) -valued Function-like V18( the carrier' of (C,(GI `1),h1), the carrier' of (C,(GI `1),h1)) Functor of (C,(GI `1),h1),(C,(GI `1),h1)

the carrier' of (C,(GI `1),h1) is non empty set

id the carrier' of (C,(GI `1),h1) is non empty Relation-like the carrier' of (C,(GI `1),h1) -defined the carrier' of (C,(GI `1),h1) -valued Function-like one-to-one total Element of bool [: the carrier' of (C,(GI `1),h1), the carrier' of (C,(GI `1),h1):]

[: the carrier' of (C,(GI `1),h1), the carrier' of (C,(GI `1),h1):] is Relation-like set

bool [: the carrier' of (C,(GI `1),h1), the carrier' of (C,(GI `1),h1):] is set

h2 is Element of I

D . h2 is Element of C

h1 is Element of I

J . h1 is Element of C

[h2,h1] is V1() set

{h2,h1} is non empty set

{h2} is non empty set

{{h2,h1},{h2}} is non empty set

E . [h2,h1] is set

(C,I,D,J,GI) . (E . [h2,h1]) is Relation-like Function-like set

(I,(D * (GI `1)),h1) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of (I,(D * (GI `1)),h1) is non empty set

(I,(J * (GI `1)),h1) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of (I,(J * (GI `1)),h1) is non empty set

(I,(D * (GI `1)),h2) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of (I,(D * (GI `1)),h2) is non empty set

(I,(J * (GI `1)),h2) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of (I,(J * (GI `1)),h2) is non empty set

(I,(D * (GI `1)),(J * (GI `1)),(C,I,D,J,GI),h1) is Relation-like the carrier' of (I,(D * (GI `1)),h1) -defined the carrier' of (I,(J * (GI `1)),h1) -valued Function-like V18( the carrier' of (I,(D * (GI `1)),h1), the carrier' of (I,(J * (GI `1)),h1)) Functor of (I,(D * (GI `1)),h1),(I,(J * (GI `1)),h1)

(I,(D * (GI `1)),(J * (GI `1)),(C,I,D,J,GI),h2) is Relation-like the carrier' of (I,(D * (GI `1)),h2) -defined the carrier' of (I,(J * (GI `1)),h2) -valued Function-like V18( the carrier' of (I,(D * (GI `1)),h2), the carrier' of (I,(J * (GI `1)),h2)) Functor of (I,(D * (GI `1)),h2),(I,(J * (GI `1)),h2)

(I,(D * (GI `1)),(J * (GI `1)),(C,I,D,J,GI),h2) * (I,(D * (GI `1)),(J * (GI `1)),(C,I,D,J,GI),h1) is Relation-like the carrier' of (I,(D * (GI `1)),h1) -defined the carrier' of (I,(J * (GI `1)),h2) -valued Function-like Element of bool [: the carrier' of (I,(D * (GI `1)),h1), the carrier' of (I,(J * (GI `1)),h2):]

[: the carrier' of (I,(D * (GI `1)),h1), the carrier' of (I,(J * (GI `1)),h2):] is Relation-like set

bool [: the carrier' of (I,(D * (GI `1)),h1), the carrier' of (I,(J * (GI `1)),h2):] is set

f2 is Element of the carrier' of F

cod f2 is Element of the carrier of F

the carrier of F is non empty set

the Target of F is Relation-like the carrier' of F -defined the carrier of F -valued Function-like V18( the carrier' of F, the carrier of F) Element of bool [: the carrier' of F, the carrier of F:]

[: the carrier' of F, the carrier of F:] is Relation-like set

bool [: the carrier' of F, the carrier of F:] is set

the Target of F . f2 is Element of the carrier of F

f1 is Element of the carrier' of F

dom f1 is Element of the carrier of F

the Source of F is Relation-like the carrier' of F -defined the carrier of F -valued Function-like V18( the carrier' of F, the carrier of F) Element of bool [: the carrier' of F, the carrier of F:]

the Source of F . f1 is Element of the carrier of F

proj1 E is Relation-like set

C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier of C is non empty set

the carrier' of C is non empty set

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like V18( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is Relation-like set

bool [: the carrier' of C, the carrier of C:] is set

the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like V18( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

the Comp of C is Relation-like [: the carrier' of C, the carrier' of C:] -defined the carrier' of C -valued Function-like Element of bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:]

[: the carrier' of C, the carrier' of C:] is Relation-like set

[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is Relation-like set

bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set

IdMap C is Relation-like the carrier of C -defined the carrier' of C -valued Function-like V18( the carrier of C, the carrier' of C) Element of bool [: the carrier of C, the carrier' of C:]

[: the carrier of C, the carrier' of C:] is Relation-like set

bool [: the carrier of C, the carrier' of C:] is set

CatStr(# the carrier of C, the carrier' of C, the Source of C, the Target of C, the Comp of C #) is non empty non void V52() strict CatStr

D is ( the carrier of C, the carrier' of C) ( the carrier of C, the carrier' of C, the Source of C, the Target of C)

D `1 is non empty Relation-like the carrier of C -defined Function-like total () set

the Source of C * (D `1) is non empty Relation-like the carrier' of C -defined Function-like total () set

the Target of C * (D `1) is non empty Relation-like the carrier' of C -defined Function-like total () set

( the carrier of C, the carrier' of C, the Source of C, the Target of C,D) is non empty Relation-like the carrier' of C -defined Function-like total Function-yielding V86() ( the carrier' of C, the Source of C * (D `1), the Target of C * (D `1))

I is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

J is Element of the carrier of C

id J is Morphism of J,J

( the carrier' of C,( the Source of C * (D `1)),(id J)) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of ( the carrier' of C,( the Source of C * (D `1)),(id J)) is non empty set

( the carrier' of C,( the Target of C * (D `1)),(id J)) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of ( the carrier' of C,( the Target of C * (D `1)),(id J)) is non empty set

( the carrier of C,(D `1),J) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of ( the carrier of C,(D `1),J) is non empty set

( the carrier' of C,( the Source of C * (D `1)),( the Target of C * (D `1)),( the carrier of C, the carrier' of C, the Source of C, the Target of C,D),(id J)) is Relation-like the carrier' of ( the carrier' of C,( the Source of C * (D `1)),(id J)) -defined the carrier' of ( the carrier' of C,( the Target of C * (D `1)),(id J)) -valued Function-like V18( the carrier' of ( the carrier' of C,( the Source of C * (D `1)),(id J)), the carrier' of ( the carrier' of C,( the Target of C * (D `1)),(id J))) Functor of ( the carrier' of C,( the Source of C * (D `1)),(id J)),( the carrier' of C,( the Target of C * (D `1)),(id J))

id ( the carrier of C,(D `1),J) is Relation-like the carrier' of ( the carrier of C,(D `1),J) -defined the carrier' of ( the carrier of C,(D `1),J) -valued Function-like V18( the carrier' of ( the carrier of C,(D `1),J), the carrier' of ( the carrier of C,(D `1),J)) Functor of ( the carrier of C,(D `1),J),( the carrier of C,(D `1),J)

id the carrier' of ( the carrier of C,(D `1),J) is non empty Relation-like the carrier' of ( the carrier of C,(D `1),J) -defined the carrier' of ( the carrier of C,(D `1),J) -valued Function-like one-to-one total Element of bool [: the carrier' of ( the carrier of C,(D `1),J), the carrier' of ( the carrier of C,(D `1),J):]

[: the carrier' of ( the carrier of C,(D `1),J), the carrier' of ( the carrier of C,(D `1),J):] is Relation-like set

bool [: the carrier' of ( the carrier of C,(D `1),J), the carrier' of ( the carrier of C,(D `1),J):] is set

(IdMap C) . J is Element of the carrier' of C

E is Element of the carrier' of C

dom E is Element of the carrier of C

the Source of C . E is Element of the carrier of C

J is Element of the carrier' of C

cod J is Element of the carrier of C

the Target of C . J is Element of the carrier of C

the Comp of C . (E,J) is set

[E,J] is V1() set

{E,J} is non empty set

{E} is non empty set

{{E,J},{E}} is non empty set

the Comp of C . [E,J] is set

( the carrier of C, the carrier' of C, the Source of C, the Target of C,D) . ( the Comp of C . (E,J)) is Relation-like Function-like set

( the carrier' of C,( the Source of C * (D `1)),J) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of ( the carrier' of C,( the Source of C * (D `1)),J) is non empty set

( the carrier' of C,( the Target of C * (D `1)),J) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of ( the carrier' of C,( the Target of C * (D `1)),J) is non empty set

( the carrier' of C,( the Source of C * (D `1)),E) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of ( the carrier' of C,( the Source of C * (D `1)),E) is non empty set

( the carrier' of C,( the Target of C * (D `1)),E) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of ( the carrier' of C,( the Target of C * (D `1)),E) is non empty set

( the carrier' of C,( the Source of C * (D `1)),( the Target of C * (D `1)),( the carrier of C, the carrier' of C, the Source of C, the Target of C,D),J) is Relation-like the carrier' of ( the carrier' of C,( the Source of C * (D `1)),J) -defined the carrier' of ( the carrier' of C,( the Target of C * (D `1)),J) -valued Function-like V18( the carrier' of ( the carrier' of C,( the Source of C * (D `1)),J), the carrier' of ( the carrier' of C,( the Target of C * (D `1)),J)) Functor of ( the carrier' of C,( the Source of C * (D `1)),J),( the carrier' of C,( the Target of C * (D `1)),J)

( the carrier' of C,( the Source of C * (D `1)),( the Target of C * (D `1)),( the carrier of C, the carrier' of C, the Source of C, the Target of C,D),E) is Relation-like the carrier' of ( the carrier' of C,( the Source of C * (D `1)),E) -defined the carrier' of ( the carrier' of C,( the Target of C * (D `1)),E) -valued Function-like V18( the carrier' of ( the carrier' of C,( the Source of C * (D `1)),E), the carrier' of ( the carrier' of C,( the Target of C * (D `1)),E)) Functor of ( the carrier' of C,( the Source of C * (D `1)),E),( the carrier' of C,( the Target of C * (D `1)),E)

( the carrier' of C,( the Source of C * (D `1)),( the Target of C * (D `1)),( the carrier of C, the carrier' of C, the Source of C, the Target of C,D),E) * ( the carrier' of C,( the Source of C * (D `1)),( the Target of C * (D `1)),( the carrier of C, the carrier' of C, the Source of C, the Target of C,D),J) is Relation-like the carrier' of ( the carrier' of C,( the Source of C * (D `1)),J) -defined the carrier' of ( the carrier' of C,( the Target of C * (D `1)),E) -valued Function-like Element of bool [: the carrier' of ( the carrier' of C,( the Source of C * (D `1)),J), the carrier' of ( the carrier' of C,( the Target of C * (D `1)),E):]

[: the carrier' of ( the carrier' of C,( the Source of C * (D `1)),J), the carrier' of ( the carrier' of C,( the Target of C * (D `1)),E):] is Relation-like set

bool [: the carrier' of ( the carrier' of C,( the Source of C * (D `1)),J), the carrier' of ( the carrier' of C,( the Target of C * (D `1)),E):] is set

E (*) J is Element of the carrier' of C

( the carrier' of C,( the Source of C * (D `1)),( the Target of C * (D `1)),( the carrier of C, the carrier' of C, the Source of C, the Target of C,D),(E (*) J)) is Relation-like the carrier' of ( the carrier' of C,( the Source of C * (D `1)),(E (*) J)) -defined the carrier' of ( the carrier' of C,( the Target of C * (D `1)),(E (*) J)) -valued Function-like V18( the carrier' of ( the carrier' of C,( the Source of C * (D `1)),(E (*) J)), the carrier' of ( the carrier' of C,( the Target of C * (D `1)),(E (*) J))) Functor of ( the carrier' of C,( the Source of C * (D `1)),(E (*) J)),( the carrier' of C,( the Target of C * (D `1)),(E (*) J))

( the carrier' of C,( the Source of C * (D `1)),(E (*) J)) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of ( the carrier' of C,( the Source of C * (D `1)),(E (*) J)) is non empty set

( the carrier' of C,( the Target of C * (D `1)),(E (*) J)) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of ( the carrier' of C,( the Target of C * (D `1)),(E (*) J)) is non empty set

J is Element of the carrier of C

id J is Morphism of J,J

(IdMap C) . J is Element of the carrier' of C

( the carrier' of C,( the Source of C * (D `1)),( the Target of C * (D `1)),( the carrier of C, the carrier' of C, the Source of C, the Target of C,D),((IdMap C) . J)) is Relation-like the carrier' of ( the carrier' of C,( the Source of C * (D `1)),((IdMap C) . J)) -defined the carrier' of ( the carrier' of C,( the Target of C * (D `1)),((IdMap C) . J)) -valued Function-like V18( the carrier' of ( the carrier' of C,( the Source of C * (D `1)),((IdMap C) . J)), the carrier' of ( the carrier' of C,( the Target of C * (D `1)),((IdMap C) . J))) Functor of ( the carrier' of C,( the Source of C * (D `1)),((IdMap C) . J)),( the carrier' of C,( the Target of C * (D `1)),((IdMap C) . J))

( the carrier' of C,( the Source of C * (D `1)),((IdMap C) . J)) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of ( the carrier' of C,( the Source of C * (D `1)),((IdMap C) . J)) is non empty set

( the carrier' of C,( the Target of C * (D `1)),((IdMap C) . J)) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of ( the carrier' of C,( the Target of C * (D `1)),((IdMap C) . J)) is non empty set

( the carrier' of C,( the Source of C * (D `1)),( the Target of C * (D `1)),( the carrier of C, the carrier' of C, the Source of C, the Target of C,D),(id J)) is Relation-like the carrier' of ( the carrier' of C,( the Source of C * (D `1)),(id J)) -defined the carrier' of ( the carrier' of C,( the Target of C * (D `1)),(id J)) -valued Function-like V18( the carrier' of ( the carrier' of C,( the Source of C * (D `1)),(id J)), the carrier' of ( the carrier' of C,( the Target of C * (D `1)),(id J))) Functor of ( the carrier' of C,( the Source of C * (D `1)),(id J)),( the carrier' of C,( the Target of C * (D `1)),(id J))

( the carrier' of C,( the Source of C * (D `1)),(id J)) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of ( the carrier' of C,( the Source of C * (D `1)),(id J)) is non empty set

( the carrier' of C,( the Target of C * (D `1)),(id J)) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of ( the carrier' of C,( the Target of C * (D `1)),(id J)) is non empty set

( the carrier of C,(D `1),J) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

id ( the carrier of C,(D `1),J) is Relation-like the carrier' of ( the carrier of C,(D `1),J) -defined the carrier' of ( the carrier of C,(D `1),J) -valued Function-like V18( the carrier' of ( the carrier of C,(D `1),J), the carrier' of ( the carrier of C,(D `1),J)) Functor of ( the carrier of C,(D `1),J),( the carrier of C,(D `1),J)

the carrier' of ( the carrier of C,(D `1),J) is non empty set

id the carrier' of ( the carrier of C,(D `1),J) is non empty Relation-like the carrier' of ( the carrier of C,(D `1),J) -defined the carrier' of ( the carrier of C,(D `1),J) -valued Function-like one-to-one total Element of bool [: the carrier' of ( the carrier of C,(D `1),J), the carrier' of ( the carrier of C,(D `1),J):]

[: the carrier' of ( the carrier of C,(D `1),J), the carrier' of ( the carrier of C,(D `1),J):] is Relation-like set

bool [: the carrier' of ( the carrier of C,(D `1),J), the carrier' of ( the carrier of C,(D `1),J):] is set

E is Element of the carrier' of C

the Source of C . E is Element of the carrier of C

J is Element of the carrier' of C

the Target of C . J is Element of the carrier of C

[E,J] is V1() set

{E,J} is non empty set

{E} is non empty set

{{E,J},{E}} is non empty set

the Comp of C . [E,J] is set

( the carrier of C, the carrier' of C, the Source of C, the Target of C,D) . ( the Comp of C . [E,J]) is Relation-like Function-like set

( the carrier' of C,( the Source of C * (D `1)),J) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of ( the carrier' of C,( the Source of C * (D `1)),J) is non empty set

( the carrier' of C,( the Target of C * (D `1)),J) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of ( the carrier' of C,( the Target of C * (D `1)),J) is non empty set

( the carrier' of C,( the Source of C * (D `1)),E) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of ( the carrier' of C,( the Source of C * (D `1)),E) is non empty set

( the carrier' of C,( the Target of C * (D `1)),E) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr

the carrier' of ( the carrier' of C,( the Target of C * (D `1)),E) is non empty set

( the carrier' of C,( the Source of C * (D `1)),( the Target of C * (D `1)),( the carrier of C, the carrier' of C, the Source of C, the Target of C,D),J) is Relation-like the carrier' of ( the carrier' of C,( the Source of C * (D `1)),J) -defined the carrier' of ( the carrier' of C,( the Target of C * (D `1)),J) -valued Function-like V18( the carrier' of ( the carrier' of C,( the Source of C * (D `1)),J), the carrier' of ( the carrier' of C,( the Target of C * (D `1)),J)) Functor of ( the carrier' of C,( the Source of C * (D `1)),J),( the carrier' of C,( the Target of C * (D `1)),J)

( the carrier' of C,( the Source of C * (D `1)),( the Target of C * (D `1)),( the carrier of C, the carrier' of C, the Source of C, the Target of C,D),E) is Relation-like the carrier' of ( the carrier' of C,( the Source of C * (D `1)),E) -defined the carrier' of ( the carrier' of C,( the Target of C * (D `1)),E) -valued Function-like V18( the carrier' of ( the carrier' of C,( the Source of C * (D `1)),E), the carrier' of ( the carrier' of C,( the Target of C * (D `1)),E)) Functor of ( the carrier' of C,( the Source of C * (D `1)),E),( the carrier' of C,( the Target of C * (D `1)),E)

( the carrier' of C,( the Source of C * (D `1)),( the Target of C * (D `1)),( the carrier of C, the carrier' of C, the Source of C, the Target of C,D),E) * ( the carrier' of C,( the Source of C * (D `1)),( the Target of C * (D `1)),( the carrier of C, the carrier' of C, the Source of C, the Target of C,D),J) is Relation-like the carrier' of ( the carrier' of C,( the Source of C * (D `1)),J) -defined the carrier' of ( the carrier' of C,( the Target of C * (D `1)),E) -valued Function-like Element of bool [: the carrier' of ( the carrier' of C,( the Source of C * (D `1)),J), the carrier' of ( the carrier' of C,( the Target of C * (D `1)),E):]

[: the carrier' of ( the carrier' of C,( the Source of C * (D `1)),J), the carrier' of ( the carrier' of C,( the Target of C * (D `1)),E):] is Relation-like set

bool [: the carrier' of ( the carrier' of C,( the Source of C * (D `1)),J), the carrier' of ( the carrier' of C,( the Target of C * (D `1)),E):] is set

dom E is Element of the carrier of C

cod J is Element of the carrier of C

E (*) J is Element of the carrier' of C

( the carrier' of C,( the Source of C * (D `1)),( the Target of C * (D `1)),( the carrier of C, the carrier' of C, the Source of C, the Target of C,D),(E (*) J)) is Relation-like the carrier' of ( the carrier' of C,( the Source of C * (D `1)),(E (*) J)) -defined the carrier' of ( the carrier' of C,( the Target of C * (D `1)),(E (*) J)) -valued Function-like V18( the carrier' of ( the carrier' of C,( the Source of C * (D `1)),(E (*) J)), the carrier' of ( the carrier' of C,( the Target of C * (D `1)),(E (*) J))) Functor of ( the carrier' of C,( the Source of C * (D `1)),(E (*) J)),( the carrier' of C,( the Target of C * (D `1)),(E (*) J))

( the carrier' of C,( the Source of C * (