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

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

{ [[b

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

[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

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

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

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

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

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

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

[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

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

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

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

(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

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

(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

FG is Element of the carrier' of CatStr(# E1,E2,D9,C9,a9 #)

c

dom c

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

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

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

[c

{c

{c

{{c

a9 . [c

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

c

[c

{c

{c

{{c

c

id (c

c

id (c

[(id (c

{(id (c

{(id (c

{{(id (c

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

{{[c

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

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