:: COMMACAT semantic presentation

K145() is Element of bool K141()
K141() is set
bool K141() is non empty set
{} is empty set
the empty set is empty set
1 is non empty set
{{},1} is non empty set
K140() is set
bool K140() is non empty set
bool K145() 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
m is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
the carrier' of m 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 carrier of C is non empty set
the carrier of c is non empty set
s is Relation-like the carrier' of C -defined the carrier' of m -valued Function-like V18( the carrier' of C, the carrier' of m) Functor of C,m
x is Relation-like the carrier' of c -defined the carrier' of m -valued Function-like V18( the carrier' of c, the carrier' of m) Functor of c,m
f1 is Element of the carrier' of m
c1 is Element of the carrier of C
s . c1 is Element of the carrier of m
the carrier of m is non empty set
Obj s is Relation-like the carrier of C -defined the carrier of m -valued Function-like V18( the carrier of C, the carrier of m) Element of bool [: the carrier of C, the carrier of m:]
[: the carrier of C, the carrier of m:] is non empty set
bool [: the carrier of C, the carrier of m:] is non empty set
(Obj s) . c1 is Element of the carrier of m
d1 is Element of the carrier of c
x . d1 is Element of the carrier of m
Obj x is Relation-like the carrier of c -defined the carrier of m -valued Function-like V18( the carrier of c, the carrier of m) Element of bool [: the carrier of c, the carrier of m:]
[: the carrier of c, the carrier of m:] is non empty set
bool [: the carrier of c, the carrier of m:] is non empty set
(Obj x) . d1 is Element of the carrier of m
Hom ((s . c1),(x . d1)) is Element of bool the carrier' of m
bool the carrier' of m is non empty set
{ b₁ where b₁ is Element of the carrier' of m : ( dom b₁ = s . c1 & cod b₁ = x . d1 ) } is set
[: the carrier of C, the carrier of c:] is non empty set
{ [[b₁,b₂],b₃] where b₁ is Element of the carrier of C, b₂ is Element of the carrier of c, b₃ is Element of the carrier' of m : b₃ in Hom ((s . b₁),(x . b₂)) } is set
[:[: the carrier of C, the carrier of c:], the carrier' of m:] is non empty set
bool [:[: the carrier of C, the carrier of c:], the carrier' of m:] is non empty set
E1 is set
E2 is Element of the carrier of C
x is Element of the carrier of c
[E2,x] is V1() Element of [: the carrier of C, the carrier of c:]
{E2,x} is non empty set
{E2} is non empty set
{{E2,x},{E2}} is non empty set
I is Element of the carrier' of m
[[E2,x],I] is V1() Element of [:[: the carrier of C, the carrier of c:], the carrier' of m:]
{[E2,x],I} is non empty set
{[E2,x]} is non empty set
{{[E2,x],I},{[E2,x]}} is non empty set
s . E2 is Element of the carrier of m
(Obj s) . E2 is Element of the carrier of m
x . x is Element of the carrier of m
(Obj x) . x is Element of the carrier of m
Hom ((s . E2),(x . x)) is Element of bool the carrier' of m
{ b₁ where b₁ is Element of the carrier' of m : ( dom b₁ = s . E2 & cod b₁ = x . x ) } is set
[c1,d1] is V1() Element of [: the carrier of C, the carrier of c:]
{c1,d1} is non empty set
{c1} is non empty set
{{c1,d1},{c1}} is non empty set
[[c1,d1],f1] is V1() Element of [:[: the carrier of C, the carrier of c:], the carrier' of m:]
{[c1,d1],f1} is non empty set
{[c1,d1]} is non empty set
{{[c1,d1],f1},{[c1,d1]}} 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 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
the carrier of c is non empty set
[: the carrier of C, the carrier of c:] is non empty set
m is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
the carrier' of m is non empty set
[:[: the carrier of C, the carrier of c:], the carrier' of m:] is non empty set
s is Relation-like the carrier' of C -defined the carrier' of m -valued Function-like V18( the carrier' of C, the carrier' of m) Functor of C,m
x is Relation-like the carrier' of c -defined the carrier' of m -valued Function-like V18( the carrier' of c, the carrier' of m) Functor of c,m
(C,c,m,s,x) is non empty Relation-like [: the carrier of C, the carrier of c:] -defined the carrier' of m -valued Element of bool [:[: the carrier of C, the carrier of c:], the carrier' of m:]
bool [:[: the carrier of C, the carrier of c:], the carrier' of m:] is non empty set
c1 is Element of (C,c,m,s,x)
c1 `11 is Element of the carrier of C
c1 `12 is Element of the carrier of c
[(c1 `11),(c1 `12)] is V1() Element of [: the carrier of C, the carrier of c:]
{(c1 `11),(c1 `12)} is non empty set
{(c1 `11)} is non empty set
{{(c1 `11),(c1 `12)},{(c1 `11)}} is non empty set
c1 `2 is Element of the carrier' of m
[[(c1 `11),(c1 `12)],(c1 `2)] is V1() Element of [:[: the carrier of C, the carrier of c:], the carrier' of m:]
{[(c1 `11),(c1 `12)],(c1 `2)} is non empty set
{[(c1 `11),(c1 `12)]} is non empty set
{{[(c1 `11),(c1 `12)],(c1 `2)},{[(c1 `11),(c1 `12)]}} is non empty set
s . (c1 `11) is Element of the carrier of m
the carrier of m is non empty set
Obj s is Relation-like the carrier of C -defined the carrier of m -valued Function-like V18( the carrier of C, the carrier of m) Element of bool [: the carrier of C, the carrier of m:]
[: the carrier of C, the carrier of m:] is non empty set
bool [: the carrier of C, the carrier of m:] is non empty set
(Obj s) . (c1 `11) is Element of the carrier of m
x . (c1 `12) is Element of the carrier of m
Obj x is Relation-like the carrier of c -defined the carrier of m -valued Function-like V18( the carrier of c, the carrier of m) Element of bool [: the carrier of c, the carrier of m:]
[: the carrier of c, the carrier of m:] is non empty set
bool [: the carrier of c, the carrier of m:] is non empty set
(Obj x) . (c1 `12) is Element of the carrier of m
Hom ((s . (c1 `11)),(x . (c1 `12))) is Element of bool the carrier' of m
bool the carrier' of m is non empty set
{ b₁ where b₁ is Element of the carrier' of m : ( dom b₁ = s . (c1 `11) & cod b<sub>1</sub> = x . (c1 `12) ) } is set
dom (c1 `2) is Element of the carrier of m
the Source of m is Relation-like the carrier' of m -defined the carrier of m -valued Function-like V18( the carrier' of m, the carrier of m) Element of bool [: the carrier' of m, the carrier of m:]
[: the carrier' of m, the carrier of m:] is non empty set
bool [: the carrier' of m, the carrier of m:] is non empty set
the Source of m . (c1 `2) is Element of the carrier of m
cod (c1 `2) is Element of the carrier of m
the Target of m is Relation-like the carrier' of m -defined the carrier of m -valued Function-like V18( the carrier' of m, the carrier of m) Element of bool [: the carrier' of m, the carrier of m:]
the Target of m . (c1 `2) is Element of the carrier of m
{ [[b₁,b₂],b₃] where b₁ is Element of the carrier of C, b₂ is Element of the carrier of c, b₃ is Element of the carrier' of m : b₃ in Hom ((s . b₁),(x . b₂)) } is set
E1 is Element of the carrier' of m
d1 is Element of the carrier of C
s . d1 is Element of the carrier of m
(Obj s) . d1 is Element of the carrier of m
f1 is Element of the carrier of c
x . f1 is Element of the carrier of m
(Obj x) . f1 is Element of the carrier of m
Hom ((s . d1),(x . f1)) is Element of bool the carrier' of m
{ b₁ where b₁ is Element of the carrier' of m : ( dom b₁ = s . d1 & cod b₁ = x . f1 ) } is set
d1 is Element of the carrier of C
f1 is Element of the carrier of c
[d1,f1] is V1() Element of [: the carrier of C, the carrier of c:]
{d1,f1} is non empty set
{d1} is non empty set
{{d1,f1},{d1}} is non empty set
E1 is Element of the carrier' of m
[[d1,f1],E1] is V1() Element of [:[: the carrier of C, the carrier of c:], the carrier' of m:]
{[d1,f1],E1} is non empty set
{[d1,f1]} is non empty set
{{[d1,f1],E1},{[d1,f1]}} is non empty set
s . d1 is Element of the carrier of m
(Obj s) . d1 is Element of the carrier of m
x . f1 is Element of the carrier of m
(Obj x) . f1 is Element of the carrier of m
Hom ((s . d1),(x . f1)) is Element of bool the carrier' of m
{ b₁ where b₁ is Element of the carrier' of m : ( dom b₁ = s . d1 & cod b₁ = x . f1 ) } 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
m is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
the carrier' of m 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 carrier of C is non empty set
the carrier of c is non empty set
s is Relation-like the carrier' of C -defined the carrier' of m -valued Function-like V18( the carrier' of C, the carrier' of m) Functor of C,m
x is Relation-like the carrier' of c -defined the carrier' of m -valued Function-like V18( the carrier' of c, the carrier' of m) Functor of c,m
f1 is Element of the carrier' of m
c1 is Element of the carrier of C
s . c1 is Element of the carrier of m
the carrier of m is non empty set
Obj s is Relation-like the carrier of C -defined the carrier of m -valued Function-like V18( the carrier of C, the carrier of m) Element of bool [: the carrier of C, the carrier of m:]
[: the carrier of C, the carrier of m:] is non empty set
bool [: the carrier of C, the carrier of m:] is non empty set
(Obj s) . c1 is Element of the carrier of m
d1 is Element of the carrier of c
x . d1 is Element of the carrier of m
Obj x is Relation-like the carrier of c -defined the carrier of m -valued Function-like V18( the carrier of c, the carrier of m) Element of bool [: the carrier of c, the carrier of m:]
[: the carrier of c, the carrier of m:] is non empty set
bool [: the carrier of c, the carrier of m:] is non empty set
(Obj x) . d1 is Element of the carrier of m
Hom ((s . c1),(x . d1)) is Element of bool the carrier' of m
bool the carrier' of m is non empty set
{ b₁ where b₁ is Element of the carrier' of m : ( dom b₁ = s . c1 & cod b₁ = x . d1 ) } is set
[: the carrier of C, the carrier of c:] is non empty set
[:[: the carrier of C, the carrier of c:], the carrier' of m:] is non empty set
(C,c,m,s,x) is non empty Relation-like [: the carrier of C, the carrier of c:] -defined the carrier' of m -valued Element of bool [:[: the carrier of C, the carrier of c:], the carrier' of m:]
bool [:[: the carrier of C, the carrier of c:], the carrier' of m:] is non empty set
[:(C,c,m,s,x),(C,c,m,s,x):] is non empty set
[: the carrier' of C, the carrier' of c:] is non empty set
{ [[b₃,b₄],[b₁,b₂]] where b₁ is Element of the carrier' of C, b₂ is Element of the carrier' of c, b₃, b₄ is Element of (C,c,m,s,x) : ( dom b₁ = b₃ `11 & cod b<sub>1</sub> = b<sub>4</sub> `11 & dom b₂ = b₃ `12 & cod b<sub>2</sub> = b<sub>4</sub> `12 & (b₄ `2) (*) (s . b<sub>1</sub>) = (x . b<sub>2</sub>) (*) (b<sub>3</sub> `2) ) } is set
[:(C,c,m,s,x),(C,c,m,s,x):] is non empty Relation-like [:[: the carrier of C, the carrier of c:], the carrier' of m:] -defined [:[: the carrier of C, the carrier of c:], the carrier' of m:] -valued Element of bool [:[:[: the carrier of C, the carrier of c:], the carrier' of m:],[:[: the carrier of C, the carrier of c:], the carrier' of m:]:]
[:[:[: the carrier of C, the carrier of c:], the carrier' of m:],[:[: the carrier of C, the carrier of c:], the carrier' of m:]:] is non empty set
bool [:[:[: the carrier of C, the carrier of c:], the carrier' of m:],[:[: the carrier of C, the carrier of c:], the carrier' of m:]:] is non empty set
[:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:] is non empty set
bool [:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:] is non empty set
{ [[b₁,b₂],b₃] where b₁ is Element of the carrier of C, b₂ is Element of the carrier of c, b₃ is Element of the carrier' of m : b₃ in Hom ((s . b₁),(x . b₂)) } is set
[c1,d1] is V1() Element of [: the carrier of C, the carrier of c:]
{c1,d1} is non empty set
{c1} is non empty set
{{c1,d1},{c1}} is non empty set
[[c1,d1],f1] is V1() Element of [:[: the carrier of C, the carrier of c:], the carrier' of m:]
{[c1,d1],f1} is non empty set
{[c1,d1]} is non empty set
{{[c1,d1],f1},{[c1,d1]}} is non empty set
id d1 is Morphism of d1,d1
dom (id d1) is Element of the carrier of c
the Source of c is Relation-like the carrier' of c -defined the carrier of c -valued Function-like V18( the carrier' of c, the carrier of c) Element of bool [: the carrier' of c, the carrier of c:]
[: the carrier' of c, the carrier of c:] is non empty set
bool [: the carrier' of c, the carrier of c:] is non empty set
the Source of c . (id d1) is Element of the carrier of c
cod (id d1) is Element of the carrier of c
the Target of c is Relation-like the carrier' of c -defined the carrier of c -valued Function-like V18( the carrier' of c, the carrier of c) Element of bool [: the carrier' of c, the carrier of c:]
the Target of c . (id d1) is Element of the carrier of c
E1 is Element of (C,c,m,s,x)
E1 `1 is Element of [: the carrier of C, the carrier of c:]
(E1 `1) `1 is Element of the carrier of C
E1 `11 is Element of the carrier of C
(E1 `1) `2 is Element of the carrier of c
E1 `12 is Element of the carrier of c
x is set
a9 is Element of (C,c,m,s,x)
C9 is Element of (C,c,m,s,x)
[a9,C9] is V1() Element of [:(C,c,m,s,x),(C,c,m,s,x):]
{a9,C9} is non empty set
{a9} is non empty set
{{a9,C9},{a9}} is non empty set
I is Element of the carrier' of C
I is Element of the carrier' of c
[I,I] is V1() Element of [: the carrier' of C, the carrier' of c:]
{I,I} is non empty set
{I} is non empty set
{{I,I},{I}} is non empty set
[[a9,C9],[I,I]] is V1() Element of [:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:]
[:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:] is non empty set
{[a9,C9],[I,I]} is non empty set
{[a9,C9]} is non empty set
{{[a9,C9],[I,I]},{[a9,C9]}} is non empty set
dom I is Element of the carrier of C
the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like V18( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is non empty set
bool [: the carrier' of C, the carrier of C:] is non empty set
the Source of C . I is Element of the carrier of C
a9 `11 is Element of the carrier of C
cod I is Element of the carrier of C
the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like V18( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
the Target of C . I is Element of the carrier of C
C9 `11 is Element of the carrier of C
dom I is Element of the carrier of c
the Source of c . I is Element of the carrier of c
a9 `12 is Element of the carrier of c
cod I is Element of the carrier of c
the Target of c . I is Element of the carrier of c
C9 `12 is Element of the carrier of c
s . I is Element of the carrier' of m
C9 `2 is Element of the carrier' of m
(C9 `2) (*) (s . I) is Element of the carrier' of m
a9 `2 is Element of the carrier' of m
x . I is Element of the carrier' of m
(x . I) (*) (a9 `2) is Element of the carrier' of m
[c1,d1] `2 is Element of the carrier of c
E1 `2 is Element of the carrier' of m
[c1,d1] `1 is Element of the carrier of C
cod f1 is Element of the carrier of m
the Target of m is Relation-like the carrier' of m -defined the carrier of m -valued Function-like V18( the carrier' of m, the carrier of m) Element of bool [: the carrier' of m, the carrier of m:]
[: the carrier' of m, the carrier of m:] is non empty set
bool [: the carrier' of m, the carrier of m:] is non empty set
the Target of m . f1 is Element of the carrier of m
id (x . d1) is Morphism of x . d1,x . d1
(id (x . d1)) (*) f1 is Element of the carrier' of m
dom f1 is Element of the carrier of m
the Source of m is Relation-like the carrier' of m -defined the carrier of m -valued Function-like V18( the carrier' of m, the carrier of m) Element of bool [: the carrier' of m, the carrier of m:]
the Source of m . f1 is Element of the carrier of m
id (s . c1) is Morphism of s . c1,s . c1
f1 (*) (id (s . c1)) is Element of the carrier' of m
id c1 is Morphism of c1,c1
s . (id c1) is Element of the carrier' of m
x . (id d1) is Element of the carrier' of m
dom (id c1) is Element of the carrier of C
the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like V18( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is non empty set
bool [: the carrier' of C, the carrier of C:] is non empty set
the Source of C . (id c1) is Element of the carrier of C
cod (id c1) is Element of the carrier of C
the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like V18( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
the Target of C . (id c1) is Element of the carrier of C
[E1,E1] is V1() Element of [:(C,c,m,s,x),(C,c,m,s,x):]
{E1,E1} is non empty set
{E1} is non empty set
{{E1,E1},{E1}} is non empty set
[(id c1),(id d1)] is V1() Element of [: the carrier' of C, the carrier' of c:]
{(id c1),(id d1)} is non empty set
{(id c1)} is non empty set
{{(id c1),(id d1)},{(id c1)}} is non empty set
[[E1,E1],[(id c1),(id d1)]] is V1() Element of [:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:]
[:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:] is non empty set
{[E1,E1],[(id c1),(id d1)]} is non empty set
{[E1,E1]} is non empty set
{{[E1,E1],[(id c1),(id d1)]},{[E1,E1]}} 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
m is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
the carrier' of m 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 carrier of C is non empty set
the carrier of c is non empty set
[: the carrier of C, the carrier of c:] is non empty set
[:[: the carrier of C, the carrier of c:], the carrier' of m:] is non empty set
s is Relation-like the carrier' of C -defined the carrier' of m -valued Function-like V18( the carrier' of C, the carrier' of m) Functor of C,m
x is Relation-like the carrier' of c -defined the carrier' of m -valued Function-like V18( the carrier' of c, the carrier' of m) Functor of c,m
(C,c,m,s,x) is non empty Relation-like [: the carrier of C, the carrier of c:] -defined the carrier' of m -valued Element of bool [:[: the carrier of C, the carrier of c:], the carrier' of m:]
bool [:[: the carrier of C, the carrier of c:], the carrier' of m:] is non empty set
[:(C,c,m,s,x),(C,c,m,s,x):] is non empty Relation-like [:[: the carrier of C, the carrier of c:], the carrier' of m:] -defined [:[: the carrier of C, the carrier of c:], the carrier' of m:] -valued Element of bool [:[:[: the carrier of C, the carrier of c:], the carrier' of m:],[:[: the carrier of C, the carrier of c:], the carrier' of m:]:]
[:[:[: the carrier of C, the carrier of c:], the carrier' of m:],[:[: the carrier of C, the carrier of c:], the carrier' of m:]:] is non empty set
bool [:[:[: the carrier of C, the carrier of c:], the carrier' of m:],[:[: the carrier of C, the carrier of c:], the carrier' of m:]:] is non empty set
[: the carrier' of C, the carrier' of c:] is non empty set
[:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:] is non empty set
(C,c,m,s,x) is non empty Relation-like [:(C,c,m,s,x),(C,c,m,s,x):] -defined [: the carrier' of C, the carrier' of c:] -valued Element of bool [:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:]
bool [:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:] is non empty set
c1 is Element of (C,c,m,s,x)
c1 `11 is set
c1 `11 is Element of (C,c,m,s,x)
c1 `12 is set
c1 `12 is Element of (C,c,m,s,x)
C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
the carrier' of C 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
the carrier of c is non empty set
[: the carrier of C, the carrier of c:] is non empty set
[: the carrier' of C, the carrier' of c:] is non empty set
m is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
the carrier' of m is non empty set
[:[: the carrier of C, the carrier of c:], the carrier' of m:] is non empty set
s is Relation-like the carrier' of C -defined the carrier' of m -valued Function-like V18( the carrier' of C, the carrier' of m) Functor of C,m
x is Relation-like the carrier' of c -defined the carrier' of m -valued Function-like V18( the carrier' of c, the carrier' of m) Functor of c,m
(C,c,m,s,x) is non empty Relation-like [: the carrier of C, the carrier of c:] -defined the carrier' of m -valued Element of bool [:[: the carrier of C, the carrier of c:], the carrier' of m:]
bool [:[: the carrier of C, the carrier of c:], the carrier' of m:] is non empty set
[:(C,c,m,s,x),(C,c,m,s,x):] is non empty Relation-like [:[: the carrier of C, the carrier of c:], the carrier' of m:] -defined [:[: the carrier of C, the carrier of c:], the carrier' of m:] -valued Element of bool [:[:[: the carrier of C, the carrier of c:], the carrier' of m:],[:[: the carrier of C, the carrier of c:], the carrier' of m:]:]
[:[:[: the carrier of C, the carrier of c:], the carrier' of m:],[:[: the carrier of C, the carrier of c:], the carrier' of m:]:] is non empty set
bool [:[:[: the carrier of C, the carrier of c:], the carrier' of m:],[:[: the carrier of C, the carrier of c:], the carrier' of m:]:] is non empty set
[:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:] is non empty set
(C,c,m,s,x) is non empty Relation-like [:(C,c,m,s,x),(C,c,m,s,x):] -defined [: the carrier' of C, the carrier' of c:] -valued Element of bool [:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:]
bool [:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:] is non empty set
[:(C,c,m,s,x),(C,c,m,s,x):] is non empty set
c1 is Element of (C,c,m,s,x)
(C,c,m,s,x,c1) is Element of (C,c,m,s,x)
(C,c,m,s,x,c1) is Element of (C,c,m,s,x)
[(C,c,m,s,x,c1),(C,c,m,s,x,c1)] is V1() Element of [:(C,c,m,s,x),(C,c,m,s,x):]
{(C,c,m,s,x,c1),(C,c,m,s,x,c1)} is non empty set
{(C,c,m,s,x,c1)} is non empty set
{{(C,c,m,s,x,c1),(C,c,m,s,x,c1)},{(C,c,m,s,x,c1)}} is non empty set
c1 `21 is Element of the carrier' of C
c1 `22 is Element of the carrier' of c
[(c1 `21),(c1 `22)] is V1() Element of [: the carrier' of C, the carrier' of c:]
{(c1 `21),(c1 `22)} is non empty set
{(c1 `21)} is non empty set
{{(c1 `21),(c1 `22)},{(c1 `21)}} is non empty set
[[(C,c,m,s,x,c1),(C,c,m,s,x,c1)],[(c1 `21),(c1 `22)]] is V1() Element of [:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:]
[:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:] is non empty set
{[(C,c,m,s,x,c1),(C,c,m,s,x,c1)],[(c1 `21),(c1 `22)]} is non empty set
{[(C,c,m,s,x,c1),(C,c,m,s,x,c1)]} is non empty set
{{[(C,c,m,s,x,c1),(C,c,m,s,x,c1)],[(c1 `21),(c1 `22)]},{[(C,c,m,s,x,c1),(C,c,m,s,x,c1)]}} is non empty set
dom (c1 `21) is Element of the carrier of C
the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like V18( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is non empty set
bool [: the carrier' of C, the carrier of C:] is non empty set
the Source of C . (c1 `21) is Element of the carrier of C
(C,c,m,s,x,c1) `11 is Element of the carrier of C
cod (c1 `21) is Element of the carrier of C
the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like V18( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
the Target of C . (c1 `21) is Element of the carrier of C
(C,c,m,s,x,c1) `11 is Element of the carrier of C
dom (c1 `22) is Element of the carrier of c
the Source of c is Relation-like the carrier' of c -defined the carrier of c -valued Function-like V18( the carrier' of c, the carrier of c) Element of bool [: the carrier' of c, the carrier of c:]
[: the carrier' of c, the carrier of c:] is non empty set
bool [: the carrier' of c, the carrier of c:] is non empty set
the Source of c . (c1 `22) is Element of the carrier of c
(C,c,m,s,x,c1) `12 is Element of the carrier of c
cod (c1 `22) is Element of the carrier of c
the Target of c is Relation-like the carrier' of c -defined the carrier of c -valued Function-like V18( the carrier' of c, the carrier of c) Element of bool [: the carrier' of c, the carrier of c:]
the Target of c . (c1 `22) is Element of the carrier of c
(C,c,m,s,x,c1) `12 is Element of the carrier of c
s . (c1 `21) is Element of the carrier' of m
(C,c,m,s,x,c1) `2 is Element of the carrier' of m
((C,c,m,s,x,c1) `2) (*) (s . (c1 `21)) is Element of the carrier' of m
(C,c,m,s,x,c1) `2 is Element of the carrier' of m
x . (c1 `22) is Element of the carrier' of m
(x . (c1 `22)) (*) ((C,c,m,s,x,c1) `2) is Element of the carrier' of m
{ [[b₃,b₄],[b₁,b₂]] where b₁ is Element of the carrier' of C, b₂ is Element of the carrier' of c, b₃, b₄ is Element of (C,c,m,s,x) : ( dom b₁ = b₃ `11 & cod b<sub>1</sub> = b<sub>4</sub> `11 & dom b₂ = b₃ `12 & cod b<sub>2</sub> = b<sub>4</sub> `12 & (b₄ `2) (*) (s . b<sub>1</sub>) = (x . b<sub>2</sub>) (*) (b<sub>3</sub> `2) ) } is set
E1 is Element of the carrier' of m
d1 is Element of the carrier of C
s . d1 is Element of the carrier of m
the carrier of m is non empty set
Obj s is Relation-like the carrier of C -defined the carrier of m -valued Function-like V18( the carrier of C, the carrier of m) Element of bool [: the carrier of C, the carrier of m:]
[: the carrier of C, the carrier of m:] is non empty set
bool [: the carrier of C, the carrier of m:] is non empty set
(Obj s) . d1 is Element of the carrier of m
f1 is Element of the carrier of c
x . f1 is Element of the carrier of m
Obj x is Relation-like the carrier of c -defined the carrier of m -valued Function-like V18( the carrier of c, the carrier of m) Element of bool [: the carrier of c, the carrier of m:]
[: the carrier of c, the carrier of m:] is non empty set
bool [: the carrier of c, the carrier of m:] is non empty set
(Obj x) . f1 is Element of the carrier of m
Hom ((s . d1),(x . f1)) is Element of bool the carrier' of m
bool the carrier' of m is non empty set
{ b₁ where b₁ is Element of the carrier' of m : ( dom b₁ = s . d1 & cod b₁ = x . f1 ) } is set
E1 is Element of (C,c,m,s,x)
E2 is Element of (C,c,m,s,x)
[E1,E2] is V1() Element of [:(C,c,m,s,x),(C,c,m,s,x):]
{E1,E2} is non empty set
{E1} is non empty set
{{E1,E2},{E1}} is non empty set
d1 is Element of the carrier' of C
f1 is Element of the carrier' of c
[d1,f1] is V1() Element of [: the carrier' of C, the carrier' of c:]
{d1,f1} is non empty set
{d1} is non empty set
{{d1,f1},{d1}} is non empty set
[[E1,E2],[d1,f1]] is V1() Element of [:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:]
{[E1,E2],[d1,f1]} is non empty set
{[E1,E2]} is non empty set
{{[E1,E2],[d1,f1]},{[E1,E2]}} is non empty set
dom d1 is Element of the carrier of C
the Source of C . d1 is Element of the carrier of C
E1 `11 is Element of the carrier of C
cod d1 is Element of the carrier of C
the Target of C . d1 is Element of the carrier of C
E2 `11 is Element of the carrier of C
dom f1 is Element of the carrier of c
the Source of c . f1 is Element of the carrier of c
E1 `12 is Element of the carrier of c
cod f1 is Element of the carrier of c
the Target of c . f1 is Element of the carrier of c
E2 `12 is Element of the carrier of c
s . d1 is Element of the carrier' of m
E2 `2 is Element of the carrier' of m
(E2 `2) (*) (s . d1) is Element of the carrier' of m
E1 `2 is Element of the carrier' of m
x . f1 is Element of the carrier' of m
(x . f1) (*) (E1 `2) is Element of the carrier' of m
C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
the carrier' of C is non empty set
m is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
the carrier' of m 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 carrier of C is non empty set
the carrier of c is non empty set
[: the carrier of C, the carrier of c:] is non empty set
[:[: the carrier of C, the carrier of c:], the carrier' of m:] is non empty set
s is Relation-like the carrier' of C -defined the carrier' of m -valued Function-like V18( the carrier' of C, the carrier' of m) Functor of C,m
x is Relation-like the carrier' of c -defined the carrier' of m -valued Function-like V18( the carrier' of c, the carrier' of m) Functor of c,m
(C,c,m,s,x) is non empty Relation-like [: the carrier of C, the carrier of c:] -defined the carrier' of m -valued Element of bool [:[: the carrier of C, the carrier of c:], the carrier' of m:]
bool [:[: the carrier of C, the carrier of c:], the carrier' of m:] is non empty set
[:(C,c,m,s,x),(C,c,m,s,x):] is non empty Relation-like [:[: the carrier of C, the carrier of c:], the carrier' of m:] -defined [:[: the carrier of C, the carrier of c:], the carrier' of m:] -valued Element of bool [:[:[: the carrier of C, the carrier of c:], the carrier' of m:],[:[: the carrier of C, the carrier of c:], the carrier' of m:]:]
[:[:[: the carrier of C, the carrier of c:], the carrier' of m:],[:[: the carrier of C, the carrier of c:], the carrier' of m:]:] is non empty set
bool [:[:[: the carrier of C, the carrier of c:], the carrier' of m:],[:[: the carrier of C, the carrier of c:], the carrier' of m:]:] is non empty set
[: the carrier' of C, the carrier' of c:] is non empty set
[:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:] is non empty set
(C,c,m,s,x) is non empty Relation-like [:(C,c,m,s,x),(C,c,m,s,x):] -defined [: the carrier' of C, the carrier' of c:] -valued Element of bool [:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:]
bool [:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:] is non empty set
E2 is Element of the carrier' of m
f1 is Element of the carrier of C
s . f1 is Element of the carrier of m
the carrier of m is non empty set
Obj s is Relation-like the carrier of C -defined the carrier of m -valued Function-like V18( the carrier of C, the carrier of m) Element of bool [: the carrier of C, the carrier of m:]
[: the carrier of C, the carrier of m:] is non empty set
bool [: the carrier of C, the carrier of m:] is non empty set
(Obj s) . f1 is Element of the carrier of m
E1 is Element of the carrier of c
x . E1 is Element of the carrier of m
Obj x is Relation-like the carrier of c -defined the carrier of m -valued Function-like V18( the carrier of c, the carrier of m) Element of bool [: the carrier of c, the carrier of m:]
[: the carrier of c, the carrier of m:] is non empty set
bool [: the carrier of c, the carrier of m:] is non empty set
(Obj x) . E1 is Element of the carrier of m
Hom ((s . f1),(x . E1)) is Element of bool the carrier' of m
bool the carrier' of m is non empty set
{ b₁ where b₁ is Element of the carrier' of m : ( dom b₁ = s . f1 & cod b₁ = x . E1 ) } is set
c1 is Element of (C,c,m,s,x)
(C,c,m,s,x,c1) is Element of (C,c,m,s,x)
d1 is Element of (C,c,m,s,x)
(C,c,m,s,x,d1) is Element of (C,c,m,s,x)
[:(C,c,m,s,x),(C,c,m,s,x):] is non empty set
(C,c,m,s,x,c1) is Element of (C,c,m,s,x)
(C,c,m,s,x,d1) is Element of (C,c,m,s,x)
[(C,c,m,s,x,c1),(C,c,m,s,x,d1)] is V1() Element of [:(C,c,m,s,x),(C,c,m,s,x):]
{(C,c,m,s,x,c1),(C,c,m,s,x,d1)} is non empty set
{(C,c,m,s,x,c1)} is non empty set
{{(C,c,m,s,x,c1),(C,c,m,s,x,d1)},{(C,c,m,s,x,c1)}} is non empty set
c1 `21 is Element of the carrier' of C
d1 `21 is Element of the carrier' of C
(d1 `21) (*) (c1 `21) is Element of the carrier' of C
c1 `22 is Element of the carrier' of c
d1 `22 is Element of the carrier' of c
(d1 `22) (*) (c1 `22) is Element of the carrier' of c
[((d1 `21) (*) (c1 `21)),((d1 `22) (*) (c1 `22))] is V1() Element of [: the carrier' of C, the carrier' of c:]
{((d1 `21) (*) (c1 `21)),((d1 `22) (*) (c1 `22))} is non empty set
{((d1 `21) (*) (c1 `21))} is non empty set
{{((d1 `21) (*) (c1 `21)),((d1 `22) (*) (c1 `22))},{((d1 `21) (*) (c1 `21))}} is non empty set
[[(C,c,m,s,x,c1),(C,c,m,s,x,d1)],[((d1 `21) (*) (c1 `21)),((d1 `22) (*) (c1 `22))]] is V1() Element of [:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:]
[:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:] is non empty set
{[(C,c,m,s,x,c1),(C,c,m,s,x,d1)],[((d1 `21) (*) (c1 `21)),((d1 `22) (*) (c1 `22))]} is non empty set
{[(C,c,m,s,x,c1),(C,c,m,s,x,d1)]} is non empty set
{{[(C,c,m,s,x,c1),(C,c,m,s,x,d1)],[((d1 `21) (*) (c1 `21)),((d1 `22) (*) (c1 `22))]},{[(C,c,m,s,x,c1),(C,c,m,s,x,d1)]}} is non empty set
cod (d1 `21) is Element of the carrier of C
the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like V18( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is non empty set
bool [: the carrier' of C, the carrier of C:] is non empty set
the Target of C . (d1 `21) is Element of the carrier of C
s . (cod (d1 `21)) is Element of the carrier of m
(Obj s) . (cod (d1 `21)) is Element of the carrier of m
s . (d1 `21) is Element of the carrier' of m
cod (s . (d1 `21)) is Element of the carrier of m
the Target of m is Relation-like the carrier' of m -defined the carrier of m -valued Function-like V18( the carrier' of m, the carrier of m) Element of bool [: the carrier' of m, the carrier of m:]
[: the carrier' of m, the carrier of m:] is non empty set
bool [: the carrier' of m, the carrier of m:] is non empty set
the Target of m . (s . (d1 `21)) is Element of the carrier of m
dom (s . (d1 `21)) is Element of the carrier of m
the Source of m is Relation-like the carrier' of m -defined the carrier of m -valued Function-like V18( the carrier' of m, the carrier of m) Element of bool [: the carrier' of m, the carrier of m:]
the Source of m . (s . (d1 `21)) is Element of the carrier of m
dom (d1 `21) is Element of the carrier of C
the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like V18( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
the Source of C . (d1 `21) is Element of the carrier of C
s . (dom (d1 `21)) is Element of the carrier of m
(Obj s) . (dom (d1 `21)) is Element of the carrier of m
s . (c1 `21) is Element of the carrier' of m
cod (s . (c1 `21)) is Element of the carrier of m
the Target of m . (s . (c1 `21)) is Element of the carrier of m
cod (c1 `21) is Element of the carrier of C
the Target of C . (c1 `21) is Element of the carrier of C
s . (cod (c1 `21)) is Element of the carrier of m
(Obj s) . (cod (c1 `21)) is Element of the carrier of m
(C,c,m,s,x,c1) `2 is Element of the carrier' of m
cod ((C,c,m,s,x,c1) `2) is Element of the carrier of m
the Target of m . ((C,c,m,s,x,c1) `2) is Element of the carrier of m
(C,c,m,s,x,c1) `12 is Element of the carrier of c
x . ((C,c,m,s,x,c1) `12) is Element of the carrier of m
(Obj x) . ((C,c,m,s,x,c1) `12) is Element of the carrier of m
dom (c1 `22) is Element of the carrier of c
the Source of c is Relation-like the carrier' of c -defined the carrier of c -valued Function-like V18( the carrier' of c, the carrier of c) Element of bool [: the carrier' of c, the carrier of c:]
[: the carrier' of c, the carrier of c:] is non empty set
bool [: the carrier' of c, the carrier of c:] is non empty set
the Source of c . (c1 `22) is Element of the carrier of c
(C,c,m,s,x,c1) `12 is Element of the carrier of c
(C,c,m,s,x,d1) `2 is Element of the carrier' of m
((C,c,m,s,x,d1) `2) (*) (s . (d1 `21)) is Element of the carrier' of m
(C,c,m,s,x,d1) `2 is Element of the carrier' of m
x . (d1 `22) is Element of the carrier' of m
(x . (d1 `22)) (*) ((C,c,m,s,x,d1) `2) is Element of the carrier' of m
dom ((C,c,m,s,x,d1) `2) is Element of the carrier of m
the Source of m . ((C,c,m,s,x,d1) `2) is Element of the carrier of m
(C,c,m,s,x,d1) `11 is Element of the carrier of C
s . ((C,c,m,s,x,d1) `11) is Element of the carrier of m
(Obj s) . ((C,c,m,s,x,d1) `11) is Element of the carrier of m
x . (c1 `22) is Element of the carrier' of m
cod (x . (c1 `22)) is Element of the carrier of m
the Target of m . (x . (c1 `22)) is Element of the carrier of m
cod (c1 `22) is Element of the carrier of c
the Target of c is Relation-like the carrier' of c -defined the carrier of c -valued Function-like V18( the carrier' of c, the carrier of c) Element of bool [: the carrier' of c, the carrier of c:]
the Target of c . (c1 `22) is Element of the carrier of c
x . (cod (c1 `22)) is Element of the carrier of m
(Obj x) . (cod (c1 `22)) is Element of the carrier of m
((C,c,m,s,x,c1) `2) (*) (s . (c1 `21)) is Element of the carrier' of m
(C,c,m,s,x,c1) `2 is Element of the carrier' of m
(x . (c1 `22)) (*) ((C,c,m,s,x,c1) `2) is Element of the carrier' of m
dom ((C,c,m,s,x,c1) `2) is Element of the carrier of m
the Source of m . ((C,c,m,s,x,c1) `2) is Element of the carrier of m
(C,c,m,s,x,c1) `11 is Element of the carrier of C
s . ((C,c,m,s,x,c1) `11) is Element of the carrier of m
(Obj s) . ((C,c,m,s,x,c1) `11) is Element of the carrier of m
dom (x . (d1 `22)) is Element of the carrier of m
the Source of m . (x . (d1 `22)) is Element of the carrier of m
dom (d1 `22) is Element of the carrier of c
the Source of c . (d1 `22) is Element of the carrier of c
x . (dom (d1 `22)) is Element of the carrier of m
(Obj x) . (dom (d1 `22)) is Element of the carrier of m
cod ((C,c,m,s,x,c1) `2) is Element of the carrier of m
the Target of m . ((C,c,m,s,x,c1) `2) is Element of the carrier of m
x . ((C,c,m,s,x,c1) `12) is Element of the carrier of m
(Obj x) . ((C,c,m,s,x,c1) `12) is Element of the carrier of m
dom (x . (c1 `22)) is Element of the carrier of m
the Source of m . (x . (c1 `22)) is Element of the carrier of m
x . (dom (c1 `22)) is Element of the carrier of m
(Obj x) . (dom (c1 `22)) is Element of the carrier of m
{ [[b₃,b₄],[b₁,b₂]] where b₁ is Element of the carrier' of C, b₂ is Element of the carrier' of c, b₃, b₄ is Element of (C,c,m,s,x) : ( dom b₁ = b₃ `11 & cod b<sub>1</sub> = b<sub>4</sub> `11 & dom b₂ = b₃ `12 & cod b<sub>2</sub> = b<sub>4</sub> `12 & (b₄ `2) (*) (s . b<sub>1</sub>) = (x . b<sub>2</sub>) (*) (b<sub>3</sub> `2) ) } is set
(C,c,m,s,x,d1) `12 is Element of the carrier of c
dom ((d1 `22) (*) (c1 `22)) is Element of the carrier of c
the Source of c . ((d1 `22) (*) (c1 `22)) is Element of the carrier of c
cod ((d1 `22) (*) (c1 `22)) is Element of the carrier of c
the Target of c . ((d1 `22) (*) (c1 `22)) is Element of the carrier of c
cod (d1 `22) is Element of the carrier of c
the Target of c . (d1 `22) is Element of the carrier of c
dom (c1 `21) is Element of the carrier of C
the Source of C . (c1 `21) is Element of the carrier of C
(C,c,m,s,x,c1) `11 is Element of the carrier of C
(C,c,m,s,x,d1) `12 is Element of the carrier of c
(C,c,m,s,x,d1) `11 is Element of the carrier of C
dom ((d1 `21) (*) (c1 `21)) is Element of the carrier of C
the Source of C . ((d1 `21) (*) (c1 `21)) is Element of the carrier of C
cod ((d1 `21) (*) (c1 `21)) is Element of the carrier of C
the Target of C . ((d1 `21) (*) (c1 `21)) is Element of the carrier of C
s . ((d1 `21) (*) (c1 `21)) is Element of the carrier' of m
((C,c,m,s,x,d1) `2) (*) (s . ((d1 `21) (*) (c1 `21))) is Element of the carrier' of m
(s . (d1 `21)) (*) (s . (c1 `21)) is Element of the carrier' of m
((C,c,m,s,x,d1) `2) (*) ((s . (d1 `21)) (*) (s . (c1 `21))) is Element of the carrier' of m
((x . (d1 `22)) (*) ((C,c,m,s,x,d1) `2)) (*) (s . (c1 `21)) is Element of the carrier' of m
(x . (d1 `22)) (*) ((x . (c1 `22)) (*) ((C,c,m,s,x,c1) `2)) is Element of the carrier' of m
(x . (d1 `22)) (*) (x . (c1 `22)) is Element of the carrier' of m
((x . (d1 `22)) (*) (x . (c1 `22))) (*) ((C,c,m,s,x,c1) `2) is Element of the carrier' of m
x . ((d1 `22) (*) (c1 `22)) is Element of the carrier' of m
(x . ((d1 `22) (*) (c1 `22))) (*) ((C,c,m,s,x,c1) `2) is Element of the carrier' of m
C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
the carrier' of C is non empty set
m is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
the carrier' of m 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 carrier of C is non empty set
the carrier of c is non empty set
[: the carrier of C, the carrier of c:] is non empty set
[:[: the carrier of C, the carrier of c:], the carrier' of m:] is non empty set
s is Relation-like the carrier' of C -defined the carrier' of m -valued Function-like V18( the carrier' of C, the carrier' of m) Functor of C,m
x is Relation-like the carrier' of c -defined the carrier' of m -valued Function-like V18( the carrier' of c, the carrier' of m) Functor of c,m
(C,c,m,s,x) is non empty Relation-like [: the carrier of C, the carrier of c:] -defined the carrier' of m -valued Element of bool [:[: the carrier of C, the carrier of c:], the carrier' of m:]
bool [:[: the carrier of C, the carrier of c:], the carrier' of m:] is non empty set
[:(C,c,m,s,x),(C,c,m,s,x):] is non empty Relation-like [:[: the carrier of C, the carrier of c:], the carrier' of m:] -defined [:[: the carrier of C, the carrier of c:], the carrier' of m:] -valued Element of bool [:[:[: the carrier of C, the carrier of c:], the carrier' of m:],[:[: the carrier of C, the carrier of c:], the carrier' of m:]:]
[:[:[: the carrier of C, the carrier of c:], the carrier' of m:],[:[: the carrier of C, the carrier of c:], the carrier' of m:]:] is non empty set
bool [:[:[: the carrier of C, the carrier of c:], the carrier' of m:],[:[: the carrier of C, the carrier of c:], the carrier' of m:]:] is non empty set
[: the carrier' of C, the carrier' of c:] is non empty set
[:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:] is non empty set
(C,c,m,s,x) is non empty Relation-like [:(C,c,m,s,x),(C,c,m,s,x):] -defined [: the carrier' of C, the carrier' of c:] -valued Element of bool [:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:]
bool [:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:] is non empty set
[:(C,c,m,s,x),(C,c,m,s,x):] is non empty Relation-like [:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:] -defined [:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:] -valued Element of bool [:[:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:],[:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:]:]
[:[:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:],[:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:]:] is non empty set
bool [:[:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:],[:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:]:] is non empty set
[:[:(C,c,m,s,x),(C,c,m,s,x):],(C,c,m,s,x):] is non empty set
bool [:[:(C,c,m,s,x),(C,c,m,s,x):],(C,c,m,s,x):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of (C,c,m,s,x) : (C,c,m,s,x,b₁) = (C,c,m,s,x,b₂) } is set
d1 is set
f1 is Element of (C,c,m,s,x)
E1 is Element of (C,c,m,s,x)
[f1,E1] is V1() Element of [:(C,c,m,s,x),(C,c,m,s,x):]
[:(C,c,m,s,x),(C,c,m,s,x):] is non empty set
{f1,E1} is non empty set
{f1} is non empty set
{{f1,E1},{f1}} is non empty set
(C,c,m,s,x,f1) is Element of (C,c,m,s,x)
(C,c,m,s,x,E1) is Element of (C,c,m,s,x)
(C,c,m,s,x,E1,f1) is Element of (C,c,m,s,x)
E2 is set
d1 is Relation-like Function-like set
dom d1 is set
rng d1 is set
f1 is set
E1 is set
d1 . E1 is set
E2 is Element of (C,c,m,s,x)
x is Element of (C,c,m,s,x)
[E2,x] is V1() Element of [:(C,c,m,s,x),(C,c,m,s,x):]
[:(C,c,m,s,x),(C,c,m,s,x):] is non empty set
{E2,x} is non empty set
{E2} is non empty set
{{E2,x},{E2}} is non empty set
(C,c,m,s,x,x,E2) is Element of (C,c,m,s,x)
f1 is set
E1 is Element of (C,c,m,s,x)
E2 is Element of (C,c,m,s,x)
[E1,E2] is V1() Element of [:(C,c,m,s,x),(C,c,m,s,x):]
[:(C,c,m,s,x),(C,c,m,s,x):] is non empty set
{E1,E2} is non empty set
{E1} is non empty set
{{E1,E2},{E1}} is non empty set
(C,c,m,s,x,E1) is Element of (C,c,m,s,x)
(C,c,m,s,x,E2) is Element of (C,c,m,s,x)
f1 is Relation-like [:(C,c,m,s,x),(C,c,m,s,x):] -defined (C,c,m,s,x) -valued Function-like Element of bool [:[:(C,c,m,s,x),(C,c,m,s,x):],(C,c,m,s,x):]
dom f1 is Relation-like set
E1 is Element of (C,c,m,s,x)
E2 is Element of (C,c,m,s,x)
[E1,E2] is V1() Element of [:(C,c,m,s,x),(C,c,m,s,x):]
[:(C,c,m,s,x),(C,c,m,s,x):] is non empty set
{E1,E2} is non empty set
{E1} is non empty set
{{E1,E2},{E1}} is non empty set
f1 . [E1,E2] is set
(C,c,m,s,x,E2,E1) is Element of (C,c,m,s,x)
x is Element of (C,c,m,s,x)
I is Element of (C,c,m,s,x)
[x,I] is V1() Element of [:(C,c,m,s,x),(C,c,m,s,x):]
{x,I} is non empty set
{x} is non empty set
{{x,I},{x}} is non empty set
(C,c,m,s,x,I,x) is Element of (C,c,m,s,x)
c1 is Relation-like [:(C,c,m,s,x),(C,c,m,s,x):] -defined (C,c,m,s,x) -valued Function-like Element of bool [:[:(C,c,m,s,x),(C,c,m,s,x):],(C,c,m,s,x):]
dom c1 is Relation-like set
d1 is Relation-like [:(C,c,m,s,x),(C,c,m,s,x):] -defined (C,c,m,s,x) -valued Function-like Element of bool [:[:(C,c,m,s,x),(C,c,m,s,x):],(C,c,m,s,x):]
dom d1 is Relation-like set
f1 is set
E1 is Element of (C,c,m,s,x)
E2 is Element of (C,c,m,s,x)
[E1,E2] is V1() Element of [:(C,c,m,s,x),(C,c,m,s,x):]
[:(C,c,m,s,x),(C,c,m,s,x):] is non empty set
{E1,E2} is non empty set
{E1} is non empty set
{{E1,E2},{E1}} is non empty set
(C,c,m,s,x,E1) is Element of (C,c,m,s,x)
(C,c,m,s,x,E2) is Element of (C,c,m,s,x)
c1 . f1 is set
(C,c,m,s,x,E2,E1) is Element of (C,c,m,s,x)
d1 . f1 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
m is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
the carrier' of m 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 carrier of C is non empty set
the carrier of c is non empty set
s is Relation-like the carrier' of C -defined the carrier' of m -valued Function-like V18( the carrier' of C, the carrier' of m) Functor of C,m
x is Relation-like the carrier' of c -defined the carrier' of m -valued Function-like V18( the carrier' of c, the carrier' of m) Functor of c,m
f1 is Element of the carrier' of m
c1 is Element of the carrier of C
s . c1 is Element of the carrier of m
the carrier of m is non empty set
Obj s is Relation-like the carrier of C -defined the carrier of m -valued Function-like V18( the carrier of C, the carrier of m) Element of bool [: the carrier of C, the carrier of m:]
[: the carrier of C, the carrier of m:] is non empty set
bool [: the carrier of C, the carrier of m:] is non empty set
(Obj s) . c1 is Element of the carrier of m
d1 is Element of the carrier of c
x . d1 is Element of the carrier of m
Obj x is Relation-like the carrier of c -defined the carrier of m -valued Function-like V18( the carrier of c, the carrier of m) Element of bool [: the carrier of c, the carrier of m:]
[: the carrier of c, the carrier of m:] is non empty set
bool [: the carrier of c, the carrier of m:] is non empty set
(Obj x) . d1 is Element of the carrier of m
Hom ((s . c1),(x . d1)) is Element of bool the carrier' of m
bool the carrier' of m is non empty set
{ b₁ where b₁ is Element of the carrier' of m : ( dom b₁ = s . c1 & cod b₁ = x . d1 ) } is set
(C,c,m,s,x) is non empty Relation-like [: the carrier of C, the carrier of c:] -defined the carrier' of m -valued Element of bool [:[: the carrier of C, the carrier of c:], the carrier' of m:]
[: the carrier of C, the carrier of c:] is non empty set
[:[: the carrier of C, the carrier of c:], the carrier' of m:] is non empty set
bool [:[: the carrier of C, the carrier of c:], the carrier' of m:] is non empty set
(C,c,m,s,x) is non empty Relation-like [:(C,c,m,s,x),(C,c,m,s,x):] -defined [: the carrier' of C, the carrier' of c:] -valued Element of bool [:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:]
[:(C,c,m,s,x),(C,c,m,s,x):] is non empty Relation-like [:[: the carrier of C, the carrier of c:], the carrier' of m:] -defined [:[: the carrier of C, the carrier of c:], the carrier' of m:] -valued Element of bool [:[:[: the carrier of C, the carrier of c:], the carrier' of m:],[:[: the carrier of C, the carrier of c:], the carrier' of m:]:]
[:[:[: the carrier of C, the carrier of c:], the carrier' of m:],[:[: the carrier of C, the carrier of c:], the carrier' of m:]:] is non empty set
bool [:[:[: the carrier of C, the carrier of c:], the carrier' of m:],[:[: the carrier of C, the carrier of c:], the carrier' of m:]:] is non empty set
[: the carrier' of C, the carrier' of c:] is non empty set
[:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:] is non empty set
bool [:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:] is non empty set
(C,c,m,s,x) is Relation-like [:(C,c,m,s,x),(C,c,m,s,x):] -defined (C,c,m,s,x) -valued Function-like Element of bool [:[:(C,c,m,s,x),(C,c,m,s,x):],(C,c,m,s,x):]
[:(C,c,m,s,x),(C,c,m,s,x):] is non empty Relation-like [:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:] -defined [:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:] -valued Element of bool [:[:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:],[:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:]:]
[:[:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:],[:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:]:] is non empty set
bool [:[:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:],[:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:]:] is non empty set
[:[:(C,c,m,s,x),(C,c,m,s,x):],(C,c,m,s,x):] is non empty set
bool [:[:(C,c,m,s,x),(C,c,m,s,x):],(C,c,m,s,x):] is non empty set
[:(C,c,m,s,x),(C,c,m,s,x):] is non empty set
[:(C,c,m,s,x),(C,c,m,s,x):] is non empty set
bool [:(C,c,m,s,x),(C,c,m,s,x):] is non empty set
x is Relation-like (C,c,m,s,x) -defined (C,c,m,s,x) -valued Function-like V18((C,c,m,s,x),(C,c,m,s,x)) Element of bool [:(C,c,m,s,x),(C,c,m,s,x):]
[:(C,c,m,s,x),(C,c,m,s,x):] is non empty set
bool [:(C,c,m,s,x),(C,c,m,s,x):] is non empty set
the Relation-like (C,c,m,s,x) -defined (C,c,m,s,x) -valued Function-like V18((C,c,m,s,x),(C,c,m,s,x)) Element of bool [:(C,c,m,s,x),(C,c,m,s,x):] is Relation-like (C,c,m,s,x) -defined (C,c,m,s,x) -valued Function-like V18((C,c,m,s,x),(C,c,m,s,x)) Element of bool [:(C,c,m,s,x),(C,c,m,s,x):]
E1 is non empty set
E2 is non empty set
[:E1,E2:] is non empty set
bool [:E1,E2:] is non empty set
[:E2,E2:] is non empty set
[:[:E2,E2:],E2:] is non empty set
bool [:[:E2,E2:],E2:] is non empty set
C9 is Relation-like (C,c,m,s,x) -defined (C,c,m,s,x) -valued Function-like V18((C,c,m,s,x),(C,c,m,s,x)) Element of bool [:(C,c,m,s,x),(C,c,m,s,x):]
[:E2,E1:] is non empty set
bool [:E2,E1:] is non empty set
D9 is Relation-like E2 -defined E1 -valued Function-like V18(E2,E1) Element of bool [:E2,E1:]
C9 is Relation-like E2 -defined E1 -valued Function-like V18(E2,E1) Element of bool [:E2,E1:]
a9 is Relation-like [:E2,E2:] -defined E2 -valued Function-like Element of bool [:[:E2,E2:],E2:]
CatStr(# E1,E2,D9,C9,a9 #) is non empty non void V55() strict CatStr
the Comp of CatStr(# E1,E2,D9,C9,a9 #) is Relation-like [: the carrier' of CatStr(# E1,E2,D9,C9,a9 #), the carrier' of CatStr(# E1,E2,D9,C9,a9 #):] -defined the carrier' of CatStr(# E1,E2,D9,C9,a9 #) -valued Function-like Element of bool [:[: the carrier' of CatStr(# E1,E2,D9,C9,a9 #), the carrier' of CatStr(# E1,E2,D9,C9,a9 #):], the carrier' of CatStr(# E1,E2,D9,C9,a9 #):]
the carrier' of CatStr(# E1,E2,D9,C9,a9 #) is non empty set
[: the carrier' of CatStr(# E1,E2,D9,C9,a9 #), the carrier' of CatStr(# E1,E2,D9,C9,a9 #):] is non empty set
[:[: the carrier' of CatStr(# E1,E2,D9,C9,a9 #), the carrier' of CatStr(# E1,E2,D9,C9,a9 #):], the carrier' of CatStr(# E1,E2,D9,C9,a9 #):] is non empty set
bool [:[: the carrier' of CatStr(# E1,E2,D9,C9,a9 #), the carrier' of CatStr(# E1,E2,D9,C9,a9 #):], the carrier' of CatStr(# E1,E2,D9,C9,a9 #):] is non empty set
dom the Comp of CatStr(# E1,E2,D9,C9,a9 #) is Relation-like set
{ [b₁,b₂] where b₁, b₂ is Element of (C,c,m,s,x) : (C,c,m,s,x,b₁) = (C,c,m,s,x,b₂) } is set
FG is Element of the carrier' of CatStr(# E1,E2,D9,C9,a9 #)
c₂₀ is Element of the carrier' of CatStr(# E1,E2,D9,C9,a9 #)
dom c₂₀ is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
the carrier of CatStr(# E1,E2,D9,C9,a9 #) is non empty set
the Source of CatStr(# E1,E2,D9,C9,a9 #) is Relation-like the carrier' of CatStr(# E1,E2,D9,C9,a9 #) -defined the carrier of CatStr(# E1,E2,D9,C9,a9 #) -valued Function-like V18( the carrier' of CatStr(# E1,E2,D9,C9,a9 #), the carrier of CatStr(# E1,E2,D9,C9,a9 #)) Element of bool [: the carrier' of CatStr(# E1,E2,D9,C9,a9 #), the carrier of CatStr(# E1,E2,D9,C9,a9 #):]
[: the carrier' of CatStr(# E1,E2,D9,C9,a9 #), the carrier of CatStr(# E1,E2,D9,C9,a9 #):] is non empty set
bool [: the carrier' of CatStr(# E1,E2,D9,C9,a9 #), the carrier of CatStr(# E1,E2,D9,C9,a9 #):] is non empty set
the Source of CatStr(# E1,E2,D9,C9,a9 #) . c₂₀ is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
cod FG is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
the Target of CatStr(# E1,E2,D9,C9,a9 #) is Relation-like the carrier' of CatStr(# E1,E2,D9,C9,a9 #) -defined the carrier of CatStr(# E1,E2,D9,C9,a9 #) -valued Function-like V18( the carrier' of CatStr(# E1,E2,D9,C9,a9 #), the carrier of CatStr(# E1,E2,D9,C9,a9 #)) Element of bool [: the carrier' of CatStr(# E1,E2,D9,C9,a9 #), the carrier of CatStr(# E1,E2,D9,C9,a9 #):]
the Target of CatStr(# E1,E2,D9,C9,a9 #) . FG is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
c₂₀ (*) FG is Element of the carrier' of CatStr(# E1,E2,D9,C9,a9 #)
f1 is Element of (C,c,m,s,x)
(C,c,m,s,x,f1) is Element of (C,c,m,s,x)
f1 `21 is Element of the carrier' of C
f1 `22 is Element of the carrier' of c
g1 is Element of (C,c,m,s,x)
(C,c,m,s,x,g1) is Element of (C,c,m,s,x)
[(C,c,m,s,x,f1),(C,c,m,s,x,g1)] is V1() Element of [:(C,c,m,s,x),(C,c,m,s,x):]
{(C,c,m,s,x,f1),(C,c,m,s,x,g1)} is non empty set
{(C,c,m,s,x,f1)} is non empty set
{{(C,c,m,s,x,f1),(C,c,m,s,x,g1)},{(C,c,m,s,x,f1)}} is non empty set
g1 `21 is Element of the carrier' of C
(g1 `21) (*) (f1 `21) is Element of the carrier' of C
g1 `22 is Element of the carrier' of c
(g1 `22) (*) (f1 `22) is Element of the carrier' of c
[((g1 `21) (*) (f1 `21)),((g1 `22) (*) (f1 `22))] is V1() Element of [: the carrier' of C, the carrier' of c:]
{((g1 `21) (*) (f1 `21)),((g1 `22) (*) (f1 `22))} is non empty set
{((g1 `21) (*) (f1 `21))} is non empty set
{{((g1 `21) (*) (f1 `21)),((g1 `22) (*) (f1 `22))},{((g1 `21) (*) (f1 `21))}} is non empty set
[[(C,c,m,s,x,f1),(C,c,m,s,x,g1)],[((g1 `21) (*) (f1 `21)),((g1 `22) (*) (f1 `22))]] is V1() Element of [:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:]
[:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:] is non empty set
{[(C,c,m,s,x,f1),(C,c,m,s,x,g1)],[((g1 `21) (*) (f1 `21)),((g1 `22) (*) (f1 `22))]} is non empty set
{[(C,c,m,s,x,f1),(C,c,m,s,x,g1)]} is non empty set
{{[(C,c,m,s,x,f1),(C,c,m,s,x,g1)],[((g1 `21) (*) (f1 `21)),((g1 `22) (*) (f1 `22))]},{[(C,c,m,s,x,f1),(C,c,m,s,x,g1)]}} is non empty set
(C,c,m,s,x,g1) is Element of (C,c,m,s,x)
(C,c,m,s,x,f1) is Element of (C,c,m,s,x)
[g1,f1] is V1() Element of [:(C,c,m,s,x),(C,c,m,s,x):]
[:(C,c,m,s,x),(C,c,m,s,x):] is non empty set
{g1,f1} is non empty set
{g1} is non empty set
{{g1,f1},{g1}} is non empty set
dom a9 is Relation-like set
a9 . (g1,f1) is set
[g1,f1] is V1() set
a9 . [g1,f1] is set
(C,c,m,s,x,f1,g1) is Element of (C,c,m,s,x)
a9 . (c₂₀,FG) is set
[c₂₀,FG] is V1() set
{c₂₀,FG} is non empty set
{c₂₀} is non empty set
{{c₂₀,FG},{c₂₀}} is non empty set
a9 . [c₂₀,FG] is set
the carrier of CatStr(# E1,E2,D9,C9,a9 #) is non empty set
FG is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
Hom (FG,FG) is Element of bool the carrier' of CatStr(# E1,E2,D9,C9,a9 #)
bool the carrier' of CatStr(# E1,E2,D9,C9,a9 #) is non empty set
{ b₁ where b₁ is Element of the carrier' of CatStr(# E1,E2,D9,C9,a9 #) : ( dom b₁ = FG & cod b₁ = FG ) } is set
c₂₀ is Element of (C,c,m,s,x)
[c₂₀,c₂₀] is V1() Element of [:(C,c,m,s,x),(C,c,m,s,x):]
{c₂₀,c₂₀} is non empty set
{c₂₀} is non empty set
{{c₂₀,c₂₀},{c₂₀}} is non empty set
c₂₀ `11 is Element of the carrier of C
id (c<sub>20</sub> `11) is Morphism of c₂₀ `11 ,c<sub>20</sub> `11
c₂₀ `12 is Element of the carrier of c
id (c<sub>20</sub> `12) is Morphism of c₂₀ `12 ,c<sub>20</sub> `12
[(id (c₂₀ `11)),(id (c<sub>20</sub> `12))] is V1() Element of [: the carrier' of C, the carrier' of c:]
{(id (c₂₀ `11)),(id (c<sub>20</sub> `12))} is non empty set
{(id (c₂₀ `11))} is non empty set
{{(id (c<sub>20</sub> `11)),(id (c₂₀ `12))},{(id (c<sub>20</sub> `11))}} is non empty set
[[c₂₀,c₂₀],[(id (c₂₀ `11)),(id (c<sub>20</sub> `12))]] is V1() Element of [:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:]
[:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:] is non empty set
{[c₂₀,c₂₀],[(id (c₂₀ `11)),(id (c<sub>20</sub> `12))]} is non empty set
{[c₂₀,c₂₀]} is non empty set
{{[c₂₀,c₂₀],[(id (c₂₀ `11)),(id (c<sub>20</sub> `12))]},{[c₂₀,c₂₀]}} is non empty set
g1 is Element of the carrier' of C
dom g1 is Element of the carrier of C
the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like V18( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is non empty set
bool [: the carrier' of C, the carrier of C:] is non empty set
the Source of C . g1 is Element of the carrier of C
cod g1 is Element of the carrier of C
the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like V18( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
the Target of C . g1 is Element of the carrier of C
k1 is Element of the carrier' of c
dom k1 is Element of the carrier of c
the Source of c is Relation-like the carrier' of c -defined the carrier of c -valued Function-like V18( the carrier' of c, the carrier of c) Element of bool [: the carrier' of c, the carrier of c:]
[: the carrier' of c, the carrier of c:] is non empty set
bool [: the carrier' of c, the carrier of c:] is non empty set
the Source of c . k1 is Element of the carrier of c
cod k1 is Element of the carrier of c
the Target of c is Relation-like the carrier' of c -defined the carrier of c -valued Function-like V18( the carrier' of c, the carrier of c) Element of bool [: the carrier' of c, the carrier of c:]
the Target of c . k1 is Element of the carrier of c
{ [[b₁,b₂],b₃] where b₁ is Element of the carrier of C, b₂ is Element of the carrier of c, b₃ is Element of the carrier' of m : b₃ in Hom ((s . b₁),(x . b₂)) } is set
k2 is Element of the carrier of C
gf is Element of the carrier of c
[k2,gf] is V1() Element of [: the carrier of C, the carrier of c:]
{k2,gf} is non empty set
{k2} is non empty set
{{k2,gf},{k2}} is non empty set
hg is Element of the carrier' of m
[[k2,gf],hg] is V1() Element of [:[: the carrier of C, the carrier of c:], the carrier' of m:]
{[k2,gf],hg} is non empty set
{[k2,gf]} is non empty set
{{[k2,gf],hg},{[k2,gf]}} is non empty set
s . k2 is Element of the carrier of m
(Obj s) . k2 is Element of the carrier of m
x . gf is Element of the carrier of m
(Obj x) . gf is Element of the carrier of m
Hom ((s . k2),(x . gf)) is Element of bool the carrier' of m
{ b₁ where b₁ is Element of the carrier' of m : ( dom b₁ = s . k2 & cod b₁ = x . gf ) } is set
s . g1 is Element of the carrier' of m
s . (c₂₀ `11) is Element of the carrier of m
(Obj s) . (c<sub>20</sub> `11) is Element of the carrier of m
id (s . (c₂₀ `11)) is Morphism of s . (c<sub>20</sub> `11),s . (c₂₀ `11)
x . k1 is Element of the carrier' of m
x . (c<sub>20</sub> `12) is Element of the carrier of m
(Obj x) . (c₂₀ `12) is Element of the carrier of m
id (x . (c<sub>20</sub> `12)) is Morphism of x . (c₂₀ `12),x . (c<sub>20</sub> `12)
[[k2,gf],hg] `2 is Element of the carrier' of m
c<sub>20</sub> `2 is Element of the carrier' of m
cod (c₂₀ `2) is Element of the carrier of m
the Target of m is Relation-like the carrier' of m -defined the carrier of m -valued Function-like V18( the carrier' of m, the carrier of m) Element of bool [: the carrier' of m, the carrier of m:]
[: the carrier' of m, the carrier of m:] is non empty set
bool [: the carrier' of m, the carrier of m:] is non empty set
the Target of m . (c<sub>20</sub> `2) is Element of the carrier of m
cod hg is Element of the carrier of m
the Target of m . hg is Element of the carrier of m
dom (c₂₀ `2) is Element of the carrier of m
the Source of m is Relation-like the carrier' of m -defined the carrier of m -valued Function-like V18( the carrier' of m, the carrier of m) Element of bool [: the carrier' of m, the carrier of m:]
the Source of m . (c<sub>20</sub> `2) is Element of the carrier of m
(c₂₀ `2) (*) (s . g1) is Element of the carrier' of m
(x . k1) (*) (c<sub>20</sub> `2) is Element of the carrier' of m
{ [[b₃,b₄],[b₁,b₂]] where b₁ is Element of the carrier' of C, b₂ is Element of the carrier' of c, b₃, b₄ is Element of (C,c,m,s,x) : ( dom b₁ = b₃ `11 & cod b<sub>1</sub> = b<sub>4</sub> `11 & dom b₂ = b₃ `12 & cod b<sub>2</sub> = b<sub>4</sub> `12 & (b₄ `2) (*) (s . b<sub>1</sub>) = (x . b<sub>2</sub>) (*) (b<sub>3</sub> `2) ) } is set
i is Element of the carrier' of CatStr(# E1,E2,D9,C9,a9 #)
cod i is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
the Target of CatStr(# E1,E2,D9,C9,a9 #) is Relation-like the carrier' of CatStr(# E1,E2,D9,C9,a9 #) -defined the carrier of CatStr(# E1,E2,D9,C9,a9 #) -valued Function-like V18( the carrier' of CatStr(# E1,E2,D9,C9,a9 #), the carrier of CatStr(# E1,E2,D9,C9,a9 #)) Element of bool [: the carrier' of CatStr(# E1,E2,D9,C9,a9 #), the carrier of CatStr(# E1,E2,D9,C9,a9 #):]
[: the carrier' of CatStr(# E1,E2,D9,C9,a9 #), the carrier of CatStr(# E1,E2,D9,C9,a9 #):] is non empty set
bool [: the carrier' of CatStr(# E1,E2,D9,C9,a9 #), the carrier of CatStr(# E1,E2,D9,C9,a9 #):] is non empty set
the Target of CatStr(# E1,E2,D9,C9,a9 #) . i is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
C9 . i is set
[g1,k1] is V1() Element of [: the carrier' of C, the carrier' of c:]
{g1,k1} is non empty set
{g1} is non empty set
{{g1,k1},{g1}} is non empty set
[[c₂₀,c₂₀],[g1,k1]] is V1() Element of [:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:]
{[c₂₀,c₂₀],[g1,k1]} is non empty set
{{[c₂₀,c₂₀],[g1,k1]},{[c₂₀,c₂₀]}} is non empty set
[[c₂₀,c₂₀],[g1,k1]] `12 is Element of (C,c,m,s,x)
dom i is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
the Source of CatStr(# E1,E2,D9,C9,a9 #) is Relation-like the carrier' of CatStr(# E1,E2,D9,C9,a9 #) -defined the carrier of CatStr(# E1,E2,D9,C9,a9 #) -valued Function-like V18( the carrier' of CatStr(# E1,E2,D9,C9,a9 #), the carrier of CatStr(# E1,E2,D9,C9,a9 #)) Element of bool [: the carrier' of CatStr(# E1,E2,D9,C9,a9 #), the carrier of CatStr(# E1,E2,D9,C9,a9 #):]
the Source of CatStr(# E1,E2,D9,C9,a9 #) . i is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
D9 . i is set
[[c<sub>20</sub>,c<sub>20</sub>],[g1,k1]] `11 is Element of (C,c,m,s,x)
FG is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
c₂₀ is Element of (C,c,m,s,x)
[c₂₀,c₂₀] is V1() Element of [:(C,c,m,s,x),(C,c,m,s,x):]
{c₂₀,c₂₀} is non empty set
{c₂₀} is non empty set
{{c₂₀,c₂₀},{c₂₀}} is non empty set
c₂₀ `11 is Element of the carrier of C
id (c<sub>20</sub> `11) is Morphism of c₂₀ `11 ,c<sub>20</sub> `11
c₂₀ `12 is Element of the carrier of c
id (c<sub>20</sub> `12) is Morphism of c₂₀ `12 ,c<sub>20</sub> `12
[(id (c₂₀ `11)),(id (c<sub>20</sub> `12))] is V1() Element of [: the carrier' of C, the carrier' of c:]
{(id (c₂₀ `11)),(id (c<sub>20</sub> `12))} is non empty set
{(id (c₂₀ `11))} is non empty set
{{(id (c<sub>20</sub> `11)),(id (c₂₀ `12))},{(id (c<sub>20</sub> `11))}} is non empty set
[[c₂₀,c₂₀],[(id (c₂₀ `11)),(id (c<sub>20</sub> `12))]] is V1() Element of [:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:]
[:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:] is non empty set
{[c₂₀,c₂₀],[(id (c₂₀ `11)),(id (c<sub>20</sub> `12))]} is non empty set
{[c₂₀,c₂₀]} is non empty set
{{[c₂₀,c₂₀],[(id (c₂₀ `11)),(id (c<sub>20</sub> `12))]},{[c₂₀,c₂₀]}} is non empty set
g1 is Element of the carrier' of C
dom g1 is Element of the carrier of C
the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like V18( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is non empty set
bool [: the carrier' of C, the carrier of C:] is non empty set
the Source of C . g1 is Element of the carrier of C
cod g1 is Element of the carrier of C
the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like V18( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
the Target of C . g1 is Element of the carrier of C
k1 is Element of the carrier' of c
dom k1 is Element of the carrier of c
the Source of c is Relation-like the carrier' of c -defined the carrier of c -valued Function-like V18( the carrier' of c, the carrier of c) Element of bool [: the carrier' of c, the carrier of c:]
[: the carrier' of c, the carrier of c:] is non empty set
bool [: the carrier' of c, the carrier of c:] is non empty set
the Source of c . k1 is Element of the carrier of c
cod k1 is Element of the carrier of c
the Target of c is Relation-like the carrier' of c -defined the carrier of c -valued Function-like V18( the carrier' of c, the carrier of c) Element of bool [: the carrier' of c, the carrier of c:]
the Target of c . k1 is Element of the carrier of c
{ [[b₁,b₂],b₃] where b₁ is Element of the carrier of C, b₂ is Element of the carrier of c, b₃ is Element of the carrier' of m : b₃ in Hom ((s . b₁),(x . b₂)) } is set
k2 is Element of the carrier of C
gf is Element of the carrier of c
[k2,gf] is V1() Element of [: the carrier of C, the carrier of c:]
{k2,gf} is non empty set
{k2} is non empty set
{{k2,gf},{k2}} is non empty set
hg is Element of the carrier' of m
[[k2,gf],hg] is V1() Element of [:[: the carrier of C, the carrier of c:], the carrier' of m:]
{[k2,gf],hg} is non empty set
{[k2,gf]} is non empty set
{{[k2,gf],hg},{[k2,gf]}} is non empty set
s . k2 is Element of the carrier of m
(Obj s) . k2 is Element of the carrier of m
x . gf is Element of the carrier of m
(Obj x) . gf is Element of the carrier of m
Hom ((s . k2),(x . gf)) is Element of bool the carrier' of m
{ b₁ where b₁ is Element of the carrier' of m : ( dom b₁ = s . k2 & cod b₁ = x . gf ) } is set
s . g1 is Element of the carrier' of m
s . (c₂₀ `11) is Element of the carrier of m
(Obj s) . (c<sub>20</sub> `11) is Element of the carrier of m
id (s . (c₂₀ `11)) is Morphism of s . (c<sub>20</sub> `11),s . (c₂₀ `11)
x . k1 is Element of the carrier' of m
x . (c<sub>20</sub> `12) is Element of the carrier of m
(Obj x) . (c₂₀ `12) is Element of the carrier of m
id (x . (c<sub>20</sub> `12)) is Morphism of x . (c₂₀ `12),x . (c<sub>20</sub> `12)
[[k2,gf],hg] `2 is Element of the carrier' of m
c<sub>20</sub> `2 is Element of the carrier' of m
cod (c₂₀ `2) is Element of the carrier of m
the Target of m is Relation-like the carrier' of m -defined the carrier of m -valued Function-like V18( the carrier' of m, the carrier of m) Element of bool [: the carrier' of m, the carrier of m:]
[: the carrier' of m, the carrier of m:] is non empty set
bool [: the carrier' of m, the carrier of m:] is non empty set
the Target of m . (c<sub>20</sub> `2) is Element of the carrier of m
cod hg is Element of the carrier of m
the Target of m . hg is Element of the carrier of m
dom (c₂₀ `2) is Element of the carrier of m
the Source of m is Relation-like the carrier' of m -defined the carrier of m -valued Function-like V18( the carrier' of m, the carrier of m) Element of bool [: the carrier' of m, the carrier of m:]
the Source of m . (c<sub>20</sub> `2) is Element of the carrier of m
(c₂₀ `2) (*) (s . g1) is Element of the carrier' of m
(x . k1) (*) (c<sub>20</sub> `2) is Element of the carrier' of m
{ [[b₃,b₄],[b₁,b₂]] where b₁ is Element of the carrier' of C, b₂ is Element of the carrier' of c, b₃, b₄ is Element of (C,c,m,s,x) : ( dom b₁ = b₃ `11 & cod b<sub>1</sub> = b<sub>4</sub> `11 & dom b₂ = b₃ `12 & cod b<sub>2</sub> = b<sub>4</sub> `12 & (b₄ `2) (*) (s . b<sub>1</sub>) = (x . b<sub>2</sub>) (*) (b<sub>3</sub> `2) ) } is set
i is Element of the carrier' of CatStr(# E1,E2,D9,C9,a9 #)
cod i is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
the Target of CatStr(# E1,E2,D9,C9,a9 #) is Relation-like the carrier' of CatStr(# E1,E2,D9,C9,a9 #) -defined the carrier of CatStr(# E1,E2,D9,C9,a9 #) -valued Function-like V18( the carrier' of CatStr(# E1,E2,D9,C9,a9 #), the carrier of CatStr(# E1,E2,D9,C9,a9 #)) Element of bool [: the carrier' of CatStr(# E1,E2,D9,C9,a9 #), the carrier of CatStr(# E1,E2,D9,C9,a9 #):]
[: the carrier' of CatStr(# E1,E2,D9,C9,a9 #), the carrier of CatStr(# E1,E2,D9,C9,a9 #):] is non empty set
bool [: the carrier' of CatStr(# E1,E2,D9,C9,a9 #), the carrier of CatStr(# E1,E2,D9,C9,a9 #):] is non empty set
the Target of CatStr(# E1,E2,D9,C9,a9 #) . i is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
C9 . i is set
[g1,k1] is V1() Element of [: the carrier' of C, the carrier' of c:]
{g1,k1} is non empty set
{g1} is non empty set
{{g1,k1},{g1}} is non empty set
[[c₂₀,c₂₀],[g1,k1]] is V1() Element of [:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:]
{[c₂₀,c₂₀],[g1,k1]} is non empty set
{{[c₂₀,c₂₀],[g1,k1]},{[c₂₀,c₂₀]}} is non empty set
[[c₂₀,c₂₀],[g1,k1]] `12 is Element of (C,c,m,s,x)
dom i is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
the Source of CatStr(# E1,E2,D9,C9,a9 #) is Relation-like the carrier' of CatStr(# E1,E2,D9,C9,a9 #) -defined the carrier of CatStr(# E1,E2,D9,C9,a9 #) -valued Function-like V18( the carrier' of CatStr(# E1,E2,D9,C9,a9 #), the carrier of CatStr(# E1,E2,D9,C9,a9 #)) Element of bool [: the carrier' of CatStr(# E1,E2,D9,C9,a9 #), the carrier of CatStr(# E1,E2,D9,C9,a9 #):]
the Source of CatStr(# E1,E2,D9,C9,a9 #) . i is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
D9 . i is set
[[c<sub>20</sub>,c<sub>20</sub>],[g1,k1]] `11 is Element of (C,c,m,s,x)
Hom (FG,FG) is Element of bool the carrier' of CatStr(# E1,E2,D9,C9,a9 #)
bool the carrier' of CatStr(# E1,E2,D9,C9,a9 #) is non empty set
{ b₁ where b₁ is Element of the carrier' of CatStr(# E1,E2,D9,C9,a9 #) : ( dom b₁ = FG & cod b₁ = FG ) } is set
i is Morphism of FG,FG
b is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
Hom (FG,b) is Element of bool the carrier' of CatStr(# E1,E2,D9,C9,a9 #)
{ b₁ where b₁ is Element of the carrier' of CatStr(# E1,E2,D9,C9,a9 #) : ( dom b₁ = FG & cod b₁ = b ) } is set
Hom (b,FG) is Element of bool the carrier' of CatStr(# E1,E2,D9,C9,a9 #)
{ b₁ where b₁ is Element of the carrier' of CatStr(# E1,E2,D9,C9,a9 #) : ( dom b₁ = b & cod b₁ = FG ) } is set
g is Morphism of FG,b
g (*) i is Element of the carrier' of CatStr(# E1,E2,D9,C9,a9 #)
gg is Element of (C,c,m,s,x)
o1 is Element of (C,c,m,s,x)
o2 is Element of (C,c,m,s,x)
[o1,o2] is V1() Element of [:(C,c,m,s,x),(C,c,m,s,x):]
{o1,o2} is non empty set
{o1} is non empty set
{{o1,o2},{o1}} is non empty set
g1 is Element of the carrier' of C
h1 is Element of the carrier' of c
[g1,h1] is V1() Element of [: the carrier' of C, the carrier' of c:]
{g1,h1} is non empty set
{g1} is non empty set
{{g1,h1},{g1}} is non empty set
[[o1,o2],[g1,h1]] is V1() Element of [:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:]
{[o1,o2],[g1,h1]} is non empty set
{[o1,o2]} is non empty set
{{[o1,o2],[g1,h1]},{[o1,o2]}} is non empty set
dom g1 is Element of the carrier of C
the Source of C . g1 is Element of the carrier of C
o1 `11 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
o2 `11 is Element of the carrier of C
dom h1 is Element of the carrier of c
the Source of c . h1 is Element of the carrier of c
o1 `12 is Element of the carrier of c
cod h1 is Element of the carrier of c
the Target of c . h1 is Element of the carrier of c
o2 `12 is Element of the carrier of c
s . g1 is Element of the carrier' of m
o2 `2 is Element of the carrier' of m
(o2 `2) (*) (s . g1) is Element of the carrier' of m
o1 `2 is Element of the carrier' of m
x . h1 is Element of the carrier' of m
(x . h1) (*) (o1 `2) is Element of the carrier' of m
dom (C,c,m,s,x) is Relation-like set
ii is Element of (C,c,m,s,x)
ii `21 is Element of the carrier' of C
[[c<sub>20</sub>,c<sub>20</sub>],[(id (c<sub>20</sub> `11)),(id (c₂₀ `12))]] `21 is Element of the carrier' of C
ii `22 is Element of the carrier' of c
[[c<sub>20</sub>,c<sub>20</sub>],[(id (c<sub>20</sub> `11)),(id (c₂₀ `12))]] `22 is Element of the carrier' of c
[[o1,o2],[g1,h1]] `11 is Element of (C,c,m,s,x)
(C,c,m,s,x,gg) is Element of (C,c,m,s,x)
[[o1,o2],[g1,h1]] `12 is Element of (C,c,m,s,x)
(C,c,m,s,x,gg) is Element of (C,c,m,s,x)
[[o1,o2],[g1,h1]] `21 is Element of the carrier' of C
gg `21 is Element of the carrier' of C
[[o1,o2],[g1,h1]] `22 is Element of the carrier' of c
gg `22 is Element of the carrier' of c
dom g is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
the Source of CatStr(# E1,E2,D9,C9,a9 #) . g is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
dom (gg `21) is Element of the carrier of C
the Source of C . (gg `21) is Element of the carrier of C
dom ([[o1,o2],[g1,h1]] `21) is Element of the carrier of C
the Source of C . ([[o1,o2],[g1,h1]] `21) is Element of the carrier of C
[[k2,gf],hg] `11 is Element of the carrier of C
dom (gg `22) is Element of the carrier of c
the Source of c . (gg `22) is Element of the carrier of c
dom ([[o1,o2],[g1,h1]] `22) is Element of the carrier of c
the Source of c . ([[o1,o2],[g1,h1]] `22) is Element of the carrier of c
[[k2,gf],hg] `12 is Element of the carrier of c
(C,c,m,s,x,ii) is Element of (C,c,m,s,x)
[[c₂₀,c₂₀],[(id (c₂₀ `11)),(id (c<sub>20</sub> `12))]] `11 is Element of (C,c,m,s,x)
D9 . gg is set
(C,c,m,s,x,ii) is Element of (C,c,m,s,x)
[gg,ii] is V1() Element of [:(C,c,m,s,x),(C,c,m,s,x):]
[:(C,c,m,s,x),(C,c,m,s,x):] is non empty set
{gg,ii} is non empty set
{gg} is non empty set
{{gg,ii},{gg}} is non empty set
(C,c,m,s,x) . (g,i) is set
[g,i] is V1() set
{g,i} is non empty set
{g} is non empty set
{{g,i},{g}} is non empty set
(C,c,m,s,x) . [g,i] is set
(C,c,m,s,x,ii,gg) is Element of (C,c,m,s,x)
[(C,c,m,s,x,gg),(C,c,m,s,x,gg)] is V1() Element of [:(C,c,m,s,x),(C,c,m,s,x):]
{(C,c,m,s,x,gg),(C,c,m,s,x,gg)} is non empty set
{(C,c,m,s,x,gg)} is non empty set
{{(C,c,m,s,x,gg),(C,c,m,s,x,gg)},{(C,c,m,s,x,gg)}} is non empty set
(gg `21) (*) (id (c₂₀ `11)) is Element of the carrier' of C
(gg `22) (*) (ii `22) is Element of the carrier' of c
[((gg `21) (*) (id (c₂₀ `11))),((gg `22) (*) (ii `22))] is V1() Element of [: the carrier' of C, the carrier' of c:]
{((gg `21) (*) (id (c₂₀ `11))),((gg `22) (*) (ii `22))} is non empty set
{((gg `21) (*) (id (c₂₀ `11)))} is non empty set
{{((gg `21) (*) (id (c₂₀ `11))),((gg `22) (*) (ii `22))},{((gg `21) (*) (id (c₂₀ `11)))}} is non empty set
[[(C,c,m,s,x,gg),(C,c,m,s,x,gg)],[((gg `21) (*) (id (c₂₀ `11))),((gg `22) (*) (ii `22))]] is V1() Element of [:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:]
{[(C,c,m,s,x,gg),(C,c,m,s,x,gg)],[((gg `21) (*) (id (c₂₀ `11))),((gg `22) (*) (ii `22))]} is non empty set
{[(C,c,m,s,x,gg),(C,c,m,s,x,gg)]} is non empty set
{{[(C,c,m,s,x,gg),(C,c,m,s,x,gg)],[((gg `21) (*) (id (c₂₀ `11))),((gg `22) (*) (ii `22))]},{[(C,c,m,s,x,gg),(C,c,m,s,x,gg)]}} is non empty set
[(gg `21),((gg `22) (*) (ii `22))] is V1() Element of [: the carrier' of C, the carrier' of c:]
{(gg `21),((gg `22) (*) (ii `22))} is non empty set
{(gg `21)} is non empty set
{{(gg `21),((gg `22) (*) (ii `22))},{(gg `21)}} is non empty set
[[(C,c,m,s,x,gg),(C,c,m,s,x,gg)],[(gg `21),((gg `22) (*) (ii `22))]] is V1() Element of [:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:]
{[(C,c,m,s,x,gg),(C,c,m,s,x,gg)],[(gg `21),((gg `22) (*) (ii `22))]} is non empty set
{{[(C,c,m,s,x,gg),(C,c,m,s,x,gg)],[(gg `21),((gg `22) (*) (ii `22))]},{[(C,c,m,s,x,gg),(C,c,m,s,x,gg)]}} is non empty set
[(gg `21),(gg `22)] is V1() Element of [: the carrier' of C, the carrier' of c:]
{(gg `21),(gg `22)} is non empty set
{{(gg `21),(gg `22)},{(gg `21)}} is non empty set
[[(C,c,m,s,x,gg),(C,c,m,s,x,gg)],[(gg `21),(gg `22)]] is V1() Element of [:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:]
{[(C,c,m,s,x,gg),(C,c,m,s,x,gg)],[(gg `21),(gg `22)]} is non empty set
{{[(C,c,m,s,x,gg),(C,c,m,s,x,gg)],[(gg `21),(gg `22)]},{[(C,c,m,s,x,gg),(C,c,m,s,x,gg)]}} is non empty set
g is Morphism of b,FG
i (*) g is Element of the carrier' of CatStr(# E1,E2,D9,C9,a9 #)
gg is Element of (C,c,m,s,x)
o1 is Element of (C,c,m,s,x)
o2 is Element of (C,c,m,s,x)
[o1,o2] is V1() Element of [:(C,c,m,s,x),(C,c,m,s,x):]
{o1,o2} is non empty set
{o1} is non empty set
{{o1,o2},{o1}} is non empty set
g1 is Element of the carrier' of C
h1 is Element of the carrier' of c
[g1,h1] is V1() Element of [: the carrier' of C, the carrier' of c:]
{g1,h1} is non empty set
{g1} is non empty set
{{g1,h1},{g1}} is non empty set
[[o1,o2],[g1,h1]] is V1() Element of [:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:]
{[o1,o2],[g1,h1]} is non empty set
{[o1,o2]} is non empty set
{{[o1,o2],[g1,h1]},{[o1,o2]}} is non empty set
dom g1 is Element of the carrier of C
the Source of C . g1 is Element of the carrier of C
o1 `11 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
o2 `11 is Element of the carrier of C
dom h1 is Element of the carrier of c
the Source of c . h1 is Element of the carrier of c
o1 `12 is Element of the carrier of c
cod h1 is Element of the carrier of c
the Target of c . h1 is Element of the carrier of c
o2 `12 is Element of the carrier of c
s . g1 is Element of the carrier' of m
o2 `2 is Element of the carrier' of m
(o2 `2) (*) (s . g1) is Element of the carrier' of m
o1 `2 is Element of the carrier' of m
x . h1 is Element of the carrier' of m
(x . h1) (*) (o1 `2) is Element of the carrier' of m
dom (C,c,m,s,x) is Relation-like set
ii is Element of (C,c,m,s,x)
ii `21 is Element of the carrier' of C
[[c<sub>20</sub>,c<sub>20</sub>],[(id (c<sub>20</sub> `11)),(id (c₂₀ `12))]] `21 is Element of the carrier' of C
ii `22 is Element of the carrier' of c
[[c<sub>20</sub>,c<sub>20</sub>],[(id (c<sub>20</sub> `11)),(id (c₂₀ `12))]] `22 is Element of the carrier' of c
[[o1,o2],[g1,h1]] `11 is Element of (C,c,m,s,x)
(C,c,m,s,x,gg) is Element of (C,c,m,s,x)
[[o1,o2],[g1,h1]] `12 is Element of (C,c,m,s,x)
(C,c,m,s,x,gg) is Element of (C,c,m,s,x)
[[o1,o2],[g1,h1]] `21 is Element of the carrier' of C
gg `21 is Element of the carrier' of C
[[o1,o2],[g1,h1]] `22 is Element of the carrier' of c
gg `22 is Element of the carrier' of c
cod g is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
the Target of CatStr(# E1,E2,D9,C9,a9 #) . g is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
cod (gg `21) is Element of the carrier of C
the Target of C . (gg `21) is Element of the carrier of C
cod ([[o1,o2],[g1,h1]] `21) is Element of the carrier of C
the Target of C . ([[o1,o2],[g1,h1]] `21) is Element of the carrier of C
[[k2,gf],hg] `11 is Element of the carrier of C
cod (gg `22) is Element of the carrier of c
the Target of c . (gg `22) is Element of the carrier of c
cod ([[o1,o2],[g1,h1]] `22) is Element of the carrier of c
the Target of c . ([[o1,o2],[g1,h1]] `22) is Element of the carrier of c
[[k2,gf],hg] `12 is Element of the carrier of c
(C,c,m,s,x,ii) is Element of (C,c,m,s,x)
[[c₂₀,c₂₀],[(id (c₂₀ `11)),(id (c<sub>20</sub> `12))]] `11 is Element of (C,c,m,s,x)
C9 . gg is set
(C,c,m,s,x,ii) is Element of (C,c,m,s,x)
[ii,gg] is V1() Element of [:(C,c,m,s,x),(C,c,m,s,x):]
[:(C,c,m,s,x),(C,c,m,s,x):] is non empty set
{ii,gg} is non empty set
{ii} is non empty set
{{ii,gg},{ii}} is non empty set
(C,c,m,s,x) . (i,g) is set
[i,g] is V1() set
{i,g} is non empty set
{i} is non empty set
{{i,g},{i}} is non empty set
(C,c,m,s,x) . [i,g] is set
(C,c,m,s,x,gg,ii) is Element of (C,c,m,s,x)
[(C,c,m,s,x,gg),(C,c,m,s,x,gg)] is V1() Element of [:(C,c,m,s,x),(C,c,m,s,x):]
{(C,c,m,s,x,gg),(C,c,m,s,x,gg)} is non empty set
{(C,c,m,s,x,gg)} is non empty set
{{(C,c,m,s,x,gg),(C,c,m,s,x,gg)},{(C,c,m,s,x,gg)}} is non empty set
(ii `21) (*) (gg `21) is Element of the carrier' of C
(ii `22) (*) (gg `22) is Element of the carrier' of c
[((ii `21) (*) (gg `21)),((ii `22) (*) (gg `22))] is V1() Element of [: the carrier' of C, the carrier' of c:]
{((ii `21) (*) (gg `21)),((ii `22) (*) (gg `22))} is non empty set
{((ii `21) (*) (gg `21))} is non empty set
{{((ii `21) (*) (gg `21)),((ii `22) (*) (gg `22))},{((ii `21) (*) (gg `21))}} is non empty set
[[(C,c,m,s,x,gg),(C,c,m,s,x,gg)],[((ii `21) (*) (gg `21)),((ii `22) (*) (gg `22))]] is V1() Element of [:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:]
{[(C,c,m,s,x,gg),(C,c,m,s,x,gg)],[((ii `21) (*) (gg `21)),((ii `22) (*) (gg `22))]} is non empty set
{[(C,c,m,s,x,gg),(C,c,m,s,x,gg)]} is non empty set
{{[(C,c,m,s,x,gg),(C,c,m,s,x,gg)],[((ii `21) (*) (gg `21)),((ii `22) (*) (gg `22))]},{[(C,c,m,s,x,gg),(C,c,m,s,x,gg)]}} is non empty set
[(gg `21),((ii `22) (*) (gg `22))] is V1() Element of [: the carrier' of C, the carrier' of c:]
{(gg `21),((ii `22) (*) (gg `22))} is non empty set
{(gg `21)} is non empty set
{{(gg `21),((ii `22) (*) (gg `22))},{(gg `21)}} is non empty set
[[(C,c,m,s,x,gg),(C,c,m,s,x,gg)],[(gg `21),((ii `22) (*) (gg `22))]] is V1() Element of [:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:]
{[(C,c,m,s,x,gg),(C,c,m,s,x,gg)],[(gg `21),((ii `22) (*) (gg `22))]} is non empty set
{{[(C,c,m,s,x,gg),(C,c,m,s,x,gg)],[(gg `21),((ii `22) (*) (gg `22))]},{[(C,c,m,s,x,gg),(C,c,m,s,x,gg)]}} is non empty set
[(gg `21),(gg `22)] is V1() Element of [: the carrier' of C, the carrier' of c:]
{(gg `21),(gg `22)} is non empty set
{{(gg `21),(gg `22)},{(gg `21)}} is non empty set
[[(C,c,m,s,x,gg),(C,c,m,s,x,gg)],[(gg `21),(gg `22)]] is V1() Element of [:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:]
{[(C,c,m,s,x,gg),(C,c,m,s,x,gg)],[(gg `21),(gg `22)]} is non empty set
{{[(C,c,m,s,x,gg),(C,c,m,s,x,gg)],[(gg `21),(gg `22)]},{[(C,c,m,s,x,gg),(C,c,m,s,x,gg)]}} is non empty set
c₂₀ is Element of the carrier' of CatStr(# E1,E2,D9,C9,a9 #)
dom c₂₀ is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
the Source of CatStr(# E1,E2,D9,C9,a9 #) is Relation-like the carrier' of CatStr(# E1,E2,D9,C9,a9 #) -defined the carrier of CatStr(# E1,E2,D9,C9,a9 #) -valued Function-like V18( the carrier' of CatStr(# E1,E2,D9,C9,a9 #), the carrier of CatStr(# E1,E2,D9,C9,a9 #)) Element of bool [: the carrier' of CatStr(# E1,E2,D9,C9,a9 #), the carrier of CatStr(# E1,E2,D9,C9,a9 #):]
[: the carrier' of CatStr(# E1,E2,D9,C9,a9 #), the carrier of CatStr(# E1,E2,D9,C9,a9 #):] is non empty set
bool [: the carrier' of CatStr(# E1,E2,D9,C9,a9 #), the carrier of CatStr(# E1,E2,D9,C9,a9 #):] is non empty set
the Source of CatStr(# E1,E2,D9,C9,a9 #) . c₂₀ is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
FG is Element of the carrier' of CatStr(# E1,E2,D9,C9,a9 #)
cod FG is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
the Target of CatStr(# E1,E2,D9,C9,a9 #) is Relation-like the carrier' of CatStr(# E1,E2,D9,C9,a9 #) -defined the carrier of CatStr(# E1,E2,D9,C9,a9 #) -valued Function-like V18( the carrier' of CatStr(# E1,E2,D9,C9,a9 #), the carrier of CatStr(# E1,E2,D9,C9,a9 #)) Element of bool [: the carrier' of CatStr(# E1,E2,D9,C9,a9 #), the carrier of CatStr(# E1,E2,D9,C9,a9 #):]
the Target of CatStr(# E1,E2,D9,C9,a9 #) . FG is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
c₂₀ (*) FG is Element of the carrier' of CatStr(# E1,E2,D9,C9,a9 #)
dom (c₂₀ (*) FG) is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
the Source of CatStr(# E1,E2,D9,C9,a9 #) . (c₂₀ (*) FG) is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
dom FG is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
the Source of CatStr(# E1,E2,D9,C9,a9 #) . FG is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
cod (c₂₀ (*) FG) is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
the Target of CatStr(# E1,E2,D9,C9,a9 #) . (c₂₀ (*) FG) is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
cod c₂₀ is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
the Target of CatStr(# E1,E2,D9,C9,a9 #) . c₂₀ is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
g1 is Element of (C,c,m,s,x)
(C,c,m,s,x,g1) is Element of (C,c,m,s,x)
f1 is Element of (C,c,m,s,x)
(C,c,m,s,x,f1) is Element of (C,c,m,s,x)
[g1,f1] is V1() Element of [:(C,c,m,s,x),(C,c,m,s,x):]
[:(C,c,m,s,x),(C,c,m,s,x):] is non empty set
{g1,f1} is non empty set
{g1} is non empty set
{{g1,f1},{g1}} is non empty set
dom a9 is Relation-like set
a9 . (c₂₀,FG) is set
[c₂₀,FG] is V1() set
{c₂₀,FG} is non empty set
{c₂₀} is non empty set
{{c₂₀,FG},{c₂₀}} is non empty set
a9 . [c₂₀,FG] is set
a9 . (g1,f1) is set
[g1,f1] is V1() set
a9 . [g1,f1] is set
(C,c,m,s,x,f1,g1) is Element of (C,c,m,s,x)
FG `11 is set
c<sub>20</sub> `12 is set
(c₂₀ (*) FG) `11 is set
(c<sub>20</sub> (*) FG) `12 is set
(C,c,m,s,x,f1) is Element of (C,c,m,s,x)
(C,c,m,s,x,g1) is Element of (C,c,m,s,x)
[(C,c,m,s,x,f1),(C,c,m,s,x,g1)] is V1() Element of [:(C,c,m,s,x),(C,c,m,s,x):]
{(C,c,m,s,x,f1),(C,c,m,s,x,g1)} is non empty set
{(C,c,m,s,x,f1)} is non empty set
{{(C,c,m,s,x,f1),(C,c,m,s,x,g1)},{(C,c,m,s,x,f1)}} is non empty set
f1 `21 is Element of the carrier' of C
g1 `21 is Element of the carrier' of C
(g1 `21) (*) (f1 `21) is Element of the carrier' of C
f1 `22 is Element of the carrier' of c
g1 `22 is Element of the carrier' of c
(g1 `22) (*) (f1 `22) is Element of the carrier' of c
[((g1 `21) (*) (f1 `21)),((g1 `22) (*) (f1 `22))] is V1() Element of [: the carrier' of C, the carrier' of c:]
{((g1 `21) (*) (f1 `21)),((g1 `22) (*) (f1 `22))} is non empty set
{((g1 `21) (*) (f1 `21))} is non empty set
{{((g1 `21) (*) (f1 `21)),((g1 `22) (*) (f1 `22))},{((g1 `21) (*) (f1 `21))}} is non empty set
[[(C,c,m,s,x,f1),(C,c,m,s,x,g1)],[((g1 `21) (*) (f1 `21)),((g1 `22) (*) (f1 `22))]] is V1() Element of [:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:]
[:[:(C,c,m,s,x),(C,c,m,s,x):],[: the carrier' of C, the carrier' of c:]:] is non empty set
{[(C,c,m,s,x,f1),(C,c,m,s,x,g1)],[((g1 `21) (*) (f1 `21)),((g1 `22) (*) (f1 `22))]} is non empty set
{[(C,c,m,s,x,f1),(C,c,m,s,x,g1)]} is non empty set
{{[(C,c,m,s,x,f1),(C,c,m,s,x,g1)],[((g1 `21) (*) (f1 `21)),((g1 `22) (*) (f1 `22))]},{[(C,c,m,s,x,f1),(C,c,m,s,x,g1)]}} is non empty set
f1 is Element of the carrier' of CatStr(# E1,E2,D9,C9,a9 #)
dom f1 is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
the Source of CatStr(# E1,E2,D9,C9,a9 #) is Relation-like the carrier' of CatStr(# E1,E2,D9,C9,a9 #) -defined the carrier of CatStr(# E1,E2,D9,C9,a9 #) -valued Function-like V18( the carrier' of CatStr(# E1,E2,D9,C9,a9 #), the carrier of CatStr(# E1,E2,D9,C9,a9 #)) Element of bool [: the carrier' of CatStr(# E1,E2,D9,C9,a9 #), the carrier of CatStr(# E1,E2,D9,C9,a9 #):]
[: the carrier' of CatStr(# E1,E2,D9,C9,a9 #), the carrier of CatStr(# E1,E2,D9,C9,a9 #):] is non empty set
bool [: the carrier' of CatStr(# E1,E2,D9,C9,a9 #), the carrier of CatStr(# E1,E2,D9,C9,a9 #):] is non empty set
the Source of CatStr(# E1,E2,D9,C9,a9 #) . f1 is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
c₂₀ is Element of the carrier' of CatStr(# E1,E2,D9,C9,a9 #)
cod c₂₀ is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
the Target of CatStr(# E1,E2,D9,C9,a9 #) is Relation-like the carrier' of CatStr(# E1,E2,D9,C9,a9 #) -defined the carrier of CatStr(# E1,E2,D9,C9,a9 #) -valued Function-like V18( the carrier' of CatStr(# E1,E2,D9,C9,a9 #), the carrier of CatStr(# E1,E2,D9,C9,a9 #)) Element of bool [: the carrier' of CatStr(# E1,E2,D9,C9,a9 #), the carrier of CatStr(# E1,E2,D9,C9,a9 #):]
the Target of CatStr(# E1,E2,D9,C9,a9 #) . c₂₀ is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
dom c₂₀ is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
the Source of CatStr(# E1,E2,D9,C9,a9 #) . c₂₀ is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
FG is Element of the carrier' of CatStr(# E1,E2,D9,C9,a9 #)
cod FG is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
the Target of CatStr(# E1,E2,D9,C9,a9 #) . FG is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
c₂₀ (*) FG is Element of the carrier' of CatStr(# E1,E2,D9,C9,a9 #)
f1 (*) (c₂₀ (*) FG) is Element of the carrier' of CatStr(# E1,E2,D9,C9,a9 #)
f1 (*) c₂₀ is Element of the carrier' of CatStr(# E1,E2,D9,C9,a9 #)
(f1 (*) c₂₀) (*) FG is Element of the carrier' of CatStr(# E1,E2,D9,C9,a9 #)
c₂₀ `11 is set
c<sub>20</sub> `12 is set
dom (f1 (*) c₂₀) is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
the Source of CatStr(# E1,E2,D9,C9,a9 #) . (f1 (*) c₂₀) is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
FG `11 is set
hg is Element of (C,c,m,s,x)
(C,c,m,s,x,hg) is Element of (C,c,m,s,x)
[(FG `11),(C,c,m,s,x,hg)] is V1() set
{(FG `11),(C,c,m,s,x,hg)} is non empty set
{(FG `11)} is non empty set
{{(FG `11),(C,c,m,s,x,hg)},{(FG `11)}} is non empty set
g1 is Element of (C,c,m,s,x)
g1 `21 is Element of the carrier' of C
hg `21 is Element of the carrier' of C
(hg `21) (*) (g1 `21) is Element of the carrier' of C
g1 `22 is Element of the carrier' of c
hg `22 is Element of the carrier' of c
(hg `22) (*) (g1 `22) is Element of the carrier' of c
[((hg `21) (*) (g1 `21)),((hg `22) (*) (g1 `22))] is V1() Element of [: the carrier' of C, the carrier' of c:]
{((hg `21) (*) (g1 `21)),((hg `22) (*) (g1 `22))} is non empty set
{((hg `21) (*) (g1 `21))} is non empty set
{{((hg `21) (*) (g1 `21)),((hg `22) (*) (g1 `22))},{((hg `21) (*) (g1 `21))}} is non empty set
[[(FG `11),(C,c,m,s,x,hg)],[((hg `21) (*) (g1 `21)),((hg `22) (*) (g1 `22))]] is V1() set
{[(FG `11),(C,c,m,s,x,hg)],[((hg `21) (*) (g1 `21)),((hg `22) (*) (g1 `22))]} is non empty set
{[(FG `11),(C,c,m,s,x,hg)]} is non empty set
{{[(FG `11),(C,c,m,s,x,hg)],[((hg `21) (*) (g1 `21)),((hg `22) (*) (g1 `22))]},{[(FG `11),(C,c,m,s,x,hg)]}} is non empty set
f1 `11 is set
FG `12 is set
cod (c<sub>20</sub> (*) FG) is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
the Target of CatStr(# E1,E2,D9,C9,a9 #) . (c<sub>20</sub> (*) FG) is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
gf is Element of (C,c,m,s,x)
(C,c,m,s,x,gf) is Element of (C,c,m,s,x)
f1 `12 is set
[(C,c,m,s,x,gf),(f1 `12)] is V1() set
{(C,c,m,s,x,gf),(f1 `12)} is non empty set
{(C,c,m,s,x,gf)} is non empty set
{{(C,c,m,s,x,gf),(f1 `12)},{(C,c,m,s,x,gf)}} is non empty set
gf `21 is Element of the carrier' of C
k2 is Element of (C,c,m,s,x)
k2 `21 is Element of the carrier' of C
(k2 `21) (*) (gf `21) is Element of the carrier' of C
gf `22 is Element of the carrier' of c
k2 `22 is Element of the carrier' of c
(k2 `22) (*) (gf `22) is Element of the carrier' of c
[((k2 `21) (*) (gf `21)),((k2 `22) (*) (gf `22))] is V1() Element of [: the carrier' of C, the carrier' of c:]
{((k2 `21) (*) (gf `21)),((k2 `22) (*) (gf `22))} is non empty set
{((k2 `21) (*) (gf `21))} is non empty set
{{((k2 `21) (*) (gf `21)),((k2 `22) (*) (gf `22))},{((k2 `21) (*) (gf `21))}} is non empty set
[[(C,c,m,s,x,gf),(f1 `12)],[((k2 `21) (*) (gf `21)),((k2 `22) (*) (gf `22))]] is V1() set
{[(C,c,m,s,x,gf),(f1 `12)],[((k2 `21) (*) (gf `21)),((k2 `22) (*) (gf `22))]} is non empty set
{[(C,c,m,s,x,gf),(f1 `12)]} is non empty set
{{[(C,c,m,s,x,gf),(f1 `12)],[((k2 `21) (*) (gf `21)),((k2 `22) (*) (gf `22))]},{[(C,c,m,s,x,gf),(f1 `12)]}} is non empty set
dom (k2 `21) is Element of the carrier of C
the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like V18( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is non empty set
bool [: the carrier' of C, the carrier of C:] is non empty set
the Source of C . (k2 `21) is Element of the carrier of C
(C,c,m,s,x,k2) is Element of (C,c,m,s,x)
(C,c,m,s,x,k2) `11 is Element of the carrier of C
cod (g1 `21) is Element of the carrier of C
the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like V18( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
the Target of C . (g1 `21) is Element of the carrier of C
(C,c,m,s,x,g1) is Element of (C,c,m,s,x)
(C,c,m,s,x,g1) `11 is Element of the carrier of C
dom (k2 `22) is Element of the carrier of c
the Source of c is Relation-like the carrier' of c -defined the carrier of c -valued Function-like V18( the carrier' of c, the carrier of c) Element of bool [: the carrier' of c, the carrier of c:]
[: the carrier' of c, the carrier of c:] is non empty set
bool [: the carrier' of c, the carrier of c:] is non empty set
the Source of c . (k2 `22) is Element of the carrier of c
(C,c,m,s,x,k2) `12 is Element of the carrier of c
cod (g1 `22) is Element of the carrier of c
the Target of c is Relation-like the carrier' of c -defined the carrier of c -valued Function-like V18( the carrier' of c, the carrier of c) Element of bool [: the carrier' of c, the carrier of c:]
the Target of c . (g1 `22) is Element of the carrier of c
(C,c,m,s,x,g1) `12 is Element of the carrier of c
k1 is Element of (C,c,m,s,x)
k1 `22 is Element of the carrier' of c
dom (k1 `22) is Element of the carrier of c
the Source of c . (k1 `22) is Element of the carrier of c
(C,c,m,s,x,k1) is Element of (C,c,m,s,x)
(C,c,m,s,x,k1) `12 is Element of the carrier of c
cod (k1 `22) is Element of the carrier of c
the Target of c . (k1 `22) is Element of the carrier of c
(C,c,m,s,x,k1) is Element of (C,c,m,s,x)
(C,c,m,s,x,k1) `12 is Element of the carrier of c
[(c<sub>20</sub> `11),(f1 `12)] is V1() set
{(c<sub>20</sub> `11),(f1 `12)} is non empty set
{(c<sub>20</sub> `11)} is non empty set
{{(c₂₀ `11),(f1 `12)},{(c₂₀ `11)}} is non empty set
k1 `21 is Element of the carrier' of C
(k2 `21) (*) (k1 `21) is Element of the carrier' of C
(k2 `22) (*) (k1 `22) is Element of the carrier' of c
[((k2 `21) (*) (k1 `21)),((k2 `22) (*) (k1 `22))] is V1() Element of [: the carrier' of C, the carrier' of c:]
{((k2 `21) (*) (k1 `21)),((k2 `22) (*) (k1 `22))} is non empty set
{((k2 `21) (*) (k1 `21))} is non empty set
{{((k2 `21) (*) (k1 `21)),((k2 `22) (*) (k1 `22))},{((k2 `21) (*) (k1 `21))}} is non empty set
[[(c₂₀ `11),(f1 `12)],[((k2 `21) (*) (k1 `21)),((k2 `22) (*) (k1 `22))]] is V1() set
{[(c₂₀ `11),(f1 `12)],[((k2 `21) (*) (k1 `21)),((k2 `22) (*) (k1 `22))]} is non empty set
{[(c₂₀ `11),(f1 `12)]} is non empty set
{{[(c₂₀ `11),(f1 `12)],[((k2 `21) (*) (k1 `21)),((k2 `22) (*) (k1 `22))]},{[(c₂₀ `11),(f1 `12)]}} is non empty set
(f1 (*) c₂₀) `12 is set
[(FG `11),(c₂₀ `12)] is V1() set
{(FG `11),(c₂₀ `12)} is non empty set
{{(FG `11),(c₂₀ `12)},{(FG `11)}} is non empty set
(k1 `21) (*) (g1 `21) is Element of the carrier' of C
(k1 `22) (*) (g1 `22) is Element of the carrier' of c
[((k1 `21) (*) (g1 `21)),((k1 `22) (*) (g1 `22))] is V1() Element of [: the carrier' of C, the carrier' of c:]
{((k1 `21) (*) (g1 `21)),((k1 `22) (*) (g1 `22))} is non empty set
{((k1 `21) (*) (g1 `21))} is non empty set
{{((k1 `21) (*) (g1 `21)),((k1 `22) (*) (g1 `22))},{((k1 `21) (*) (g1 `21))}} is non empty set
[[(FG `11),(c<sub>20</sub> `12)],[((k1 `21) (*) (g1 `21)),((k1 `22) (*) (g1 `22))]] is V1() set
{[(FG `11),(c<sub>20</sub> `12)],[((k1 `21) (*) (g1 `21)),((k1 `22) (*) (g1 `22))]} is non empty set
{[(FG `11),(c<sub>20</sub> `12)]} is non empty set
{{[(FG `11),(c<sub>20</sub> `12)],[((k1 `21) (*) (g1 `21)),((k1 `22) (*) (g1 `22))]},{[(FG `11),(c<sub>20</sub> `12)]}} is non empty set
(c₂₀ (*) FG) `11 is set
dom (k1 `21) is Element of the carrier of C
the Source of C . (k1 `21) is Element of the carrier of C
(C,c,m,s,x,k1) `11 is Element of the carrier of C
cod (k1 `21) is Element of the carrier of C
the Target of C . (k1 `21) is Element of the carrier of C
(C,c,m,s,x,k1) `11 is Element of the carrier of C
((k2 `21) (*) (k1 `21)) (*) (g1 `21) is Element of the carrier' of C
(k2 `21) (*) ((k1 `21) (*) (g1 `21)) is Element of the carrier' of C
c<sub>20</sub> is Element of the carrier' of CatStr(# E1,E2,D9,C9,a9 #)
FG is Element of the carrier' of CatStr(# E1,E2,D9,C9,a9 #)
[c<sub>20</sub>,FG] is V1() Element of [: the carrier' of CatStr(# E1,E2,D9,C9,a9 #), the carrier' of CatStr(# E1,E2,D9,C9,a9 #):]
{c<sub>20</sub>,FG} is non empty set
{c<sub>20</sub>} is non empty set
{{c<sub>20</sub>,FG},{c<sub>20</sub>}} is non empty set
dom c<sub>20</sub> is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
the Source of CatStr(# E1,E2,D9,C9,a9 #) is Relation-like the carrier' of CatStr(# E1,E2,D9,C9,a9 #) -defined the carrier of CatStr(# E1,E2,D9,C9,a9 #) -valued Function-like V18( the carrier' of CatStr(# E1,E2,D9,C9,a9 #), the carrier of CatStr(# E1,E2,D9,C9,a9 #)) Element of bool [: the carrier' of CatStr(# E1,E2,D9,C9,a9 #), the carrier of CatStr(# E1,E2,D9,C9,a9 #):]
[: the carrier' of CatStr(# E1,E2,D9,C9,a9 #), the carrier of CatStr(# E1,E2,D9,C9,a9 #):] is non empty set
bool [: the carrier' of CatStr(# E1,E2,D9,C9,a9 #), the carrier of CatStr(# E1,E2,D9,C9,a9 #):] is non empty set
the Source of CatStr(# E1,E2,D9,C9,a9 #) . c<sub>20</sub> is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
cod FG is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
the Target of CatStr(# E1,E2,D9,C9,a9 #) is Relation-like the carrier' of CatStr(# E1,E2,D9,C9,a9 #) -defined the carrier of CatStr(# E1,E2,D9,C9,a9 #) -valued Function-like V18( the carrier' of CatStr(# E1,E2,D9,C9,a9 #), the carrier of CatStr(# E1,E2,D9,C9,a9 #)) Element of bool [: the carrier' of CatStr(# E1,E2,D9,C9,a9 #), the carrier of CatStr(# E1,E2,D9,C9,a9 #):]
the Target of CatStr(# E1,E2,D9,C9,a9 #) . FG is Element of the carrier of CatStr(# E1,E2,D9,C9,a9 #)
g1 is Element of (C,c,m,s,x)
(C,c,m,s,x,g1) is Element of (C,c,m,s,x)
f1 is Element of (C,c,m,s,x)
(C,c,m,s,x,f1) is Element of (C,c,m,s,x)
k1 is Element of (C,c,m,s,x)
k2 is Element of (C,c,m,s,x)
[k1,k2] is V1() Element of [:(C,c,m,s,x),(C,c,m,s,x):]
[:(C,c,m,s,x),(C,c,m,s,x):] is non empty set
{k1,k2} is non empty set
{k1} is non empty set
{{k1,k2},{k1}} is non empty set
(C,c,m,s,x,k1) is Element of (C,c,m,s,x)
(C,c,m,s,x,k2) is Element of (C,c,m,s,x)
FG is non empty non void V55() strict Category-like transitive associative reflexive with_identities CatStr
the carrier of FG is non empty set
the carrier' of FG is non empty set
the Source of FG is Relation-like the carrier' of FG -defined the carrier of FG -valued Function-like V18( the carrier' of FG, the carrier of FG) Element of bool [: the carrier' of FG, the carrier of FG:]
[: the carrier' of FG, the carrier of FG:] is non empty set
bool [: the carrier' of FG, the carrier of FG:] is non empty set
the Target of FG is Relation-like the carrier' of FG -defined the carrier of FG -valued Function-like V18( the carrier' of FG, the carrier of FG) Element of bool [: the carrier' of FG, the carrier of FG:]
the Comp of FG is Relation-like [: the carrier' of FG, the carrier' of FG:] -defined the carrier' of FG -valued Function-like Element of bool [:[: the carrier' of FG, the carrier' of FG:], the carrier' of FG:]
[: the carrier' of FG, the carrier' of FG:] is non empty set
[:[: the carrier' of FG, the carrier' of FG:], the carrier' of FG:] is non empty set
bool [:[: the carrier' of FG, the carrier' of FG:], the carrier' of FG:] is non empty set
c<sub>20</sub> is Element of (C,c,m,s,x)
the Source of FG . c<sub>20</sub> is set
(C,c,m,s,x,c<sub>20</sub>) is Element of (C,c,m,s,x)
f1 is Element of (C,c,m,s,x)
the Target of FG . f1 is set
(C,c,m,s,x,f1) is Element of (C,c,m,s,x)
E1 is non empty non void V55() strict Category-like transitive associative reflexive with_identities CatStr
the carrier of E1 is non empty set
the carrier' of E1 is non empty set
the Source of E1 is Relation-like the carrier' of E1 -defined the carrier of E1 -valued Function-like V18( the carrier' of E1, the carrier of E1) Element of bool [: the carrier' of E1, the carrier of E1:]
[: the carrier' of E1, the carrier of E1:] is non empty set
bool [: the carrier' of E1, the carrier of E1:] is non empty set
the Target of E1 is Relation-like the carrier' of E1 -defined the carrier of E1 -valued Function-like V18( the carrier' of E1, the carrier of E1) Element of bool [: the carrier' of E1, the carrier of E1:]
the Comp of E1 is Relation-like [: the carrier' of E1, the carrier' of E1:] -defined the carrier' of E1 -valued Function-like Element of bool [:[: the carrier' of E1, the carrier' of E1:], the carrier' of E1:]
[: the carrier' of E1, the carrier' of E1:] is non empty set
[:[: the carrier' of E1, the carrier' of E1:], the carrier' of E1:] is non empty set
bool [:[: the carrier' of E1, the carrier' of E1:], the carrier' of E1:] is non empty set
E2 is non empty non void V55() strict Category-like transitive associative reflexive with_identities CatStr
the carrier of E2 is non empty set
the carrier' of E2 is non empty set
the Source of E2 is Relation-like the carrier' of E2 -defined the carrier of E2 -valued Function-like V18( the carrier' of E2, the carrier of E2) Element of bool [: the carrier' of E2, the carrier of E2:]
[: the carrier' of E2, the carrier of E2:] is non empty set
bool [: the carrier' of E2, the carrier of E2:] is non empty set
the Target of E2 is Relation-like the carrier' of E2 -defined the carrier of E2 -valued Function-like V18( the carrier' of E2, the carrier of E2) Element of bool [: the carrier' of E2, the carrier of E2:]
the Comp of E2 is Relation-like [: the carrier' of E2, the carrier' of E2:] -defined the carrier' of E2 -valued Function-like Element of bool [:[: the carrier' of E2, the carrier' of E2:], the carrier' of E2:]
[: the carrier' of E2, the carrier' of E2:] is non empty set
[:[: the carrier' of E2, the carrier' of E2:], the carrier' of E2:] is non empty set
bool [:[: the carrier' of E2, the carrier' of E2:], the carrier' of E2:] is non empty set
x is Element of H<sub>2</sub>(E1)
the Target of E1 . x is set
x `12 is set
the Target of E2 . x is set
x is Element of H₂(E1)
the Source of E1 . x is set
x `11 is set
the Source of E2 . x is set
c is set
C is set
1Cat (c,C) is non empty trivial V49() non void V54(1) V55() trivial' strict Category-like transitive associative reflexive with_identities CatStr
{c} is non empty set
{C} is non empty set
C :-> c is Relation-like {C} -defined {c} -valued Function-like V18({C},{c}) Element of bool [:{C},{c}:]
[:{C},{c}:] is non empty set
bool [:{C},{c}:] is non empty set
{C} --> c is Relation-like {C} -defined {c} -valued Function-like V18({C},{c}) Element of bool [:{C},{c}:]
(C,C) :-> C is Relation-like [:{C},{C}:] -defined {C} -valued Function-like V18([:{C},{C}:],{C}) Element of bool [:[:{C},{C}:],{C}:]
[:{C},{C}:] is non empty set
[:[:{C},{C}:],{C}:] is non empty set
bool [:[:{C},{C}:],{C}:] is non empty set
[C,C] is V1() set
{C,C} is non empty set
{{C,C},{C}} is non empty set
{[C,C]} is non empty set
{[C,C]} --> C is Relation-like {[C,C]} -defined {C} -valued Function-like V18({[C,C]},{C}) Element of bool [:{[C,C]},{C}:]
[:{[C,C]},{C}:] is non empty set
bool [:{[C,C]},{C}:] is non empty set
CatStr(# {c},{C},(C :-> c),(C :-> c),((C,C) :-> C) #) is non empty non void V55() strict CatStr
the carrier of (1Cat (c,C)) is non empty trivial V31() set
s is set
m is set
1Cat (s,m) is non empty trivial V49() non void V54(1) V55() trivial' strict Category-like transitive associative reflexive with_identities CatStr
{s} is non empty set
{m} is non empty set
m :-> s is Relation-like {m} -defined {s} -valued Function-like V18({m},{s}) Element of bool [:{m},{s}:]
[:{m},{s}:] is non empty set
bool [:{m},{s}:] is non empty set
{m} --> s is Relation-like {m} -defined {s} -valued Function-like V18({m},{s}) Element of bool [:{m},{s}:]
(m,m) :-> m is Relation-like [:{m},{m}:] -defined {m} -valued Function-like V18([:{m},{m}:],{m}) Element of bool [:[:{m},{m}:],{m}:]
[:{m},{m}:] is non empty set
[:[:{m},{m}:],{m}:] is non empty set
bool [:[:{m},{m}:],{m}:] is non empty set
[m,m] is V1() set
{m,m} is non empty set
{{m,m},{m}} is non empty set
{[m,m]} is non empty set
{[m,m]} --> m is Relation-like {[m,m]} -defined {m} -valued Function-like V18({[m,m]},{m}) Element of bool [:{[m,m]},{m}:]
[:{[m,m]},{m}:] is non empty set
bool [:{[m,m]},{m}:] is non empty set
CatStr(# {s},{m},(m :-> s),(m :-> s),((m,m) :-> m) #) is non empty non void V55() strict CatStr
the carrier' of (1Cat (s,m)) is non empty trivial set
C is set
{C} is non empty set
c is set
1Cat (c,C) is non empty trivial V49() non void V54(1) V55() trivial' strict Category-like transitive associative reflexive with_identities CatStr
{c} is non empty set
C :-> c is Relation-like {C} -defined {c} -valued Function-like V18({C},{c}) Element of bool [:{C},{c}:]
[:{C},{c}:] is non empty set
bool [:{C},{c}:] is non empty set
{C} --> c is Relation-like {C} -defined {c} -valued Function-like V18({C},{c}) Element of bool [:{C},{c}:]
(C,C) :-> C is Relation-like [:{C},{C}:] -defined {C} -valued Function-like V18([:{C},{C}:],{C}) Element of bool [:[:{C},{C}:],{C}:]
[:{C},{C}:] is non empty set
[:[:{C},{C}:],{C}:] is non empty set
bool [:[:{C},{C}:],{C}:] is non empty set
[C,C] is V1() set
{C,C} is non empty set
{{C,C},{C}} is non empty set
{[C,C]} is non empty set
{[C,C]} --> C is Relation-like {[C,C]} -defined {C} -valued Function-like V18({[C,C]},{C}) Element of bool [:{[C,C]},{C}:]
[:{[C,C]},{C}:] is non empty set
bool [:{[C,C]},{C}:] is non empty set
CatStr(# {c},{C},(C :-> c),(C :-> c),((C,C) :-> C) #) is non empty non void V55() strict CatStr
the carrier of (1Cat (c,C)) is non empty trivial V31() set
m is Element of the carrier of (1Cat (c,C))
s is Element of the carrier of (1Cat (c,C))
Hom (m,s) is trivial Element of bool the carrier' of (1Cat (c,C))
the carrier' of (1Cat (c,C)) is non empty trivial set
bool the carrier' of (1Cat (c,C)) is non empty set
{ b₁ where b₁ is Element of the carrier' of (1Cat (c,C)) : ( dom b₁ = m & cod b₁ = s ) } 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
c is Element of the carrier of C
id c is Morphism of c,c
1Cat (c,(id c)) is non empty trivial V49() non void V54(1) V55() trivial' strict Category-like transitive associative reflexive with_identities CatStr
{c} is non empty set
{(id c)} is non empty set
(id c) :-> c is Relation-like {(id c)} -defined {c} -valued Function-like V18({(id c)},{c}) Element of bool [:{(id c)},{c}:]
[:{(id c)},{c}:] is non empty set
bool [:{(id c)},{c}:] is non empty set
{(id c)} --> c is Relation-like {(id c)} -defined {c} -valued Function-like V18({(id c)},{c}) Element of bool [:{(id c)},{c}:]
((id c),(id c)) :-> (id c) is Relation-like [:{(id c)},{(id c)}:] -defined {(id c)} -valued Function-like V18([:{(id c)},{(id c)}:],{(id c)}) Element of bool [:[:{(id c)},{(id c)}:],{(id c)}:]
[:{(id c)},{(id c)}:] is non empty set
[:[:{(id c)},{(id c)}:],{(id c)}:] is non empty set
bool [:[:{(id c)},{(id c)}:],{(id c)}:] is non empty set
[(id c),(id c)] is V1() set
{(id c),(id c)} is non empty set
{{(id c),(id c)},{(id c)}} is non empty set
{[(id c),(id c)]} is non empty set
{[(id c),(id c)]} --> (id c) is Relation-like {[(id c),(id c)]} -defined {(id c)} -valued Function-like V18({[(id c),(id c)]},{(id c)}) Element of bool [:{[(id c),(id c)]},{(id c)}:]
[:{[(id c),(id c)]},{(id c)}:] is non empty set
bool [:{[(id c),(id c)]},{(id c)}:] is non empty set
CatStr(# {c},{(id c)},((id c) :-> c),((id c) :-> c),(((id c),(id c)) :-> (id c)) #) is non empty non void V55() strict CatStr
the carrier of (1Cat (c,(id c))) is non empty trivial V31() set
m is Element of the carrier of (1Cat (c,(id c)))
id m is Morphism of m,m
s is Element of the carrier of C
id s is Morphism of s,s
m is Element of the carrier of (1Cat (c,(id c)))
s is Element of the carrier of (1Cat (c,(id c)))
Hom (c,c) is non empty 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₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = c ) } is set
Hom (m,m) is non empty trivial Element of bool the carrier' of (1Cat (c,(id c)))
the carrier' of (1Cat (c,(id c))) is non empty trivial set
bool the carrier' of (1Cat (c,(id c))) is non empty set
{ b₁ where b₁ is Element of the carrier' of (1Cat (c,(id c))) : ( dom b₁ = m & cod b₁ = m ) } is set
{(id c)} is non empty Element of bool the carrier' of C
Hom (m,s) is trivial Element of bool the carrier' of (1Cat (c,(id c)))
{ b₁ where b₁ is Element of the carrier' of (1Cat (c,(id c))) : ( dom b₁ = m & cod b₁ = s ) } is set
x is Element of the carrier of C
c1 is Element of the carrier of C
Hom (x,c1) is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = x & cod b₁ = c1 ) } is set
((id c),(id c)) .--> (id c) is Relation-like Function-like set
dom (((id c),(id c)) .--> (id c)) is set
[: the carrier' of C, the carrier' of C:] is non empty set
[(id c),(id c)] is V1() Element of [: the carrier' of C, the carrier' of C:]
{[(id c),(id c)]} is non empty Relation-like the carrier' of C -defined the carrier' of C -valued Element of bool [: the carrier' of C, the carrier' of C:]
bool [: the carrier' of C, the carrier' of C:] is non empty set
dom (id 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 V18( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is non empty set
bool [: the carrier' of C, the carrier of C:] is non empty set
the Source of C . (id c) is Element of the carrier of C
cod (id 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 V18( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
the Target of C . (id c) is Element of the carrier of C
(((id c),(id c)) .--> (id c)) . ((id c),(id c)) is set
(((id c),(id c)) .--> (id c)) . [(id c),(id c)] is set
x is set
the Comp of (1Cat (c,(id c))) is Relation-like [: the carrier' of (1Cat (c,(id c))), the carrier' of (1Cat (c,(id c))):] -defined the carrier' of (1Cat (c,(id c))) -valued Function-like Element of bool [:[: the carrier' of (1Cat (c,(id c))), the carrier' of (1Cat (c,(id c))):], the carrier' of (1Cat (c,(id c))):]
[: the carrier' of (1Cat (c,(id c))), the carrier' of (1Cat (c,(id c))):] is non empty set
[:[: the carrier' of (1Cat (c,(id c))), the carrier' of (1Cat (c,(id c))):], the carrier' of (1Cat (c,(id c))):] is non empty set
bool [:[: the carrier' of (1Cat (c,(id c))), the carrier' of (1Cat (c,(id c))):], the carrier' of (1Cat (c,(id c))):] is non empty set
dom the Comp of (1Cat (c,(id c))) is Relation-like set
the Comp of (1Cat (c,(id c))) . x is set
(id c) (*) (id c) 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:], the carrier' of C:] is non empty set
bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is non empty set
the Comp of C . ((id c),(id c)) is set
the Comp of C . [(id c),(id c)] is set
the Comp of C . x is set
dom the Comp of C is Relation-like set
{c} is non empty Element of bool the carrier of C
bool 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
c is Element of the carrier of C
(C,c) is non empty non void V55() strict Category-like transitive associative reflexive with_identities Subcategory of C
id c is Morphism of c,c
1Cat (c,(id c)) is non empty trivial V49() non void V54(1) V55() trivial' strict Category-like transitive associative reflexive with_identities CatStr
{c} is non empty set
{(id c)} is non empty set
(id c) :-> c is Relation-like {(id c)} -defined {c} -valued Function-like V18({(id c)},{c}) Element of bool [:{(id c)},{c}:]
[:{(id c)},{c}:] is non empty set
bool [:{(id c)},{c}:] is non empty set
{(id c)} --> c is Relation-like {(id c)} -defined {c} -valued Function-like V18({(id c)},{c}) Element of bool [:{(id c)},{c}:]
((id c),(id c)) :-> (id c) is Relation-like [:{(id c)},{(id c)}:] -defined {(id c)} -valued Function-like V18([:{(id c)},{(id c)}:],{(id c)}) Element of bool [:[:{(id c)},{(id c)}:],{(id c)}:]
[:{(id c)},{(id c)}:] is non empty set
[:[:{(id c)},{(id c)}:],{(id c)}:] is non empty set
bool [:[:{(id c)},{(id c)}:],{(id c)}:] is non empty set
[(id c),(id c)] is V1() set
{(id c),(id c)} is non empty set
{{(id c),(id c)},{(id c)}} is non empty set
{[(id c),(id c)]} is non empty set
{[(id c),(id c)]} --> (id c) is Relation-like {[(id c),(id c)]} -defined {(id c)} -valued Function-like V18({[(id c),(id c)]},{(id c)}) Element of bool [:{[(id c),(id c)]},{(id c)}:]
[:{[(id c),(id c)]},{(id c)}:] is non empty set
bool [:{[(id c),(id c)]},{(id c)}:] is non empty set
CatStr(# {c},{(id c)},((id c) :-> c),((id c) :-> c),(((id c),(id c)) :-> (id c)) #) is non empty non void V55() strict CatStr
incl (C,c) is Relation-like the carrier' of (C,c) -defined the carrier' of C -valued Function-like V18( the carrier' of (C,c), the carrier' of C) Functor of (C,c),C
the carrier' of (C,c) is non empty set
the carrier' of C is non empty set
id C is Relation-like the carrier' of C -defined the carrier' of C -valued Function-like V18( the carrier' of C, the carrier' of C) Functor of C,C
id the carrier' of C is non empty Relation-like the carrier' of C -defined the carrier' of C -valued total Element of bool [: the carrier' of C, the carrier' of C:]
[: the carrier' of C, the carrier' of C:] is non empty set
bool [: the carrier' of C, the carrier' of C:] is non empty set
((C,c),C,C,(incl (C,c)),(id C)) is non empty non void V55() strict Category-like transitive associative reflexive with_identities CatStr
(C,(C,c),C,(id C),(incl (C,c))) is non empty non void V55() strict Category-like transitive associative reflexive with_identities CatStr