:: ISOCAT_1 semantic presentation

K120() is M2( bool K116())

K116() is set

bool K116() is set

{} is set

the empty set is empty set

1 is non empty set

{{},1} is set

K115() is set

bool K115() is set

bool K120() is set

C is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

the carrier' of C is non empty set

F is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

the carrier' of F is non empty set

the carrier of F is non empty set

G is Relation-like the carrier' of F -defined the carrier' of C -valued Function-like non empty total V18( the carrier' of F, the carrier' of C) Functor of F,C

o is M2( the carrier of F)

s is M2( the carrier of F)

G . o is M2( the carrier of C)

the carrier of C is non empty set

Obj G is Relation-like the carrier of F -defined the carrier of C -valued Function-like non empty total V18( the carrier of F, the carrier of C) M2( bool [: the carrier of F, the carrier of C:])

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

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

(Obj G) . o is M2( the carrier of C)

G . s is M2( the carrier of C)

(Obj G) . s is M2( the carrier of C)

b is Morphism of o,s

G /. b is Morphism of G . o,G . s

Hom (o,s) is M2( bool the carrier' of F)

bool the carrier' of F is set

{ b

Hom (s,o) is M2( bool the carrier' of F)

{ b

id s is Morphism of s,s

id o is Morphism of o,o

c

b * c

c

dom c

cod b is M2( the carrier of F)

cod c

dom b is M2( the carrier of F)

b (*) c

id (cod b) is Morphism of cod b, cod b

c

id (dom b) is Morphism of dom b, dom b

Hom ((G . o),(G . s)) is M2( bool the carrier' of C)

bool the carrier' of C is set

{ b

Hom ((G . s),(G . o)) is M2( bool the carrier' of C)

{ b

id (G . s) is Morphism of G . s,G . s

id (G . o) is Morphism of G . o,G . o

G /. c

(G /. b) * (G /. c

(G /. c

G . b is M2( the carrier' of C)

G . c

(G . b) (*) (G . c

G . (b (*) c

cod (G /. b) is M2( the carrier of C)

id (cod (G /. b)) is Morphism of cod (G /. b), cod (G /. b)

(G . c

G . (c

dom (G /. b) is M2( the carrier of C)

id (dom (G /. b)) is Morphism of dom (G /. b), dom (G /. b)

C is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

the carrier' of C is non empty set

the carrier of C is non empty set

F is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

the carrier' of F is non empty set

G is Relation-like the carrier' of C -defined the carrier' of F -valued Function-like non empty total V18( the carrier' of C, the carrier' of F) Functor of C,F

o is Relation-like the carrier' of C -defined the carrier' of F -valued Function-like non empty total V18( the carrier' of C, the carrier' of F) Functor of C,F

s is Relation-like the carrier of C -defined the carrier' of F -valued Function-like non empty total V18( the carrier of C, the carrier' of F) transformation of G,o

b is M2( the carrier of C)

s . b is Morphism of G . b,o . b

G . b is M2( the carrier of F)

the carrier of F is non empty set

Obj G is Relation-like the carrier of C -defined the carrier of F -valued Function-like non empty total V18( the carrier of C, the carrier of F) M2( bool [: the carrier of C, the carrier of F:])

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

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

(Obj G) . b is M2( the carrier of F)

o . b is M2( the carrier of F)

Obj o is Relation-like the carrier of C -defined the carrier of F -valued Function-like non empty total V18( the carrier of C, the carrier of F) M2( bool [: the carrier of C, the carrier of F:])

(Obj o) . b is M2( the carrier of F)

Hom ((G . b),(o . b)) is M2( bool the carrier' of F)

bool the carrier' of F is set

{ b

C is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

the carrier' of C is non empty set

F is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

the carrier' of F is non empty set

G is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

the carrier' of G is non empty set

o is Relation-like the carrier' of C -defined the carrier' of F -valued Function-like non empty total V18( the carrier' of C, the carrier' of F) Functor of C,F

s is Relation-like the carrier' of C -defined the carrier' of F -valued Function-like non empty total V18( the carrier' of C, the carrier' of F) Functor of C,F

b is Relation-like the carrier' of F -defined the carrier' of G -valued Function-like non empty total V18( the carrier' of F, the carrier' of G) Functor of F,G

c

b * o is Relation-like the carrier' of C -defined the carrier' of C -defined the carrier' of G -valued the carrier' of G -valued Function-like non empty total V18( the carrier' of C, the carrier' of G) V18( the carrier' of C, the carrier' of G) Functor of C,G

c

the carrier of C is non empty set

f2 is M2( the carrier of C)

(b * o) . f2 is M2( the carrier of G)

the carrier of G is non empty set

Obj (b * o) is Relation-like the carrier of C -defined the carrier of G -valued Function-like non empty total V18( the carrier of C, the carrier of G) M2( bool [: the carrier of C, the carrier of G:])

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

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

(Obj (b * o)) . f2 is M2( the carrier of G)

(c

Obj (c

(Obj (c

Hom (((b * o) . f2),((c

bool the carrier' of G is set

{ b

o . f2 is M2( the carrier of F)

the carrier of F is non empty set

Obj o is Relation-like the carrier of C -defined the carrier of F -valued Function-like non empty total V18( the carrier of C, the carrier of F) M2( bool [: the carrier of C, the carrier of F:])

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

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

(Obj o) . f2 is M2( the carrier of F)

s . f2 is M2( the carrier of F)

Obj s is Relation-like the carrier of C -defined the carrier of F -valued Function-like non empty total V18( the carrier of C, the carrier of F) M2( bool [: the carrier of C, the carrier of F:])

(Obj s) . f2 is M2( the carrier of F)

Hom ((o . f2),(s . f2)) is M2( bool the carrier' of F)

bool the carrier' of F is set

{ b

b . (o . f2) is M2( the carrier of G)

Obj b is Relation-like the carrier of F -defined the carrier of G -valued Function-like non empty total V18( the carrier of F, the carrier of G) M2( bool [: the carrier of F, the carrier of G:])

[: the carrier of F, the carrier of G:] is set

bool [: the carrier of F, the carrier of G:] is set

(Obj b) . (o . f2) is M2( the carrier of G)

b . (s . f2) is M2( the carrier of G)

(Obj b) . (s . f2) is M2( the carrier of G)

Hom ((b . (o . f2)),(b . (s . f2))) is M2( bool the carrier' of G)

{ b

c

Obj c

(Obj c

Hom ((b . (s . f2)),(c

{ b

C is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

the carrier' of C is non empty set

the carrier of C is non empty set

F is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

the carrier' of F is non empty set

G is Relation-like the carrier' of C -defined the carrier' of F -valued Function-like non empty total V18( the carrier' of C, the carrier' of F) Functor of C,F

o is Relation-like the carrier' of C -defined the carrier' of F -valued Function-like non empty total V18( the carrier' of C, the carrier' of F) Functor of C,F

s is Relation-like the carrier of C -defined the carrier' of F -valued Function-like non empty total V18( the carrier of C, the carrier' of F) transformation of G,o

b is M2( the carrier of C)

G . b is M2( the carrier of F)

the carrier of F is non empty set

Obj G is Relation-like the carrier of C -defined the carrier of F -valued Function-like non empty total V18( the carrier of C, the carrier of F) M2( bool [: the carrier of C, the carrier of F:])

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

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

(Obj G) . b is M2( the carrier of F)

o . b is M2( the carrier of F)

Obj o is Relation-like the carrier of C -defined the carrier of F -valued Function-like non empty total V18( the carrier of C, the carrier of F) M2( bool [: the carrier of C, the carrier of F:])

(Obj o) . b is M2( the carrier of F)

s . b is Morphism of G . b,o . b

C is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

the carrier' of C is non empty set

F is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

the carrier' of F is non empty set

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

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

the carrier of C is non empty set

the carrier of F is non empty set

G is Relation-like the carrier' of C -defined the carrier' of F -valued Function-like non empty total V18( the carrier' of C, the carrier' of F) M2( bool [: the carrier' of C, the carrier' of F:])

o is M2( the carrier of C)

id o is Morphism of o,o

G . (id o) is M2( the carrier' of F)

s is M2( the carrier' of C)

dom s is M2( the carrier of C)

id (dom s) is Morphism of dom s, dom s

G . (id (dom s)) is M2( the carrier' of F)

G . s is M2( the carrier' of F)

dom (G . s) is M2( the carrier of F)

id (dom (G . s)) is Morphism of dom (G . s), dom (G . s)

b is M2( the carrier' of C)

cod b is M2( the carrier of C)

id (cod b) is Morphism of cod b, cod b

G . (id (cod b)) is M2( the carrier' of F)

G . b is M2( the carrier' of F)

cod (G . b) is M2( the carrier of F)

id (cod (G . b)) is Morphism of cod (G . b), cod (G . b)

f2 is M2( the carrier' of C)

dom f2 is M2( the carrier of C)

c

cod c

f2 (*) c

G . (f2 (*) c

G . c

G . f2 is M2( the carrier' of F)

(G . f2) (*) (G . c

f1 is Relation-like the carrier' of C -defined the carrier' of F -valued Function-like non empty total V18( the carrier' of C, the carrier' of F) M2( bool [: the carrier' of C, the carrier' of F:])

C is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

the carrier' of C is non empty set

F is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

the carrier' of F is non empty set

G is Relation-like the carrier' of F -defined the carrier' of C -valued Function-like non empty total V18( the carrier' of F, the carrier' of C) Functor of F,C

o is M2( the carrier' of C)

rng G is M2( bool the carrier' of C)

bool the carrier' of C is set

dom G is M2( bool the carrier' of F)

bool the carrier' of F is set

s is set

G . s is set

b is M2( the carrier' of F)

G . b is M2( the carrier' of C)

C is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

the carrier' of C is non empty set

the carrier of C is non empty set

F is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

the carrier' of F is non empty set

the carrier of F is non empty set

G is Relation-like the carrier' of F -defined the carrier' of C -valued Function-like non empty total V18( the carrier' of F, the carrier' of C) Functor of F,C

o is M2( the carrier of C)

Obj G is Relation-like the carrier of F -defined the carrier of C -valued Function-like non empty total V18( the carrier of F, the carrier of C) M2( bool [: the carrier of F, the carrier of C:])

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

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

rng (Obj G) is M2( bool the carrier of C)

bool the carrier of C is set

dom (Obj G) is M2( bool the carrier of F)

bool the carrier of F is set

s is set

(Obj G) . s is set

b is M2( the carrier of F)

G . b is M2( the carrier of C)

(Obj G) . b is M2( the carrier of C)

C is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

the carrier' of C is non empty set

F is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

the carrier' of F is non empty set

G is Relation-like the carrier' of C -defined the carrier' of F -valued Function-like non empty total V18( the carrier' of C, the carrier' of F) Functor of C,F

Obj G is Relation-like the carrier of C -defined the carrier of F -valued Function-like non empty total V18( the carrier of C, the carrier of F) M2( bool [: the carrier of C, the carrier of F:])

the carrier of C is non empty set

the carrier of F is non empty set

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

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

o is set

dom (Obj G) is set

s is set

(Obj G) . o is set

(Obj G) . s is set

dom (Obj G) is M2( bool the carrier of C)

bool the carrier of C is set

b is M2( the carrier of C)

G . b is M2( the carrier of F)

(Obj G) . b is M2( the carrier of F)

c

G . c

(Obj G) . c

id b is Morphism of b,b

G . (id b) is M2( the carrier' of F)

id (G . c

id c

G . (id c

dom G is M2( bool the carrier' of C)

bool the carrier' of C is set

C is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

the carrier' of C is non empty set

F is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

the carrier' of F is non empty set

G is Relation-like the carrier' of C -defined the carrier' of F -valued Function-like non empty total V18( the carrier' of C, the carrier' of F) Functor of C,F

G " is Relation-like Function-like set

rng G is M2( bool the carrier' of F)

bool the carrier' of F is set

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

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

dom G is M2( bool the carrier' of C)

bool the carrier' of C is set

Obj G is Relation-like the carrier of C -defined the carrier of F -valued Function-like non empty total V18( the carrier of C, the carrier of F) M2( bool [: the carrier of C, the carrier of F:])

the carrier of C is non empty set

the carrier of F is non empty set

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

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

o is Relation-like the carrier' of F -defined the carrier' of C -valued Function-like non empty total V18( the carrier' of F, the carrier' of C) M2( bool [: the carrier' of F, the carrier' of C:])

s is M2( the carrier of F)

id s is Morphism of s,s

o . (id s) is M2( the carrier' of C)

b is M2( the carrier of C)

G . b is M2( the carrier of F)

(Obj G) . b is M2( the carrier of F)

id b is Morphism of b,b

G . (id b) is M2( the carrier' of F)

o . (G . (id b)) is M2( the carrier' of C)

s is M2( the carrier' of F)

dom s is M2( the carrier of F)

id (dom s) is Morphism of dom s, dom s

o . (id (dom s)) is M2( the carrier' of C)

o . s is M2( the carrier' of C)

dom (o . s) is M2( the carrier of C)

id (dom (o . s)) is Morphism of dom (o . s), dom (o . s)

cod s is M2( the carrier of F)

id (cod s) is Morphism of cod s, cod s

o . (id (cod s)) is M2( the carrier' of C)

cod (o . s) is M2( the carrier of C)

id (cod (o . s)) is Morphism of cod (o . s), cod (o . s)

b is M2( the carrier' of C)

G . b is M2( the carrier' of F)

dom b is M2( the carrier of C)

G . (dom b) is M2( the carrier of F)

(Obj G) . (dom b) is M2( the carrier of F)

id (G . (dom b)) is Morphism of G . (dom b),G . (dom b)

o . (id (G . (dom b))) is M2( the carrier' of C)

id (dom b) is Morphism of dom b, dom b

G . (id (dom b)) is M2( the carrier' of F)

o . (G . (id (dom b))) is M2( the carrier' of C)

cod b is M2( the carrier of C)

G . (cod b) is M2( the carrier of F)

(Obj G) . (cod b) is M2( the carrier of F)

id (G . (cod b)) is Morphism of G . (cod b),G . (cod b)

o . (id (G . (cod b))) is M2( the carrier' of C)

id (cod b) is Morphism of cod b, cod b

G . (id (cod b)) is M2( the carrier' of F)

o . (G . (id (cod b))) is M2( the carrier' of C)

b is M2( the carrier' of F)

dom b is M2( the carrier of F)

s is M2( the carrier' of F)

cod s is M2( the carrier of F)

b (*) s is M2( the carrier' of F)

o . (b (*) s) is M2( the carrier' of C)

o . s is M2( the carrier' of C)

o . b is M2( the carrier' of C)

(o . b) (*) (o . s) is M2( the carrier' of C)

dom (Obj G) is M2( bool the carrier of C)

bool the carrier of C is set

c

G . c

f2 is M2( the carrier' of C)

G . f2 is M2( the carrier' of F)

dom f2 is M2( the carrier of C)

(Obj G) . (dom f2) is M2( the carrier of F)

G . (dom f2) is M2( the carrier of F)

cod c

G . (cod c

(Obj G) . (cod c

f2 (*) c

G . (f2 (*) c

o . (G . (f2 (*) c

f2 (*) (o . s) is M2( the carrier' of C)

C is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

the carrier' of C is non empty set

F is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

the carrier' of F is non empty set

G is Relation-like the carrier' of C -defined the carrier' of F -valued Function-like non empty total V18( the carrier' of C, the carrier' of F) Functor of C,F

rng G is M2( bool the carrier' of F)

bool the carrier' of F is set

Obj G is Relation-like the carrier of C -defined the carrier of F -valued Function-like non empty total V18( the carrier of C, the carrier of F) M2( bool [: the carrier of C, the carrier of F:])

the carrier of C is non empty set

the carrier of F is non empty set

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

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

rng (Obj G) is set

rng (Obj G) is M2( bool the carrier of F)

bool the carrier of F is set

o is set

dom G is M2( bool the carrier' of C)

bool the carrier' of C is set

s is M2( the carrier of F)

id s is Morphism of s,s

b is set

G . b is set

c

dom c

id (dom c

f2 is M2( the carrier' of C)

G . f2 is M2( the carrier' of F)

dom (id s) is M2( the carrier of F)

id (dom (id s)) is Morphism of dom (id s), dom (id s)

dom (Obj G) is M2( bool the carrier of C)

bool the carrier of C is set

(Obj G) . (dom c

C is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

the carrier' of C is non empty set

F is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

the carrier' of F is non empty set

G is Relation-like the carrier' of C -defined the carrier' of F -valued Function-like non empty total V18( the carrier' of C, the carrier' of F) Functor of C,F

(C,F,G) is Relation-like the carrier' of F -defined the carrier' of C -valued Function-like non empty total V18( the carrier' of F, the carrier' of C) Functor of F,C

G " is Relation-like Function-like set

rng (C,F,G) is M2( bool the carrier' of C)

bool the carrier' of C is set

dom G is M2( bool the carrier' of C)

C is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

the carrier' of C is non empty set

F is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

the carrier' of F is non empty set

G is Relation-like the carrier' of C -defined the carrier' of F -valued Function-like non empty total V18( the carrier' of C, the carrier' of F) Functor of C,F

Obj G is Relation-like the carrier of C -defined the carrier of F -valued Function-like non empty total V18( the carrier of C, the carrier of F) M2( bool [: the carrier of C, the carrier of F:])

the carrier of C is non empty set

the carrier of F is non empty set

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

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

(Obj G) " is Relation-like Function-like set

(C,F,G) is Relation-like the carrier' of F -defined the carrier' of C -valued Function-like non empty total V18( the carrier' of F, the carrier' of C) Functor of F,C

Obj (C,F,G) is Relation-like the carrier of F -defined the carrier of C -valued Function-like non empty total V18( the carrier of F, the carrier of C) M2( bool [: the carrier of F, the carrier of C:])

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

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

rng (Obj G) is M2( bool the carrier of F)

bool the carrier of F is set

o is Relation-like the carrier of F -defined the carrier of C -valued Function-like non empty total V18( the carrier of F, the carrier of C) M2( bool [: the carrier of F, the carrier of C:])

s is M2( the carrier of F)

o . s is M2( the carrier of C)

id (o . s) is Morphism of o . s,o . s

G . (id (o . s)) is M2( the carrier' of F)

(Obj G) . (o . s) is M2( the carrier of F)

id ((Obj G) . (o . s)) is Morphism of (Obj G) . (o . s),(Obj G) . (o . s)

id s is Morphism of s,s

G " is Relation-like Function-like set

(G ") . (id s) is set

(C,F,G) . (id s) is M2( the carrier' of C)

(Obj (C,F,G)) . s is M2( the carrier of C)

C is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

the carrier' of C is non empty set

F is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

the carrier' of F is non empty set

G is Relation-like the carrier' of C -defined the carrier' of F -valued Function-like non empty total V18( the carrier' of C, the carrier' of F) Functor of C,F

(C,F,G) is Relation-like the carrier' of F -defined the carrier' of C -valued Function-like non empty total V18( the carrier' of F, the carrier' of C) Functor of F,C

(F,C,(C,F,G)) is Relation-like the carrier' of C -defined the carrier' of F -valued Function-like non empty total V18( the carrier' of C, the carrier' of F) Functor of C,F

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

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

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

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

s is Relation-like the carrier' of F -defined the carrier' of C -valued Function-like non empty total V18( the carrier' of F, the carrier' of C) M2( bool [: the carrier' of F, the carrier' of C:])

s " is Relation-like Function-like set

o is Relation-like the carrier' of C -defined the carrier' of F -valued Function-like non empty total V18( the carrier' of C, the carrier' of F) M2( bool [: the carrier' of C, the carrier' of F:])

o " is Relation-like Function-like set

(o ") " is Relation-like Function-like set

C is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

the carrier' of C is non empty set

id C is Relation-like the carrier' of C -defined the carrier' of C -valued Function-like non empty total V18( the carrier' of C, the carrier' of C) Functor of C,C

id the carrier' of C is Relation-like the carrier' of C -defined the carrier' of C -valued non empty total V18( the carrier' of C, the carrier' of C) M2( 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

F is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

the carrier' of F is non empty set

id F is Relation-like the carrier' of F -defined the carrier' of F -valued Function-like non empty total V18( the carrier' of F, the carrier' of F) Functor of F,F

id the carrier' of F is Relation-like the carrier' of F -defined the carrier' of F -valued non empty total V18( the carrier' of F, the carrier' of F) M2( bool [: the carrier' of F, the carrier' of F:])

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

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

G is Relation-like the carrier' of F -defined the carrier' of C -valued Function-like non empty total V18( the carrier' of F, the carrier' of C) Functor of F,C

(F,C,G) is Relation-like the carrier' of C -defined the carrier' of F -valued Function-like non empty total V18( the carrier' of C, the carrier' of F) Functor of C,F

G * (F,C,G) is Relation-like the carrier' of C -defined the carrier' of C -defined the carrier' of C -valued the carrier' of C -valued Function-like non empty total V18( the carrier' of C, the carrier' of C) V18( the carrier' of C, the carrier' of C) Functor of C,C

(F,C,G) * G is Relation-like the carrier' of F -defined the carrier' of F -defined the carrier' of F -valued the carrier' of F -valued Function-like non empty total V18( the carrier' of F, the carrier' of F) V18( the carrier' of F, the carrier' of F) Functor of F,F

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

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

o is Relation-like the carrier' of F -defined the carrier' of C -valued Function-like non empty total V18( the carrier' of F, the carrier' of C) M2( bool [: the carrier' of F, the carrier' of C:])

dom o is M2( bool the carrier' of F)

bool the carrier' of F is set

rng o is M2( bool the carrier' of C)

bool the carrier' of C is set

o " is Relation-like Function-like set

(o ") (#) o is Relation-like set

o (#) (o ") is Relation-like set

C is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

the carrier' of C is non empty set

F is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

the carrier' of F is non empty set

G is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

the carrier' of G is non empty set

o is Relation-like the carrier' of C -defined the carrier' of F -valued Function-like non empty total V18( the carrier' of C, the carrier' of F) Functor of C,F

s is Relation-like the carrier' of F -defined the carrier' of G -valued Function-like non empty total V18( the carrier' of F, the carrier' of G) Functor of F,G

s * o is Relation-like the carrier' of C -defined the carrier' of C -defined the carrier' of G -valued the carrier' of G -valued Function-like non empty total V18( the carrier' of C, the carrier' of G) V18( the carrier' of C, the carrier' of G) Functor of C,G

rng o is M2( bool the carrier' of F)

bool the carrier' of F is set

rng s is M2( bool the carrier' of G)

bool the carrier' of G is set

rng (s * o) is M2( bool the carrier' of G)

dom s is M2( bool the carrier' of F)

G is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

the carrier' of G is non empty set

id G is Relation-like the carrier' of G -defined the carrier' of G -valued Function-like non empty total V18( the carrier' of G, the carrier' of G) Functor of G,G

id the carrier' of G is Relation-like the carrier' of G -defined the carrier' of G -valued non empty total V18( the carrier' of G, the carrier' of G) M2( bool [: the carrier' of G, the carrier' of G:])

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

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

G is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

the carrier' of G is non empty set

o is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

the carrier' of o is non empty set

s is Relation-like the carrier' of G -defined the carrier' of o -valued Function-like non empty total V18( the carrier' of G, the carrier' of o) Functor of G,o

(G,o,s) is Relation-like the carrier' of o -defined the carrier' of G -valued Function-like non empty total V18( the carrier' of o, the carrier' of G) Functor of o,G

C is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

F is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

G is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

the carrier' of C is non empty set

the carrier' of F is non empty set

o is Relation-like the carrier' of C -defined the carrier' of F -valued Function-like non empty total V18( the carrier' of C, the carrier' of F) Functor of C,F

the carrier' of G is non empty set

s is Relation-like the carrier' of F -defined the carrier' of G -valued Function-like non empty total V18( the carrier' of F, the carrier' of G) Functor of F,G

s * o is Relation-like the carrier' of C -defined the carrier' of C -defined the carrier' of G -valued the carrier' of G -valued Function-like non empty total V18( the carrier' of C, the carrier' of G) V18( the carrier' of C, the carrier' of G) Functor of C,G

C is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

F is set

G is set

1Cat (F,G) is non empty trivial V49() non void V54(1) V55() trivial' strict Category-like V68() V69() V70() with_identities CatStr

{F} is set

{G} is set

K224(G,F) is Relation-like {G} -defined {F} -valued Function-like V18({G},{F}) M2( bool [:{G},{F}:])

[:{G},{F}:] is set

bool [:{G},{F}:] is set

K223(G,G,G) is Relation-like [:{G},{G}:] -defined {G} -valued Function-like V18([:{G},{G}:],{G}) M2( bool [:[:{G},{G}:],{G}:])

[:{G},{G}:] is set

[:[:{G},{G}:],{G}:] is set

bool [:[:{G},{G}:],{G}:] is set

CatStr(# {F},{G},K224(G,F),K224(G,F),K223(G,G,G) #) is strict CatStr

[:(1Cat (F,G)),C:] is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

the carrier of (1Cat (F,G)) is non empty trivial V31() set

the carrier of C is non empty set

[: the carrier of (1Cat (F,G)), the carrier of C:] is set

the carrier' of (1Cat (F,G)) is non empty trivial set

the carrier' of C is non empty set

[: the carrier' of (1Cat (F,G)), the carrier' of C:] is set

the Source of (1Cat (F,G)) is Relation-like the carrier' of (1Cat (F,G)) -defined the carrier of (1Cat (F,G)) -valued Function-like non empty total V18( the carrier' of (1Cat (F,G)), the carrier of (1Cat (F,G))) M2( bool [: the carrier' of (1Cat (F,G)), the carrier of (1Cat (F,G)):])

[: the carrier' of (1Cat (F,G)), the carrier of (1Cat (F,G)):] is set

bool [: the carrier' of (1Cat (F,G)), the carrier of (1Cat (F,G)):] is set

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V18( the carrier' of C, the carrier of C) M2( 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 (1Cat (F,G)), the Source of C:] is Relation-like [: the carrier' of (1Cat (F,G)), the carrier' of C:] -defined [: the carrier of (1Cat (F,G)), the carrier of C:] -valued Function-like V18([: the carrier' of (1Cat (F,G)), the carrier' of C:],[: the carrier of (1Cat (F,G)), the carrier of C:]) M2( bool [:[: the carrier' of (1Cat (F,G)), the carrier' of C:],[: the carrier of (1Cat (F,G)), the carrier of C:]:])

[:[: the carrier' of (1Cat (F,G)), the carrier' of C:],[: the carrier of (1Cat (F,G)), the carrier of C:]:] is set

bool [:[: the carrier' of (1Cat (F,G)), the carrier' of C:],[: the carrier of (1Cat (F,G)), the carrier of C:]:] is set

the Target of (1Cat (F,G)) is Relation-like the carrier' of (1Cat (F,G)) -defined the carrier of (1Cat (F,G)) -valued Function-like non empty total V18( the carrier' of (1Cat (F,G)), the carrier of (1Cat (F,G))) M2( bool [: the carrier' of (1Cat (F,G)), the carrier of (1Cat (F,G)):])

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

[: the Target of (1Cat (F,G)), the Target of C:] is Relation-like [: the carrier' of (1Cat (F,G)), the carrier' of C:] -defined [: the carrier of (1Cat (F,G)), the carrier of C:] -valued Function-like V18([: the carrier' of (1Cat (F,G)), the carrier' of C:],[: the carrier of (1Cat (F,G)), the carrier of C:]) M2( bool [:[: the carrier' of (1Cat (F,G)), the carrier' of C:],[: the carrier of (1Cat (F,G)), the carrier of C:]:])

the Comp of (1Cat (F,G)) is Relation-like [: the carrier' of (1Cat (F,G)), the carrier' of (1Cat (F,G)):] -defined the carrier' of (1Cat (F,G)) -valued Function-like M2( bool [:[: the carrier' of (1Cat (F,G)), the carrier' of (1Cat (F,G)):], the carrier' of (1Cat (F,G)):])

[: the carrier' of (1Cat (F,G)), the carrier' of (1Cat (F,G)):] is set

[:[: the carrier' of (1Cat (F,G)), the carrier' of (1Cat (F,G)):], the carrier' of (1Cat (F,G)):] is set

bool [:[: the carrier' of (1Cat (F,G)), the carrier' of (1Cat (F,G)):], the carrier' of (1Cat (F,G)):] is set

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

K184( the carrier' of (1Cat (F,G)), the carrier' of C, the Comp of (1Cat (F,G)), the Comp of C) is Relation-like [:[: the carrier' of (1Cat (F,G)), the carrier' of C:],[: the carrier' of (1Cat (F,G)), the carrier' of C:]:] -defined [: the carrier' of (1Cat (F,G)), the carrier' of C:] -valued Function-like M2( bool [:[:[: the carrier' of (1Cat (F,G)), the carrier' of C:],[: the carrier' of (1Cat (F,G)), the carrier' of C:]:],[: the carrier' of (1Cat (F,G)), the carrier' of C:]:])

[:[: the carrier' of (1Cat (F,G)), the carrier' of C:],[: the carrier' of (1Cat (F,G)), the carrier' of C:]:] is set

[:[:[: the carrier' of (1Cat (F,G)), the carrier' of C:],[: the carrier' of (1Cat (F,G)), the carrier' of C:]:],[: the carrier' of (1Cat (F,G)), the carrier' of C:]:] is set

bool [:[:[: the carrier' of (1Cat (F,G)), the carrier' of C:],[: the carrier' of (1Cat (F,G)), the carrier' of C:]:],[: the carrier' of (1Cat (F,G)), the carrier' of C:]:] is set

CatStr(# [: the carrier of (1Cat (F,G)), the carrier of C:],[: the carrier' of (1Cat (F,G)), the carrier' of C:],[: the Source of (1Cat (F,G)), the Source of C:],[: the Target of (1Cat (F,G)), the Target of C:],K184( the carrier' of (1Cat (F,G)), the carrier' of C, the Comp of (1Cat (F,G)), the Comp of C) #) is strict CatStr

the carrier' of [:(1Cat (F,G)),C:] is non empty set

pr2 ((1Cat (F,G)),C) is Relation-like the carrier' of [:(1Cat (F,G)),C:] -defined the carrier' of C -valued Function-like non empty total V18( the carrier' of [:(1Cat (F,G)),C:], the carrier' of C) Functor of [:(1Cat (F,G)),C:],C

pr2 ( the carrier' of (1Cat (F,G)), the carrier' of C) is Relation-like [: the carrier' of (1Cat (F,G)), the carrier' of C:] -defined the carrier' of C -valued Function-like total V18([: the carrier' of (1Cat (F,G)), the carrier' of C:], the carrier' of C) M2( bool [:[: the carrier' of (1Cat (F,G)), the carrier' of C:], the carrier' of C:])

[:[: the carrier' of (1Cat (F,G)), the carrier' of C:], the carrier' of C:] is set

bool [:[: the carrier' of (1Cat (F,G)), the carrier' of C:], the carrier' of C:] is set

o is Relation-like the carrier' of [:(1Cat (F,G)),C:] -defined the carrier' of C -valued Function-like non empty total V18( the carrier' of [:(1Cat (F,G)),C:], the carrier' of C) Functor of [:(1Cat (F,G)),C:],C

b is set

f2 is set

f1 is set

[f2,f1] is set

{f2,f1} is set

{f2} is set

{{f2,f1},{f2}} is set

c

g is set

h is set

[g,h] is set

{g,h} is set

{g} is set

{{g,h},{g}} is set

o . b is set

o . c

f is M2( the carrier' of (1Cat (F,G)))

t9 is M2( the carrier' of (1Cat (F,G)))

x21 is M2( the carrier' of C)

o . (f,x21) is M2( the carrier' of C)

[f,x21] is set

{f,x21} is set

{f} is set

{{f,x21},{f}} is set

o . [f,x21] is set

x11 is M2( the carrier' of C)

o . (t9,x11) is M2( the carrier' of C)

[t9,x11] is set

{t9,x11} is set

{t9} is set

{{t9,x11},{t9}} is set

o . [t9,x11] is set

rng o is M2( bool the carrier' of C)

bool the carrier' of C is set

C is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

F is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

[:C,F:] is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

the carrier of C is non empty set

the carrier of F is non empty set

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

the carrier' of C is non empty set

the carrier' of F is non empty set

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

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V18( the carrier' of C, the carrier of C) M2( 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 F is Relation-like the carrier' of F -defined the carrier of F -valued Function-like non empty total V18( the carrier' of F, the carrier of F) M2( bool [: the carrier' of F, the carrier of F:])

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

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

[: the Source of C, the Source of F:] is Relation-like [: the carrier' of C, the carrier' of F:] -defined [: the carrier of C, the carrier of F:] -valued Function-like V18([: the carrier' of C, the carrier' of F:],[: the carrier of C, the carrier of F:]) M2( bool [:[: the carrier' of C, the carrier' of F:],[: the carrier of C, the carrier of F:]:])

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

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

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

the Target of F is Relation-like the carrier' of F -defined the carrier of F -valued Function-like non empty total V18( the carrier' of F, the carrier of F) M2( bool [: the carrier' of F, the carrier of F:])

[: the Target of C, the Target of F:] is Relation-like [: the carrier' of C, the carrier' of F:] -defined [: the carrier of C, the carrier of F:] -valued Function-like V18([: the carrier' of C, the carrier' of F:],[: the carrier of C, the carrier of F:]) M2( bool [:[: the carrier' of C, the carrier' of F:],[: the carrier of C, the carrier of F:]:])

the Comp of C is Relation-like [: the carrier' of C, the carrier' of C:] -defined the carrier' of C -valued Function-like M2( 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 Comp of F is Relation-like [: the carrier' of F, the carrier' of F:] -defined the carrier' of F -valued Function-like M2( bool [:[: the carrier' of F, the carrier' of F:], the carrier' of F:])

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

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

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

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

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

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

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

CatStr(# [: the carrier of C, the carrier of F:],[: the carrier' of C, the carrier' of F:],[: the Source of C, the Source of F:],[: the Target of C, the Target of F:],K184( the carrier' of C, the carrier' of F, the Comp of C, the Comp of F) #) is strict CatStr

[:F,C:] is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

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

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

[: the Source of F, the Source of C:] is Relation-like [: the carrier' of F, the carrier' of C:] -defined [: the carrier of F, the carrier of C:] -valued Function-like V18([: the carrier' of F, the carrier' of C:],[: the carrier of F, the carrier of C:]) M2( bool [:[: the carrier' of F, the carrier' of C:],[: the carrier of F, the carrier of C:]:])

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

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

[: the Target of F, the Target of C:] is Relation-like [: the carrier' of F, the carrier' of C:] -defined [: the carrier of F, the carrier of C:] -valued Function-like V18([: the carrier' of F, the carrier' of C:],[: the carrier of F, the carrier of C:]) M2( bool [:[: the carrier' of F, the carrier' of C:],[: the carrier of F, the carrier of C:]:])

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

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

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

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

CatStr(# [: the carrier of F, the carrier of C:],[: the carrier' of F, the carrier' of C:],[: the Source of F, the Source of C:],[: the Target of F, the Target of C:],K184( the carrier' of F, the carrier' of C, the Comp of F, the Comp of C) #) is strict CatStr

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

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

pr2 (C,F) is Relation-like the carrier' of [:C,F:] -defined the carrier' of F -valued Function-like non empty total V18( the carrier' of [:C,F:], the carrier' of F) Functor of [:C,F:],F

pr2 ( the carrier' of C, the carrier' of F) is Relation-like [: the carrier' of C, the carrier' of F:] -defined the carrier' of F -valued Function-like total V18([: the carrier' of C, the carrier' of F:], the carrier' of F) M2( bool [:[: the carrier' of C, the carrier' of F:], the carrier' of F:])

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

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

pr1 (C,F) is Relation-like the carrier' of [:C,F:] -defined the carrier' of C -valued Function-like non empty total V18( the carrier' of [:C,F:], the carrier' of C) Functor of [:C,F:],C

pr1 ( the carrier' of C, the carrier' of F) is Relation-like [: the carrier' of C, the carrier' of F:] -defined the carrier' of C -valued Function-like total V18([: the carrier' of C, the carrier' of F:], the carrier' of C) M2( bool [:[: the carrier' of C, the carrier' of F:], the carrier' of C:])

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

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

<:(pr2 (C,F)),(pr1 (C,F)):> is Relation-like the carrier' of [:C,F:] -defined the carrier' of [:F,C:] -valued Function-like non empty total V18( the carrier' of [:C,F:], the carrier' of [:F,C:]) Functor of [:C,F:],[:F,C:]

G is Relation-like the carrier' of [:C,F:] -defined the carrier' of [:F,C:] -valued Function-like non empty total V18( the carrier' of [:C,F:], the carrier' of [:F,C:]) Functor of [:C,F:],[:F,C:]

dom (pr1 (C,F)) is M2( bool the carrier' of [:C,F:])

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

dom (pr2 (C,F)) is M2( bool the carrier' of [:C,F:])

o is set

b is set

c

[b,c

{b,c

{b} is set

{{b,c

s is set

f2 is set

f1 is set

[f2,f1] is set

{f2,f1} is set

{f2} is set

{{f2,f1},{f2}} is set

t9 is M2( the carrier' of C)

h is M2( the carrier' of F)

[t9,h] is M2( the carrier' of [:C,F:])

{t9,h} is set

{t9} is set

{{t9,h},{t9}} is set

G . o is set

G . s is set

f is M2( the carrier' of C)

g is M2( the carrier' of F)

[f,g] is M2( the carrier' of [:C,F:])

{f,g} is set

{f} is set

{{f,g},{f}} is set

[g,f] is M2( the carrier' of [:F,C:])

{g,f} is set

{g} is set

{{g,f},{g}} is set

(pr1 (C,F)) . (f,g) is M2( the carrier' of C)

[f,g] is set

(pr1 (C,F)) . [f,g] is set

[g,((pr1 (C,F)) . (f,g))] is M2( the carrier' of [:F,C:])

{g,((pr1 (C,F)) . (f,g))} is set

{{g,((pr1 (C,F)) . (f,g))},{g}} is set

(pr2 (C,F)) . (f,g) is M2( the carrier' of F)

(pr2 (C,F)) . [f,g] is set

[((pr2 (C,F)) . (f,g)),((pr1 (C,F)) . (f,g))] is M2( the carrier' of [:F,C:])

{((pr2 (C,F)) . (f,g)),((pr1 (C,F)) . (f,g))} is set

{((pr2 (C,F)) . (f,g))} is set

{{((pr2 (C,F)) . (f,g)),((pr1 (C,F)) . (f,g))},{((pr2 (C,F)) . (f,g))}} is set

G . (t9,h) is M2( the carrier' of [:F,C:])

[t9,h] is set

G . [t9,h] is set

(pr2 (C,F)) . (t9,h) is M2( the carrier' of F)

(pr2 (C,F)) . [t9,h] is set

(pr1 (C,F)) . (t9,h) is M2( the carrier' of C)

(pr1 (C,F)) . [t9,h] is set

[((pr2 (C,F)) . (t9,h)),((pr1 (C,F)) . (t9,h))] is M2( the carrier' of [:F,C:])

{((pr2 (C,F)) . (t9,h)),((pr1 (C,F)) . (t9,h))} is set

{((pr2 (C,F)) . (t9,h))} is set

{{((pr2 (C,F)) . (t9,h)),((pr1 (C,F)) . (t9,h))},{((pr2 (C,F)) . (t9,h))}} is set

[h,((pr1 (C,F)) . (t9,h))] is M2( the carrier' of [:F,C:])

{h,((pr1 (C,F)) . (t9,h))} is set

{h} is set

{{h,((pr1 (C,F)) . (t9,h))},{h}} is set

[h,t9] is M2( the carrier' of [:F,C:])

{h,t9} is set

{{h,t9},{h}} is set

rng G is M2( bool the carrier' of [:F,C:])

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

o is set

s is set

b is set

[s,b] is set

{s,b} is set

{s} is set

{{s,b},{s}} is set

c

f2 is M2( the carrier' of F)

[c

{c

{c

{{c

G . [c

(pr2 (C,F)) . (c

[c

(pr2 (C,F)) . [c

(pr1 (C,F)) . (c

(pr1 (C,F)) . [c

[((pr2 (C,F)) . (c

{((pr2 (C,F)) . (c

{((pr2 (C,F)) . (c

{{((pr2 (C,F)) . (c

[f2,((pr1 (C,F)) . (c

{f2,((pr1 (C,F)) . (c

{f2} is set

{{f2,((pr1 (C,F)) . (c

[f2,c

{f2,c

{{f2,c

C is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

F is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

[:C,F:] is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

the carrier of C is non empty set

the carrier of F is non empty set

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

the carrier' of C is non empty set

the carrier' of F is non empty set

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

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V18( the carrier' of C, the carrier of C) M2( 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 F is Relation-like the carrier' of F -defined the carrier of F -valued Function-like non empty total V18( the carrier' of F, the carrier of F) M2( bool [: the carrier' of F, the carrier of F:])

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

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

[: the Source of C, the Source of F:] is Relation-like [: the carrier' of C, the carrier' of F:] -defined [: the carrier of C, the carrier of F:] -valued Function-like V18([: the carrier' of C, the carrier' of F:],[: the carrier of C, the carrier of F:]) M2( bool [:[: the carrier' of C, the carrier' of F:],[: the carrier of C, the carrier of F:]:])

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

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

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

the Target of F is Relation-like the carrier' of F -defined the carrier of F -valued Function-like non empty total V18( the carrier' of F, the carrier of F) M2( bool [: the carrier' of F, the carrier of F:])

[: the Target of C, the Target of F:] is Relation-like [: the carrier' of C, the carrier' of F:] -defined [: the carrier of C, the carrier of F:] -valued Function-like V18([: the carrier' of C, the carrier' of F:],[: the carrier of C, the carrier of F:]) M2( bool [:[: the carrier' of C, the carrier' of F:],[: the carrier of C, the carrier of F:]:])

the Comp of C is Relation-like [: the carrier' of C, the carrier' of C:] -defined the carrier' of C -valued Function-like M2( 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 Comp of F is Relation-like [: the carrier' of F, the carrier' of F:] -defined the carrier' of F -valued Function-like M2( bool [:[: the carrier' of F, the carrier' of F:], the carrier' of F:])

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

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

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

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

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

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

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

CatStr(# [: the carrier of C, the carrier of F:],[: the carrier' of C, the carrier' of F:],[: the Source of C, the Source of F:],[: the Target of C, the Target of F:],K184( the carrier' of C, the carrier' of F, the Comp of C, the Comp of F) #) is strict CatStr

G is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

[:[:C,F:],G:] is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

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

the carrier of G is non empty set

[: the carrier of [:C,F:], the carrier of G:] is set

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

the carrier' of G is non empty set

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

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

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

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

the Source of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like non empty total V18( the carrier' of G, the carrier of G) M2( bool [: the carrier' of G, the carrier of G:])

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

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

[: the Source of [:C,F:], the Source of G:] is Relation-like [: the carrier' of [:C,F:], the carrier' of G:] -defined [: the carrier of [:C,F:], the carrier of G:] -valued Function-like V18([: the carrier' of [:C,F:], the carrier' of G:],[: the carrier of [:C,F:], the carrier of G:]) M2( bool [:[: the carrier' of [:C,F:], the carrier' of G:],[: the carrier of [:C,F:], the carrier of G:]:])

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

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

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

the Target of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like non empty total V18( the carrier' of G, the carrier of G) M2( bool [: the carrier' of G, the carrier of G:])

[: the Target of [:C,F:], the Target of G:] is Relation-like [: the carrier' of [:C,F:], the carrier' of G:] -defined [: the carrier of [:C,F:], the carrier of G:] -valued Function-like V18([: the carrier' of [:C,F:], the carrier' of G:],[: the carrier of [:C,F:], the carrier of G:]) M2( bool [:[: the carrier' of [:C,F:], the carrier' of G:],[: the carrier of [:C,F:], the carrier of G:]:])

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

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

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

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

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

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

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

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

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

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

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

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

CatStr(# [: the carrier of [:C,F:], the carrier of G:],[: the carrier' of [:C,F:], the carrier' of G:],[: the Source of [:C,F:], the Source of G:],[: the Target of [:C,F:], the Target of G:],K184( the carrier' of [:C,F:], the carrier' of G, the Comp of [:C,F:], the Comp of G) #) is strict CatStr

[:F,G:] is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

[: the carrier of F, the carrier of G:] is set

[: the carrier' of F, the carrier' of G:] is set

[: the Source of F, the Source of G:] is Relation-like [: the carrier' of F, the carrier' of G:] -defined [: the carrier of F, the carrier of G:] -valued Function-like V18([: the carrier' of F, the carrier' of G:],[: the carrier of F, the carrier of G:]) M2( bool [:[: the carrier' of F, the carrier' of G:],[: the carrier of F, the carrier of G:]:])

[:[: the carrier' of F, the carrier' of G:],[: the carrier of F, the carrier of G:]:] is set

bool [:[: the carrier' of F, the carrier' of G:],[: the carrier of F, the carrier of G:]:] is set

[: the Target of F, the Target of G:] is Relation-like [: the carrier' of F, the carrier' of G:] -defined [: the carrier of F, the carrier of G:] -valued Function-like V18([: the carrier' of F, the carrier' of G:],[: the carrier of F, the carrier of G:]) M2( bool [:[: the carrier' of F, the carrier' of G:],[: the carrier of F, the carrier of G:]:])

K184( the carrier' of F, the carrier' of G, the Comp of F, the Comp of G) is Relation-like [:[: the carrier' of F, the carrier' of G:],[: the carrier' of F, the carrier' of G:]:] -defined [: the carrier' of F, the carrier' of G:] -valued Function-like M2( bool [:[:[: the carrier' of F, the carrier' of G:],[: the carrier' of F, the carrier' of G:]:],[: the carrier' of F, the carrier' of G:]:])

[:[: the carrier' of F, the carrier' of G:],[: the carrier' of F, the carrier' of G:]:] is set

[:[:[: the carrier' of F, the carrier' of G:],[: the carrier' of F, the carrier' of G:]:],[: the carrier' of F, the carrier' of G:]:] is set

bool [:[:[: the carrier' of F, the carrier' of G:],[: the carrier' of F, the carrier' of G:]:],[: the carrier' of F, the carrier' of G:]:] is set

CatStr(# [: the carrier of F, the carrier of G:],[: the carrier' of F, the carrier' of G:],[: the Source of F, the Source of G:],[: the Target of F, the Target of G:],K184( the carrier' of F, the carrier' of G, the Comp of F, the Comp of G) #) is strict CatStr

[:C,[:F,G:]:] is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

the carrier of [:F,G:] is non empty set

[: the carrier of C, the carrier of [:F,G:]:] is set

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

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

the Source of [:F,G:] is Relation-like the carrier' of [:F,G:] -defined the carrier of [:F,G:] -valued Function-like non empty total V18( the carrier' of [:F,G:], the carrier of [:F,G:]) M2( bool [: the carrier' of [:F,G:], the carrier of [:F,G:]:])

[: the carrier' of [:F,G:], the carrier of [:F,G:]:] is set

bool [: the carrier' of [:F,G:], the carrier of [:F,G:]:] is set

[: the Source of C, the Source of [:F,G:]:] is Relation-like [: the carrier' of C, the carrier' of [:F,G:]:] -defined [: the carrier of C, the carrier of [:F,G:]:] -valued Function-like V18([: the carrier' of C, the carrier' of [:F,G:]:],[: the carrier of C, the carrier of [:F,G:]:]) M2( bool [:[: the carrier' of C, the carrier' of [:F,G:]:],[: the carrier of C, the carrier of [:F,G:]:]:])

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

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

the Target of [:F,G:] is Relation-like the carrier' of [:F,G:] -defined the carrier of [:F,G:] -valued Function-like non empty total V18( the carrier' of [:F,G:], the carrier of [:F,G:]) M2( bool [: the carrier' of [:F,G:], the carrier of [:F,G:]:])

[: the Target of C, the Target of [:F,G:]:] is Relation-like [: the carrier' of C, the carrier' of [:F,G:]:] -defined [: the carrier of C, the carrier of [:F,G:]:] -valued Function-like V18([: the carrier' of C, the carrier' of [:F,G:]:],[: the carrier of C, the carrier of [:F,G:]:]) M2( bool [:[: the carrier' of C, the carrier' of [:F,G:]:],[: the carrier of C, the carrier of [:F,G:]:]:])

the Comp of [:F,G:] is Relation-like [: the carrier' of [:F,G:], the carrier' of [:F,G:]:] -defined the carrier' of [:F,G:] -valued Function-like M2( bool [:[: the carrier' of [:F,G:], the carrier' of [:F,G:]:], the carrier' of [:F,G:]:])

[: the carrier' of [:F,G:], the carrier' of [:F,G:]:] is set

[:[: the carrier' of [:F,G:], the carrier' of [:F,G:]:], the carrier' of [:F,G:]:] is set

bool [:[: the carrier' of [:F,G:], the carrier' of [:F,G:]:], the carrier' of [:F,G:]:] is set

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