:: OPPCAT_1 semantic presentation

K104() is Element of bool K100()

K100() is set

bool K100() is set

K99() is set

bool K99() is set

bool K104() is set

{} is empty set

the empty set is empty set

1 is non empty set

C is non empty set

a is non empty set

[:C,a:] is set

S is non empty set

[:[:C,a:],S:] is set

bool [:[:C,a:],S:] is set

f is Relation-like [:C,a:] -defined S -valued Function-like Element of bool [:[:C,a:],S:]

~ f is Relation-like Function-like set

[:a,C:] is set

[:[:a,C:],S:] is set

bool [:[:a,C:],S:] is set

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

the carrier of C is non empty set

the carrier' of C is non empty set

the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is set

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

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]

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

[: the carrier' of C, the carrier' of C:] is set

[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set

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

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

CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) #) is strict CatStr

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

the carrier of C is non empty set

a is Element of the carrier of C

(C) is non empty non void V55() strict CatStr

the carrier' of C is non empty set

the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is set

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

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]

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

[: the carrier' of C, the carrier' of C:] is set

[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set

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

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

CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) #) is strict CatStr

the carrier of (C) is non empty set

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

(C) is non empty non void V55() strict CatStr

the carrier of C is non empty set

the carrier' of C is non empty set

the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is set

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

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]

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

[: the carrier' of C, the carrier' of C:] is set

[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set

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

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

CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) #) is strict CatStr

the carrier' of (C) is non empty set

g is Element of the carrier' of (C)

Sgg is Element of the carrier' of (C)

[g,Sgg] is set

{g,Sgg} is non empty set

{g} is non empty set

{{g,Sgg},{g}} is non empty set

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

[: the carrier' of (C), the carrier' of (C):] is set

[:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set

bool [:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set

dom the Comp of (C) is Relation-like set

dom g is Element of the carrier of (C)

the carrier of (C) is non empty set

the Source of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]

[: the carrier' of (C), the carrier of (C):] is set

bool [: the carrier' of (C), the carrier of (C):] is set

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

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

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

d is Element of the carrier' of C

c

[d,c

{d,c

{d} is non empty set

{{d,c

dom the Comp of C is Relation-like set

dom d is Element of the carrier of C

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

cod c

the Target of C . c

c

cod c

the Target of C . c

d is Element of the carrier' of C

dom d is Element of the carrier of C

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

[d,c

{d,c

{d} is non empty set

{{d,c

dom the Comp of C is Relation-like set

g is Element of the carrier' of C

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

Sgg is Element of the carrier' of C

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

( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . (g,Sgg) is set

[g,Sgg] is set

{g,Sgg} is non empty set

{g} is non empty set

{{g,Sgg},{g}} is non empty set

( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . [g,Sgg] is set

the Comp of C . (Sgg,g) is set

[Sgg,g] is set

{Sgg,g} is non empty set

{Sgg} is non empty set

{{Sgg,g},{Sgg}} is non empty set

the Comp of C . [Sgg,g] is set

the carrier' of (C) is non empty set

c

dom c

the carrier of (C) is non empty set

the Source of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]

[: the carrier' of (C), the carrier of (C):] is set

bool [: the carrier' of (C), the carrier of (C):] is set

the Source of (C) . c

d is Element of the carrier' of (C)

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

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

[c

{c

{c

{{c

dom ( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) is Relation-like set

the carrier' of (C) is non empty set

g is Element of the carrier' of (C)

dom g is Element of the carrier of (C)

the carrier of (C) is non empty set

the Source of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]

[: the carrier' of (C), the carrier of (C):] is set

bool [: the carrier' of (C), the carrier of (C):] is set

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

Sgg is Element of the carrier' of (C)

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

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

g (*) Sgg is Element of the carrier' of (C)

dom (g (*) Sgg) is Element of the carrier of (C)

the Source of (C) . (g (*) Sgg) is Element of the carrier of (C)

dom Sgg is Element of the carrier of (C)

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

cod (g (*) Sgg) is Element of the carrier of (C)

the Target of (C) . (g (*) Sgg) is Element of the carrier of (C)

cod g is Element of the carrier of (C)

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

c

cod c

the Target of C . c

d is Element of the carrier' of C

dom d is Element of the carrier of C

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

[d,c

{d,c

{d} is non empty set

{{d,c

dom the Comp of C is Relation-like set

[g,Sgg] is set

{g,Sgg} is non empty set

{g} is non empty set

{{g,Sgg},{g}} is non empty set

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

[: the carrier' of (C), the carrier' of (C):] is set

[:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set

bool [:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set

dom the Comp of (C) is Relation-like set

( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . (c

[c

{c

{c

{{c

( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . [c

the Comp of C . (d,c

the Comp of C . [d,c

d (*) c

cod (d (*) c

the Target of C . (d (*) c

cod d is Element of the carrier of C

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

dom (d (*) c

the Source of C . (d (*) c

dom c

the Source of C . c

the carrier' of (C) is non empty set

d is Element of the carrier' of (C)

dom d is Element of the carrier of (C)

the carrier of (C) is non empty set

the Source of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]

[: the carrier' of (C), the carrier of (C):] is set

bool [: the carrier' of (C), the carrier of (C):] is set

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

g is Element of the carrier' of (C)

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

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

dom g is Element of the carrier of (C)

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

Sgg is Element of the carrier' of (C)

cod Sgg is Element of the carrier of (C)

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

g (*) Sgg is Element of the carrier' of (C)

d (*) (g (*) Sgg) is Element of the carrier' of (C)

d (*) g is Element of the carrier' of (C)

(d (*) g) (*) Sgg is Element of the carrier' of (C)

bb is Element of the carrier' of C

b is Element of the carrier' of C

[bb,b] is set

{bb,b} is non empty set

{bb} is non empty set

{{bb,b},{bb}} is non empty set

dom ( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) is Relation-like set

( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . (bb,b) is set

( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . [bb,b] is set

c

[b,c

{b,c

{b} is non empty set

{{b,c

( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . (b,c

( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . [b,c

the Comp of C . (b,bb) is set

[b,bb] is set

{b,bb} is non empty set

{{b,bb},{b}} is non empty set

the Comp of C . [b,bb] is set

the Target of C . (( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . (bb,b)) is set

dom (d (*) g) is Element of the carrier of (C)

the Source of (C) . (d (*) g) is Element of the carrier of (C)

( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . ((( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . (bb,b)),c

[(( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . (bb,b)),c

{(( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . (bb,b)),c

{(( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . (bb,b))} is non empty set

{{(( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . (bb,b)),c

( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . [(( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . (bb,b)),c

the Comp of C . (c

[c

{c

{c

{{c

the Comp of C . [c

cod bb is Element of the carrier of C

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

dom b is Element of the carrier of C

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

cod b is Element of the carrier of C

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

dom c

the Source of C . c

the Comp of C . (c

[c

{c

{{c

the Comp of C . [c

the Source of C . (( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . (b,c

cod (g (*) Sgg) is Element of the carrier of (C)

the Target of (C) . (g (*) Sgg) is Element of the carrier of (C)

[(d (*) g),Sgg] is set

{(d (*) g),Sgg} is non empty set

{(d (*) g)} is non empty set

{{(d (*) g),Sgg},{(d (*) g)}} is non empty set

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

[: the carrier' of (C), the carrier' of (C):] is set

[:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set

bool [:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set

dom the Comp of (C) is Relation-like set

[d,(g (*) Sgg)] is set

{d,(g (*) Sgg)} is non empty set

{d} is non empty set

{{d,(g (*) Sgg)},{d}} is non empty set

[d,g] is set

{d,g} is non empty set

{{d,g},{d}} is non empty set

c

dom (c

the Source of C . (c

b (*) bb is Element of the carrier' of C

cod (b (*) bb) is Element of the carrier of C

the Target of C . (b (*) bb) is Element of the carrier of C

[g,Sgg] is set

{g,Sgg} is non empty set

{g} is non empty set

{{g,Sgg},{g}} is non empty set

( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . (bb,(( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . (b,c

[bb,(( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . (b,c

{bb,(( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . (b,c

{{bb,(( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . (b,c

( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . [bb,(( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . (b,c

the Comp of C . (( the Comp of C . (c

[( the Comp of C . (c

{( the Comp of C . (c

{( the Comp of C . (c

{{( the Comp of C . (c

the Comp of C . [( the Comp of C . (c

(c

c

the carrier of (C) is non empty set

Sgg is Element of the carrier of (C)

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

the carrier' of (C) is non empty set

bool the carrier' of (C) is set

{ b

g is Element of the carrier of C

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

bool the carrier' of C is set

{ b

d is Element of the carrier' of C

c

dom c

the Source of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]

[: the carrier' of (C), the carrier of (C):] is set

bool [: the carrier' of (C), the carrier of (C):] is set

the Source of (C) . c

cod d is Element of the carrier of C

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

cod c

the Target of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]

the Target of (C) . c

dom d is Element of the carrier of C

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

the carrier of (C) is non empty set

Sgg is Element of the carrier of (C)

the carrier' of (C) is non empty set

g is Element of the carrier of C

id g is Morphism of g,g

d is Element of the carrier' of (C)

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

[: the carrier' of (C), the carrier of (C):] is set

bool [: the carrier' of (C), the carrier of (C):] is set

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

cod (id g) is Element of the carrier of C

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

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

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

dom (id g) is Element of the carrier of C

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

c

b is Element of the carrier of (C)

Hom (Sgg,b) is Element of bool the carrier' of (C)

bool the carrier' of (C) is set

{ b

Hom (b,Sgg) is Element of bool the carrier' of (C)

{ b

g is Morphism of Sgg,b

g (*) c

gg is Element of the carrier' of C

dom gg is Element of the carrier of C

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

cod g is Element of the carrier of (C)

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

bb is Element of the carrier of C

cod gg is Element of the carrier of C

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

dom g is Element of the carrier of (C)

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

the Source of C . c

the Target of C . g is set

cod c

the Target of (C) . c

[g,c

{g,c

{g} is non empty set

{{g,c

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

[: the carrier' of (C), the carrier' of (C):] is set

[:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set

bool [:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set

dom the Comp of (C) is Relation-like set

( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . (g,c

( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . [g,c

the Comp of C . (c

[c

{c

{c

{{c

the Comp of C . [c

gg is Morphism of bb,g

(id g) (*) gg is Element of the carrier' of C

g is Morphism of b,Sgg

c

gg is Element of the carrier' of C

cod gg is Element of the carrier of C

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

dom g is Element of the carrier of (C)

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

bb is Element of the carrier of C

dom gg is Element of the carrier of C

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

cod g is Element of the carrier of (C)

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

the Target of C . c

the Source of C . g is set

dom c

the Source of (C) . c

[c

{c

{c

{{c

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

[: the carrier' of (C), the carrier' of (C):] is set

[:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set

bool [:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set

dom the Comp of (C) is Relation-like set

( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . (c

( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . [c

the Comp of C . (g,c

[g,c

{g,c

{g} is non empty set

{{g,c

the Comp of C . [g,c

gg is Morphism of g,bb

gg (*) (id g) is Element of the carrier' of C

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

(C) is non empty non void V55() strict 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 Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is set

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

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]

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

[: the carrier' of C, the carrier' of C:] is set

[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set

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

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

CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) #) is strict CatStr

the carrier of (C) is non empty set

a is Element of the carrier of (C)

((C),a) is Element of the carrier of ((C))

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

the carrier' of (C) is non empty set

the Target of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]

[: the carrier' of (C), the carrier of (C):] is set

bool [: the carrier' of (C), the carrier of (C):] is set

the Source of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]

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

[: the carrier' of (C), the carrier' of (C):] is set

[:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set

bool [:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set

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

CatStr(# the carrier of (C), the carrier' of (C), the Target of (C), the Source of (C),( the carrier' of (C), the carrier' of (C), the carrier' of (C), the Comp of (C)) #) is strict CatStr

the carrier of ((C)) is non empty set

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

the carrier of C is non empty set

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

the carrier' of C is non empty set

the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is set

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

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]

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

[: the carrier' of C, the carrier' of C:] is set

[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set

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

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

CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) #) is strict CatStr

a is Element of the carrier of C

(C,a) is Element of the carrier of (C)

the carrier of (C) is non empty set

((C),(C,a)) is Element of the carrier of ((C))

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

the carrier' of (C) is non empty set

the Target of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]

[: the carrier' of (C), the carrier of (C):] is set

bool [: the carrier' of (C), the carrier of (C):] is set

the Source of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]

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

[: the carrier' of (C), the carrier' of (C):] is set

[:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set

bool [:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set

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

CatStr(# the carrier of (C), the carrier' of (C), the Target of (C), the Source of (C),( the carrier' of (C), the carrier' of (C), the carrier' of (C), the Comp of (C)) #) is strict CatStr

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

a is Element of the carrier of C

(C,a) is Element of the carrier of (C)

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

the carrier' of C is non empty set

the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is set

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

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]

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

[: the carrier' of C, the carrier' of C:] is set

[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set

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

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

CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) #) is strict CatStr

the carrier of (C) is non empty set

(C,(C,a)) is Element of the carrier of C

((C),(C,a)) is Element of the carrier of ((C))

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

the carrier' of (C) is non empty set

the Target of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]

[: the carrier' of (C), the carrier of (C):] is set

bool [: the carrier' of (C), the carrier of (C):] is set

the Source of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]

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

[: the carrier' of (C), the carrier' of (C):] is set

[:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set

bool [:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set

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

CatStr(# the carrier of (C), the carrier' of (C), the Target of (C), the Source of (C),( the carrier' of (C), the carrier' of (C), the carrier' of (C), the Comp of (C)) #) is strict CatStr

the carrier of ((C)) is non empty set

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

(C) is non empty non void V55() strict 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 Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is set

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

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]

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

[: the carrier' of C, the carrier' of C:] is set

[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set

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

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

CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) #) is strict CatStr

the carrier of (C) is non empty set

a is Element of the carrier of (C)

(C,a) is Element of the carrier of C

((C),a) is Element of the carrier of ((C))

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

the carrier' of (C) is non empty set

the Target of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]

[: the carrier' of (C), the carrier of (C):] is set

bool [: the carrier' of (C), the carrier of (C):] is set

the Source of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]

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

[: the carrier' of (C), the carrier' of (C):] is set

[:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set

bool [:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set

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

CatStr(# the carrier of (C), the carrier' of (C), the Target of (C), the Source of (C),( the carrier' of (C), the carrier' of (C), the carrier' of (C), the Comp of (C)) #) is strict CatStr

the carrier of ((C)) is non empty set

(C,(C,a)) is Element of the carrier of (C)

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

the carrier of C is non empty set

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

the carrier' of C is non empty set

the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is set

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

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]

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

[: the carrier' of C, the carrier' of C:] is set

[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set

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

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

CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) #) is strict CatStr

a is Element of the carrier of C

S is Element of the carrier of C

Hom (a,S) is Element of bool the carrier' of C

bool the carrier' of C is set

{ b

(C,S) is Element of the carrier of (C)

the carrier of (C) is non empty set

(C,a) is Element of the carrier of (C)

Hom ((C,S),(C,a)) is Element of bool the carrier' of (C)

the carrier' of (C) is non empty set

bool the carrier' of (C) is set

{ b

f is set

S2 is Element of the carrier' of C

dom S2 is Element of the carrier of C

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

cod S2 is Element of the carrier of C

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

Sff is Element of the carrier' of (C)

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

[: the carrier' of (C), the carrier of (C):] is set

bool [: the carrier' of (C), the carrier of (C):] is set

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

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

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

f is set

S2 is Element of the carrier' of (C)

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

[: the carrier' of (C), the carrier of (C):] is set

bool [: the carrier' of (C), the carrier of (C):] is set

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

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

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

Sff is Element of the carrier' of C

dom Sff is Element of the carrier of C

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

cod Sff is Element of the carrier of C

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

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

(C) is non empty non void V55() strict 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 Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is set

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

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]

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

[: the carrier' of C, the carrier' of C:] is set

[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set

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

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

CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) #) is strict CatStr

the carrier of (C) is non empty set

a is Element of the carrier of (C)

S is Element of the carrier of (C)

Hom (a,S) is Element of bool the carrier' of (C)

the carrier' of (C) is non empty set

bool the carrier' of (C) is set

{ b

(C,S) is Element of the carrier of C

((C),S) is Element of the carrier of ((C))

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

the Target of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]

[: the carrier' of (C), the carrier of (C):] is set

bool [: the carrier' of (C), the carrier of (C):] is set

the Source of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]

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

[: the carrier' of (C), the carrier' of (C):] is set

[:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set

bool [:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set

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

CatStr(# the carrier of (C), the carrier' of (C), the Target of (C), the Source of (C),( the carrier' of (C), the carrier' of (C), the carrier' of (C), the Comp of (C)) #) is strict CatStr

the carrier of ((C)) is non empty set

(C,a) is Element of the carrier of C

((C),a) is Element of the carrier of ((C))

Hom ((C,S),(C,a)) is Element of bool the carrier' of C

bool the carrier' of C is set

{ b

(C,(C,a)) is Element of the carrier of (C)

(C,(C,S)) is Element of the carrier of (C)

Hom ((C,(C,a)),(C,(C,S))) is Element of bool the carrier' of (C)

{ b

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

the carrier' of C is non empty set

a is Element of the carrier' of C

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

the carrier of C is non empty set

the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is set

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

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]

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

[: the carrier' of C, the carrier' of C:] is set

[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set

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

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

CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) #) is strict CatStr

the carrier' of (C) is non empty set

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

(C) is non empty non void V55() strict 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 Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is set

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

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]

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

[: the carrier' of C, the carrier' of C:] is set

[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set

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

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

CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) #) is strict CatStr

the carrier' of (C) is non empty set

a is Element of the carrier' of (C)

((C),a) is Element of the carrier' of ((C))

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

the carrier of (C) is non empty set

the Target of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]

[: the carrier' of (C), the carrier of (C):] is set

bool [: the carrier' of (C), the carrier of (C):] is set

the Source of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]

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

[: the carrier' of (C), the carrier' of (C):] is set

[:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set

bool [:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set

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

CatStr(# the carrier of (C), the carrier' of (C), the Target of (C), the Source of (C),( the carrier' of (C), the carrier' of (C), the carrier' of (C), the Comp of (C)) #) is strict CatStr

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

a is Element of the carrier of C

S is Element of the carrier of C

Hom (a,S) is Element of bool the carrier' of C

the carrier' of C is non empty set

bool the carrier' of C is set

{ b

f is Morphism of a,S

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

the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is set

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

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]

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

[: the carrier' of C, the carrier' of C:] is set

[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set

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

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

CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) #) is strict CatStr

(C,S) is Element of the carrier of (C)

the carrier of (C) is non empty set

(C,a) is Element of the carrier of (C)

Hom ((C,S),(C,a)) is Element of bool the carrier' of (C)

the carrier' of (C) is non empty set

bool the carrier' of (C) is set

{ b

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

the carrier of C is non empty set

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

the carrier' of C is non empty set

the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is set

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

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]

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

[: the carrier' of C, the carrier' of C:] is set

[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set

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

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

CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) #) is strict CatStr

a is Element of the carrier of C

(C,a) is Element of the carrier of (C)

the carrier of (C) is non empty set

S is Element of the carrier of C

(C,S) is Element of the carrier of (C)

Hom ((C,a),(C,S)) is Element of bool the carrier' of (C)

the carrier' of (C) is non empty set

bool the carrier' of (C) is set

{ b

f is Morphism of (C,a),(C,S)

Hom (S,a) is Element of bool the carrier' of C

bool the carrier' of C is set

{ b

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

the carrier of C is non empty set

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

the carrier' of C is non empty set

the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is set

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

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]

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

[: the carrier' of C, the carrier' of C:] is set

[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set

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

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

CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) #) is strict CatStr

a is Element of the carrier of C

S is Element of the carrier of C

Hom (a,S) is Element of bool the carrier' of C

bool the carrier' of C is set

{ b

(C,S) is Element of the carrier of (C)

the carrier of (C) is non empty set

(C,a) is Element of the carrier of (C)

Hom ((C,S),(C,a)) is Element of bool the carrier' of (C)

the carrier' of (C) is non empty set

bool the carrier' of (C) is set

{ b

f is Morphism of a,S

(C,a,S,f) is Morphism of (C,S),(C,a)

((C),(C,S),(C,a),(C,a,S,f)) is Morphism of ((C),(C,a)),((C),(C,S))

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

the Target of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]

[: the carrier' of (C), the carrier of (C):] is set

bool [: the carrier' of (C), the carrier of (C):] is set

the Source of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]

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

[: the carrier' of (C), the carrier' of (C):] is set

[:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set

bool [:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set

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

CatStr(# the carrier of (C), the carrier' of (C), the Target of (C), the Source of (C),( the carrier' of (C), the carrier' of (C), the carrier' of (C), the Comp of (C)) #) is strict CatStr

((C),(C,a)) is Element of the carrier of ((C))

the carrier of ((C)) is non empty set

((C),(C,S)) is Element of the carrier of ((C))

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

the carrier of C is non empty set

a is Element of the carrier of C

S is Element of the carrier of C

Hom (a,S) is Element of bool the carrier' of C

the carrier' of C is non empty set

bool the carrier' of C is set

{ b

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

the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is set

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

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]

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

[: the carrier' of C, the carrier' of C:] is set

[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set

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

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

CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) #) is strict CatStr

(C,S) is Element of the carrier of (C)

the carrier of (C) is non empty set

(C,a) is Element of the carrier of (C)

Hom ((C,S),(C,a)) is Element of bool the carrier' of (C)

the carrier' of (C) is non empty set

bool the carrier' of (C) is set

{ b

f is Morphism of a,S

(C,a,S,f) is Morphism of (C,S),(C,a)

(C,S,a,(C,a,S,f)) is Morphism of a,S

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

(C) is non empty non void V55() strict 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 Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is set

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

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]

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

[: the carrier' of C, the carrier' of C:] is set

[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set

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

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

CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) #) is strict CatStr

the carrier of (C) is non empty set

a is Element of the carrier of (C)

S is Element of the carrier of (C)

f is Morphism of a,S

(C,f) is Element of the carrier' of C

((C),f) is Element of the carrier' of ((C))

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

the carrier' of (C) is non empty set

the Target of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]

[: the carrier' of (C), the carrier of (C):] is set

bool [: the carrier' of (C), the carrier of (C):] is set

the Source of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]

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

[: the carrier' of (C), the carrier' of (C):] is set

[:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set

bool [:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set

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

CatStr(# the carrier of (C), the carrier' of (C), the Target of (C), the Source of (C),( the carrier' of (C), the carrier' of (C), the carrier' of (C), the Comp of (C)) #) is strict CatStr

the carrier' of ((C)) is non empty set

(C,(C,f)) is Element of the carrier' of (C)

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

the carrier of C is non empty set

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

the carrier' of C is non empty set

the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is set

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

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]

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

[: the carrier' of C, the carrier' of C:] is set

[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set

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

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

CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) #) is strict CatStr

a is Element of the carrier of C

S is Element of the carrier of C

Hom (a,S) is Element of bool the carrier' of C

bool the carrier' of C is set

{ b

(C,S) is Element of the carrier of (C)

the carrier of (C) is non empty set

(C,a) is Element of the carrier of (C)

Hom ((C,S),(C,a)) is Element of bool the carrier' of (C)

the carrier' of (C) is non empty set

bool the carrier' of (C) is set

{ b

f is Morphism of a,S

(C,a,S,f) is Morphism of (C,S),(C,a)

dom (C,a,S,f) 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 non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]

[: the carrier' of (C), the carrier of (C):] is set

bool [: the carrier' of (C), the carrier of (C):] is set

the Source of (C) . (C,a,S,f) is Element of the carrier of (C)

cod f is Element of the carrier of C

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

cod (C,a,S,f) 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 non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]

the Target of (C) . (C,a,S,f) is Element of the carrier of (C)

dom f is Element of the carrier of C

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

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

(C) is non empty non void V55() strict 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 Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is set

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

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]

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

[: the carrier' of C, the carrier' of C:] is set

[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set

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

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

CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) #) is strict CatStr

the carrier of (C) is non empty set

a is Element of the carrier of (C)

S is Element of the carrier of (C)

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

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

the carrier of S2 is non empty set

the carrier' of S2 is non empty set

the Target of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like non empty total quasi_total Element of bool [: the carrier' of S2, the carrier of S2:]

[: the carrier' of S2, the carrier of S2:] is set

bool [: the carrier' of S2, the carrier of S2:] is set

the Source of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like non empty total quasi_total Element of bool [: the carrier' of S2, the carrier of S2:]

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

[: the carrier' of S2, the carrier' of S2:] is set

[:[: the carrier' of S2, the carrier' of S2:], the carrier' of S2:] is set

bool [:[: the carrier' of S2, the carrier' of S2:], the carrier' of S2:] is set

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

CatStr(# the carrier of S2, the carrier' of S2, the Target of S2, the Source of S2,( the carrier' of S2, the carrier' of S2, the carrier' of S2, the Comp of S2) #) is strict CatStr

the carrier of (S2) is non empty set

Sff is Element of the carrier of (S2)

Sgg is Element of the carrier of (S2)

f is Morphism of a,S

(C,f) is Element of the carrier' of C

((C),f) is Element of the carrier' of ((C))

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

the carrier' of (C) is non empty set

the Target of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]

[: the carrier' of (C), the carrier of (C):] is set

bool [: the carrier' of (C), the carrier of (C):] is set

the Source of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]

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

[: the carrier' of (C), the carrier' of (C):] is set

[:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set

bool [:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set

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

CatStr(# the carrier of (C), the carrier' of (C), the Target of (C), the Source of (C),( the carrier' of (C), the carrier' of (C), the carrier' of (C), the Comp of (C)) #) is strict CatStr

the carrier' of ((C)) is non empty set

dom (C,f) is Element of the carrier of C

the Source of C . (C,f) is Element of the carrier of C

cod f is Element of the carrier of (C)

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

g is Morphism of Sff,Sgg

(S2,g) is Element of the carrier' of S2

((S2),g) is Element of the carrier' of ((S2))

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

the carrier' of (S2) is non empty set

the Target of (S2) is Relation-like the carrier' of (S2) -defined the carrier of (S2) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (S2), the carrier of (S2):]

[: the carrier' of (S2), the carrier of (S2):] is set

bool [: the carrier' of (S2), the carrier of (S2):] is set

the Source of (S2) is Relation-like the carrier' of (S2) -defined the carrier of (S2) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (S2), the carrier of (S2):]

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

[: the carrier' of (S2), the carrier' of (S2):] is set

[:[: the carrier' of (S2), the carrier' of (S2):], the carrier' of (S2):] is set

bool [:[: the carrier' of (S2), the carrier' of (S2):], the carrier' of (S2):] is set

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

CatStr(# the carrier of (S2), the carrier' of (S2), the Target of (S2), the Source of (S2),( the carrier' of (S2), the carrier' of (S2), the carrier' of (S2), the Comp of (S2)) #) is strict CatStr

the carrier' of ((S2)) is non empty set

cod (S2,g) is Element of the carrier of S2

the Target of S2 . (S2,g) is Element of the carrier of S2

dom g is Element of the carrier of (S2)

the Source of (S2) . g is Element of the carrier of (S2)

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

the carrier of C is non empty set

a is Element of the carrier of C

S is Element of the carrier of C

Hom (a,S) is Element of bool the carrier' of C

the carrier' of C is non empty set

bool the carrier' of C is set

{ b

f is Morphism of a,S

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

[: the carrier' of C, the carrier of C:] is set

bool [: the carrier' of