:: 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