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
{ b1 where b1 is Element of the carrier' of D : ( dom b1 = C9 & cod b1 = C9 ) } is set
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
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = C9 ) } is set
Hom (D9,T) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D9 & cod b1 = T ) } is set
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
{ b1 where b1 is Element of the carrier' of (1Cat ( the Element of the carrier of C,(id the Element of the carrier of C))) : ( dom b1 = D9 & cod b1 = T ) } is set
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
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = T9 & cod b1 = c ) } is set
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
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = the Element of the carrier of C & cod b1 = the Element of the carrier of C ) } is set
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
{ b1 where b1 is Element of the carrier' of D : ( dom b1 = dom D9 & cod b1 = cod D9 ) } 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
bool the carrier' of C is non empty set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = c & cod b1 = c9 ) } 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
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
{ b1 where b1 is Element of the carrier' of D : ( dom b1 = dom C9 & cod b1 = cod C9 ) } 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
bool the carrier' of C is non empty set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = c & cod b1 = c9 ) } 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
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
{ b1 where b1 is Element of the carrier' of D : ( dom b1 = C9 & cod b1 = D9 ) } is set
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
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = T & cod b1 = T9 ) } 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
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
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = C9 ) } is set
Hom (D9,T) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D9 & cod b1 = T ) } is set
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
{ b1 where b1 is Element of the carrier' of D : ( dom b1 = C9 & cod b1 = D9 ) } is set
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
{ b1 where b1 is Element of the carrier' of D : ( dom b1 = D9 & cod b1 = T ) } is set
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
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = T9 & cod b1 = c ) } is set
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
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = (C,D) . D9 & cod b1 = (C,D) . T ) } is set
Hom (D9,T) is Element of bool the carrier' of D
bool the carrier' of D is non empty set
{ b1 where b1 is Element of the carrier' of D : ( dom b1 = D9 & cod b1 = T ) } is set
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
{ b1 where b1 is Element of the carrier' of D : ( dom b1 = C9 & cod b1 = D9 ) } is set
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
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = T & cod b1 = T9 ) } 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 (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
{ b1 where b1 is Element of the carrier' of D : ( dom b1 = C9 & cod b1 = D9 ) } is set
Hom (T,T9) is Element of bool the carrier' of C
bool the carrier' of C is non empty set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = T & cod b1 = T9 ) } is 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
{ b1 where b1 is Element of the carrier' of D : ( dom b1 = C9 & cod b1 = D9 ) } is set
Hom (T,T9) is Element of bool the carrier' of C
bool the carrier' of C is non empty set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = T & cod b1 = T9 ) } 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
bool the carrier' of C is non empty set
D is non empty Element of bool the carrier of C
{ (Hom (b1,b2)) where b1, b2 is Element of the carrier of C : ( b1 in D & b2 in D ) } is set
union { (Hom (b1,b2)) where b1, b2 is Element of the carrier of C : ( b1 in D & b2 in D ) } is set
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
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = c & cod b1 = c9 ) } is set
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
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = T9 & cod b1 = T9 ) } is set
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 (b1,b2)) where b1, b2 is Element of the carrier of C : ( b1 in D & b2 in D ) } is set
union { (Hom (b1,b2)) where b1, b2 is Element of the carrier of C : ( b1 in D & b2 in D ) } is set
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
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = c & cod b1 = c9 ) } is set
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
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = dom (dd9 (*) g1) & cod b1 = cod (dd9 (*) g1) ) } is set
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 (b1,b2)) where b1, b2 is Element of the carrier of C : ( b1 in D & b2 in D ) } is set
union { (Hom (b1,b2)) where b1, b2 is Element of the carrier of C : ( b1 in D & b2 in D ) } is set
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
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = f2 & cod b1 = g2 ) } is set
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