:: 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<sub>1</sub>() is non empty set
F<sub>2</sub>() is non empty Relation-like F<sub>1</sub>() -defined Function-like total () set
F<sub>3</sub>() is non empty Relation-like F<sub>1</sub>() -defined Function-like total () set
C is non empty Relation-like F<sub>1</sub>() -defined Function-like total set
I is set
proj1 C is non empty set
C . I is set
D is Element of F<sub>1</sub>()
C . D is set
F<sub>4</sub>(D) is set
I is non empty Relation-like F<sub>1</sub>() -defined Function-like total Function-yielding V86() set
D is Element of F<sub>1</sub>()
I . D is Relation-like Function-like set
(F<sub>1</sub>(),F<sub>2</sub>(),D) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier' of (F<sub>1</sub>(),F<sub>2</sub>(),D) is non empty set
(F<sub>1</sub>(),F<sub>3</sub>(),D) is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier' of (F<sub>1</sub>(),F<sub>3</sub>(),D) is non empty set
F<sub>4</sub>(D) is set
D is non empty Relation-like F<sub>1</sub>() -defined Function-like total Function-yielding V86() (F<sub>1</sub>(),F<sub>2</sub>(),F<sub>3</sub>())
J is Element of F<sub>1</sub>()
D . J is Relation-like Function-like set
F<sub>4</sub>(J) is 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 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 * (