:: CAT_5 semantic presentation

K158() is Element of bool K154()

K154() is set

bool K154() is non empty set

{} is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional set

the empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional set is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional set

1 is non empty set

{{},1} is non empty set

K153() is set

bool K153() is non empty set

bool K158() is non empty set

C is non empty non void V58() 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 Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like V21( 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 Relation-like set

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

the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like V21( the carrier' of C, the carrier of C) 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 non empty Relation-like set

[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is non empty Relation-like set

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

CatStr(# the carrier of C, the carrier' of C, the Source of C, the Target of C, the Comp of C #) is non empty non void V58() strict CatStr

f is non empty non void V58() CatStr

the carrier of f is non empty set

the carrier' of f is non empty set

the Source of f is Relation-like the carrier' of f -defined the carrier of f -valued Function-like V21( the carrier' of f, the carrier of f) Element of bool [: the carrier' of f, the carrier of f:]

[: the carrier' of f, the carrier of f:] is non empty Relation-like set

bool [: the carrier' of f, the carrier of f:] is non empty set

the Target of f is Relation-like the carrier' of f -defined the carrier of f -valued Function-like V21( the carrier' of f, the carrier of f) Element of bool [: the carrier' of f, the carrier of f:]

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

[: the carrier' of f, the carrier' of f:] is non empty Relation-like set

[:[: the carrier' of f, the carrier' of f:], the carrier' of f:] is non empty Relation-like set

bool [:[: the carrier' of f, the carrier' of f:], the carrier' of f:] is non empty set

CatStr(# the carrier of f, the carrier' of f, the Source of f, the Target of f, the Comp of f #) is non empty non void V58() strict CatStr

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

bool [: the carrier' of f, the carrier' of f:] is non empty set

A1 is Element of the carrier' of f

g is Element of the carrier' of f

[A1,g] is V18() Element of [: the carrier' of f, the carrier' of f:]

{A1,g} is non empty set

{A1} is non empty set

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

dom A1 is Element of the carrier of f

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

cod g is Element of the carrier of f

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

A3 is Element of the carrier' of C

A2 is Element of the carrier' of C

[A3,A2] is V18() Element of the carrier' of [:C,C:]

[:C,C:] is non empty non void V58() Category-like transitive associative reflexive with_identities CatStr

[: the carrier of C, the carrier of C:] is non empty Relation-like set

[: the Source of C, the Source of C:] is Relation-like [: the carrier' of C, the carrier' of C:] -defined [: the carrier of C, the carrier of C:] -valued Function-like V21([: the carrier' of C, the carrier' of C:],[: 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:]:]

[:[: the carrier' of C, the carrier' of C:],[: the carrier of C, the carrier of C:]:] is non empty Relation-like set

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

[: the Target of C, the Target of C:] is Relation-like [: the carrier' of C, the carrier' of C:] -defined [: the carrier of C, the carrier of C:] -valued Function-like V21([: the carrier' of C, the carrier' of C:],[: 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:]:]

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

[:[: the carrier' of C, the carrier' of C:],[: the carrier' of C, the carrier' of C:]:] is non empty Relation-like set

[:[:[: the carrier' of C, the carrier' of C:],[: the carrier' of C, the carrier' of C:]:],[: the carrier' of C, the carrier' of C:]:] is non empty Relation-like set

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

CatStr(# [: the carrier of C, the carrier of C:],[: the carrier' of C, the carrier' of C:],[: the Source of C, the Source of C:],[: the Target of C, the Target of C:],K222( the carrier' of C, the carrier' of C, the Comp of C, the Comp of C) #) is non empty non void V58() strict CatStr

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

{A3,A2} is non empty set

{A3} is non empty set

{{A3,A2},{A3}} is non empty set

dom A3 is Element of the carrier of C

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

cod A2 is Element of the carrier of C

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

A1 is Element of the carrier' of f

dom A1 is Element of the carrier of f

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

g is Element of the carrier' of f

cod g is Element of the carrier of f

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

A1 (*) g is Element of the carrier' of f

dom (A1 (*) g) is Element of the carrier of f

the Source of f . (A1 (*) g) is Element of the carrier of f

dom g is Element of the carrier of f

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

cod (A1 (*) g) is Element of the carrier of f

the Target of f . (A1 (*) g) is Element of the carrier of f

cod A1 is Element of the carrier of f

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

A3 is Element of the carrier' of C

dom A3 is Element of the carrier of C

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

A2 is Element of the carrier' of C

cod A2 is Element of the carrier of C

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

[A3,A2] is V18() Element of the carrier' of [:C,C:]

[:C,C:] is non empty non void V58() Category-like transitive associative reflexive with_identities CatStr

[: the carrier of C, the carrier of C:] is non empty Relation-like set

[: the Source of C, the Source of C:] is Relation-like [: the carrier' of C, the carrier' of C:] -defined [: the carrier of C, the carrier of C:] -valued Function-like V21([: the carrier' of C, the carrier' of C:],[: 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:]:]

[:[: the carrier' of C, the carrier' of C:],[: the carrier of C, the carrier of C:]:] is non empty Relation-like set

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

[: the Target of C, the Target of C:] is Relation-like [: the carrier' of C, the carrier' of C:] -defined [: the carrier of C, the carrier of C:] -valued Function-like V21([: the carrier' of C, the carrier' of C:],[: 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:]:]

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

[:[: the carrier' of C, the carrier' of C:],[: the carrier' of C, the carrier' of C:]:] is non empty Relation-like set

[:[:[: the carrier' of C, the carrier' of C:],[: the carrier' of C, the carrier' of C:]:],[: the carrier' of C, the carrier' of C:]:] is non empty Relation-like set

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

CatStr(# [: the carrier of C, the carrier of C:],[: the carrier' of C, the carrier' of C:],[: the Source of C, the Source of C:],[: the Target of C, the Target of C:],K222( the carrier' of C, the carrier' of C, the Comp of C, the Comp of C) #) is non empty non void V58() strict CatStr

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

{A3,A2} is non empty set

{A3} is non empty set

{{A3,A2},{A3}} is non empty set

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

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

the Comp of C . (A3,A2) is set

[A3,A2] is V18() set

the Comp of C . [A3,A2] is set

A3 (*) A2 is Element of the carrier' of C

dom (A3 (*) A2) is Element of the carrier of C

the Source of C . (A3 (*) A2) is Element of the carrier of C

dom A2 is Element of the carrier of C

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

cod (A3 (*) A2) is Element of the carrier of C

the Target of C . (A3 (*) A2) is Element of the carrier of C

cod A3 is Element of the carrier of C

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

A1 is Element of the carrier' of f

cod A1 is Element of the carrier of f

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

g is Element of the carrier' of f

dom g is Element of the carrier of f

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

g (*) A1 is Element of the carrier' of f

A2 is Element of the carrier' of C

A3 is Element of the carrier' of C

A2 (*) A3 is Element of the carrier' of C

cod A3 is Element of the carrier of C

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

dom A2 is Element of the carrier of C

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

the Comp of f . (g,A1) is set

[g,A1] is V18() set

{g,A1} is non empty set

{g} is non empty set

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

the Comp of f . [g,A1] is set

the Comp of C . (A2,A3) is set

[A2,A3] is V18() set

{A2,A3} is non empty set

{A2} is non empty set

{{A2,A3},{A2}} is non empty set

the Comp of C . [A2,A3] is set

A2 is Element of the carrier' of f

dom A2 is Element of the carrier of f

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

A1 is Element of the carrier' of f

cod A1 is Element of the carrier of f

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

dom A1 is Element of the carrier of f

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

g is Element of the carrier' of f

cod g is Element of the carrier of f

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

A1 (*) g is Element of the carrier' of f

A2 (*) (A1 (*) g) is Element of the carrier' of f

A2 (*) A1 is Element of the carrier' of f

(A2 (*) A1) (*) g is Element of the carrier' of f

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

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

dom F is Element of the carrier of C

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

A3 is Element of the carrier' of C

cod A3 is Element of the carrier of C

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

F (*) A3 is Element of the carrier' of C

G (*) F is Element of the carrier' of C

dom (A2 (*) A1) is Element of the carrier of f

the Source of f . (A2 (*) A1) is Element of the carrier of f

cod (A1 (*) g) is Element of the carrier of f

the Target of f . (A1 (*) g) is Element of the carrier of f

G (*) (F (*) A3) is Element of the carrier' of C

(G (*) F) (*) A3 is Element of the carrier' of C

g is Element of the carrier of f

Hom (g,g) is Element of bool the carrier' of f

bool the carrier' of f is non empty set

{ b

A1 is Element of the carrier of C

id A1 is Morphism of A1,A1

A2 is Element of the carrier' of f

cod A2 is Element of the carrier of f

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

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

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

dom A2 is Element of the carrier of f

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

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

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

g is Element of the carrier of f

A1 is Element of the carrier of C

id A1 is Morphism of A1,A1

A2 is Element of the carrier' of f

cod A2 is Element of the carrier of f

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

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

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

dom A2 is Element of the carrier of f

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

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

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

A3 is Morphism of g,g

F is Element of the carrier of f

Hom (g,F) is Element of bool the carrier' of f

bool the carrier' of f is non empty set

{ b

Hom (F,g) is Element of bool the carrier' of f

{ b

FG is Morphism of g,F

FG (*) A3 is Element of the carrier' of f

m is Element of the carrier' of C

cod m is Element of the carrier of C

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

cod FG is Element of the carrier of f

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

G is Element of the carrier of C

dom m is Element of the carrier of C

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

dom FG is Element of the carrier of f

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

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

bool the carrier' of C is non empty set

{ b

g1 is Morphism of A1,G

dom g1 is Element of the carrier of C

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

cod A3 is Element of the carrier of f

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

the Comp of f . (FG,A3) is set

[FG,A3] is V18() set

{FG,A3} is non empty set

{FG} is non empty set

{{FG,A3},{FG}} is non empty set

the Comp of f . [FG,A3] is set

the Comp of C . (g1,(id A1)) is set

[g1,(id A1)] is V18() set

{g1,(id A1)} is non empty set

{g1} is non empty set

{{g1,(id A1)},{g1}} is non empty set

the Comp of C . [g1,(id A1)] is set

g1 (*) (id A1) is Element of the carrier' of C

FG is Morphism of F,g

A3 (*) FG is Element of the carrier' of f

m is Element of the carrier' of C

dom m is Element of the carrier of C

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

dom FG is Element of the carrier of f

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

G is Element of the carrier of C

cod m is Element of the carrier of C

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

cod FG is Element of the carrier of f

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

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

bool the carrier' of C is non empty set

{ b

g1 is Morphism of G,A1

cod g1 is Element of the carrier of C

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

dom A3 is Element of the carrier of f

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

the Comp of f . (A3,FG) is set

[A3,FG] is V18() set

{A3,FG} is non empty set

{A3} is non empty set

{{A3,FG},{A3}} is non empty set

the Comp of f . [A3,FG] is set

the Comp of C . ((id A1),g1) is set

[(id A1),g1] is V18() set

{(id A1),g1} is non empty set

{(id A1)} is non empty set

{{(id A1),g1},{(id A1)}} is non empty set

the Comp of C . [(id A1),g1] is set

(id A1) (*) g1 is Element of the carrier' of C

C is non empty non void V58() 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 Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like V21( 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 Relation-like set

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

the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like V21( the carrier' of C, the carrier of C) 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 non empty Relation-like set

[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is non empty Relation-like set

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

CatStr(# the carrier of C, the carrier' of C, the Source of C, the Target of C, the Comp of C #) is non empty non void V58() strict CatStr

f is non empty non void V58() Category-like transitive associative reflexive with_identities CatStr

the carrier of f is non empty set

the carrier' of f is non empty set

the Source of f is Relation-like the carrier' of f -defined the carrier of f -valued Function-like V21( the carrier' of f, the carrier of f) Element of bool [: the carrier' of f, the carrier of f:]

[: the carrier' of f, the carrier of f:] is non empty Relation-like set

bool [: the carrier' of f, the carrier of f:] is non empty set

the Target of f is Relation-like the carrier' of f -defined the carrier of f -valued Function-like V21( the carrier' of f, the carrier of f) Element of bool [: the carrier' of f, the carrier of f:]

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

[: the carrier' of f, the carrier' of f:] is non empty Relation-like set

[:[: the carrier' of f, the carrier' of f:], the carrier' of f:] is non empty Relation-like set

bool [:[: the carrier' of f, the carrier' of f:], the carrier' of f:] is non empty set

CatStr(# the carrier of f, the carrier' of f, the Source of f, the Target of f, the Comp of f #) is non empty non void V58() strict CatStr

g is Element of the carrier of C

id g is Morphism of g,g

A1 is Element of the carrier of f

id A1 is Morphism of A1,A1

A2 is Element of the carrier' of f

cod A2 is Element of the carrier of f

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

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

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

dom A2 is Element of the carrier of f

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

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

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

A3 is Morphism of A1,A1

F is Element of the carrier of f

Hom (A1,F) is Element of bool the carrier' of f

bool the carrier' of f is non empty set

{ b

Hom (F,A1) is Element of bool the carrier' of f

{ b

FG is Morphism of A1,F

FG (*) A3 is Element of the carrier' of f

m is Element of the carrier' of C

dom m is Element of the carrier of C

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

dom FG is Element of the carrier of f

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

cod A3 is Element of the carrier of f

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

the Comp of f . (FG,A3) is set

[FG,A3] is V18() set

{FG,A3} is non empty set

{FG} is non empty set

{{FG,A3},{FG}} is non empty set

the Comp of f . [FG,A3] is set

the Comp of C . (m,(id g)) is set

[m,(id g)] is V18() set

{m,(id g)} is non empty set

{m} is non empty set

{{m,(id g)},{m}} is non empty set

the Comp of C . [m,(id g)] is set

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

FG is Morphism of F,A1

A3 (*) FG is Element of the carrier' of f

m is Element of the carrier' of C

cod m is Element of the carrier of C

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

cod FG is Element of the carrier of f

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

dom A3 is Element of the carrier of f

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

the Comp of f . (A3,FG) is set

[A3,FG] is V18() set

{A3,FG} is non empty set

{A3} is non empty set

{{A3,FG},{A3}} is non empty set

the Comp of f . [A3,FG] is set

the Comp of C . ((id g),m) is set

[(id g),m] is V18() set

{(id g),m} is non empty set

{(id g)} is non empty set

{{(id g),m},{(id g)}} is non empty set

the Comp of C . [(id g),m] is set

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

0 is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Element of K158()

[0,0] is V18() set

{0,0} is non empty functional set

{0} is non empty functional set

{{0,0},{0}} is non empty set

[[0,0],1] is V18() set

{[0,0],1} is non empty set

{[0,0]} is non empty Relation-like Function-like set

{{[0,0],1},{[0,0]}} is non empty set

1Cat (0,[[0,0],1]) is non empty trivial V52() non void 1 -element V58() trivial' strict Category-like transitive associative reflexive with_identities CatStr

{[[0,0],1]} is non empty Relation-like Function-like set

K262([[0,0],1],0) is Relation-like {[[0,0],1]} -defined {0} -valued Function-like V21({[[0,0],1]},{0}) Element of bool [:{[[0,0],1]},{0}:]

[:{[[0,0],1]},{0}:] is non empty Relation-like set

bool [:{[[0,0],1]},{0}:] is non empty set

K261([[0,0],1],[[0,0],1],[[0,0],1]) is Relation-like [:{[[0,0],1]},{[[0,0],1]}:] -defined {[[0,0],1]} -valued Function-like V21([:{[[0,0],1]},{[[0,0],1]}:],{[[0,0],1]}) Element of bool [:[:{[[0,0],1]},{[[0,0],1]}:],{[[0,0],1]}:]

[:{[[0,0],1]},{[[0,0],1]}:] is non empty Relation-like set

[:[:{[[0,0],1]},{[[0,0],1]}:],{[[0,0],1]}:] is non empty Relation-like set

bool [:[:{[[0,0],1]},{[[0,0],1]}:],{[[0,0],1]}:] is non empty set

CatStr(# {0},{[[0,0],1]},K262([[0,0],1],0),K262([[0,0],1],0),K261([[0,0],1],[[0,0],1],[[0,0],1]) #) is non empty non void V58() strict CatStr

C is non empty trivial V52() non void 1 -element V58() trivial' strict Category-like transitive associative reflexive with_identities CatStr

the carrier' of C is non empty trivial set

f is Element of the carrier' of C

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

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 V21( 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 Relation-like set

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

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

cod 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 V21( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

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

[(dom f),(cod f)] is V18() Element of [: the carrier of C, the carrier of C:]

[: the carrier of C, the carrier of C:] is non empty Relation-like set

{(dom f),(cod f)} is non empty set

{(dom f)} is non empty set

{{(dom f),(cod f)},{(dom f)}} is non empty set

[[(dom f),(cod f)],1] is V18() set

{[(dom f),(cod f)],1} is non empty set

{[(dom f),(cod f)]} is non empty Relation-like Function-like set

{{[(dom f),(cod f)],1},{[(dom f),(cod f)]}} is non empty set

C is non empty non void V58() () CatStr

the carrier' of C is non empty set

the carrier of C is non empty set

f is Element of the carrier' of C

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 V21( 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 Relation-like set

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

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

f `11 is set

cod 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 V21( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

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

f `12 is set

[(dom f),(cod f)] is V18() Element of [: the carrier of C, the carrier of C:]

[: the carrier of C, the carrier of C:] is non empty Relation-like set

{(dom f),(cod f)} is non empty set

{(dom f)} is non empty set

{{(dom f),(cod f)},{(dom f)}} is non empty set

f `2 is set

[[(dom f),(cod f)],(f `2)] is V18() set

{[(dom f),(cod f)],(f `2)} is non empty set

{[(dom f),(cod f)]} is non empty Relation-like Function-like set

{{[(dom f),(cod f)],(f `2)},{[(dom f),(cod f)]}} is non empty set

g is set

[[(dom f),(cod f)],g] is V18() set

{[(dom f),(cod f)],g} is non empty set

{{[(dom f),(cod f)],g},{[(dom f),(cod f)]}} is non empty set

C is non empty non void V58() () CatStr

the carrier' of C is non empty set

f is Element of the carrier' of C

f `11 is set

the carrier of C is non empty set

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 V21( 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 Relation-like set

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

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

f `12 is set

cod 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 V21( 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 Relation-like set

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

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

F

F

[:F

{ [[b

the Element of F

g is Element of F

[ the Element of F

{ the Element of F

{ the Element of F

{{ the Element of F

[[ the Element of F

[:[:F

{[ the Element of F

{[ the Element of F

{{[ the Element of F

A1 is set

A2 is Element of F

A3 is Element of F

[A2,A3] is V18() Element of [:F

{A2,A3} is non empty set

{A2} is non empty set

{{A2,A3},{A2}} is non empty set

F is Element of F

[[A2,A3],F] is V18() Element of [:[:F

{[A2,A3],F} is non empty set

{[A2,A3]} is non empty Relation-like Function-like set

{{[A2,A3],F},{[A2,A3]}} is non empty set

bool [:[:F

A1 is non empty Relation-like [:F

A2 is Element of A1

A3 is Element of F

F is Element of F

[A3,F] is V18() Element of [:F

{A3,F} is non empty set

{A3} is non empty set

{{A3,F},{A3}} is non empty set

G is Element of F

[[A3,F],G] is V18() Element of [:[:F

{[A3,F],G} is non empty set

{[A3,F]} is non empty Relation-like Function-like set

{{[A3,F],G},{[A3,F]}} is non empty set

A2 `11 is Element of F

A2 `12 is Element of F

[(A2 `11),(A2 `12)] is V18() Element of [:F

{(A2 `11),(A2 `12)} is non empty set

{(A2 `11)} is non empty set

{{(A2 `11),(A2 `12)},{(A2 `11)}} is non empty set

A2 `2 is Element of F

[[(A2 `11),(A2 `12)],(A2 `2)] is V18() Element of [:[:F

{[(A2 `11),(A2 `12)],(A2 `2)} is non empty set

{[(A2 `11),(A2 `12)]} is non empty Relation-like Function-like set

{{[(A2 `11),(A2 `12)],(A2 `2)},{[(A2 `11),(A2 `12)]}} is non empty set

[:A1,F

bool [:A1,F

A2 is Relation-like A1 -defined F

A3 is Relation-like A1 -defined F

F is set

G is set

F `11 is set

G `12 is set

FG is Element of F

m is Element of F

[FG,m] is V18() Element of [:F

{FG,m} is non empty set

{FG} is non empty set

{{FG,m},{FG}} is non empty set

g1 is Element of F

[[FG,m],g1] is V18() Element of [:[:F

{[FG,m],g1} is non empty set

{[FG,m]} is non empty Relation-like Function-like set

{{[FG,m],g1},{[FG,m]}} is non empty set

a2 is Element of F

b2 is Element of F

[a2,b2] is V18() Element of [:F

{a2,b2} is non empty set

{a2} is non empty set

{{a2,b2},{a2}} is non empty set

g2 is Element of F

[[a2,b2],g2] is V18() Element of [:[:F

{[a2,b2],g2} is non empty set

{[a2,b2]} is non empty Relation-like Function-like set

{{[a2,b2],g2},{[a2,b2]}} is non empty set

F `12 is set

G `11 is set

F `2 is set

G `2 is set

F

[(G `11),(F `12)] is V18() set

{(G `11),(F `12)} is non empty set

{(G `11)} is non empty set

{{(G `11),(F `12)},{(G `11)}} is non empty set

F

[[(G `11),(F `12)],F

{[(G `11),(F `12)],F

{[(G `11),(F `12)]} is non empty Relation-like Function-like set

{{[(G `11),(F `12)],F

[:A1,A1:] is non empty Relation-like [:[:F

[:[:[:F

bool [:[:[:F

[:[:A1,A1:],A1:] is non empty Relation-like set

bool [:[:A1,A1:],A1:] is non empty set

F is Relation-like [:A1,A1:] -defined A1 -valued Function-like Element of bool [:[:A1,A1:],A1:]

dom F is Relation-like [:[:F

bool [:A1,A1:] is non empty set

G is Element of F

FG is Element of F

[G,G] is V18() Element of [:F

{G,G} is non empty set

{G} is non empty set

{{G,G},{G}} is non empty set

[[G,G],FG] is V18() Element of [:[:F

{[G,G],FG} is non empty set

{[G,G]} is non empty Relation-like Function-like set

{{[G,G],FG},{[G,G]}} is non empty set

m is Element of A1

g1 is Element of A1

[:F

bool [:F

G is Relation-like F

CatStr(# F

the carrier' of CatStr(# F

g1 is Element of the carrier' of CatStr(# F

m is Element of the carrier' of CatStr(# F

[g1,m] is V18() Element of [: the carrier' of CatStr(# F

[: the carrier' of CatStr(# F

{g1,m} is non empty set

{g1} is non empty set

{{g1,m},{g1}} is non empty set

g1 `11 is set

m `12 is set

A2 . g1 is set

the Comp of CatStr(# F

[:[: the carrier' of CatStr(# F

bool [:[: the carrier' of CatStr(# F

dom the Comp of CatStr(# F

bool [: the carrier' of CatStr(# F

dom g1 is Element of the carrier of CatStr(# F

the carrier of CatStr(# F

the Source of CatStr(# F

[: the carrier' of CatStr(# F

bool [: the carrier' of CatStr(# F

the Source of CatStr(# F

cod m is Element of the carrier of CatStr(# F

the Target of CatStr(# F

the Target of CatStr(# F

the carrier' of CatStr(# F

[: the carrier' of CatStr(# F

the Comp of CatStr(# F

[:[: the carrier' of CatStr(# F

bool [:[: the carrier' of CatStr(# F

dom the Comp of CatStr(# F

bool [: the carrier' of CatStr(# F

g1 is Element of the carrier' of CatStr(# F

m is Element of the carrier' of CatStr(# F

[g1,m] is V18() Element of [: the carrier' of CatStr(# F

{g1,m} is non empty set

{g1} is non empty set

{{g1,m},{g1}} is non empty set

dom g1 is Element of the carrier of CatStr(# F

the carrier of CatStr(# F

the Source of CatStr(# F

[: the carrier' of CatStr(# F

bool [: the carrier' of CatStr(# F

the Source of CatStr(# F

cod m is Element of the carrier of CatStr(# F

the Target of CatStr(# F

the Target of CatStr(# F

b2 is Element of the carrier' of CatStr(# F

dom b2 is Element of the carrier of CatStr(# F

the Source of CatStr(# F

a2 is Element of the carrier' of CatStr(# F

cod a2 is Element of the carrier of CatStr(# F

the Target of CatStr(# F

[b2,a2] is V18() Element of [: the carrier' of CatStr(# F

{b2,a2} is non empty set

{b2} is non empty set

{{b2,a2},{b2}} is non empty set

g1 is Element of the carrier' of CatStr(# F

dom g1 is Element of the carrier of CatStr(# F

the carrier of CatStr(# F

the Source of CatStr(# F

[: the carrier' of CatStr(# F

bool [: the carrier' of CatStr(# F

the Source of CatStr(# F

m is Element of the carrier' of CatStr(# F

cod m is Element of the carrier of CatStr(# F

the Target of CatStr(# F

the Target of CatStr(# F

g1 (*) m is Element of the carrier' of CatStr(# F

dom (g1 (*) m) is Element of the carrier of CatStr(# F

the Source of CatStr(# F

dom m is Element of the carrier of CatStr(# F

the Source of CatStr(# F

cod (g1 (*) m) is Element of the carrier of CatStr(# F

the Target of CatStr(# F

cod g1 is Element of the carrier of CatStr(# F

the Target of CatStr(# F

m `11 is set

g1 `11 is set

m `12 is set

g1 `12 is set

F . (g1,m) is set

[g1,m] is V18() set

{g1,m} is non empty set

{g1} is non empty set

{{g1,m},{g1}} is non empty set

F . [g1,m] is set

[(m `11),(g1 `12)] is V18() set

{(m `11),(g1 `12)} is non empty set

{(m `11)} is non empty set

{{(m `11),(g1 `12)},{(m `11)}} is non empty set

g1 `2 is set

m `2 is set

F

[[(m `11),(g1 `12)],F

{[(m `11),(g1 `12)],F

{[(m `11),(g1 `12)]} is non empty Relation-like Function-like set

{{[(m `11),(g1 `12)],F

[g1,m] is V18() Element of [: the carrier' of CatStr(# F

F . [g1,m] is set

(F . [g1,m]) `11 is set

the Comp of CatStr(# F

the Comp of CatStr(# F

(F . [g1,m]) `12 is set

a2 is Element of the carrier' of CatStr(# F

dom a2 is Element of the carrier of CatStr(# F

the carrier of CatStr(# F

the Source of CatStr(# F

[: the carrier' of CatStr(# F

bool [: the carrier' of CatStr(# F

the Source of CatStr(# F

g1 is Element of the carrier' of CatStr(# F

cod g1 is Element of the carrier of CatStr(# F

the Target of CatStr(# F

the Target of CatStr(# F

dom g1 is Element of the carrier of CatStr(# F

the Source of CatStr(# F

m is Element of the carrier' of CatStr(# F

cod m is Element of the carrier of CatStr(# F

the Target of CatStr(# F

g1 (*) m is Element of the carrier' of CatStr(# F

a2 (*) (g1 (*) m) is Element of the carrier' of CatStr(# F

a2 (*) g1 is Element of the carrier' of CatStr(# F

(a2 (*) g1) (*) m is Element of the carrier' of CatStr(# F

g1 `11 is set

a2 `11 is set

m `12 is set

g1 `12 is set

[g1,m] is V18() Element of [: the carrier' of CatStr(# F

{g1,m} is non empty set

{g1} is non empty set

{{g1,m},{g1}} is non empty set

[a2,g1] is V18() Element of [: the carrier' of CatStr(# F

{a2,g1} is non empty set

{a2} is non empty set

{{a2,g1},{a2}} is non empty set

F . [g1,m] is set

rng F is Relation-like [:F

bool A1 is non empty set

F . [a2,g1] is set

F . (g1,m) is set

[g1,m] is V18() set

F . [g1,m] is set

F . (a2,g1) is set

[a2,g1] is V18() set

F . [a2,g1] is set

b2 is Element of A1

m `11 is set

[(m `11),(g1 `12)] is V18() set

{(m `11),(g1 `12)} is non empty set

{(m `11)} is non empty set

{{(m `11),(g1 `12)},{(m `11)}} is non empty set

g1 `2 is set

m `2 is set

F

[[(m `11),(g1 `12)],F

{[(m `11),(g1 `12)],F

{[(m `11),(g1 `12)]} is non empty Relation-like Function-like set

{{[(m `11),(g1 `12)],F

g2 is Element of A1

a2 `12 is set

[(g1 `11),(a2 `12)] is V18() set

{(g1 `11),(a2 `12)} is non empty set

{(g1 `11)} is non empty set

{{(g1 `11),(a2 `12)},{(g1 `11)}} is non empty set

a2 `2 is set

F

[[(g1 `11),(a2 `12)],F

{[(g1 `11),(a2 `12)],F

{[(g1 `11),(a2 `12)]} is non empty Relation-like Function-like set

{{[(g1 `11),(a2 `12)],F

A2 . b2 is Element of F

b2 `11 is Element of F

A2 . g2 is Element of F

g2 `11 is Element of F

A3 . b2 is Element of F

b2 `12 is Element of F

A3 . g2 is Element of F

g2 `12 is Element of F

[a2,b2] is V18() Element of [: the carrier' of CatStr(# F

[: the carrier' of CatStr(# F

{a2,b2} is non empty set

{{a2,b2},{a2}} is non empty set

[g2,m] is V18() Element of [:A1, the carrier' of CatStr(# F

[:A1, the carrier' of CatStr(# F

{g2,m} is non empty set

{g2} is non empty set

{{g2,m},{g2}} is non empty set

ha1 is Element of A1

ha1 `11 is Element of F

ha1 `12 is Element of F

ha1 `2 is Element of F

ha2 is Element of A1

ha2 `11 is Element of F

ha2 `12 is Element of F

ha2 `2 is Element of F

hb1 is Element of A1

hb1 `11 is Element of F

hb1 `12 is Element of F

hb1 `2 is Element of F

the Comp of CatStr(# F

the Comp of CatStr(# F

dom (a2 (*) g1) is Element of the carrier of CatStr(# F

the Source of CatStr(# F

the Comp of CatStr(# F

the Comp of CatStr(# F

cod (g1 (*) m) is Element of the carrier of CatStr(# F

the Target of CatStr(# F

the Comp of CatStr(# F

[a2,( the Comp of CatStr(# F

{a2,( the Comp of CatStr(# F

{{a2,( the Comp of CatStr(# F

the Comp of CatStr(# F

[(m `11),(a2 `12)] is V18() set

{(m `11),(a2 `12)} is non empty set

{{(m `11),(a2 `12)},{(m `11)}} is non empty set

b2 `2 is Element of F

F

[[(m `11),(a2 `12)],F

{[(m `11),(a2 `12)],F

{[(m `11),(a2 `12)]} is non empty Relation-like Function-like set

{{[(m `11),(a2 `12)],F

F

F

[[(m `11),(a2 `12)],F

{[(m `11),(a2 `12)],F

{{[(m `11),(a2 `12)],F

F

F

[[(m `11),(a2 `12)],F

{[(m `11),(a2 `12)],F

{{[(m `11),(a2 `12)],F

g2 `2 is Element of F

F

[[(m `11),(a2 `12)],F

{[(m `11),(a2 `12)],F

{{[(m `11),(a2 `12)],F

the Comp of CatStr(# F

[( the Comp of CatStr(# F

{( the Comp of CatStr(# F

{( the Comp of CatStr(# F

{{( the Comp of CatStr(# F

the Comp of CatStr(# F

the carrier of CatStr(# F

m is Element of the carrier of CatStr(# F

Hom (m,m) is Element of bool the carrier' of CatStr(# F

bool the carrier' of CatStr(# F

{ b

G . m is set

[: the carrier of CatStr(# F

[m,m] is V18() Element of [: the carrier of CatStr(# F

{m,m} is non empty set

{m} is non empty set

{{m,m},{m}} is non empty set

g1 is Element of F

[[m,m],g1] is V18() Element of [:[: the carrier of CatStr(# F

[:[: the carrier of CatStr(# F

{[m,m],g1} is non empty set

{[m,m]} is non empty Relation-like Function-like set

{{[m,m],g1},{[m,m]}} is non empty set

a2 is Element of F

G . a2 is Element of A1

g2 is Element of the carrier' of CatStr(# F

cod g2 is Element of the carrier of CatStr(# F

the Target of CatStr(# F

[: the carrier' of CatStr(# F

bool [: the carrier' of CatStr(# F

the Target of CatStr(# F

(G . m) `12 is set

dom g2 is Element of the carrier of CatStr(# F

the Source of CatStr(# F

the Source of CatStr(# F

(G . m) `11 is set

the carrier of CatStr(# F

m is Element of the carrier of CatStr(# F

G . m is set

[: the carrier of CatStr(# F

[m,m] is V18() Element of [: the carrier of CatStr(# F

{m,m} is non empty set

{m} is non empty set

{{m,m},{m}} is non empty set

g1 is Element of F

[[m,m],g1] is V18() Element of [:[: the carrier of CatStr(# F

[:[: the carrier of CatStr(# F

{[m,m],g1} is non empty set

{[m,m]} is non empty Relation-like Function-like set

{{[m,m],g1},{[m,m]}} is non empty set

a2 is Element of F

G . a2 is Element of A1

g2 is Element of the carrier' of CatStr(# F

cod g2 is Element of the carrier of CatStr(# F

the Target of CatStr(# F

[: the carrier' of CatStr(# F

bool [: the carrier' of CatStr(# F

the Target of CatStr(# F

(G . m) `12 is set

dom g2 is Element of the carrier of CatStr(# F

the Source of CatStr(# F

the Source of CatStr(# F

(G . m) `11 is set

ha1 is Morphism of m,m

ha2 is Element of the carrier of CatStr(# F

Hom (m,ha2) is Element of bool the carrier' of CatStr(# F

bool the carrier' of CatStr(# F

{ b

Hom (ha2,m) is Element of bool the carrier' of CatStr(# F

{ b

hb1 is Morphism of m,ha2

hb1 (*) ha1 is Element of the carrier' of CatStr(# F

C is Element of F

F is Element of F

[C,F] is V18() Element of [:F

{C,F} is non empty set

{C} is non empty set

{{C,F},{C}} is non empty set

G is Element of F

[[C,F],G] is V18() Element of [:[:F

{[C,F],G} is non empty set

{[C,F]} is non empty Relation-like Function-like set

{{[C,F],G},{[C,F]}} is non empty set

dom hb1 is Element of the carrier of CatStr(# F

the Source of CatStr(# F

A2 . hb1 is set

[[C,F],G] `11 is Element of F

F

[[m,m],g1] `11 is Element of the carrier of CatStr(# F

[[m,m],g1] `2 is Element of F

[[C,F],G] `12 is Element of F

[[C,F],G] `2 is Element of F

hb1 `11 is set

[[m,m],g1] `12 is Element of the carrier of CatStr(# F

ha1 `12 is set

[hb1,ha1] is V18() Element of [: the carrier' of CatStr(# F

{hb1,ha1} is non empty set

{hb1} is non empty set

{{hb1,ha1},{hb1}} is non empty set

the Comp of CatStr(# F

[hb1,ha1] is V18() set

the Comp of CatStr(# F

F . (hb1,ha1) is set

F . [hb1,ha1] is set

ha1 `11 is set

hb1 `12 is set

[(ha1 `11),(hb1 `12)] is V18() set

{(ha1 `11),(hb1 `12)} is non empty set

{(ha1 `11)} is non empty set

{{(ha1 `11),(hb1 `12)},{(ha1 `11)}} is non empty set

hb1 `2 is set

ha1 `2 is set

F

[[(ha1 `11),(hb1 `12)],F

{[(ha1 `11),(hb1 `12)],F

{[(ha1 `11),(hb1 `12)]} is non empty Relation-like Function-like set

{{[(ha1 `11),(hb1 `12)],F

hb1 is Morphism of ha2,m

ha1 (*) hb1 is Element of the carrier' of CatStr(# F

C is Element of F

F is Element of F

[C,F] is V18() Element of [:F

{C,F} is non empty set

{C} is non empty set

{{C,F},{C}} is non empty set

G is Element of F

[[C,F],G] is V18() Element of [:[:F

{[C,F],G} is non empty set

{[C,F]} is non empty Relation-like Function-like set

{{[C,F],G},{[C,F]}} is non empty set

cod hb1 is Element of the carrier of CatStr(# F

the Target of CatStr(# F

A3 . hb1 is set

[[C,F],G] `12 is Element of F

F

[[m,m],g1] `12 is Element of the carrier of CatStr(# F

[[m,m],g1] `2 is Element of F

[[C,F],G] `11 is Element of F

[[C,F],G] `2 is Element of F

hb1 `12 is set

[[m,m],g1] `11 is Element of the carrier of CatStr(# F

ha1 `11 is set

[ha1,hb1] is V18() Element of [: the carrier' of CatStr(# F

{ha1,hb1} is non empty set

{ha1} is non empty set

{{ha1,hb1},{ha1}} is non empty set

the Comp of CatStr(# F

[ha1,hb1] is V18() set

the Comp of CatStr(# F

F . (ha1