:: ISOCAT_2 semantic presentation

K145() is Element of bool K141()

K141() is set

bool K141() is non empty set

{} is empty Relation-like non-empty empty-yielding set

the empty Relation-like non-empty empty-yielding set is empty Relation-like non-empty empty-yielding set

1 is non empty set

{{},1} is non empty set

K140() is set

bool K140() is non empty set

bool K145() is non empty set

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

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

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

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

A is non empty set

B is non empty set

C is non empty set

Funcs (B,C) is non empty functional FUNCTION_DOMAIN of B,C

[:A,(Funcs (B,C)):] is non empty Relation-like set

bool [:A,(Funcs (B,C)):] is non empty set

c

uncurry c

[:A,B:] is non empty Relation-like set

[:[:A,B:],C:] is non empty Relation-like set

bool [:[:A,B:],C:] is non empty set

rng c

bool (Funcs (B,C)) is non empty set

uncurry c

dom (uncurry c

bool [:A,B:] is non empty set

dom c

bool A is non empty set

[:(dom c

A is non empty set

B is non empty set

C is non empty set

Funcs (B,C) is non empty functional FUNCTION_DOMAIN of B,C

[:A,(Funcs (B,C)):] is non empty Relation-like set

bool [:A,(Funcs (B,C)):] is non empty set

c

(A,B,C,c

[:A,B:] is non empty Relation-like set

[:[:A,B:],C:] is non empty Relation-like set

bool [:[:A,B:],C:] is non empty set

curry (A,B,C,c

rng c

bool (Funcs (B,C)) is non empty set

A is non empty set

B is non empty set

C is non empty set

Funcs (B,C) is non empty functional FUNCTION_DOMAIN of B,C

[:A,(Funcs (B,C)):] is non empty Relation-like set

bool [:A,(Funcs (B,C)):] is non empty set

c

(A,B,C,c

[:A,B:] is non empty Relation-like set

[:[:A,B:],C:] is non empty Relation-like set

bool [:[:A,B:],C:] is non empty set

o1 is Element of A

c

o2 is Element of B

(A,B,C,c

[o1,o2] is set

{o1,o2} is non empty set

{o1} is non empty set

{{o1,o2},{o1}} is non empty set

(A,B,C,c

(c

dom c

bool A is non empty set

dom (c

bool B is non empty set

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

the carrier' of A is non empty set

B is Element of the carrier' of A

cod B is Element of the carrier of A

the carrier of A is non empty set

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

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

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

the Target of A . B is Element of the carrier of A

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

(id (cod B)) (*) B is Element of the carrier' of A

dom B is Element of the carrier of A

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

the Source of A . B is Element of the carrier of A

Hom ((dom B),(cod B)) is Element of bool the carrier' of A

bool the carrier' of A is non empty set

{ b

Hom ((cod B),(cod B)) is non empty Element of bool the carrier' of A

{ b

C is Morphism of dom B, cod B

(id (cod B)) * C is Morphism of dom B, cod B

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

the carrier' of A is non empty set

B is Element of the carrier' of A

dom B is Element of the carrier of A

the carrier of A is non empty set

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

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

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

the Source of A . B is Element of the carrier of A

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

B (*) (id (dom B)) is Element of the carrier' of A

cod B is Element of the carrier of A

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

the Target of A . B is Element of the carrier of A

Hom ((dom B),(cod B)) is Element of bool the carrier' of A

bool the carrier' of A is non empty set

{ b

Hom ((dom B),(dom B)) is non empty Element of bool the carrier' of A

{ b

C is Morphism of dom B, cod B

C * (id (dom B)) is Morphism of dom B, cod B

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

the carrier' of A is non empty set

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

Functors (A,B) is non empty non void V55() strict Category-like V68() V69() V70() with_identities CatStr

the carrier of (Functors (A,B)) is non empty set

the carrier' of B is non empty set

C is set

Funct (A,B) is non empty FUNCTOR-DOMAIN of A,B

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

the carrier' of A is non empty set

the carrier of A is non empty set

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

Functors (A,B) is non empty non void V55() strict Category-like V68() V69() V70() with_identities CatStr

the carrier' of (Functors (A,B)) is non empty set

the carrier' of B is non empty set

C is Element of the carrier' of (Functors (A,B))

dom C is Element of the carrier of (Functors (A,B))

the carrier of (Functors (A,B)) is non empty set

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

[: the carrier' of (Functors (A,B)), the carrier of (Functors (A,B)):] is non empty Relation-like set

bool [: the carrier' of (Functors (A,B)), the carrier of (Functors (A,B)):] is non empty set

the Source of (Functors (A,B)) . C is Element of the carrier of (Functors (A,B))

cod C is Element of the carrier of (Functors (A,B))

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

the Target of (Functors (A,B)) . C is Element of the carrier of (Functors (A,B))

Hom ((dom C),(cod C)) is Element of bool the carrier' of (Functors (A,B))

bool the carrier' of (Functors (A,B)) is non empty set

{ b

c

o1 is non empty Relation-like the carrier' of A -defined the carrier' of B -valued Function-like total quasi_total Functor of A,B

[c

{c

{c

{{c

o2 is non empty Relation-like the carrier of A -defined the carrier' of B -valued Function-like total quasi_total natural_transformation of c

[[c

{[c

{[c

{{[c

NatTrans (A,B) is non empty NatTrans-DOMAIN of A,B

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

the carrier of A is non empty set

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

Functors (A,B) is non empty non void V55() strict Category-like V68() V69() V70() with_identities CatStr

the carrier' of (Functors (A,B)) is non empty set

the carrier' of B is non empty set

the carrier' of A is non empty set

C is Element of the carrier of A

NatTrans (A,B) is non empty NatTrans-DOMAIN of A,B

c

o1 is non empty Relation-like the carrier' of A -defined the carrier' of B -valued Function-like total quasi_total Functor of A,B

o2 is non empty Relation-like the carrier' of A -defined the carrier' of B -valued Function-like total quasi_total Functor of A,B

[o1,o2] is set

{o1,o2} is non empty set

{o1} is non empty set

{{o1,o2},{o1}} is non empty set

G1 is non empty Relation-like the carrier of A -defined the carrier' of B -valued Function-like total quasi_total natural_transformation of o1,o2

[[o1,o2],G1] is set

{[o1,o2],G1} is non empty set

{[o1,o2]} is non empty Relation-like set

{{[o1,o2],G1},{[o1,o2]}} is non empty set

G1 . C is Morphism of o1 . C,o2 . C

o1 . C is Element of the carrier of B

the carrier of B is non empty set

Obj o1 is non empty Relation-like the carrier of A -defined the carrier of B -valued Function-like total quasi_total Element of bool [: the carrier of A, the carrier of B:]

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

bool [: the carrier of A, the carrier of B:] is non empty set

(Obj o1) . C is Element of the carrier of B

o2 . C is Element of the carrier of B

Obj o2 is non empty Relation-like the carrier of A -defined the carrier of B -valued Function-like total quasi_total Element of bool [: the carrier of A, the carrier of B:]

(Obj o2) . C is Element of the carrier of B

G2 is Element of the carrier' of B

t is Element of the carrier' of B

F1 is non empty Relation-like the carrier' of A -defined the carrier' of B -valued Function-like total quasi_total Functor of A,B

F2 is non empty Relation-like the carrier' of A -defined the carrier' of B -valued Function-like total quasi_total Functor of A,B

[F1,F2] is set

{F1,F2} is non empty set

{F1} is non empty set

{{F1,F2},{F1}} is non empty set

s is non empty Relation-like the carrier of A -defined the carrier' of B -valued Function-like total quasi_total natural_transformation of F1,F2

[[F1,F2],s] is set

{[F1,F2],s} is non empty set

{[F1,F2]} is non empty Relation-like set

{{[F1,F2],s},{[F1,F2]}} is non empty set

s . C is Morphism of F1 . C,F2 . C

F1 . C is Element of the carrier of B

Obj F1 is non empty Relation-like the carrier of A -defined the carrier of B -valued Function-like total quasi_total Element of bool [: the carrier of A, the carrier of B:]

(Obj F1) . C is Element of the carrier of B

F2 . C is Element of the carrier of B

Obj F2 is non empty Relation-like the carrier of A -defined the carrier of B -valued Function-like total quasi_total Element of bool [: the carrier of A, the carrier of B:]

(Obj F2) . C is Element of the carrier of B

[:(NatTrans (A,B)), the carrier' of B:] is non empty Relation-like set

bool [:(NatTrans (A,B)), the carrier' of B:] is non empty set

c

[: the carrier' of (Functors (A,B)), the carrier' of B:] is non empty Relation-like set

bool [: the carrier' of (Functors (A,B)), the carrier' of B:] is non empty set

the carrier of (Functors (A,B)) is non empty set

o2 is Element of the carrier of (Functors (A,B))

G1 is non empty Relation-like the carrier' of A -defined the carrier' of B -valued Function-like total quasi_total Functor of A,B

G1 . C is Element of the carrier of B

Obj G1 is non empty Relation-like the carrier of A -defined the carrier of B -valued Function-like total quasi_total Element of bool [: the carrier of A, the carrier of B:]

(Obj G1) . C is Element of the carrier of B

[G1,G1] is set

{G1,G1} is non empty set

{G1} is non empty set

{{G1,G1},{G1}} is non empty set

id G1 is non empty Relation-like the carrier of A -defined the carrier' of B -valued Function-like total quasi_total natural_transformation of G1,G1

[[G1,G1],(id G1)] is set

{[G1,G1],(id G1)} is non empty set

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

{{[G1,G1],(id G1)},{[G1,G1]}} is non empty set

id o2 is Morphism of o2,o2

c

c

(id G1) . C is Morphism of G1 . C,G1 . C

G2 is Element of the carrier of B

id G2 is Morphism of G2,G2

G1 is Element of the carrier' of (Functors (A,B))

o2 is Element of the carrier' of (Functors (A,B))

[G1,o2] is Element of the carrier' of [:(Functors (A,B)),(Functors (A,B)):]

[:(Functors (A,B)),(Functors (A,B)):] is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr

[: the carrier of (Functors (A,B)), the carrier of (Functors (A,B)):] is non empty Relation-like set

[: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):] is non empty Relation-like set

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

[: the carrier' of (Functors (A,B)), the carrier of (Functors (A,B)):] is non empty Relation-like set

bool [: the carrier' of (Functors (A,B)), the carrier of (Functors (A,B)):] is non empty set

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

[:[: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):],[: the carrier of (Functors (A,B)), the carrier of (Functors (A,B)):]:] is non empty Relation-like set

bool [:[: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):],[: the carrier of (Functors (A,B)), the carrier of (Functors (A,B)):]:] is non empty set

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

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

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

[:[: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):], the carrier' of (Functors (A,B)):] is non empty Relation-like set

bool [:[: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):], the carrier' of (Functors (A,B)):] is non empty set

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

[:[: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):],[: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):]:] is non empty Relation-like set

[:[:[: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):],[: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):]:],[: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):]:] is non empty Relation-like set

bool [:[:[: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):],[: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):]:],[: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):]:] is non empty set

CatStr(# [: the carrier of (Functors (A,B)), the carrier of (Functors (A,B)):],[: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):],[: the Source of (Functors (A,B)), the Source of (Functors (A,B)):],[: the Target of (Functors (A,B)), the Target of (Functors (A,B)):],K209( the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)), the Comp of (Functors (A,B)), the Comp of (Functors (A,B))) #) is strict CatStr

the carrier' of [:(Functors (A,B)),(Functors (A,B)):] is non empty set

{G1,o2} is non empty set

{G1} is non empty set

{{G1,o2},{G1}} is non empty set

dom the Comp of (Functors (A,B)) is Relation-like the carrier' of (Functors (A,B)) -defined the carrier' of (Functors (A,B)) -valued Element of bool [: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):]

bool [: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):] is non empty set

dom o2 is Element of the carrier of (Functors (A,B))

the Source of (Functors (A,B)) . o2 is Element of the carrier of (Functors (A,B))

cod o2 is Element of the carrier of (Functors (A,B))

the Target of (Functors (A,B)) . o2 is Element of the carrier of (Functors (A,B))

F1 is non empty Relation-like the carrier' of A -defined the carrier' of B -valued Function-like total quasi_total Functor of A,B

F2 is non empty Relation-like the carrier' of A -defined the carrier' of B -valued Function-like total quasi_total Functor of A,B

[F1,F2] is set

{F1,F2} is non empty set

{F1} is non empty set

{{F1,F2},{F1}} is non empty set

s is non empty Relation-like the carrier of A -defined the carrier' of B -valued Function-like total quasi_total natural_transformation of F1,F2

[[F1,F2],s] is set

{[F1,F2],s} is non empty set

{[F1,F2]} is non empty Relation-like set

{{[F1,F2],s},{[F1,F2]}} is non empty set

F1 . C is Element of the carrier of B

Obj F1 is non empty Relation-like the carrier of A -defined the carrier of B -valued Function-like total quasi_total Element of bool [: the carrier of A, the carrier of B:]

(Obj F1) . C is Element of the carrier of B

F2 . C is Element of the carrier of B

Obj F2 is non empty Relation-like the carrier of A -defined the carrier of B -valued Function-like total quasi_total Element of bool [: the carrier of A, the carrier of B:]

(Obj F2) . C is Element of the carrier of B

Hom ((F1 . C),(F2 . C)) is Element of bool the carrier' of B

bool the carrier' of B is non empty set

{ b

G2 is Element of NatTrans (A,B)

c

s . C is Morphism of F1 . C,F2 . C

dom G1 is Element of the carrier of (Functors (A,B))

the Source of (Functors (A,B)) . G1 is Element of the carrier of (Functors (A,B))

cod G1 is Element of the carrier of (Functors (A,B))

the Target of (Functors (A,B)) . G1 is Element of the carrier of (Functors (A,B))

f is non empty Relation-like the carrier' of A -defined the carrier' of B -valued Function-like total quasi_total Functor of A,B

f is non empty Relation-like the carrier' of A -defined the carrier' of B -valued Function-like total quasi_total Functor of A,B

[f,f] is set

{f,f} is non empty set

{f} is non empty set

{{f,f},{f}} is non empty set

f2 is non empty Relation-like the carrier of A -defined the carrier' of B -valued Function-like total quasi_total natural_transformation of f,f

[[f,f],f2] is set

{[f,f],f2} is non empty set

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

{{[f,f],f2},{[f,f]}} is non empty set

f . C is Element of the carrier of B

Obj f is non empty Relation-like the carrier of A -defined the carrier of B -valued Function-like total quasi_total Element of bool [: the carrier of A, the carrier of B:]

(Obj f) . C is Element of the carrier of B

Hom ((F2 . C),(f . C)) is Element of bool the carrier' of B

{ b

t is Element of NatTrans (A,B)

c

g1 is non empty Relation-like the carrier of A -defined the carrier' of B -valued Function-like total quasi_total natural_transformation of F2,f

g1 . C is Morphism of F2 . C,f . C

G1 (*) o2 is Element of the carrier' of (Functors (A,B))

[F1,f] is set

{F1,f} is non empty set

{{F1,f},{F1}} is non empty set

g1 `*` s is non empty Relation-like the carrier of A -defined the carrier' of B -valued Function-like total quasi_total natural_transformation of F1,f

[[F1,f],(g1 `*` s)] is set

{[F1,f],(g1 `*` s)} is non empty set

{[F1,f]} is non empty Relation-like set

{{[F1,f],(g1 `*` s)},{[F1,f]}} is non empty set

o1 is non empty Relation-like the carrier' of (Functors (A,B)) -defined the carrier' of B -valued Function-like total quasi_total Element of bool [: the carrier' of (Functors (A,B)), the carrier' of B:]

o1 . (G1 (*) o2) is Element of the carrier' of B

(g1 `*` s) . C is Morphism of F1 . C,f . C

(g1 . C) * (s . C) is Morphism of F1 . C,f . C

(g1 . C) (*) (s . C) is Element of the carrier' of B

o1 . o2 is Element of the carrier' of B

o1 . G1 is Element of the carrier' of B

(o1 . G1) (*) (o1 . o2) is Element of the carrier' of B

o2 is Element of the carrier' of (Functors (A,B))

dom o2 is Element of the carrier of (Functors (A,B))

the Source of (Functors (A,B)) . o2 is Element of the carrier of (Functors (A,B))

cod o2 is Element of the carrier of (Functors (A,B))

the Target of (Functors (A,B)) . o2 is Element of the carrier of (Functors (A,B))

G2 is non empty Relation-like the carrier' of A -defined the carrier' of B -valued Function-like total quasi_total Functor of A,B

t is non empty Relation-like the carrier' of A -defined the carrier' of B -valued Function-like total quasi_total Functor of A,B

[G2,t] is set

{G2,t} is non empty set

{G2} is non empty set

{{G2,t},{G2}} is non empty set

F1 is non empty Relation-like the carrier of A -defined the carrier' of B -valued Function-like total quasi_total natural_transformation of G2,t

[[G2,t],F1] is set

{[G2,t],F1} is non empty set

{[G2,t]} is non empty Relation-like set

{{[G2,t],F1},{[G2,t]}} is non empty set

G2 . C is Element of the carrier of B

Obj G2 is non empty Relation-like the carrier of A -defined the carrier of B -valued Function-like total quasi_total Element of bool [: the carrier of A, the carrier of B:]

(Obj G2) . C is Element of the carrier of B

t . C is Element of the carrier of B

Obj t is non empty Relation-like the carrier of A -defined the carrier of B -valued Function-like total quasi_total Element of bool [: the carrier of A, the carrier of B:]

(Obj t) . C is Element of the carrier of B

Hom ((G2 . C),(t . C)) is Element of bool the carrier' of B

{ b

[G2,G2] is set

{G2,G2} is non empty set

{{G2,G2},{G2}} is non empty set

id G2 is non empty Relation-like the carrier of A -defined the carrier' of B -valued Function-like total quasi_total natural_transformation of G2,G2

[[G2,G2],(id G2)] is set

{[G2,G2],(id G2)} is non empty set

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

{{[G2,G2],(id G2)},{[G2,G2]}} is non empty set

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

c

c

(id G2) . C is Morphism of G2 . C,G2 . C

id (G2 . C) is Morphism of G2 . C,G2 . C

F1 . C is Morphism of G2 . C,t . C

dom (F1 . C) is Element of the carrier of B

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

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

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

the Source of B . (F1 . C) is Element of the carrier of B

id (dom (F1 . C)) is Morphism of dom (F1 . C), dom (F1 . C)

G1 is Element of NatTrans (A,B)

c

dom (c

the Source of B . (c

id (dom (c

o1 . o2 is Element of the carrier' of B

dom (o1 . o2) is Element of the carrier of B

the Source of B . (o1 . o2) is Element of the carrier of B

id (dom (o1 . o2)) is Morphism of dom (o1 . o2), dom (o1 . o2)

[t,t] is set

{t,t} is non empty set

{t} is non empty set

{{t,t},{t}} is non empty set

id t is non empty Relation-like the carrier of A -defined the carrier' of B -valued Function-like total quasi_total natural_transformation of t,t

[[t,t],(id t)] is set

{[t,t],(id t)} is non empty set

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

{{[t,t],(id t)},{[t,t]}} is non empty set

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

c

c

(id t) . C is Morphism of t . C,t . C

id (t . C) is Morphism of t . C,t . C

cod (F1 . C) is Element of the carrier of B

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

the Target of B . (F1 . C) is Element of the carrier of B

id (cod (F1 . C)) is Morphism of cod (F1 . C), cod (F1 . C)

cod (c

the Target of B . (c

id (cod (c

cod (o1 . o2) is Element of the carrier of B

the Target of B . (o1 . o2) is Element of the carrier of B

id (cod (o1 . o2)) is Morphism of cod (o1 . o2), cod (o1 . o2)

o2 is non empty Relation-like the carrier' of (Functors (A,B)) -defined the carrier' of B -valued Function-like total quasi_total Functor of Functors (A,B),B

G1 is non empty Relation-like the carrier' of A -defined the carrier' of B -valued Function-like total quasi_total Functor of A,B

G2 is non empty Relation-like the carrier' of A -defined the carrier' of B -valued Function-like total quasi_total Functor of A,B

[G1,G2] is set

{G1,G2} is non empty set

{G1} is non empty set

{{G1,G2},{G1}} is non empty set

t is non empty Relation-like the carrier of A -defined the carrier' of B -valued Function-like total quasi_total natural_transformation of G1,G2

[[G1,G2],t] is set

{[G1,G2],t} is non empty set

{[G1,G2]} is non empty Relation-like set

{{[G1,G2],t},{[G1,G2]}} is non empty set

o2 . [[G1,G2],t] is set

t . C is Morphism of G1 . C,G2 . C

G1 . C is Element of the carrier of B

Obj G1 is non empty Relation-like the carrier of A -defined the carrier of B -valued Function-like total quasi_total Element of bool [: the carrier of A, the carrier of B:]

(Obj G1) . C is Element of the carrier of B

G2 . C is Element of the carrier of B

Obj G2 is non empty Relation-like the carrier of A -defined the carrier of B -valued Function-like total quasi_total Element of bool [: the carrier of A, the carrier of B:]

(Obj G2) . C is Element of the carrier of B

c

o1 is non empty Relation-like the carrier' of (Functors (A,B)) -defined the carrier' of B -valued Function-like total quasi_total Functor of Functors (A,B),B

NatTrans (A,B) is non empty NatTrans-DOMAIN of A,B

o2 is Element of the carrier' of (Functors (A,B))

G1 is non empty Relation-like the carrier' of A -defined the carrier' of B -valued Function-like total quasi_total Functor of A,B

G2 is non empty Relation-like the carrier' of A -defined the carrier' of B -valued Function-like total quasi_total Functor of A,B

[G1,G2] is set

{G1,G2} is non empty set

{G1} is non empty set

{{G1,G2},{G1}} is non empty set

t is non empty Relation-like the carrier of A -defined the carrier' of B -valued Function-like total quasi_total natural_transformation of G1,G2

[[G1,G2],t] is set

{[G1,G2],t} is non empty set

{[G1,G2]} is non empty Relation-like set

{{[G1,G2],t},{[G1,G2]}} is non empty set

c

t . C is Morphism of G1 . C,G2 . C

G1 . C is Element of the carrier of B

the carrier of B is non empty set

Obj G1 is non empty Relation-like the carrier of A -defined the carrier of B -valued Function-like total quasi_total Element of bool [: the carrier of A, the carrier of B:]

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

bool [: the carrier of A, the carrier of B:] is non empty set

(Obj G1) . C is Element of the carrier of B

G2 . C is Element of the carrier of B

Obj G2 is non empty Relation-like the carrier of A -defined the carrier of B -valued Function-like total quasi_total Element of bool [: the carrier of A, the carrier of B:]

(Obj G2) . C is Element of the carrier of B

o1 . o2 is Element of the carrier' of B

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

B is set

C is set

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

{B} is non empty set

{C} is non empty set

C :-> B is non empty Relation-like {C} -defined {B} -valued Function-like total quasi_total Element of bool [:{C},{B}:]

[:{C},{B}:] is non empty Relation-like set

bool [:{C},{B}:] is non empty set

(C,C) :-> C is non empty Relation-like [:{C},{C}:] -defined {C} -valued Function-like total quasi_total Element of bool [:[:{C},{C}:],{C}:]

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

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

bool [:[:{C},{C}:],{C}:] is non empty set

CatStr(# {B},{C},(C :-> B),(C :-> B),((C,C) :-> C) #) is strict CatStr

Functors ((1Cat (B,C)),A) is non empty non void V55() strict Category-like V68() V69() V70() with_identities CatStr

the carrier of (1Cat (B,C)) is non empty trivial V31() set

the carrier' of (Functors ((1Cat (B,C)),A)) is non empty set

the carrier' of A is non empty set

c

((1Cat (B,C)),A,c

o1 is non empty Relation-like the carrier' of (Functors ((1Cat (B,C)),A)) -defined the carrier' of A -valued Function-like total quasi_total Functor of Functors ((1Cat (B,C)),A),A

NatTrans ((1Cat (B,C)),A) is non empty NatTrans-DOMAIN of 1Cat (B,C),A

o2 is set

the carrier' of (1Cat (B,C)) is non empty trivial set

G2 is non empty Relation-like the carrier' of (1Cat (B,C)) -defined the carrier' of A -valued Function-like total quasi_total Functor of 1Cat (B,C),A

t is non empty Relation-like the carrier' of (1Cat (B,C)) -defined the carrier' of A -valued Function-like total quasi_total Functor of 1Cat (B,C),A

[G2,t] is set

{G2,t} is non empty set

{G2} is non empty set

{{G2,t},{G2}} is non empty set

F1 is non empty Relation-like the carrier of (1Cat (B,C)) -defined the carrier' of A -valued Function-like total quasi_total natural_transformation of G2,t

[[G2,t],F1] is set

{[G2,t],F1} is non empty set

{[G2,t]} is non empty Relation-like set

{{[G2,t],F1},{[G2,t]}} is non empty set

G1 is set

F2 is non empty Relation-like the carrier' of (1Cat (B,C)) -defined the carrier' of A -valued Function-like total quasi_total Functor of 1Cat (B,C),A

s is non empty Relation-like the carrier' of (1Cat (B,C)) -defined the carrier' of A -valued Function-like total quasi_total Functor of 1Cat (B,C),A

[F2,s] is set

{F2,s} is non empty set

{F2} is non empty set

{{F2,s},{F2}} is non empty set

f is non empty Relation-like the carrier of (1Cat (B,C)) -defined the carrier' of A -valued Function-like total quasi_total natural_transformation of F2,s

[[F2,s],f] is set

{[F2,s],f} is non empty set

{[F2,s]} is non empty Relation-like set

{{[F2,s],f},{[F2,s]}} is non empty set

o1 . o2 is set

o1 . G1 is set

F1 . c

G2 . c

the carrier of A is non empty set

Obj G2 is non empty Relation-like the carrier of (1Cat (B,C)) -defined the carrier of A -valued Function-like total quasi_total Element of bool [: the carrier of (1Cat (B,C)), the carrier of A:]

[: the carrier of (1Cat (B,C)), the carrier of A:] is non empty Relation-like set

bool [: the carrier of (1Cat (B,C)), the carrier of A:] is non empty set

(Obj G2) . c

t . c

Obj t is non empty Relation-like the carrier of (1Cat (B,C)) -defined the carrier of A -valued Function-like total quasi_total Element of bool [: the carrier of (1Cat (B,C)), the carrier of A:]

(Obj t) . c

f . c

F2 . c

Obj F2 is non empty Relation-like the carrier of (1Cat (B,C)) -defined the carrier of A -valued Function-like total quasi_total Element of bool [: the carrier of (1Cat (B,C)), the carrier of A:]

(Obj F2) . c

s . c

Obj s is non empty Relation-like the carrier of (1Cat (B,C)) -defined the carrier of A -valued Function-like total quasi_total Element of bool [: the carrier of (1Cat (B,C)), the carrier of A:]

(Obj s) . c

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

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

{c

[:{c

bool [:{c

id c

Hom ((G2 . c

bool the carrier' of A is non empty set

{ b

Hom ((F2 . c

{ b

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

f . (id c

id (F2 . c

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

f2 . (id c

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

g1 . (id c

id (s . c

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

f1 . (id c

t2 is non empty Relation-like {c

t2 . c

a1 is non empty Relation-like {c

a1 . c

rng o1 is non empty Element of bool the carrier' of A

o2 is set

[: the carrier' of (1Cat (B,C)), the carrier' of A:] is non empty Relation-like set

bool [: the carrier' of (1Cat (B,C)), the carrier' of A:] is non empty set

G1 is Element of the carrier' of A

dom G1 is Element of the carrier of A

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

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

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

the Source of A . G1 is Element of the carrier of A

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

{C} --> (id (dom G1)) is non empty Relation-like {C} -defined the carrier' of A -valued Function-like total quasi_total Element of bool [:{C}, the carrier' of A:]

cod G1 is Element of the carrier of A

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

the Target of A . G1 is Element of the carrier of A

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

{C} --> (id (cod G1)) is non empty Relation-like {C} -defined the carrier' of A -valued Function-like total quasi_total Element of bool [:{C}, the carrier' of A:]

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

F1 is Element of the carrier' of (1Cat (B,C))

dom F1 is Element of the carrier of (1Cat (B,C))

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

[: the carrier' of (1Cat (B,C)), the carrier of (1Cat (B,C)):] is non empty Relation-like set

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

the Source of (1Cat (B,C)) . F1 is Element of the carrier of (1Cat (B,C))

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

G2 . (id (dom F1)) is Element of the carrier' of A

dom (id (dom G1)) is Element of the carrier of A

the Source of A . (id (dom G1)) is Element of the carrier of A

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

G2 . F1 is Element of the carrier' of A

dom (G2 . F1) is Element of the carrier of A

the Source of A . (G2 . F1) is Element of the carrier of A

id (dom (G2 . F1)) is Morphism of dom (G2 . F1), dom (G2 . F1)

cod F1 is Element of the carrier of (1Cat (B,C))

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

the Target of (1Cat (B,C)) . F1 is Element of the carrier of (1Cat (B,C))

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

G2 . (id (cod F1)) is Element of the carrier' of A

cod (id (dom G1)) is Element of the carrier of A

the Target of A . (id (dom G1)) is Element of the carrier of A

id (cod (id (dom G1))) is Morphism of cod (id (dom G1)), cod (id (dom G1))

cod (G2 . F1) is Element of the carrier of A

the Target of A . (G2 . F1) is Element of the carrier of A

id (cod (G2 . F1)) is Morphism of cod (G2 . F1), cod (G2 . F1)

F2 is Element of the carrier' of (1Cat (B,C))

dom F2 is Element of the carrier of (1Cat (B,C))

the Source of (1Cat (B,C)) . F2 is Element of the carrier of (1Cat (B,C))

F1 is Element of the carrier' of (1Cat (B,C))

cod F1 is Element of the carrier of (1Cat (B,C))

the Target of (1Cat (B,C)) . F1 is Element of the carrier of (1Cat (B,C))

Hom ((dom G1),(dom G1)) is non empty Element of bool the carrier' of A

{ b

F2 (*) F1 is Element of the carrier' of (1Cat (B,C))

G2 . (F2 (*) F1) is Element of the carrier' of A

(id (dom G1)) * (id (dom G1)) is Morphism of dom G1, dom G1

(id (dom G1)) (*) (id (dom G1)) is Element of the carrier' of A

G2 . F1 is Element of the carrier' of A

(id (dom G1)) (*) (G2 . F1) is Element of the carrier' of A

G2 . F2 is Element of the carrier' of A

(G2 . F2) (*) (G2 . F1) is Element of the carrier' of A

F2 is Element of the carrier' of (1Cat (B,C))

dom F2 is Element of the carrier of (1Cat (B,C))

the Source of (1Cat (B,C)) . F2 is Element of the carrier of (1Cat (B,C))

F1 is Element of the carrier' of (1Cat (B,C))

cod F1 is Element of the carrier of (1Cat (B,C))

the Target of (1Cat (B,C)) . F1 is Element of the carrier of (1Cat (B,C))

Hom ((cod G1),(cod G1)) is non empty Element of bool the carrier' of A

{ b

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

F2 (*) F1 is Element of the carrier' of (1Cat (B,C))

t . (F2 (*) F1) is Element of the carrier' of A

(id (cod G1)) * (id (cod G1)) is Morphism of cod G1, cod G1

(id (cod G1)) (*) (id (cod G1)) is Element of the carrier' of A

t . F1 is Element of the carrier' of A

(id (cod G1)) (*) (t . F1) is Element of the carrier' of A

t . F2 is Element of the carrier' of A

(t . F2) (*) (t . F1) is Element of the carrier' of A

F1 is Element of the carrier' of (1Cat (B,C))

dom F1 is Element of the carrier of (1Cat (B,C))

the Source of (1Cat (B,C)) . F1 is Element of the carrier of (1Cat (B,C))

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

t . (id (dom F1)) is Element of the carrier' of A

dom (id (cod G1)) is Element of the carrier of A

the Source of A . (id (cod G1)) is Element of the carrier of A

id (dom (id (cod G1))) is Morphism of dom (id (cod G1)), dom (id (cod G1))

t . F1 is Element of the carrier' of A

dom (t . F1) is Element of the carrier of A

the Source of A . (t . F1) is Element of the carrier of A

id (dom (t . F1)) is Morphism of dom (t . F1), dom (t . F1)

cod F1 is Element of the carrier of (1Cat (B,C))

the Target of (1Cat (B,C)) . F1 is Element of the carrier of (1Cat (B,C))

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

t . (id (cod F1)) is Element of the carrier' of A

cod (id (cod G1)) is Element of the carrier of A

the Target of A . (id (cod G1)) is Element of the carrier of A

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

cod (t . F1) is Element of the carrier of A

the Target of A . (t . F1) is Element of the carrier of A

id (cod (t . F1)) is Morphism of cod (t . F1), cod (t . F1)

F1 is Element of the carrier of (1Cat (B,C))

id F1 is Morphism of F1,F1

G2 . (id F1) is Element of the carrier' of A

F2 is Element of the carrier of (1Cat (B,C))

id F2 is Morphism of F2,F2

t . (id F2) is Element of the carrier' of A

[: the carrier of (1Cat (B,C)), the carrier' of A:] is non empty Relation-like set

bool [: the carrier of (1Cat (B,C)), the carrier' of A:] is non empty set

{c

F1 is non empty Relation-like the carrier' of (1Cat (B,C)) -defined the carrier' of A -valued Function-like total quasi_total Functor of 1Cat (B,C),A

F2 is non empty Relation-like the carrier' of (1Cat (B,C)) -defined the carrier' of A -valued Function-like total quasi_total Functor of 1Cat (B,C),A

f is Element of the carrier of (1Cat (B,C))

F1 . f is Element of the carrier of A

Obj F1 is non empty Relation-like the carrier of (1Cat (B,C)) -defined the carrier of A -valued Function-like total quasi_total Element of bool [: the carrier of (1Cat (B,C)), the carrier of A:]

(Obj F1) . f is Element of the carrier of A

F2 . f is Element of the carrier of A

Obj F2 is non empty Relation-like the carrier of (1Cat (B,C)) -defined the carrier of A -valued Function-like total quasi_total Element of bool [: the carrier of (1Cat (B,C)), the carrier of A:]

(Obj F2) . f is Element of the carrier of A

id f is Morphism of f,f

F2 . (id f) is Element of the carrier' of A

id (F2 . f) is Morphism of F2 . f,F2 . f

F1 . (id f) is Element of the carrier' of A

id (F1 . f) is Morphism of F1 . f,F1 . f

f is Element of the carrier of (1Cat (B,C))

F2 . f is Element of the carrier of A

Obj F2 is non empty Relation-like the carrier of (1Cat (B,C)) -defined the carrier of A -valued Function-like total quasi_total Element of bool [: the carrier of (1Cat (B,C)), the carrier of A:]

(Obj F2) . f is Element of the carrier of A

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

s . f is Element of the carrier' of A

F1 . f is Element of the carrier of A

Obj F1 is non empty Relation-like the carrier of (1Cat (B,C)) -defined the carrier of A -valued Function-like total quasi_total Element of bool [: the carrier of (1Cat (B,C)), the carrier of A:]

(Obj F1) . f is Element of the carrier of A

Hom ((F1 . f),(F2 . f)) is Element of bool the carrier' of A

{ b

f is Element of the carrier of (1Cat (B,C))

F1 . f is Element of the carrier of A

(Obj F1) . f is Element of the carrier of A

F2 . f is Element of the carrier of A

(Obj F2) . f is Element of the carrier of A

Hom ((F1 . f),(F2 . f)) is Element of bool the carrier' of A

{ b

f is non empty Relation-like the carrier of (1Cat (B,C)) -defined the carrier' of A -valued Function-like total quasi_total transformation of F1,F2

f is Element of the carrier of (1Cat (B,C))

f . f is Morphism of F1 . f,F2 . f

F1 . f is Element of the carrier of A

(Obj F1) . f is Element of the carrier of A

F2 . f is Element of the carrier of A

(Obj F2) . f is Element of the carrier of A

({c

f is Element of the carrier of (1Cat (B,C))

f2 is Element of the carrier of (1Cat (B,C))

Hom (f,f2) is trivial Element of bool the carrier' of (1Cat (B,C))

bool the carrier' of (1Cat (B,C)) is non empty set

{ b

F2 . f is Element of the carrier of A

(Obj F2) . f is Element of the carrier of A

F2 . f2 is Element of the carrier of A

(Obj F2) . f2 is Element of the carrier of A

Hom ((F2 . f),(F2 . f2)) is Element of bool the carrier' of A

{ b

f . f is Morphism of F1 . f,F2 . f

F1 . f is Element of the carrier of A

(Obj F1) . f is Element of the carrier of A

Hom ((F1 . f),(F2 . f)) is Element of bool the carrier' of A

{ b

F1 . f2 is Element of the carrier of A

(Obj F1) . f2 is Element of the carrier of A

Hom ((F1 . f),(F1 . f2)) is Element of bool the carrier' of A

{ b

g1 is Morphism of f,f2

F2 /. g1 is Morphism of F2 . f,F2 . f2

F2 . C is set

F1 /. g1 is Morphism of F1 . f,F1 . f2

F1 . C is set

f . f2 is Morphism of F1 . f2,F2 . f2

Hom ((F1 . f2),(F2 . f2)) is Element of bool the carrier' of A

{ b

(f . f2) * (F1 /. g1) is Morphism of F1 . f,F2 . f2

G1 (*) (F1 /. g1) is Element of the carrier' of A

(F2 /. g1) (*) G1 is Element of the carrier' of A

(F2 /. g1) * (f . f) is Morphism of F1 . f,F2 . f2

[F1,F2] is set

{F1,F2} is non empty set

{F1} is non empty set

{{F1,F2},{F1}} is non empty set

f is non empty Relation-like the carrier of (1Cat (B,C)) -defined the carrier' of A -valued Function-like total quasi_total natural_transformation of F1,F2

[[F1,F2],f] is set

{[F1,F2],f} is non empty set

{[F1,F2]} is non empty Relation-like set

{{[F1,F2],f},{[F1,F2]}} is non empty set

o1 . [[F1,F2],f] is set

f . c

F1 . c

(Obj F1) . c

F2 . c

(Obj F2) . c

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

the carrier of A is non empty set

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

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

the carrier of B is non empty set

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

the carrier' of A is non empty set

the carrier' of B is non empty set

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

CatStr(# [: the carrier of A, the carrier of B:],[: the carrier' of A, the carrier' of B:],[: the Source of A, the Source of B:],[: the Target of A, the Target of B:],K209( the carrier' of A, the carrier' of B, the Comp of A, the Comp of B) #) is strict CatStr

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

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

the carrier' of C is non empty set

c

o1 is Element of the carrier of A

c

curry c

id o1 is Morphism of o1,o1

(curry c

o2 is Element of the carrier of B

(c

the carrier of C is non empty set

Obj (c

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

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

(Obj (c

[o1,o2] is Element of the carrier of [:A,B:]

the carrier of [:A,B:] is non empty set

{o1,o2} is non empty set

{o1} is non empty set

{{o1,o2},{o1}} is non empty set

c

Obj c

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

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

(Obj c

(Obj c

[o1,o2] is set

(Obj c

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

the carrier of A is non empty set

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

the carrier of B is non empty set

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

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

the carrier' of A is non empty set

the carrier' of B is non empty set

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

CatStr(# [: the carrier of A, the carrier of B:],[: the carrier' of A, the carrier' of B:],[: the Source of A, the Source of B:],[: the Target of A, the Target of B:],K209( the carrier' of A, the carrier' of B, the Comp of A, the Comp of B) #) is strict CatStr

C is Element of the carrier of A

c

Hom (C,c

bool the carrier' of A is non empty set

{ b

o1 is Element of the carrier of B

o2 is Element of the carrier of B

Hom (o1,o2) is Element of bool the carrier' of B

bool the carrier' of B is non empty set

{ b

[C,o1] is Element of the carrier of [:A,B:]

the carrier of [:A,B:] is non empty set

{C,o1} is non empty set

{C} is non empty set

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

[c

{c

{c

{{c

Hom ([C,o1],[c

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

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

{ b

[:(Hom (C,c

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

the carrier of A is non empty set

the carrier' of A is non empty set

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

the carrier of B is non empty set

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

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

the carrier' of B is non empty set

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

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

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

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

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

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

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

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

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

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

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

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

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

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