:: CAT_2 semantic presentation

K162() is Element of bool K158()

K158() is set

bool K158() is non empty set

{} is Relation-like non-empty empty-yielding empty set

1 is non empty set

{{},1} is non empty set

[:1,1:] is Relation-like non empty set

bool [:1,1:] is non empty set

[:[:1,1:],1:] is Relation-like non empty set

bool [:[:1,1:],1:] is non empty set

K157() is set

bool K157() is non empty set

bool K162() is non empty set

D is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr

the carrier of D is non empty set

the carrier' of D is non empty set

C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr

the carrier' of C is non empty set

C9 is Element of the carrier of D

id C9 is Morphism of C9,C9

the carrier' of C --> (id C9) is Relation-like the carrier' of C -defined the carrier' of D -valued Function-like quasi_total Element of bool [: the carrier' of C, the carrier' of D:]

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

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

{(id C9)} is non empty set

[: the carrier' of C,{(id C9)}:] is Relation-like non empty set

the carrier of C is non empty set

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

T is Element of the carrier of C

id T is Morphism of T,T

D9 . (id T) is Element of the carrier' of D

T is Element of the carrier' of C

dom T 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 quasi_total Element of bool [: the carrier' of C, the carrier of C:]

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

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

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

id (dom T) is Morphism of dom T, dom T

D9 . (id (dom T)) is Element of the carrier' of D

D9 . T is Element of the carrier' of D

dom (D9 . T) 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 quasi_total Element of bool [: the carrier' of D, the carrier of D:]

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

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

the Source of D . (D9 . T) is Element of the carrier of D

id (dom (D9 . T)) is Morphism of dom (D9 . T), dom (D9 . T)

cod T 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 quasi_total Element of bool [: the carrier' of C, the carrier of C:]

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

id (cod T) is Morphism of cod T, cod T

D9 . (id (cod T)) is Element of the carrier' of D

cod (D9 . T) is Element of the carrier of D

the Target of D is Relation-like the carrier' of D -defined the carrier of D -valued Function-like quasi_total Element of bool [: the carrier' of D, the carrier of D:]

the Target of D . (D9 . T) is Element of the carrier of D

id (cod (D9 . T)) is Morphism of cod (D9 . T), cod (D9 . T)

cod (id C9) is Element of the carrier of D

the Target of D . (id C9) is Element of the carrier of D

id (cod (id C9)) is Morphism of cod (id C9), cod (id C9)

dom (id C9) is Element of the carrier of D

the Source of D . (id C9) is Element of the carrier of D

id (dom (id C9)) is Morphism of dom (id C9), dom (id C9)

T9 is Element of the carrier' of C

dom T9 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 quasi_total Element of bool [: the carrier' of C, the carrier of C:]

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

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

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

T is Element of the carrier' of C

cod T 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 quasi_total Element of bool [: the carrier' of C, the carrier of C:]

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

Hom (C9,C9) is non empty Element of bool the carrier' of D

bool the carrier' of D is non empty set

{ b

D9 . T is Element of the carrier' of D

(id C9) * (id C9) is Morphism of C9,C9

(id C9) (*) (id C9) is Element of the carrier' of D

T9 (*) T is Element of the carrier' of C

D9 . (T9 (*) T) is Element of the carrier' of D

D9 . T9 is Element of the carrier' of D

(D9 . T9) (*) (D9 . T) is Element of the carrier' of D

C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr

the carrier of C is non empty set

D is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr

the carrier of D is non empty set

C9 is Element of the carrier of C

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

the carrier' of D is non empty set

the carrier' of C is non empty set

id C9 is Morphism of C9,C9

the carrier' of D --> (id C9) is Relation-like the carrier' of D -defined the carrier' of C -valued Function-like quasi_total Element of bool [: the carrier' of D, the carrier' of C:]

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

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

{(id C9)} is non empty set

[: the carrier' of D,{(id C9)}:] is Relation-like non empty set

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

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

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

D9 is Element of the carrier of D

(Obj (D,C,C9)) . D9 is Element of the carrier of C

id D9 is Morphism of D9,D9

(D,C,C9) . (id D9) is Element of the carrier' of C

C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr

the carrier' of C is non empty set

D is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr

the carrier' of D is non empty set

Funcs ( the carrier' of C, the carrier' of D) is non empty FUNCTION_DOMAIN of the carrier' of C, the carrier' of D

C9 is set

D9 is set

C9 is set

D9 is set

T is set

C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr

D is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr

(C,D) is set

the carrier' of C is non empty set

the carrier' of D is non empty set

the Relation-like the carrier' of C -defined the carrier' of D -valued Function-like quasi_total Functor of C,D is Relation-like the carrier' of C -defined the carrier' of D -valued Function-like quasi_total Functor of C,D

C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr

the carrier' of C is non empty set

D is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr

the carrier' of D is non empty set

(C,D) is non empty set

C9 is Element of (C,D)

C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr

D is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr

C9 is non empty (C,D)

the carrier' of C is non empty set

the carrier' of D is non empty set

D9 is Element of C9

D is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr

C9 is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr

C is non empty set

D9 is non empty (D,C9)

[:C,D9:] is Relation-like non empty set

bool [:C,D9:] is non empty set

T is Relation-like C -defined D9 -valued Function-like quasi_total Element of bool [:C,D9:]

T9 is Element of C

T . T9 is set

the carrier' of D is non empty set

the carrier' of C9 is non empty set

T . T9 is Element of D9

C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr

D is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr

(C,D) is non empty set

C9 is Element of (C,D)

the carrier' of C is non empty set

the carrier' of D is non empty set

C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr

the carrier of C is non empty set

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 is non empty set

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

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

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

D is Element of the carrier of C

D9 is Element of the carrier of C

C9 is Element of the carrier of C

T is Element of the carrier of C

Hom (D,C9) is Element of bool the carrier' of C

bool the carrier' of C is non empty set

{ b

Hom (D9,T) is Element of bool the carrier' of C

{ b

T9 is Element of the carrier of C

c is Element of the carrier of C

id T9 is Morphism of T9,T9

id c is Morphism of c,c

C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr

the carrier of C is non empty set

the Element of the carrier of C is Element of the carrier of C

id the Element of the carrier of C is Morphism of the Element of the carrier of C, the Element of the carrier of C

1Cat ( the Element of the carrier of C,(id the Element of the carrier of C)) is non empty trivial V49() non void V54(1) V55() trivial' strict Category-like transitive associative reflexive with_identities CatStr

{ the Element of the carrier of C} is non empty set

{(id the Element of the carrier of C)} is non empty set

(id the Element of the carrier of C) :-> the Element of the carrier of C is Relation-like {(id the Element of the carrier of C)} -defined { the Element of the carrier of C} -valued Function-like quasi_total Element of bool [:{(id the Element of the carrier of C)},{ the Element of the carrier of C}:]

[:{(id the Element of the carrier of C)},{ the Element of the carrier of C}:] is Relation-like non empty set

bool [:{(id the Element of the carrier of C)},{ the Element of the carrier of C}:] is non empty set

{(id the Element of the carrier of C)} --> the Element of the carrier of C is Relation-like {(id the Element of the carrier of C)} -defined { the Element of the carrier of C} -valued Function-like quasi_total Element of bool [:{(id the Element of the carrier of C)},{ the Element of the carrier of C}:]

((id the Element of the carrier of C),(id the Element of the carrier of C)) :-> (id the Element of the carrier of C) is Relation-like [:{(id the Element of the carrier of C)},{(id the Element of the carrier of C)}:] -defined {(id the Element of the carrier of C)} -valued Function-like quasi_total Element of bool [:[:{(id the Element of the carrier of C)},{(id the Element of the carrier of C)}:],{(id the Element of the carrier of C)}:]

[:{(id the Element of the carrier of C)},{(id the Element of the carrier of C)}:] is Relation-like non empty set

[:[:{(id the Element of the carrier of C)},{(id the Element of the carrier of C)}:],{(id the Element of the carrier of C)}:] is Relation-like non empty set

bool [:[:{(id the Element of the carrier of C)},{(id the Element of the carrier of C)}:],{(id the Element of the carrier of C)}:] is non empty set

[(id the Element of the carrier of C),(id the Element of the carrier of C)] is V15() set

{(id the Element of the carrier of C),(id the Element of the carrier of C)} is non empty set

{{(id the Element of the carrier of C),(id the Element of the carrier of C)},{(id the Element of the carrier of C)}} is non empty set

{[(id the Element of the carrier of C),(id the Element of the carrier of C)]} is Relation-like non empty set

{[(id the Element of the carrier of C),(id the Element of the carrier of C)]} --> (id the Element of the carrier of C) is Relation-like {[(id the Element of the carrier of C),(id the Element of the carrier of C)]} -defined {(id the Element of the carrier of C)} -valued Function-like quasi_total Element of bool [:{[(id the Element of the carrier of C),(id the Element of the carrier of C)]},{(id the Element of the carrier of C)}:]

[:{[(id the Element of the carrier of C),(id the Element of the carrier of C)]},{(id the Element of the carrier of C)}:] is Relation-like non empty set

bool [:{[(id the Element of the carrier of C),(id the Element of the carrier of C)]},{(id the Element of the carrier of C)}:] is non empty set

CatStr(# { the Element of the carrier of C},{(id the Element of the carrier of C)},((id the Element of the carrier of C) :-> the Element of the carrier of C),((id the Element of the carrier of C) :-> the Element of the carrier of C),(((id the Element of the carrier of C),(id the Element of the carrier of C)) :-> (id the Element of the carrier of C)) #) is strict CatStr

the carrier of (1Cat ( the Element of the carrier of C,(id the Element of the carrier of C))) is non empty trivial V31() set

D9 is set

D9 is Element of the carrier of (1Cat ( the Element of the carrier of C,(id the Element of the carrier of C)))

T is Element of the carrier of (1Cat ( the Element of the carrier of C,(id the Element of the carrier of C)))

Hom (D9,T) is trivial Element of bool the carrier' of (1Cat ( the Element of the carrier of C,(id the Element of the carrier of C)))

the carrier' of (1Cat ( the Element of the carrier of C,(id the Element of the carrier of C))) is non empty trivial set

bool the carrier' of (1Cat ( the Element of the carrier of C,(id the Element of the carrier of C))) is non empty set

{ b

T9 is Element of the carrier of C

c is Element of the carrier of C

Hom (T9,c) is Element of bool the carrier' of C

the carrier' of C is non empty set

bool the carrier' of C is non empty set

{ b

c9 is set

the Comp of (1Cat ( the Element of the carrier of C,(id the Element of the carrier of C))) is Relation-like [: the carrier' of (1Cat ( the Element of the carrier of C,(id the Element of the carrier of C))), the carrier' of (1Cat ( the Element of the carrier of C,(id the Element of the carrier of C))):] -defined the carrier' of (1Cat ( the Element of the carrier of C,(id the Element of the carrier of C))) -valued Function-like Element of bool [:[: the carrier' of (1Cat ( the Element of the carrier of C,(id the Element of the carrier of C))), the carrier' of (1Cat ( the Element of the carrier of C,(id the Element of the carrier of C))):], the carrier' of (1Cat ( the Element of the carrier of C,(id the Element of the carrier of C))):]

the carrier' of (1Cat ( the Element of the carrier of C,(id the Element of the carrier of C))) is non empty trivial set

[: the carrier' of (1Cat ( the Element of the carrier of C,(id the Element of the carrier of C))), the carrier' of (1Cat ( the Element of the carrier of C,(id the Element of the carrier of C))):] is Relation-like non empty set

[:[: the carrier' of (1Cat ( the Element of the carrier of C,(id the Element of the carrier of C))), the carrier' of (1Cat ( the Element of the carrier of C,(id the Element of the carrier of C))):], the carrier' of (1Cat ( the Element of the carrier of C,(id the Element of the carrier of C))):] is Relation-like non empty set

bool [:[: the carrier' of (1Cat ( the Element of the carrier of C,(id the Element of the carrier of C))), the carrier' of (1Cat ( the Element of the carrier of C,(id the Element of the carrier of C))):], the carrier' of (1Cat ( the Element of the carrier of C,(id the Element of the carrier of C))):] is non empty set

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 is non empty set

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

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

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

Hom ( the Element of the carrier of C, the Element of the carrier of C) is non empty Element of bool the carrier' of C

bool the carrier' of C is non empty set

{ b

dom (id the Element of the carrier of C) 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 quasi_total Element of bool [: the carrier' of C, the carrier of C:]

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

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

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

cod (id the Element of the carrier of C) 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 quasi_total Element of bool [: the carrier' of C, the carrier of C:]

the Target of C . (id the Element of the carrier of C) is Element of the carrier of C

[(id the Element of the carrier of C),(id the Element of the carrier of C)] is V15() Element of [: the carrier' of C, the carrier' of C:]

dom the Comp of C is Relation-like set

(id the Element of the carrier of C) * (id the Element of the carrier of C) is Morphism of the Element of the carrier of C, the Element of the carrier of C

((id the Element of the carrier of C),(id the Element of the carrier of C)) .--> ((id the Element of the carrier of C) * (id the Element of the carrier of C)) is Relation-like Function-like set

{[(id the Element of the carrier of C),(id the Element of the carrier of C)]} --> ((id the Element of the carrier of C) * (id the Element of the carrier of C)) is Relation-like {[(id the Element of the carrier of C),(id the Element of the carrier of C)]} -defined {((id the Element of the carrier of C) * (id the Element of the carrier of C))} -valued Function-like quasi_total Element of bool [:{[(id the Element of the carrier of C),(id the Element of the carrier of C)]},{((id the Element of the carrier of C) * (id the Element of the carrier of C))}:]

{((id the Element of the carrier of C) * (id the Element of the carrier of C))} is non empty set

[:{[(id the Element of the carrier of C),(id the Element of the carrier of C)]},{((id the Element of the carrier of C) * (id the Element of the carrier of C))}:] is Relation-like non empty set

bool [:{[(id the Element of the carrier of C),(id the Element of the carrier of C)]},{((id the Element of the carrier of C) * (id the Element of the carrier of C))}:] is non empty set

D9 is Element of the carrier' of C

(id the Element of the carrier of C) (*) D9 is Element of the carrier' of C

((id the Element of the carrier of C),(id the Element of the carrier of C)) .--> ((id the Element of the carrier of C) (*) D9) is Relation-like Function-like set

{[(id the Element of the carrier of C),(id the Element of the carrier of C)]} --> ((id the Element of the carrier of C) (*) D9) is Relation-like {[(id the Element of the carrier of C),(id the Element of the carrier of C)]} -defined {((id the Element of the carrier of C) (*) D9)} -valued Function-like quasi_total Element of bool [:{[(id the Element of the carrier of C),(id the Element of the carrier of C)]},{((id the Element of the carrier of C) (*) D9)}:]

{((id the Element of the carrier of C) (*) D9)} is non empty set

[:{[(id the Element of the carrier of C),(id the Element of the carrier of C)]},{((id the Element of the carrier of C) (*) D9)}:] is Relation-like non empty set

bool [:{[(id the Element of the carrier of C),(id the Element of the carrier of C)]},{((id the Element of the carrier of C) (*) D9)}:] is non empty set

the Comp of C . ((id the Element of the carrier of C),(id the Element of the carrier of C)) is set

the Comp of C . [(id the Element of the carrier of C),(id the Element of the carrier of C)] is set

[(id the Element of the carrier of C),(id the Element of the carrier of C)] .--> ( the Comp of C . ((id the Element of the carrier of C),(id the Element of the carrier of C))) is set

{[(id the Element of the carrier of C),(id the Element of the carrier of C)]} is Relation-like non empty set

{[(id the Element of the carrier of C),(id the Element of the carrier of C)]} --> ( the Comp of C . ((id the Element of the carrier of C),(id the Element of the carrier of C))) is Relation-like {[(id the Element of the carrier of C),(id the Element of the carrier of C)]} -defined {( the Comp of C . ((id the Element of the carrier of C),(id the Element of the carrier of C)))} -valued Function-like quasi_total Element of bool [:{[(id the Element of the carrier of C),(id the Element of the carrier of C)]},{( the Comp of C . ((id the Element of the carrier of C),(id the Element of the carrier of C)))}:]

{( the Comp of C . ((id the Element of the carrier of C),(id the Element of the carrier of C)))} is non empty set

[:{[(id the Element of the carrier of C),(id the Element of the carrier of C)]},{( the Comp of C . ((id the Element of the carrier of C),(id the Element of the carrier of C)))}:] is Relation-like non empty set

bool [:{[(id the Element of the carrier of C),(id the Element of the carrier of C)]},{( the Comp of C . ((id the Element of the carrier of C),(id the Element of the carrier of C)))}:] is non empty set

D9 is Element of the carrier of (1Cat ( the Element of the carrier of C,(id the Element of the carrier of C)))

T is Element of the carrier of C

id D9 is Morphism of D9,D9

id T is Morphism of T,T

C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr

the carrier of C is non empty set

D is non empty non void V55() Category-like transitive associative reflexive with_identities (C)

the carrier of D is non empty set

C9 is Element of the carrier of D

C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr

the carrier' of C is non empty set

D is non empty non void V55() Category-like transitive associative reflexive with_identities (C)

the carrier' of D is non empty set

C9 is set

D9 is Element of the carrier' of D

dom D9 is Element of the carrier of D

the carrier of D is non empty set

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

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

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

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

cod D9 is Element of the carrier of D

the Target of D is Relation-like the carrier' of D -defined the carrier of D -valued Function-like quasi_total Element of bool [: the carrier' of D, the carrier of D:]

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

the carrier of C is non empty set

Hom ((dom D9),(cod D9)) is Element of bool the carrier' of D

bool the carrier' of D is non empty set

{ b

c is Element of the carrier of C

c9 is Element of the carrier of C

Hom (c,c9) is Element of bool the carrier' of C

bool the carrier' of C is non empty set

{ b

C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr

the carrier' of C is non empty set

D is non empty non void V55() Category-like transitive associative reflexive with_identities (C)

the carrier' of D is non empty set

C9 is Element of the carrier' of D

C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr

the carrier' of C is non empty set

D is non empty non void V55() Category-like transitive associative reflexive with_identities (C)

the carrier' of D is non empty set

C9 is Element of the carrier' of D

dom C9 is Element of the carrier of D

the carrier of D is non empty set

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

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

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

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

cod C9 is Element of the carrier of D

the Target of D is Relation-like the carrier' of D -defined the carrier of D -valued Function-like quasi_total Element of bool [: the carrier' of D, the carrier of D:]

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

D9 is Element of the carrier' of C

dom D9 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 quasi_total Element of bool [: the carrier' of C, the carrier of C:]

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

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

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

cod D9 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 quasi_total Element of bool [: the carrier' of C, the carrier of C:]

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

Hom ((dom C9),(cod C9)) is Element of bool the carrier' of D

bool the carrier' of D is non empty set

{ b

c is Element of the carrier of C

c9 is Element of the carrier of C

Hom (c,c9) is Element of bool the carrier' of C

bool the carrier' of C is non empty set

{ b

C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr

the carrier of C is non empty set

D is non empty non void V55() Category-like transitive associative reflexive with_identities (C)

the carrier of D is non empty set

C9 is Element of the carrier of D

D9 is Element of the carrier of D

Hom (C9,D9) is Element of bool the carrier' of D

the carrier' of D is non empty set

bool the carrier' of D is non empty set

{ b

T is Element of the carrier of C

T9 is Element of the carrier of C

c is Morphism of C9,D9

Hom (T,T9) is Element of bool the carrier' of C

the carrier' of C is non empty set

bool the carrier' of C is non empty set

{ b

C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr

the carrier' of C is non empty set

D is non empty non void V55() Category-like transitive associative reflexive with_identities (C)

the carrier' of D is non empty set

C9 is Element of the carrier' of D

D9 is Element of the carrier' of D

dom D9 is Element of the carrier of D

the carrier of D is non empty set

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

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

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

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

cod C9 is Element of the carrier of D

the Target of D is Relation-like the carrier' of D -defined the carrier of D -valued Function-like quasi_total Element of bool [: the carrier' of D, the carrier of D:]

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

D9 (*) C9 is Element of the carrier' of D

T is Element of the carrier' of C

T9 is Element of the carrier' of C

T9 (*) T is Element of the carrier' of C

dom T9 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 quasi_total Element of bool [: the carrier' of C, the carrier of C:]

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

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

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

cod T 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 quasi_total Element of bool [: the carrier' of C, the carrier of C:]

the Target of C . T is Element of 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 non empty set

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

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

the Comp of C . (T9,T) is set

[T9,T] is V15() set

{T9,T} is non empty set

{T9} is non empty set

{{T9,T},{T9}} is non empty set

the Comp of C . [T9,T] is set

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

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

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

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

the Comp of D . (D9,C9) is set

[D9,C9] is V15() set

{D9,C9} is non empty set

{D9} is non empty set

{{D9,C9},{D9}} is non empty set

the Comp of D . [D9,C9] is set

[D9,C9] is V15() Element of [: the carrier' of D, the carrier' of D:]

dom the Comp of D is Relation-like set

C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr

the carrier of C is non empty set

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 is non empty set

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

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

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

D is Element of the carrier of C

D9 is Element of the carrier of C

C9 is Element of the carrier of C

T is Element of the carrier of C

Hom (D,C9) is Element of bool the carrier' of C

bool the carrier' of C is non empty set

{ b

Hom (D9,T) is Element of bool the carrier' of C

{ b

T9 is Element of the carrier of C

c is Element of the carrier of C

id T9 is Morphism of T9,T9

id c is Morphism of c,c

C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr

the carrier' of C is non empty set

D is non empty non void V55() Category-like transitive associative reflexive with_identities (C)

id D is Relation-like the carrier' of D -defined the carrier' of D -valued Function-like quasi_total Functor of D,D

the carrier' of D is non empty set

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

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

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

rng (id D) is set

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

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

the carrier of D is non empty set

the carrier of C is non empty set

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

D9 is Element of the carrier of D

id D9 is Morphism of D9,D9

C9 . (id D9) is Element of the carrier' of C

T is Element of the carrier of C

id T is Morphism of T,T

D9 is Element of the carrier' of D

dom D9 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 quasi_total Element of bool [: the carrier' of D, the carrier of D:]

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

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

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

id (dom D9) is Morphism of dom D9, dom D9

C9 . (id (dom D9)) is Element of the carrier' of C

C9 . D9 is Element of the carrier' of C

dom (C9 . D9) 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 quasi_total Element of bool [: the carrier' of C, the carrier of C:]

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

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

the Source of C . (C9 . D9) is Element of the carrier of C

id (dom (C9 . D9)) is Morphism of dom (C9 . D9), dom (C9 . D9)

cod D9 is Element of the carrier of D

the Target of D is Relation-like the carrier' of D -defined the carrier of D -valued Function-like quasi_total Element of bool [: the carrier' of D, the carrier of D:]

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

id (cod D9) is Morphism of cod D9, cod D9

C9 . (id (cod D9)) is Element of the carrier' of C

cod (C9 . D9) 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 quasi_total Element of bool [: the carrier' of C, the carrier of C:]

the Target of C . (C9 . D9) is Element of the carrier of C

id (cod (C9 . D9)) is Morphism of cod (C9 . D9), cod (C9 . D9)

(id D) . D9 is Element of the carrier' of D

dom ((id D) . D9) is Element of the carrier of D

the Source of D . ((id D) . D9) is Element of the carrier of D

id (dom ((id D) . D9)) is Morphism of dom ((id D) . D9), dom ((id D) . D9)

cod ((id D) . D9) is Element of the carrier of D

the Target of D . ((id D) . D9) is Element of the carrier of D

id (cod ((id D) . D9)) is Morphism of cod ((id D) . D9), cod ((id D) . D9)

D9 is Element of the carrier' of D

C9 . D9 is Element of the carrier' of C

T is Element of the carrier' of D

C9 . T is Element of the carrier' of C

dom T 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 quasi_total Element of bool [: the carrier' of D, the carrier of D:]

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

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

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

cod D9 is Element of the carrier of D

the Target of D is Relation-like the carrier' of D -defined the carrier of D -valued Function-like quasi_total Element of bool [: the carrier' of D, the carrier of D:]

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

T (*) D9 is Element of the carrier' of D

C9 . (T (*) D9) is Element of the carrier' of C

(id D) . D9 is Element of the carrier' of D

(id D) . T is Element of the carrier' of D

((id D) . T) (*) ((id D) . D9) is Element of the carrier' of D

(C9 . T) (*) (C9 . D9) is Element of the carrier' of C

C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr

D is non empty non void V55() Category-like transitive associative reflexive with_identities (C)

id D is Relation-like the carrier' of D -defined the carrier' of D -valued Function-like quasi_total Functor of D,D

the carrier' of D is non empty set

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

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

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

the carrier' of C is non empty set

C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr

the carrier of C is non empty set

D is non empty non void V55() Category-like transitive associative reflexive with_identities (C)

the carrier of D is non empty set

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

the carrier' of D is non empty set

the carrier' of C is non empty set

id D is Relation-like the carrier' of D -defined the carrier' of D -valued Function-like quasi_total Functor of D,D

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

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

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

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

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

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

C9 is Element of the carrier of D

(Obj (C,D)) . C9 is Element of the carrier of C

D9 is Element of the carrier of C

id D9 is Morphism of D9,D9

id C9 is Morphism of C9,C9

(C,D) . (id C9) is Element of the carrier' of C

id ((Obj (C,D)) . C9) is Morphism of (Obj (C,D)) . C9,(Obj (C,D)) . C9

C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr

D is non empty non void V55() Category-like transitive associative reflexive with_identities (C)

the carrier of D is non empty set

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

the carrier' of D is non empty set

the carrier' of C is non empty set

id D is Relation-like the carrier' of D -defined the carrier' of D -valued Function-like quasi_total Functor of D,D

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

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

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

C9 is Element of the carrier of D

(C,D) . C9 is Element of the carrier of C

the carrier of C is non empty set

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

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

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

(Obj (C,D)) . C9 is Element of the carrier of C

C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr

D is non empty non void V55() Category-like transitive associative reflexive with_identities (C)

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

the carrier' of D is non empty set

the carrier' of C is non empty set

id D is Relation-like the carrier' of D -defined the carrier' of D -valued Function-like quasi_total Functor of D,D

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

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

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

the carrier of D is non empty set

C9 is Element of the carrier of D

D9 is Element of the carrier of D

Hom (C9,D9) is Element of bool the carrier' of D

bool the carrier' of D is non empty set

{ b

T is Morphism of C9,D9

(C,D) . T is Element of the carrier' of C

T9 is Morphism of C9,D9

(C,D) . T9 is Element of the carrier' of C

C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr

the carrier of C is non empty set

D is non empty non void V55() Category-like transitive associative reflexive with_identities (C)

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

the carrier' of D is non empty set

the carrier' of C is non empty set

id D is Relation-like the carrier' of D -defined the carrier' of D -valued Function-like quasi_total Functor of D,D

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

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

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

the carrier of D is non empty set

D9 is Element of the carrier of D

T is Element of the carrier of D

Hom (D9,T) is Element of bool the carrier' of D

bool the carrier' of D is non empty set

{ b

T9 is Element of the carrier of C

c is Element of the carrier of C

Hom (T9,c) is Element of bool the carrier' of C

bool the carrier' of C is non empty set

{ b

c9 is set

(C,D) . D9 is Element of the carrier of C

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

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

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

(Obj (C,D)) . D9 is Element of the carrier of C

(C,D) . T is Element of the carrier of C

(Obj (C,D)) . T is Element of the carrier of C

d9 is Morphism of (C,D) . D9,(C,D) . T

dd9 is Morphism of D9,T

(C,D) . dd9 is Element of the carrier' of C

D9 is Element of the carrier of D

(C,D) . D9 is Element of the carrier of C

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

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

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

(Obj (C,D)) . D9 is Element of the carrier of C

T is Element of the carrier of D

(C,D) . T is Element of the carrier of C

(Obj (C,D)) . T is Element of the carrier of C

Hom (((C,D) . D9),((C,D) . T)) is Element of bool the carrier' of C

bool the carrier' of C is non empty set

{ b

Hom (D9,T) is Element of bool the carrier' of D

bool the carrier' of D is non empty set

{ b

T9 is Morphism of (C,D) . D9,(C,D) . T

c is Morphism of D9,T

(C,D) . c is Element of the carrier' of C

C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr

C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr

D is non empty non void V55() Category-like transitive associative reflexive with_identities (C)

the carrier of D is non empty set

the carrier of C is non empty set

C9 is Element of the carrier of D

D9 is Element of the carrier of D

Hom (C9,D9) is Element of bool the carrier' of D

the carrier' of D is non empty set

bool the carrier' of D is non empty set

{ b

T is Element of the carrier of C

T9 is Element of the carrier of C

Hom (T,T9) is Element of bool the carrier' of C

the carrier' of C is non empty set

bool the carrier' of C is non empty set

{ b

C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr

D is non empty non void V55() Category-like transitive associative reflexive with_identities (C)

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

the carrier' of D is non empty set

the carrier' of C is non empty set

id D is Relation-like the carrier' of D -defined the carrier' of D -valued Function-like quasi_total Functor of D,D

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

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

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

the carrier of D is non empty set

the carrier of C is non empty set

C9 is Element of the carrier of D

T is Element of the carrier of C

D9 is Element of the carrier of D

T9 is Element of the carrier of C

Hom (C9,D9) is Element of bool the carrier' of D

bool the carrier' of D is non empty set

{ b

Hom (T,T9) is Element of bool the carrier' of C

bool the carrier' of C is non empty set

{ b

the carrier of D is non empty set

the carrier of C is non empty set

C9 is Element of the carrier of D

T is Element of the carrier of C

D9 is Element of the carrier of D

T9 is Element of the carrier of C

Hom (C9,D9) is Element of bool the carrier' of D

bool the carrier' of D is non empty set

{ b

Hom (T,T9) is Element of bool the carrier' of C

bool the carrier' of C is non empty set

{ b

C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr

the carrier of C is non empty set

bool the carrier of C is non empty set

the carrier' of C is non empty set

bool the carrier' of C is non empty set

D is non empty Element of bool the carrier of C

{ (Hom (b

union { (Hom (b

T is set

T9 is set

c is Element of the carrier of C

c9 is Element of the carrier of C

Hom (c,c9) is Element of bool the carrier' of C

{ b

the Element of D is Element of D

T9 is Element of the carrier of C

id T9 is Morphism of T9,T9

Hom (T9,T9) is non empty Element of bool the carrier' of C

{ b

T is set

C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr

the carrier of C is non empty set

bool 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 quasi_total Element of bool [: the carrier' of C, the carrier of C:]

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

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

the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like quasi_total 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 non empty set

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

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

D is non empty Element of bool the carrier of C

{ (Hom (b

union { (Hom (b

dom the Source of C is set

D9 is non empty set

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

[:D9,D:] is Relation-like non empty set

bool [:D9,D:] is non empty set

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

the Comp of C || D9 is Relation-like Function-like set

[:D9,D9:] is Relation-like non empty set

the Comp of C | [:D9,D9:] is Relation-like [:D9,D9:] -defined [: the carrier' of C, the carrier' of C:] -defined the carrier' of C -valued set

[:[:D9,D9:],D9:] is Relation-like non empty set

bool [:[:D9,D9:],D9:] is non empty set

T is Element of the carrier' of C

T9 is set

dom T is Element of the carrier of C

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

cod T is Element of the carrier of C

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

c is Element of the carrier of C

c9 is Element of the carrier of C

Hom (c,c9) is Element of bool the carrier' of C

bool the carrier' of C is non empty set

{ b

dom the Target of C is set

dom ( the Source of C | D9) is set

(dom the Source of C) /\ D9 is set

rng ( the Source of C | D9) is set

c9 is set

d9 is set

( the Source of C | D9) . d9 is set

dd9 is Element of the carrier' of C

( the Source of C | D9) . dd9 is set

dom dd9 is Element of the carrier of C

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

bool the carrier' of C is non empty set

dom ( the Target of C | D9) is set

(dom the Target of C) /\ D9 is set

rng ( the Target of C | D9) is set

c9 is set

d9 is set

( the Target of C | D9) . d9 is set

dd9 is Element of the carrier' of C

( the Target of C | D9) . dd9 is set

cod dd9 is Element of the carrier of C

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

dom ( the Comp of C || D9) is set

dom the Comp of C is Relation-like set

(dom the Comp of C) /\ [:D9,D9:] is Relation-like set

rng ( the Comp of C || D9) is set

c9 is set

d9 is set

( the Comp of C || D9) . d9 is set

dd9 is Element of the carrier' of C

g1 is Element of the carrier' of C

[dd9,g1] is V15() Element of [: the carrier' of C, the carrier' of C:]

{dd9,g1} is non empty set

{dd9} is non empty set

{{dd9,g1},{dd9}} is non empty set

cod dd9 is Element of the carrier of C

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

dom dd9 is Element of the carrier of C

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

cod g1 is Element of the carrier of C

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

dd9 (*) g1 is Element of the carrier' of C

dom (dd9 (*) g1) is Element of the carrier of C

the Source of C . (dd9 (*) g1) is Element of the carrier of C

dom g1 is Element of the carrier of C

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

cod (dd9 (*) g1) is Element of the carrier of C

the Target of C . (dd9 (*) g1) is Element of the carrier of C

Hom ((dom (dd9 (*) g1)),(cod (dd9 (*) g1))) is Element of bool the carrier' of C

{ b

the Comp of C . (dd9,g1) is set

[dd9,g1] is V15() set

the Comp of C . [dd9,g1] is set

D is non empty set

C is non empty set

[:D,C:] is Relation-like non empty set

bool [:D,C:] is non empty set

[:D,D:] is Relation-like non empty set

[:[:D,D:],D:] is Relation-like non empty set

bool [:[:D,D:],D:] is non empty set

C9 is Relation-like D -defined C -valued Function-like quasi_total Element of bool [:D,C:]

D9 is Relation-like D -defined C -valued Function-like quasi_total Element of bool [:D,C:]

T is Relation-like [:D,D:] -defined D -valued Function-like Element of bool [:[:D,D:],D:]

CatStr(# C,D,C9,D9,T #) is strict CatStr

C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr

the carrier of C is non empty set

bool 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 quasi_total Element of bool [: the carrier' of C, the carrier of C:]

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

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

the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like quasi_total 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 non empty set

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

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

D is non empty Element of bool the carrier of C

{ (Hom (b

union { (Hom (b

C9 is non empty set

[:C9,D:] is Relation-like non empty set

bool [:C9,D:] is non empty set

[:C9,C9:] is Relation-like non empty set

[:[:C9,C9:],C9:] is Relation-like non empty set

bool [:[:C9,C9:],C9:] is non empty set

[:D,C9:] is Relation-like non empty set

bool [:D,C9:] is non empty set

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

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

the Comp of C || C9 is Relation-like Function-like set

the Comp of C | [:C9,C9:] is Relation-like [:C9,C9:] -defined [: the carrier' of C, the carrier' of C:] -defined the carrier' of C -valued set

D9 is Relation-like C9 -defined D -valued Function-like quasi_total Element of bool [:C9,D:]

T is Relation-like C9 -defined D -valued Function-like quasi_total Element of bool [:C9,D:]

T9 is Relation-like [:C9,C9:] -defined C9 -valued Function-like Element of bool [:[:C9,C9:],C9:]

CatStr(# D,C9,D9,T,T9 #) is non empty non void V55() strict CatStr

the carrier' of CatStr(# D,C9,D9,T,T9 #) is non empty set

dd9 is Element of the carrier' of CatStr(# D,C9,D9,T,T9 #)

g1 is set

f2 is Element of the carrier of C

g2 is Element of the carrier of C

Hom (f2,g2) is Element of bool the carrier' of C

bool the carrier' of C is non empty set

{ b

dom T9 is Relation-like set

g1 is Element of the carrier' of CatStr(# D,C9,D9,T,T9 #)

dd9 is Element of the carrier' of CatStr(# D,C9,D9,T,T9 #)

[g1,dd9] is V15() Element of [: the carrier' of CatStr(# D,C9,D9,T,T9 #), the carrier' of CatStr(# D,C9,D9,T,T9 #):]

[: the carrier' of CatStr(# D,C9,D9,T,T9 #), the carrier' of CatStr(# D,C9,D9,T,T9 #):] is Relation-like non empty set

{g1,dd9} is non empty set

{g1} is non empty set

{{g1,dd9},{g1}} is non empty set

D9 . g1 is set

T . dd9 is set

f2 is Element of the carrier' of C

dom f2 is Element of the carrier of C

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

g2 is Element of the carrier' of C

cod g2 is Element of the carrier of C

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

dom the Comp of C is Relation-like set

(dom the Comp of C) /\ [:C9,C9:] is Relation-like set

[f2,g2] is V15() Element of [: the carrier' of C, the carrier' of C:]

{f2,g2} is non empty set

{f2} is non empty set

{{f2,g2},{f2}} is non empty set

dom the Comp of C is Relation-like set

(dom the Comp of C) /\ [:C9,C9:] is Relation-like set

the Comp of CatStr(# D,C9,D9,T,T9 #) is Relation-like [: the carrier' of CatStr(# D,C9,D9,T,T9 #), the carrier' of CatStr(# D,C9,D9,T,T9 #):] -defined the carrier' of CatStr(# D,C9,D9,T,T9 #) -valued Function-like Element of bool [:[: the carrier' of CatStr(# D,C9,D9,T,T9 #), the carrier' of CatStr(# D,C9,D9,T,T9 #):], the carrier' of CatStr(# D,C9,D9,T,T9 #):]

[: the carrier' of CatStr(# D,C9,D9,T,T9 #), the carrier' of CatStr(# D,C9,D9,T,T9 #):] is Relation-like non empty set

[:[: the carrier' of CatStr(# D,C9,D9,T,T9 #), the carrier' of CatStr(# D,C9,D9,T,T9 #):], the carrier' of CatStr(# D,C9,D9,T,T9 #):] is Relation-like non empty set

bool [:[: the carrier' of CatStr(# D,C9,D9,T,T9 #), the carrier' of CatStr(# D,C9,D9,T,T9 #):], the carrier' of CatStr(# D,C9,D9,T,T9 #):] is non empty set

dom the Comp of CatStr(# D,C9,D9,T,T9 #) is Relation-like set

g1 is Element of the carrier' of CatStr(# D,C9,D9,T,T9 #)

dd9 is Element of the carrier' of CatStr(# D,C9,D9,T,T9 #)

[g1,dd9] is V15() Element of [: the carrier' of CatStr(# D,C9,D9,T,T9 #), the carrier' of CatStr(# D,C9,D9,T,T9 #):]

{g1,dd9} is non empty set

{g1} is non empty set

{{g1,dd9},{g1}} is non empty set

dom g1 is Element of the carrier of CatStr(# D,C9,D9,T,T9 #)

the carrier of CatStr(# D,C9,D9,T,T9 #) is non empty set

the Source of CatStr(# D,C9,D9,T,T9 #) is Relation-like the carrier' of CatStr(# D,C9,D9,T,T9 #) -defined the carrier of CatStr(# D,C9,D9,T,T9 #) -valued Function-like quasi_total Element of bool [: the carrier' of CatStr(# D,C9,D9,T,T9 #), the carrier of CatStr(# D,C9,D9,T,T9 #):]

[: the carrier' of CatStr(# D,C9,D9,T,T9 #), the carrier of CatStr(# D,C9,D9,T,T9 #):] is Relation-like non empty set

bool [: the carrier' of CatStr(# D,C9,D9,T,T9 #), the carrier of CatStr(# D,C9,D9,T,T9 #):] is non empty set

the Source of CatStr(# D,C9,D9,T,T9 #) . g1 is Element of the carrier of CatStr(# D,C9,D9,T,T9 #)

cod dd9 is Element of the carrier of CatStr(# D,C9,D9,T,T9 #)

the Target of CatStr(# D,C9,D9,T,T9 #) is Relation-like the carrier' of CatStr(# D,C9,D9,T,T9 #) -defined the carrier of CatStr(# D,C9,D9,T,T9 #) -valued Function-like quasi_total Element of bool [: the carrier' of CatStr(# D,C9,D9,T,T9 #), the carrier of CatStr(# D,C9,D9,T,T9 #):]

the Target of CatStr(# D,C9,D9,T,T9 #) . dd9 is Element of the carrier of CatStr(# D,C9,D9,T,T9 #)

g2 is Element of the carrier' of CatStr(# D,C9,D9,T,T9 #)

dom g2 is Element of the carrier of CatStr(# D,C9,D9,T,T9 #)

the Source of CatStr(# D,C9,D9,T,T9 #) . g2 is Element of the carrier of CatStr(# D,C9,D9,T,T9 #)

f2 is Element of the carrier' of CatStr(# D,C9,D9,T,T9 #)

cod f2 is Element of the carrier of CatStr(# D,C9,D9,T,T9 #)

the Target of CatStr(# D,C9,D9,T,T9 #) . f2 is Element of the carrier of CatStr(# D,C9,D9,T,T9 #)

[g2,f2] is V15() Element of [: the carrier' of CatStr(# D,C9,D9,T,T9 #), the carrier' of CatStr(# D,C9,D9,T,T9 #):]

{g2,f2} is non empty set

{g2} is non empty set

{{g2,f2},{g2}} is non empty set

g1 is Element of the carrier' of CatStr(# D,C9,D9,T,T9 #)

dom g1 is Element of the carrier of CatStr(# D,C9,D9,T,T9 #)

the carrier of CatStr(# D,C9,D9,T,T9 #) is non empty set

the Source of CatStr(# D,C9,D9,T,T9 #) is Relation-like the carrier' of CatStr(# D,C9,D9,T,T9 #) -defined the carrier of CatStr(# D,C9,D9,T,T9 #) -valued Function-like quasi_total Element of bool [: the carrier' of CatStr(# D,C9,D9,T,T9 #), the carrier of CatStr(# D,C9,D9,T,T9 #):]

[: the carrier' of CatStr(# D,C9,D9,T,T9 #), the carrier of CatStr(# D,C9,D9,T,T9 #):] is Relation-like non empty set

bool [: the carrier' of CatStr(# D,C9,D9,T,T9 #), the carrier of CatStr(# D,C9,D9,T,T9 #):] is non empty set

the Source of CatStr(# D,C9,D9,T,T9 #) . g1 is Element of the carrier of CatStr(# D,C9,D9,T,T9 #)

dd9 is Element of the carrier' of CatStr(# D,C9,D9,T,T9 #)

cod dd9 is Element of the carrier of CatStr(# D,C9,D9,T,T9 #)

the Target of CatStr(# D,C9,D9,T,T9 #) is Relation-like the carrier' of CatStr(# D,C9,D9,T,T9 #) -defined the carrier of CatStr(# D,C9,D9,T,T9 #) -valued Function-like quasi_total Element of bool [: the carrier' of CatStr(# D,C9,D9,T,T9 #), the carrier of CatStr(# D,C9,D9,T,T9 #):]

the Target of CatStr(# D,C9,D9,T,T9 #) . dd9 is Element of the carrier of CatStr(# D,C9,D9,T,T9 #)

g1 (*) dd9 is Element of the carrier' of CatStr(# D,C9,D9,T,T9 #)

dom (g1 (*) dd9) is Element of the carrier of CatStr(# D,C9,D9,T,T9 #)

the Source of CatStr(# D,C9,D9,T,T9 #) . (g1 (*) dd9) is Element of the carrier of CatStr(# D,C9,D9,T,T9 #)

dom dd9 is Element of the carrier of CatStr(# D,C9,D9,T,T9 #)

the Source of CatStr(# D,C9,D9,T,T9 #) . dd9 is Element of the carrier of CatStr(# D,C9,D9,T,T9 #)

cod (g1 (*) dd9) is Element of the carrier of CatStr(# D,C9,D9,T,T9 #)

the Target of CatStr(# D,C9,D9,T,T9 #) . (g1 (*) dd9) is Element of the carrier of CatStr(# D,C9,D9,T,T9 #)

cod g1 is Element of the carrier of CatStr(# D,C9,D9,T,T9 #)

the Target of CatStr(# D,C9,D9,T,T9 #) . g1 is Element of the carrier of CatStr(# D,C9,D9,T,T9 #)

D9 . g1 is set

g2 is Element of the carrier' of C

dom g2 is Element of the carrier of C

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

T . dd9 is set

f2 is Element of the carrier' of C

cod f2 is Element of the carrier of C

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

[g1,dd9] is V15() Element of [: the carrier' of CatStr(# D,C9,D9,T,T9 #), the carrier' of CatStr(# D,C9,D9,T,T9 #):]

[: the carrier' of CatStr(# D,C9,D9,T,T9 #), the carrier' of CatStr(# D,C9,D9,T,T9 #):] is Relation-like non empty set

{g1,dd9} is non empty set

{g1} is non empty set

{{g1,dd9},{g1}} is non empty set

the Comp of CatStr(# D,C9,D9,T,T9 #) is Relation-like [: the carrier' of CatStr(# D,C9,D9,T,T9 #), the carrier' of CatStr(# D,C9,D9,T,T9 #):] -defined the carrier' of CatStr(# D,C9,D9,T,T9 #) -valued Function-like Element of bool [:[: the carrier' of CatStr(# D,C9,D9,T,T9 #), the carrier' of CatStr(# D,C9,D9,T,T9 #):], the carrier' of CatStr(# D,C9,D9,T,T9 #):]

[:[: the carrier' of CatStr(# D,C9,D9,T,T9 #), the carrier' of CatStr(# D,C9,D9,T,T9 #):], the carrier' of CatStr(# D,C9,D9,T,T9 #):] is Relation-like non empty set

bool [:[: the carrier' of CatStr(# D,C9,D9,T,T9 #), the carrier' of CatStr(# D,C9,D9,T,T9 #):], the carrier' of CatStr(# D,C9,D9,T,T9 #):] is non empty set

dom the Comp of CatStr(# D,C9,D9,T,T9 #) is Relation-like set

T9 . (g1,dd9) is set

[g1,dd9] is V15() set

T9 . [g1,dd9] is set

dom the Comp of C is Relation-like set

T9 . [g1,dd9] is set

the Comp of C . (g1,dd9) is set

the Comp of C . [g1,dd9] is set

g2 (*) f2 is Element of the carrier' of C

dom (g2 (*) f2) is Element of the carrier of C

the Source of C . (g2 (*) f2) is Element of the carrier of C

dom f2 is Element of the carrier of C

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

cod (g2 (*) f2) is Element of the carrier of C

the Target of C . (g2 (*) f2) is Element of the carrier of C

cod g2 is Element of the carrier of C

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

f2 is Element of the carrier' of CatStr(# D,C9,D9,T,T9 #)

dom f2 is Element of the carrier of CatStr(# D,C9,D9,T,T9 #)

the carrier of CatStr(# D,C9,D9,T,T9 #) is non empty set

the Source of CatStr(# D,C9,D9,T,T9 #) is Relation-like the carrier' of CatStr(# D,C9,D9,T,T9 #) -defined the carrier of CatStr(# D,C9,D9,T,T9 #) -valued Function-like quasi_total Element of bool [: the carrier' of CatStr(# D,C9,D9,T,T9 #), the carrier of CatStr(# D,C9,D9,T,T9 #):]

[: the carrier' of CatStr(# D,C9,D9,T,T9 #), the carrier of CatStr(# D,C9,D9,T,T9 #):] is Relation-like non empty set

bool [: the carrier' of CatStr(# D,C9,D9,T,T9 #), the carrier of CatStr(# D,C9,D9,T,T9 #):] is non empty set

the Source of CatStr(# D,C9,D9,T,T9 #) . f2 is Element of the carrier of CatStr(# D,C9,D9,T,T9 #)

g1 is Element of the carrier' of CatStr(# D,C9,D9,T,T9 #)

cod g1 is Element of the carrier of CatStr(# D,C9,D9,T,T9 #)

the Target of CatStr(# D,C9,D9,T,T9 #) is Relation-like the carrier' of CatStr(# D,C9,D9,T,T9 #) -defined the carrier of CatStr(# D,C9,D9,T,T9 #) -valued Function-like quasi_total Element of bool [: the carrier' of CatStr(# D,C9,D9,T,T9 #), the carrier of CatStr(# D,C9,D9,T,T9 #):]

the Target of CatStr(# D,C9,D9,T,T9 #) . g1 is Element of the carrier of CatStr(# D,C9,D9,T,T9 #)

dom g1 is Element of the carrier of CatStr(# D,C9,D9,T,T9 #)

the Source of CatStr(# D,C9,D9,T,T9 #) . g1 is Element of the carrier of CatStr(# D,C9,D9,T,T9 #)

dd9 is Element of the carrier' of CatStr(# D,C9,D9,T,T9 #)

cod dd9 is Element of the carrier of CatStr(# D,C9,D9,T,T9 #)

the Target of CatStr(# D,C9,D9,T,T9 #) . dd9 is Element of the carrier of CatStr(# D,C9,D9,T,T9 #)

g1 (*) dd9 is Element of the carrier' of CatStr(# D,C9,D9,T,T9 #)

f2 (*) (g1 (*) dd9) is Element of the carrier' of CatStr(# D,C9,D9,T,T9 #)

f2 (*) g1 is Element of the carrier' of CatStr(# D,C9,D9,T,T9 #)

(f2 (*) g1) (*) dd9 is Element of the carrier' of CatStr(# D,C9,D9,T,T9 #)

the Comp of CatStr(# D,C9,D9,T,T9 #) is Relation-like [: the carrier' of CatStr(# D,C9,D9,T,T9 #), the carrier' of CatStr(# D,C9,D9,T,T9 #):] -defined the carrier' of CatStr(# D,C9,D9,T,T9 #) -valued Function-like Element of bool [:[: the carrier' of CatStr(# D,C9,D9,T,T9 #), the carrier' of CatStr(# D,C9,D9,T,T9 #):], the carrier' of CatStr(# D,C9,D9,T,T9 #):]

[: the carrier' of CatStr(# D,C9,D9,T,T9 #), the carrier' of CatStr(# D,C9,D9,T,T9 #):] is Relation-like non empty set

[:[: the carrier' of CatStr(# D,C9,D9,T,T9 #), the carrier' of CatStr(# D,C9,D9,T,T9 #):], the carrier' of CatStr(# D,C9,D9,T,T9 #):] is Relation-like non empty set

bool [:[: the carrier' of CatStr(# D,C9,D9,T,T9 #), the carrier' of CatStr(# D,C9,D9,T,T9 #):], the carrier' of CatStr(# D,C9,D9,T,T9 #):] is non empty set

the Comp of CatStr(# D,C9,D9,T,T9 #) . (f2,g1) is set

[f2,g1] is V15() set

{f2,g1} is non empty set

{f2} is non empty set

{{f2,g1},{f2}} is non empty set

the Comp of CatStr(# D,C9,D9,T,T9 #) . [f2,g1] is set

the Comp of CatStr(# D,C9,D9,T,T9 #) . (g1,dd9) is set

[g1,dd9] is V15() set

{g1,dd9} is non empty set

{g1} is non empty set

{{g1,dd9},{g1}} is non empty set

the Comp of CatStr(# D,C9,D9,T,T9 #) . [g1,dd9] is set

dom (f2 (*) g1) is Element of the carrier of CatStr(# D,C9,D9,T,T9 #)

the Source of CatStr(# D,C9,D9,T,T9 #) . (f2 (*) g1) is Element of the carrier of CatStr(# D,C9,D9,T,T9 #)

T . g1 is set

L1 is Element of the carrier' of C

cod L1 is Element of the carrier of C

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

D9 . g1 is set

dom L1 is Element of the carrier of C

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

T . dd9 is set

g2 is Element of the carrier' of C

cod g2 is Element of the carrier of C

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

D9 . f2 is set

L2 is Element of the carrier' of C

dom L2 is Element of the carrier of C

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

L1 (*) g2 is Element of the carrier' of C

the Comp of C . (L1,g2) is set

[L1,g2] is V15() set

{L1,g2} is non empty set

{L1} is non empty set

{{L1,g2},{L1}} is non empty set

the Comp of C . [L1,g2] is set

cod (L1 (*) g2) is Element of the carrier of C

the Target of C . (L1 (*) g2) is Element of the carrier of C

L2 (*) L1 is Element of the carrier' of C

the Comp of C . (L2,L1) is set

[L2,L1] is V15() set

{L2,L1} is non empty set

{L2} is non empty set

{{L2,L1},{L2}} is non empty set

the Comp of C . [L2,L1] is set

dom (L2 (*) L1) is Element of the carrier of C

the Source of C . (L2 (*) L1) is Element of the carrier of C

cod (g1 (*) dd9) is Element of the carrier of CatStr(# D,C9,D9,T,T9 #)

the Target of CatStr(# D,C9,D9,T,T9 #) . (g1 (*) dd9) is Element of the carrier of CatStr(# D,C9,D9,T,T9 #)

the Comp of CatStr(# D,C9,D9,T,T9 #) . (f2,( the Comp of CatStr(# D,C9,D9,T,T9 #) . (g1,dd9))) is set

[f2,( the Comp of CatStr(# D,C9,D9,T,T9 #) . (g1,dd9))] is V15() set

{f2,( the Comp of CatStr(# D,C9,D9,T,T9 #) . (g1,dd9))} is non empty set

{{f2,( the Comp of CatStr(# D,C9,D9,T,T9 #) . (g1,dd9))},{f2}} is non empty set

the Comp of CatStr(# D,C9,D9,T,T9 #) . [f2,( the Comp of CatStr(# D,C9,D9,T,T9 #) . (g1,dd9))] is set

[g1,dd9] is V15() Element of [: the carrier' of CatStr(# D,C9,D9,T,T9 #), the carrier' of CatStr(# D,C9,D9,T,T9 #):]

T9 . [g1,dd9] is set

[f2,(T9 . [g1,dd9])] is V15() set

{f2,(T9 . [g1,dd9])} is non empty set

{{f2,(T9 . [g1,dd9])},{f2}} is non empty set

the Comp of C . [f2,(T9 . [g1,dd9])] is set

the Comp of C . (L2,(L1 (*) g2)) is set

[L2,(L1 (*) g2)] is V15() set

{L2,(L1 (*) g2)} is non empty set

{{L2,(L1 (*) g2)},{L2}} is non empty set

the Comp of C . [L2,(L1 (*) g2)] is set

L2 (*) (L1 (*) g2) is Element of the carrier' of C

(L2 (*) L1) (*) g2 is Element of the carrier' of C

the Comp of C . (( the Comp of C . (L2,L1)),g2) is set

[( the Comp of C . (L2,L1)),g2] is V15() set

{( the Comp of C . (L2,L1)),g2} is non empty set

{( the Comp of C . (L2,L1))} is non empty set

{{( the Comp of C . (L2,L1)),g2},{( the Comp of C . (L2,L1))}} is non empty set

the Comp of C . [( the Comp of C . (L2,L1)),g2] is set

[f2,g1] is V15() Element of [: the carrier' of CatStr(# D,C9,D9,T,T9 #), the carrier' of CatStr(# D,C9,D9,T,T9 #):]

T9 . [f2,g1] is set

[(T9 . [f2,g1]),dd9] is V15() set

{(T9 . [f2,g1]),dd9} is non empty set

{(T9 . [f2,g1])} is non empty set

{{(T9 . [f2,g1]),dd9},{(T9 . [f2,g1])}} is non empty set

the Comp of C