:: YONEDA_1 semantic presentation

K145() is Element of K32(K141())

K141() is set

K32(K141()) is set

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

1 is non empty set

{{},1} is non empty set

K140() is set

K32(K140()) is set

K32(K145()) is set

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

Hom A is non empty set

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

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

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

Hom A is non empty set

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

the carrier' of (A) is non empty set

F is Relation-like Function-like set

c is Relation-like Function-like set

F * c is Relation-like Function-like set

c9 is Element of the carrier' of (A)

cod c9 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 V17( the carrier' of (A)) quasi_total Element of K32(K33( the carrier' of (A), the carrier of (A)))

K33( the carrier' of (A), the carrier of (A)) is Relation-like set

K32(K33( the carrier' of (A), the carrier of (A))) is set

the Target of (A) . c9 is Element of the carrier of (A)

g is Element of the carrier' of (A)

dom g 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 V17( the carrier' of (A)) quasi_total Element of K32(K33( the carrier' of (A), the carrier of (A)))

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

dom c9 is Element of the carrier of (A)

the Source of (A) . c9 is Element of the carrier of (A)

[(dom c9),(cod c9)] is V1() Element of the carrier of K210((A),(A))

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

the carrier of K210((A),(A)) is non empty set

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

{(dom c9)} is non empty set

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

[[(dom c9),(cod c9)],F] is V1() set

{[(dom c9),(cod c9)],F} is non empty set

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

{{[(dom c9),(cod c9)],F},{[(dom c9),(cod c9)]}} is non empty set

cod g is Element of the carrier of (A)

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

[(dom g),(cod g)] is V1() Element of the carrier of K210((A),(A))

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

{(dom g)} is non empty set

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

[[(dom g),(cod g)],c] is V1() set

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

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

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

[(dom c9),(cod g)] is V1() Element of the carrier of K210((A),(A))

{(dom c9),(cod g)} is non empty set

{{(dom c9),(cod g)},{(dom c9)}} is non empty set

[[(dom c9),(cod g)],(F * c)] is V1() set

{[(dom c9),(cod g)],(F * c)} is non empty set

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

{{[(dom c9),(cod g)],(F * c)},{[(dom c9),(cod g)]}} is non empty set

g (*) c9 is Element of the carrier' of (A)

Maps (Hom A) is non empty set

fDom (Hom A) is non empty Relation-like Maps (Hom A) -defined Hom A -valued Function-like V17( Maps (Hom A)) quasi_total Element of K32(K33((Maps (Hom A)),(Hom A)))

K33((Maps (Hom A)),(Hom A)) is Relation-like set

K32(K33((Maps (Hom A)),(Hom A))) is set

fCod (Hom A) is non empty Relation-like Maps (Hom A) -defined Hom A -valued Function-like V17( Maps (Hom A)) quasi_total Element of K32(K33((Maps (Hom A)),(Hom A)))

fComp (Hom A) is Relation-like K33((Maps (Hom A)),(Maps (Hom A))) -defined Maps (Hom A) -valued Function-like Element of K32(K33(K33((Maps (Hom A)),(Maps (Hom A))),(Maps (Hom A))))

K33((Maps (Hom A)),(Maps (Hom A))) is Relation-like set

K33(K33((Maps (Hom A)),(Maps (Hom A))),(Maps (Hom A))) is Relation-like set

K32(K33(K33((Maps (Hom A)),(Maps (Hom A))),(Maps (Hom A)))) is set

CatStr(# (Hom A),(Maps (Hom A)),(fDom (Hom A)),(fCod (Hom A)),(fComp (Hom A)) #) is strict CatStr

F1 is Element of Maps (Hom A)

cod F1 is Element of Hom A

c9 `1 is set

(c9 `1) `2 is set

[(dom c9),(cod c9)] `2 is set

[(dom g),(cod g)] `1 is set

g `1 is set

(g `1) `1 is set

F2 is Element of Maps (Hom A)

dom F2 is Element of Hom A

dom F1 is Element of Hom A

[(dom F1),(cod F1)] is V1() set

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

{(dom F1)} is non empty set

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

F1 `2 is Relation-like Function-like set

[[(dom F1),(cod F1)],(F1 `2)] is V1() set

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

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

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

cod F2 is Element of Hom A

[(dom F2),(cod F2)] is V1() set

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

{(dom F2)} is non empty set

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

F2 `2 is Relation-like Function-like set

[[(dom F2),(cod F2)],(F2 `2)] is V1() set

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

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

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

[(dom g),(cod g)] `2 is set

(g `1) `2 is set

(c9 `1) `1 is set

[(dom c9),(cod c9)] `1 is set

[g,c9] is V1() Element of the carrier' of K210((A),(A))

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

{g,c9} is non empty set

{g} is non empty set

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

the Comp of (A) is Relation-like K33( the carrier' of (A), the carrier' of (A)) -defined the carrier' of (A) -valued Function-like Element of K32(K33(K33( the carrier' of (A), the carrier' of (A)), the carrier' of (A)))

K33( the carrier' of (A), the carrier' of (A)) is Relation-like set

K33(K33( the carrier' of (A), the carrier' of (A)), the carrier' of (A)) is Relation-like set

K32(K33(K33( the carrier' of (A), the carrier' of (A)), the carrier' of (A))) is set

proj1 the Comp of (A) is Relation-like set

(fComp (Hom A)) . (F2,F1) is set

[F2,F1] is V1() set

{F2,F1} is non empty set

{F2} is non empty set

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

(fComp (Hom A)) . [F2,F1] is set

F2 * F1 is Element of Maps (Hom A)

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

the carrier of A is non empty set

F is Element of the carrier of A

hom?- F is non empty Relation-like the carrier' of A -defined Maps (Hom A) -valued Function-like V17( the carrier' of A) quasi_total Element of K32(K33( the carrier' of A,(Maps (Hom A))))

the carrier' of A is non empty set

Hom A is non empty set

Maps (Hom A) is non empty set

K33( the carrier' of A,(Maps (Hom A))) is Relation-like set

K32(K33( the carrier' of A,(Maps (Hom A)))) is set

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

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

the carrier' of (A) 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

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

Hom A is non empty set

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

F is Element of the carrier' of A

cod F 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 V17( the carrier' of A) quasi_total Element of K32(K33( the carrier' of A, the carrier of A))

K33( the carrier' of A, the carrier of A) is Relation-like set

K32(K33( the carrier' of A, the carrier of A)) is set

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

(A,(cod F)) is non empty Relation-like the carrier' of A -defined the carrier' of (A) -valued Function-like V17( the carrier' of A) quasi_total Functor of A,(A)

the carrier' of (A) is non empty set

hom?- (cod F) is non empty Relation-like the carrier' of A -defined Maps (Hom A) -valued Function-like V17( the carrier' of A) quasi_total Element of K32(K33( the carrier' of A,(Maps (Hom A))))

Maps (Hom A) is non empty set

K33( the carrier' of A,(Maps (Hom A))) is Relation-like set

K32(K33( the carrier' of A,(Maps (Hom A)))) is set

dom F 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 V17( the carrier' of A) quasi_total Element of K32(K33( the carrier' of A, the carrier of A))

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

(A,(dom F)) is non empty Relation-like the carrier' of A -defined the carrier' of (A) -valued Function-like V17( the carrier' of A) quasi_total Functor of A,(A)

hom?- (dom F) is non empty Relation-like the carrier' of A -defined Maps (Hom A) -valued Function-like V17( the carrier' of A) quasi_total Element of K32(K33( the carrier' of A,(Maps (Hom A))))

F1 is Element of the carrier of A

Hom ((cod F),F1) is Element of K32( the carrier' of A)

K32( the carrier' of A) is set

{ b

Hom ((dom F),F1) is Element of K32( the carrier' of A)

{ b

[(Hom ((cod F),F1)),(Hom ((dom F),F1))] is V1() set

{(Hom ((cod F),F1)),(Hom ((dom F),F1))} is non empty set

{(Hom ((cod F),F1))} is non empty set

{{(Hom ((cod F),F1)),(Hom ((dom F),F1))},{(Hom ((cod F),F1))}} is non empty set

hom (F,F1) is Relation-like Hom ((cod F),F1) -defined Hom ((dom F),F1) -valued Function-like quasi_total Element of K32(K33((Hom ((cod F),F1)),(Hom ((dom F),F1))))

K33((Hom ((cod F),F1)),(Hom ((dom F),F1))) is Relation-like set

K32(K33((Hom ((cod F),F1)),(Hom ((dom F),F1)))) is set

[[(Hom ((cod F),F1)),(Hom ((dom F),F1))],(hom (F,F1))] is V1() set

{[(Hom ((cod F),F1)),(Hom ((dom F),F1))],(hom (F,F1))} is non empty set

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

{{[(Hom ((cod F),F1)),(Hom ((dom F),F1))],(hom (F,F1))},{[(Hom ((cod F),F1)),(Hom ((dom F),F1))]}} is non empty set

(A,(cod F)) . F1 is Element of the carrier of (A)

the carrier of (A) is non empty set

Obj (A,(cod F)) is non empty Relation-like the carrier of A -defined the carrier of (A) -valued Function-like V17( the carrier of A) quasi_total Element of K32(K33( the carrier of A, the carrier of (A)))

K33( the carrier of A, the carrier of (A)) is Relation-like set

K32(K33( the carrier of A, the carrier of (A))) is set

(Obj (A,(cod F))) . F1 is Element of the carrier of (A)

(A,(dom F)) . F1 is Element of the carrier of (A)

Obj (A,(dom F)) is non empty Relation-like the carrier of A -defined the carrier of (A) -valued Function-like V17( the carrier of A) quasi_total Element of K32(K33( the carrier of A, the carrier of (A)))

(Obj (A,(dom F))) . F1 is Element of the carrier of (A)

Hom (((A,(cod F)) . F1),((A,(dom F)) . F1)) is Element of K32( the carrier' of (A))

K32( the carrier' of (A)) is set

{ b

fDom (Hom A) is non empty Relation-like Maps (Hom A) -defined Hom A -valued Function-like V17( Maps (Hom A)) quasi_total Element of K32(K33((Maps (Hom A)),(Hom A)))

K33((Maps (Hom A)),(Hom A)) is Relation-like set

K32(K33((Maps (Hom A)),(Hom A))) is set

fCod (Hom A) is non empty Relation-like Maps (Hom A) -defined Hom A -valued Function-like V17( Maps (Hom A)) quasi_total Element of K32(K33((Maps (Hom A)),(Hom A)))

fComp (Hom A) is Relation-like K33((Maps (Hom A)),(Maps (Hom A))) -defined Maps (Hom A) -valued Function-like Element of K32(K33(K33((Maps (Hom A)),(Maps (Hom A))),(Maps (Hom A))))

K33((Maps (Hom A)),(Maps (Hom A))) is Relation-like set

K33(K33((Maps (Hom A)),(Maps (Hom A))),(Maps (Hom A))) is Relation-like set

K32(K33(K33((Maps (Hom A)),(Maps (Hom A))),(Maps (Hom A)))) is set

CatStr(# (Hom A),(Maps (Hom A)),(fDom (Hom A)),(fCod (Hom A)),(fComp (Hom A)) #) is strict CatStr

F2 is Element of the carrier' of (A)

cod F2 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 V17( the carrier' of (A)) quasi_total Element of K32(K33( the carrier' of (A), the carrier of (A)))

K33( the carrier' of (A), the carrier of (A)) is Relation-like set

K32(K33( the carrier' of (A), the carrier of (A))) is set

the Target of (A) . F2 is Element of the carrier of (A)

(fCod (Hom A)) . F2 is set

t is Element of Maps (Hom A)

cod t is Element of Hom A

F2 `1 is set

(F2 `1) `2 is set

[(Hom ((cod F),F1)),(Hom ((dom F),F1))] `2 is set

the carrier of (Ens (Hom A)) is non empty set

hom?- ((Hom A),(dom F)) is non empty Relation-like the carrier' of A -defined the carrier' of (Ens (Hom A)) -valued Function-like V17( the carrier' of A) quasi_total Functor of A, Ens (Hom A)

the carrier' of (Ens (Hom A)) is non empty set

Obj (hom?- ((Hom A),(dom F))) is non empty Relation-like the carrier of A -defined the carrier of (Ens (Hom A)) -valued Function-like V17( the carrier of A) quasi_total Element of K32(K33( the carrier of A, the carrier of (Ens (Hom A))))

K33( the carrier of A, the carrier of (Ens (Hom A))) is Relation-like set

K32(K33( the carrier of A, the carrier of (Ens (Hom A)))) is set

(Obj (hom?- ((Hom A),(dom F)))) . F1 is Element of the carrier of (Ens (Hom A))

(hom?- ((Hom A),(dom F))) . F1 is Element of the carrier of (Ens (Hom A))

dom F2 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 V17( the carrier' of (A)) quasi_total Element of K32(K33( the carrier' of (A), the carrier of (A)))

the Source of (A) . F2 is Element of the carrier of (A)

(fDom (Hom A)) . F2 is set

dom t is Element of Hom A

(F2 `1) `1 is set

[(Hom ((cod F),F1)),(Hom ((dom F),F1))] `1 is set

hom?- ((Hom A),(cod F)) is non empty Relation-like the carrier' of A -defined the carrier' of (Ens (Hom A)) -valued Function-like V17( the carrier' of A) quasi_total Functor of A, Ens (Hom A)

Obj (hom?- ((Hom A),(cod F))) is non empty Relation-like the carrier of A -defined the carrier of (Ens (Hom A)) -valued Function-like V17( the carrier of A) quasi_total Element of K32(K33( the carrier of A, the carrier of (Ens (Hom A))))

(Obj (hom?- ((Hom A),(cod F)))) . F1 is Element of the carrier of (Ens (Hom A))

(hom?- ((Hom A),(cod F))) . F1 is Element of the carrier of (Ens (Hom A))

F1 is Element of the carrier of A

Hom ((cod F),F1) is Element of K32( the carrier' of A)

K32( the carrier' of A) is set

{ b

Hom ((dom F),F1) is Element of K32( the carrier' of A)

{ b

[(Hom ((cod F),F1)),(Hom ((dom F),F1))] is V1() set

{(Hom ((cod F),F1)),(Hom ((dom F),F1))} is non empty set

{(Hom ((cod F),F1))} is non empty set

{{(Hom ((cod F),F1)),(Hom ((dom F),F1))},{(Hom ((cod F),F1))}} is non empty set

hom (F,F1) is Relation-like Hom ((cod F),F1) -defined Hom ((dom F),F1) -valued Function-like quasi_total Element of K32(K33((Hom ((cod F),F1)),(Hom ((dom F),F1))))

K33((Hom ((cod F),F1)),(Hom ((dom F),F1))) is Relation-like set

K32(K33((Hom ((cod F),F1)),(Hom ((dom F),F1)))) is set

[[(Hom ((cod F),F1)),(Hom ((dom F),F1))],(hom (F,F1))] is V1() set

{[(Hom ((cod F),F1)),(Hom ((dom F),F1))],(hom (F,F1))} is non empty set

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

{{[(Hom ((cod F),F1)),(Hom ((dom F),F1))],(hom (F,F1))},{[(Hom ((cod F),F1)),(Hom ((dom F),F1))]}} is non empty set

(A,(cod F)) . F1 is Element of the carrier of (A)

the carrier of (A) is non empty set

Obj (A,(cod F)) is non empty Relation-like the carrier of A -defined the carrier of (A) -valued Function-like V17( the carrier of A) quasi_total Element of K32(K33( the carrier of A, the carrier of (A)))

K33( the carrier of A, the carrier of (A)) is Relation-like set

K32(K33( the carrier of A, the carrier of (A))) is set

(Obj (A,(cod F))) . F1 is Element of the carrier of (A)

(A,(dom F)) . F1 is Element of the carrier of (A)

Obj (A,(dom F)) is non empty Relation-like the carrier of A -defined the carrier of (A) -valued Function-like V17( the carrier of A) quasi_total Element of K32(K33( the carrier of A, the carrier of (A)))

(Obj (A,(dom F))) . F1 is Element of the carrier of (A)

Hom (((A,(cod F)) . F1),((A,(dom F)) . F1)) is Element of K32( the carrier' of (A))

K32( the carrier' of (A)) is set

{ b

K33( the carrier of A, the carrier' of (A)) is Relation-like set

K32(K33( the carrier of A, the carrier' of (A))) is set

F1 is non empty Relation-like the carrier of A -defined the carrier' of (A) -valued Function-like V17( the carrier of A) quasi_total Element of K32(K33( the carrier of A, the carrier' of (A)))

F2 is Element of the carrier of A

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

(A,(cod F)) . F2 is Element of the carrier of (A)

the carrier of (A) is non empty set

Obj (A,(cod F)) is non empty Relation-like the carrier of A -defined the carrier of (A) -valued Function-like V17( the carrier of A) quasi_total Element of K32(K33( the carrier of A, the carrier of (A)))

K33( the carrier of A, the carrier of (A)) is Relation-like set

K32(K33( the carrier of A, the carrier of (A))) is set

(Obj (A,(cod F))) . F2 is Element of the carrier of (A)

(A,(dom F)) . F2 is Element of the carrier of (A)

Obj (A,(dom F)) is non empty Relation-like the carrier of A -defined the carrier of (A) -valued Function-like V17( the carrier of A) quasi_total Element of K32(K33( the carrier of A, the carrier of (A)))

(Obj (A,(dom F))) . F2 is Element of the carrier of (A)

Hom ((cod F),F2) is Element of K32( the carrier' of A)

K32( the carrier' of A) is set

{ b

Hom ((dom F),F2) is Element of K32( the carrier' of A)

{ b

[(Hom ((cod F),F2)),(Hom ((dom F),F2))] is V1() set

{(Hom ((cod F),F2)),(Hom ((dom F),F2))} is non empty set

{(Hom ((cod F),F2))} is non empty set

{{(Hom ((cod F),F2)),(Hom ((dom F),F2))},{(Hom ((cod F),F2))}} is non empty set

hom (F,F2) is Relation-like Hom ((cod F),F2) -defined Hom ((dom F),F2) -valued Function-like quasi_total Element of K32(K33((Hom ((cod F),F2)),(Hom ((dom F),F2))))

K33((Hom ((cod F),F2)),(Hom ((dom F),F2))) is Relation-like set

K32(K33((Hom ((cod F),F2)),(Hom ((dom F),F2)))) is set

[[(Hom ((cod F),F2)),(Hom ((dom F),F2))],(hom (F,F2))] is V1() set

{[(Hom ((cod F),F2)),(Hom ((dom F),F2))],(hom (F,F2))} is non empty set

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

{{[(Hom ((cod F),F2)),(Hom ((dom F),F2))],(hom (F,F2))},{[(Hom ((cod F),F2)),(Hom ((dom F),F2))]}} is non empty set

Hom (((A,(cod F)) . F2),((A,(dom F)) . F2)) is Element of K32( the carrier' of (A))

K32( the carrier' of (A)) is set

{ b

F2 is Element of the carrier of A

(A,(cod F)) . F2 is Element of the carrier of (A)

the carrier of (A) is non empty set

Obj (A,(cod F)) is non empty Relation-like the carrier of A -defined the carrier of (A) -valued Function-like V17( the carrier of A) quasi_total Element of K32(K33( the carrier of A, the carrier of (A)))

K33( the carrier of A, the carrier of (A)) is Relation-like set

K32(K33( the carrier of A, the carrier of (A))) is set

(Obj (A,(cod F))) . F2 is Element of the carrier of (A)

(A,(dom F)) . F2 is Element of the carrier of (A)

Obj (A,(dom F)) is non empty Relation-like the carrier of A -defined the carrier of (A) -valued Function-like V17( the carrier of A) quasi_total Element of K32(K33( the carrier of A, the carrier of (A)))

(Obj (A,(dom F))) . F2 is Element of the carrier of (A)

Hom (((A,(cod F)) . F2),((A,(dom F)) . F2)) is Element of K32( the carrier' of (A))

K32( the carrier' of (A)) is set

{ b

F2 is non empty Relation-like the carrier of A -defined the carrier' of (A) -valued Function-like V17( the carrier of A) quasi_total transformation of (A,(cod F)),(A,(dom F))

t is Element of the carrier of A

d1 is Element of the carrier of A

Hom (t,d1) is Element of K32( the carrier' of A)

K32( the carrier' of A) is set

{ b

(A,(cod F)) . t is Element of the carrier of (A)

the carrier of (A) is non empty set

Obj (A,(cod F)) is non empty Relation-like the carrier of A -defined the carrier of (A) -valued Function-like V17( the carrier of A) quasi_total Element of K32(K33( the carrier of A, the carrier of (A)))

K33( the carrier of A, the carrier of (A)) is Relation-like set

K32(K33( the carrier of A, the carrier of (A))) is set

(Obj (A,(cod F))) . t is Element of the carrier of (A)

(A,(cod F)) . d1 is Element of the carrier of (A)

(Obj (A,(cod F))) . d1 is Element of the carrier of (A)

(A,(dom F)) . d1 is Element of the carrier of (A)

Obj (A,(dom F)) is non empty Relation-like the carrier of A -defined the carrier of (A) -valued Function-like V17( the carrier of A) quasi_total Element of K32(K33( the carrier of A, the carrier of (A)))

(Obj (A,(dom F))) . d1 is Element of the carrier of (A)

F2 . d1 is Morphism of (A,(cod F)) . d1,(A,(dom F)) . d1

(A,(dom F)) . t is Element of the carrier of (A)

(Obj (A,(dom F))) . t is Element of the carrier of (A)

F2 . t is Morphism of (A,(cod F)) . t,(A,(dom F)) . t

Hom (((A,(cod F)) . t),((A,(cod F)) . d1)) is Element of K32( the carrier' of (A))

K32( the carrier' of (A)) is set

{ b

d is Morphism of t,d1

(A,(cod F)) /. d is Morphism of (A,(cod F)) . t,(A,(cod F)) . d1

(F2 . d1) * ((A,(cod F)) /. d) is Morphism of (A,(cod F)) . t,(A,(dom F)) . d1

(A,(dom F)) /. d is Morphism of (A,(dom F)) . t,(A,(dom F)) . d1

((A,(dom F)) /. d) * (F2 . t) is Morphism of (A,(cod F)) . t,(A,(dom F)) . d1

dom d is Element of the carrier of A

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

hom ((cod F),d) is Relation-like Hom ((cod F),(dom d)) -defined Hom ((cod F),(cod d)) -valued Function-like quasi_total Element of K32(K33((Hom ((cod F),(dom d))),(Hom ((cod F),(cod d)))))

Hom ((cod F),(dom d)) is Element of K32( the carrier' of A)

{ b

cod d is Element of the carrier of A

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

Hom ((cod F),(cod d)) is Element of K32( the carrier' of A)

{ b

K33((Hom ((cod F),(dom d))),(Hom ((cod F),(cod d)))) is Relation-like set

K32(K33((Hom ((cod F),(dom d))),(Hom ((cod F),(cod d))))) is set

proj2 (hom ((cod F),d)) is set

hom (F,d1) is Relation-like Hom ((cod F),d1) -defined Hom ((dom F),d1) -valued Function-like quasi_total Element of K32(K33((Hom ((cod F),d1)),(Hom ((dom F),d1))))

Hom ((cod F),d1) is Element of K32( the carrier' of A)

{ b

Hom ((dom F),d1) is Element of K32( the carrier' of A)

{ b

K33((Hom ((cod F),d1)),(Hom ((dom F),d1))) is Relation-like set

K32(K33((Hom ((cod F),d1)),(Hom ((dom F),d1)))) is set

proj1 (hom (F,d1)) is set

t is set

hom (F,t) is Relation-like Hom ((cod F),t) -defined Hom ((dom F),t) -valued Function-like quasi_total Element of K32(K33((Hom ((cod F),t)),(Hom ((dom F),t))))

Hom ((cod F),t) is Element of K32( the carrier' of A)

{ b

Hom ((dom F),t) is Element of K32( the carrier' of A)

{ b

K33((Hom ((cod F),t)),(Hom ((dom F),t))) is Relation-like set

K32(K33((Hom ((cod F),t)),(Hom ((dom F),t)))) is set

proj2 (hom (F,t)) is set

hom ((dom F),d) is Relation-like Hom ((dom F),(dom d)) -defined Hom ((dom F),(cod d)) -valued Function-like quasi_total Element of K32(K33((Hom ((dom F),(dom d))),(Hom ((dom F),(cod d)))))

Hom ((dom F),(dom d)) is Element of K32( the carrier' of A)

{ b

Hom ((dom F),(cod d)) is Element of K32( the carrier' of A)

{ b

K33((Hom ((dom F),(dom d))),(Hom ((dom F),(cod d)))) is Relation-like set

K32(K33((Hom ((dom F),(dom d))),(Hom ((dom F),(cod d))))) is set

proj1 (hom ((dom F),d)) is set

t is set

(hom ((cod F),d)) * (hom (F,d1)) is Relation-like Hom ((cod F),(dom d)) -defined Hom ((dom F),d1) -valued Function-like set

proj1 ((hom ((cod F),d)) * (hom (F,d1))) is set

(hom (F,t)) * (hom ((dom F),d)) is Relation-like Hom ((cod F),t) -defined Hom ((dom F),(cod d)) -valued Function-like set

proj1 ((hom (F,t)) * (hom ((dom F),d))) is set

proj1 (hom ((cod F),d)) is set

proj1 (hom (F,t)) is set

proj1 (hom ((cod F),d)) is set

proj1 (hom (F,t)) is set

t is set

((hom ((cod F),d)) * (hom (F,d1))) . t is set

((hom (F,t)) * (hom ((dom F),d))) . t is set

proj1 (hom ((cod F),d)) is set

t1 is Element of the carrier' of A

cod t1 is Element of the carrier of A

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

dom t1 is Element of the carrier of A

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

d (*) t1 is Element of the carrier' of A

cod (d (*) t1) is Element of the carrier of A

the Target of A . (d (*) t1) is Element of the carrier of A

(hom (F,t)) . t1 is set

t1 (*) F is Element of the carrier' of A

dom (t1 (*) F) is Element of the carrier of A

the Source of A . (t1 (*) F) is Element of the carrier of A

dom (d (*) t1) is Element of the carrier of A

the Source of A . (d (*) t1) is Element of the carrier of A

cod (t1 (*) F) is Element of the carrier of A

the Target of A . (t1 (*) F) is Element of the carrier of A

((hom ((cod F),d)) * (hom (F,d1))) . t1 is set

(hom ((cod F),d)) . t1 is set

(hom (F,d1)) . ((hom ((cod F),d)) . t1) is set

(hom (F,d1)) . (d (*) t1) is set

(d (*) t1) (*) F is Element of the carrier' of A

d (*) (t1 (*) F) is Element of the carrier' of A

f is Element of the carrier' of A

d (*) f is Element of the carrier' of A

(hom ((dom F),d)) . ((hom (F,t)) . t1) is set

((hom (F,t)) * (hom ((dom F),d))) . t1 is set

proj1 (hom ((cod F),d)) is set

Hom (((A,(dom F)) . t),((A,(dom F)) . d1)) is Element of K32( the carrier' of (A))

{ b

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

[(Hom ((cod F),t)),(Hom ((dom F),t))] is V1() set

{(Hom ((cod F),t)),(Hom ((dom F),t))} is non empty set

{(Hom ((cod F),t))} is non empty set

{{(Hom ((cod F),t)),(Hom ((dom F),t))},{(Hom ((cod F),t))}} is non empty set

[[(Hom ((cod F),t)),(Hom ((dom F),t))],(hom (F,t))] is V1() set

{[(Hom ((cod F),t)),(Hom ((dom F),t))],(hom (F,t))} is non empty set

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

{{[(Hom ((cod F),t)),(Hom ((dom F),t))],(hom (F,t))},{[(Hom ((cod F),t)),(Hom ((dom F),t))]}} is non empty set

t is Element of the carrier' of (A)

Hom (((A,(cod F)) . t),((A,(dom F)) . t)) is Element of K32( the carrier' of (A))

{ b

F2 . d1 is Element of the carrier' of (A)

[(Hom ((cod F),d1)),(Hom ((dom F),d1))] is V1() set

{(Hom ((cod F),d1)),(Hom ((dom F),d1))} is non empty set

{(Hom ((cod F),d1))} is non empty set

{{(Hom ((cod F),d1)),(Hom ((dom F),d1))},{(Hom ((cod F),d1))}} is non empty set

[[(Hom ((cod F),d1)),(Hom ((dom F),d1))],(hom (F,d1))] is V1() set

{[(Hom ((cod F),d1)),(Hom ((dom F),d1))],(hom (F,d1))} is non empty set

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

{{[(Hom ((cod F),d1)),(Hom ((dom F),d1))],(hom (F,d1))},{[(Hom ((cod F),d1)),(Hom ((dom F),d1))]}} is non empty set

f is Element of the carrier' of (A)

fDom (Hom A) is non empty Relation-like Maps (Hom A) -defined Hom A -valued Function-like V17( Maps (Hom A)) quasi_total Element of K32(K33((Maps (Hom A)),(Hom A)))

K33((Maps (Hom A)),(Hom A)) is Relation-like set

K32(K33((Maps (Hom A)),(Hom A))) is set

fCod (Hom A) is non empty Relation-like Maps (Hom A) -defined Hom A -valued Function-like V17( Maps (Hom A)) quasi_total Element of K32(K33((Maps (Hom A)),(Hom A)))

fComp (Hom A) is Relation-like K33((Maps (Hom A)),(Maps (Hom A))) -defined Maps (Hom A) -valued Function-like Element of K32(K33(K33((Maps (Hom A)),(Maps (Hom A))),(Maps (Hom A))))

K33((Maps (Hom A)),(Maps (Hom A))) is Relation-like set

K33(K33((Maps (Hom A)),(Maps (Hom A))),(Maps (Hom A))) is Relation-like set

K32(K33(K33((Maps (Hom A)),(Maps (Hom A))),(Maps (Hom A)))) is set

CatStr(# (Hom A),(Maps (Hom A)),(fDom (Hom A)),(fCod (Hom A)),(fComp (Hom A)) #) is strict CatStr

cod f 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 V17( the carrier' of (A)) quasi_total Element of K32(K33( the carrier' of (A), the carrier of (A)))

K33( the carrier' of (A), the carrier of (A)) is Relation-like set

K32(K33( the carrier' of (A), the carrier of (A))) is set

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

(fCod (Hom A)) . f is set

a is Element of Maps (Hom A)

cod a is Element of Hom A

f `1 is set

(f `1) `2 is set

[(Hom ((cod F),d1)),(Hom ((dom F),d1))] `2 is set

dom t 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 V17( the carrier' of (A)) quasi_total Element of K32(K33( the carrier' of (A), the carrier of (A)))

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

(fDom (Hom A)) . t is set

t1 is Element of Maps (Hom A)

dom t1 is Element of Hom A

t `1 is set

(t `1) `1 is set

[(Hom ((cod F),t)),(Hom ((dom F),t))] `1 is set

cod t is Element of the carrier of (A)

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

(fCod (Hom A)) . t is set

cod t1 is Element of Hom A

(t `1) `2 is set

[(Hom ((cod F),t)),(Hom ((dom F),t))] `2 is set

ta1 is Element of the carrier' of (A)

(hom?- (cod F)) . d is Element of Maps (Hom A)

[(Hom ((cod F),(dom d))),(Hom ((cod F),(cod d)))] is V1() set

{(Hom ((cod F),(dom d))),(Hom ((cod F),(cod d)))} is non empty set

{(Hom ((cod F),(dom d)))} is non empty set

{{(Hom ((cod F),(dom d))),(Hom ((cod F),(cod d)))},{(Hom ((cod F),(dom d)))}} is non empty set

[[(Hom ((cod F),(dom d))),(Hom ((cod F),(cod d)))],(hom ((cod F),d))] is V1() set

{[(Hom ((cod F),(dom d))),(Hom ((cod F),(cod d)))],(hom ((cod F),d))} is non empty set

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

{{[(Hom ((cod F),(dom d))),(Hom ((cod F),(cod d)))],(hom ((cod F),d))},{[(Hom ((cod F),(dom d))),(Hom ((cod F),(cod d)))]}} is non empty set

dom ta1 is Element of the carrier of (A)

the Source of (A) . ta1 is Element of the carrier of (A)

(fDom (Hom A)) . ta1 is set

X is Element of Maps (Hom A)

dom X is Element of Hom A

ta1 `1 is set

(ta1 `1) `1 is set

[(Hom ((cod F),(dom d))),(Hom ((cod F),(cod d)))] `1 is set

cod ta1 is Element of the carrier of (A)

the Target of (A) . ta1 is Element of the carrier of (A)

(fCod (Hom A)) . ta1 is set

cod X is Element of Hom A

(ta1 `1) `2 is set

[(Hom ((cod F),(dom d))),(Hom ((cod F),(cod d)))] `2 is set

dom f is Element of the carrier of (A)

the Source of (A) . f is Element of the carrier of (A)

(fDom (Hom A)) . f is set

dom a is Element of Hom A

(f `1) `1 is set

[(Hom ((cod F),d1)),(Hom ((dom F),d1))] `1 is set

t1 is Element of the carrier' of (A)

(hom?- (dom F)) . d is Element of Maps (Hom A)

[(Hom ((dom F),(dom d))),(Hom ((dom F),(cod d)))] is V1() set

{(Hom ((dom F),(dom d))),(Hom ((dom F),(cod d)))} is non empty set

{(Hom ((dom F),(dom d)))} is non empty set

{{(Hom ((dom F),(dom d))),(Hom ((dom F),(cod d)))},{(Hom ((dom F),(dom d)))}} is non empty set

[[(Hom ((dom F),(dom d))),(Hom ((dom F),(cod d)))],(hom ((dom F),d))] is V1() set

{[(Hom ((dom F),(dom d))),(Hom ((dom F),(cod d)))],(hom ((dom F),d))} is non empty set

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

{{[(Hom ((dom F),(dom d))),(Hom ((dom F),(cod d)))],(hom ((dom F),d))},{[(Hom ((dom F),(dom d))),(Hom ((dom F),(cod d)))]}} is non empty set

cod t1 is Element of the carrier of (A)

the Target of (A) . t1 is Element of the carrier of (A)

(fCod (Hom A)) . t1 is set

x is Element of Maps (Hom A)

cod x is Element of Hom A

t1 `1 is set

(t1 `1) `2 is set

[(Hom ((dom F),(dom d))),(Hom ((dom F),(cod d)))] `2 is set

dom t1 is Element of the carrier of (A)

the Source of (A) . t1 is Element of the carrier of (A)

(fDom (Hom A)) . t1 is set

dom x is Element of Hom A

(t1 `1) `1 is set

[(Hom ((dom F),(dom d))),(Hom ((dom F),(cod d)))] `1 is set

Hom (((A,(cod F)) . d1),((A,(dom F)) . d1)) is Element of K32( the carrier' of (A))

{ b

f (*) ta1 is Element of the carrier' of (A)

[(Hom ((cod F),(dom d))),(Hom ((dom F),d1))] is V1() set

{(Hom ((cod F),(dom d))),(Hom ((dom F),d1))} is non empty set

{{(Hom ((cod F),(dom d))),(Hom ((dom F),d1))},{(Hom ((cod F),(dom d)))}} is non empty set

[[(Hom ((cod F),(dom d))),(Hom ((dom F),d1))],((hom ((cod F),d)) * (hom (F,d1)))] is V1() set

{[(Hom ((cod F),(dom d))),(Hom ((dom F),d1))],((hom ((cod F),d)) * (hom (F,d1)))} is non empty set

{[(Hom ((cod F),(dom d))),(Hom ((dom F),d1))]} is non empty Relation-like Function-like set

{{[(Hom ((cod F),(dom d))),(Hom ((dom F),d1))],((hom ((cod F),d)) * (hom (F,d1)))},{[(Hom ((cod F),(dom d))),(Hom ((dom F),d1))]}} is non empty set

[(Hom ((cod F),t)),(Hom ((dom F),(cod d)))] is V1() set

{(Hom ((cod F),t)),(Hom ((dom F),(cod d)))} is non empty set

{{(Hom ((cod F),t)),(Hom ((dom F),(cod d)))},{(Hom ((cod F),t))}} is non empty set

[[(Hom ((cod F),t)),(Hom ((dom F),(cod d)))],((hom (F,t)) * (hom ((dom F),d)))] is V1() set

{[(Hom ((cod F),t)),(Hom ((dom F),(cod d)))],((hom (F,t)) * (hom ((dom F),d)))} is non empty set

{[(Hom ((cod F),t)),(Hom ((dom F),(cod d)))]} is non empty Relation-like Function-like set

{{[(Hom ((cod F),t)),(Hom ((dom F),(cod d)))],((hom (F,t)) * (hom ((dom F),d)))},{[(Hom ((cod F),t)),(Hom ((dom F),(cod d)))]}} is non empty set

t1 (*) t is Element of the carrier' of (A)

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

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

Hom A is non empty set

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

the carrier' of (A) is non empty set

F is Element of the carrier' of A

cod F 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 V17( the carrier' of A) quasi_total Element of K32(K33( the carrier' of A, the carrier of A))

K33( the carrier' of A, the carrier of A) is Relation-like set

K32(K33( the carrier' of A, the carrier of A)) is set

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

(A,(cod F)) is non empty Relation-like the carrier' of A -defined the carrier' of (A) -valued Function-like V17( the carrier' of A) quasi_total Functor of A,(A)

hom?- (cod F) is non empty Relation-like the carrier' of A -defined Maps (Hom A) -valued Function-like V17( the carrier' of A) quasi_total Element of K32(K33( the carrier' of A,(Maps (Hom A))))

Maps (Hom A) is non empty set

K33( the carrier' of A,(Maps (Hom A))) is Relation-like set

K32(K33( the carrier' of A,(Maps (Hom A)))) is set

dom F 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 V17( the carrier' of A) quasi_total Element of K32(K33( the carrier' of A, the carrier of A))

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

(A,(dom F)) is non empty Relation-like the carrier' of A -defined the carrier' of (A) -valued Function-like V17( the carrier' of A) quasi_total Functor of A,(A)

hom?- (dom F) is non empty Relation-like the carrier' of A -defined Maps (Hom A) -valued Function-like V17( the carrier' of A) quasi_total Element of K32(K33( the carrier' of A,(Maps (Hom A))))

F1 is Element of the carrier of A

Hom ((cod F),F1) is Element of K32( the carrier' of A)

K32( the carrier' of A) is set

{ b

Hom ((dom F),F1) is Element of K32( the carrier' of A)

{ b

[(Hom ((cod F),F1)),(Hom ((dom F),F1))] is V1() set

{(Hom ((cod F),F1)),(Hom ((dom F),F1))} is non empty set

{(Hom ((cod F),F1))} is non empty set

{{(Hom ((cod F),F1)),(Hom ((dom F),F1))},{(Hom ((cod F),F1))}} is non empty set

id F1 is Morphism of F1,F1

hom (F,(id F1)) is Relation-like Hom ((cod F),(dom (id F1))) -defined Hom ((dom F),(cod (id F1))) -valued Function-like quasi_total Element of K32(K33((Hom ((cod F),(dom (id F1)))),(Hom ((dom F),(cod (id F1))))))

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

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

Hom ((cod F),(dom (id F1))) is Element of K32( the carrier' of A)

{ b

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

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

Hom ((dom F),(cod (id F1))) is Element of K32( the carrier' of A)

{ b

K33((Hom ((cod F),(dom (id F1)))),(Hom ((dom F),(cod (id F1))))) is Relation-like set

K32(K33((Hom ((cod F),(dom (id F1)))),(Hom ((dom F),(cod (id F1)))))) is set

[[(Hom ((cod F),F1)),(Hom ((dom F),F1))],(hom (F,(id F1)))] is V1() set

{[(Hom ((cod F),F1)),(Hom ((dom F),F1))],(hom (F,(id F1)))} is non empty set

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

{{[(Hom ((cod F),F1)),(Hom ((dom F),F1))],(hom (F,(id F1)))},{[(Hom ((cod F),F1)),(Hom ((dom F),F1))]}} is non empty set

(A,(cod F)) . F1 is Element of the carrier of (A)

the carrier of (A) is non empty set

Obj (A,(cod F)) is non empty Relation-like the carrier of A -defined the carrier of (A) -valued Function-like V17( the carrier of A) quasi_total Element of K32(K33( the carrier of A, the carrier of (A)))

K33( the carrier of A, the carrier of (A)) is Relation-like set

K32(K33( the carrier of A, the carrier of (A))) is set

(Obj (A,(cod F))) . F1 is Element of the carrier of (A)

(A,(dom F)) . F1 is Element of the carrier of (A)

Obj (A,(dom F)) is non empty Relation-like the carrier of A -defined the carrier of (A) -valued Function-like V17( the carrier of A) quasi_total Element of K32(K33( the carrier of A, the carrier of (A)))

(Obj (A,(dom F))) . F1 is Element of the carrier of (A)

Hom (((A,(cod F)) . F1),((A,(dom F)) . F1)) is Element of K32( the carrier' of (A))

K32( the carrier' of (A)) is set

{ b

fDom (Hom A) is non empty Relation-like Maps (Hom A) -defined Hom A -valued Function-like V17( Maps (Hom A)) quasi_total Element of K32(K33((Maps (Hom A)),(Hom A)))

K33((Maps (Hom A)),(Hom A)) is Relation-like set

K32(K33((Maps (Hom A)),(Hom A))) is set

fCod (Hom A) is non empty Relation-like Maps (Hom A) -defined Hom A -valued Function-like V17( Maps (Hom A)) quasi_total Element of K32(K33((Maps (Hom A)),(Hom A)))

fComp (Hom A) is Relation-like K33((Maps (Hom A)),(Maps (Hom A))) -defined Maps (Hom A) -valued Function-like Element of K32(K33(K33((Maps (Hom A)),(Maps (Hom A))),(Maps (Hom A))))

K33((Maps (Hom A)),(Maps (Hom A))) is Relation-like set

K33(K33((Maps (Hom A)),(Maps (Hom A))),(Maps (Hom A))) is Relation-like set

K32(K33(K33((Maps (Hom A)),(Maps (Hom A))),(Maps (Hom A)))) is set

CatStr(# (Hom A),(Maps (Hom A)),(fDom (Hom A)),(fCod (Hom A)),(fComp (Hom A)) #) is strict CatStr

hom (F,F1) is Relation-like Hom ((cod F),F1) -defined Hom ((dom F),F1) -valued Function-like quasi_total Element of K32(K33((Hom ((cod F),F1)),(Hom ((dom F),F1))))

K33((Hom ((cod F),F1)),(Hom ((dom F),F1))) is Relation-like set

K32(K33((Hom ((cod F),F1)),(Hom ((dom F),F1)))) is set

F2 is Element of the carrier' of (A)

cod F2 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 V17( the carrier' of (A)) quasi_total Element of K32(K33( the carrier' of (A), the carrier of (A)))

K33( the carrier' of (A), the carrier of (A)) is Relation-like set

K32(K33( the carrier' of (A), the carrier of (A))) is set

the Target of (A) . F2 is Element of the carrier of (A)

(fCod (Hom A)) . F2 is set

t is Element of Maps (Hom A)

cod t is Element of Hom A

F2 `1 is set

(F2 `1) `2 is set

[(Hom ((cod F),F1)),(Hom ((dom F),F1))] `2 is set

the carrier of (Ens (Hom A)) is non empty set

hom?- ((Hom A),(dom F)) is non empty Relation-like the carrier' of A -defined the carrier' of (Ens (Hom A)) -valued Function-like V17( the carrier' of A) quasi_total Functor of A, Ens (Hom A)

the carrier' of (Ens (Hom A)) is non empty set

Obj (hom?- ((Hom A),(dom F))) is non empty Relation-like the carrier of A -defined the carrier of (Ens (Hom A)) -valued Function-like V17( the carrier of A) quasi_total Element of K32(K33( the carrier of A, the carrier of (Ens (Hom A))))

K33( the carrier of A, the carrier of (Ens (Hom A))) is Relation-like set

K32(K33( the carrier of A, the carrier of (Ens (Hom A)))) is set

(Obj (hom?- ((Hom A),(dom F)))) . F1 is Element of the carrier of (Ens (Hom A))

(hom?- ((Hom A),(dom F))) . F1 is Element of the carrier of (Ens (Hom A))

dom F2 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 V17( the carrier' of (A)) quasi_total Element of K32(K33( the carrier' of (A), the carrier of (A)))

the Source of (A) . F2 is Element of the carrier of (A)

(fDom (Hom A)) . F2 is set

dom t is Element of Hom A

(F2 `1) `1 is set

[(Hom ((cod F),F1)),(Hom ((dom F),F1))] `1 is set

hom?- ((Hom A),(cod F)) is non empty Relation-like the carrier' of A -defined the carrier' of (Ens (Hom A)) -valued Function-like V17( the carrier' of A) quasi_total Functor of A, Ens (Hom A)

Obj (hom?- ((Hom A),(cod F))) is non empty Relation-like the carrier of A -defined the carrier of (Ens (Hom A)) -valued Function-like V17( the carrier of A) quasi_total Element of K32(K33( the carrier of A, the carrier of (Ens (Hom A))))

(Obj (hom?- ((Hom A),(cod F)))) . F1 is Element of the carrier of (Ens (Hom A))

(hom?- ((Hom A),(cod F))) . F1 is Element of the carrier of (Ens (Hom A))

F1 is Element of the carrier of A

Hom ((cod F),F1) is Element of K32( the carrier' of A)

K32( the carrier' of A) is set

{ b

Hom ((dom F),F1) is Element of K32( the carrier' of A)

{ b

[(Hom ((cod F),F1)),(Hom ((dom F),F1))] is V1() set

{(Hom ((cod F),F1)),(Hom ((dom F),F1))} is non empty set

{(Hom ((cod F),F1))} is non empty set

{{(Hom ((cod F),F1)),(Hom ((dom F),F1))},{(Hom ((cod F),F1))}} is non empty set

id F1 is Morphism of F1,F1

hom (F,(id F1)) is Relation-like Hom ((cod F),(dom (id F1))) -defined Hom ((dom F),(cod (id F1))) -valued Function-like quasi_total Element of K32(K33((Hom ((cod F),(dom (id F1)))),(Hom ((dom F),(cod (id F1))))))

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

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

Hom ((cod F),(dom (id F1))) is Element of K32( the carrier' of A)

{ b

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

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

Hom ((dom F),(cod (id F1))) is Element of K32( the carrier' of A)

{ b

K33((Hom ((cod F),(dom (id F1)))),(Hom ((dom F),(cod (id F1))))) is Relation-like set

K32(K33((Hom ((cod F),(dom (id F1)))),(Hom ((dom F),(cod (id F1)))))) is set

[[(Hom ((cod F),F1)),(Hom ((dom F),F1))],(hom (F,(id F1)))] is V1() set

{[(Hom ((cod F),F1)),(Hom ((dom F),F1))],(hom (F,(id F1)))} is non empty set

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

{{[(Hom ((cod F),F1)),(Hom ((dom F),F1))],(hom (F,(id F1)))},{[(Hom ((cod F),F1)),(Hom ((dom F),F1))]}} is non empty set

(A,(cod F)) . F1 is Element of the carrier of (A)

the carrier of (A) is non empty set

Obj (A,(cod F)) is non empty Relation-like the carrier of A -defined the carrier of (A) -valued Function-like V17( the carrier of A) quasi_total Element of K32(K33( the carrier of A, the carrier of (A)))

K33( the carrier of A, the carrier of (A)) is Relation-like set

K32(K33( the carrier of A, the carrier of (A))) is set

(Obj (A,(cod F))) . F1 is Element of the carrier of (A)

(A,(dom F)) . F1 is Element of the carrier of (A)

Obj (A,(dom F)) is non empty Relation-like the carrier of A -defined the carrier of (A) -valued Function-like V17( the carrier of A) quasi_total Element of K32(K33( the carrier of A, the carrier of (A)))

(Obj (A,(dom F))) . F1 is Element of the carrier of (A)

Hom (((A,(cod F)) . F1),((A,(dom F)) . F1)) is Element of K32( the carrier' of (A))

K32( the carrier' of (A)) is set

{ b

K33( the carrier of A, the carrier' of (A)) is Relation-like set

K32(K33( the carrier of A, the carrier' of (A))) is set

F1 is non empty Relation-like the carrier of A -defined the carrier' of (A) -valued Function-like V17( the carrier of A) quasi_total Element of K32(K33( the carrier of A, the carrier' of (A)))

F2 is Element of the carrier of A

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

(A,(cod F)) . F2 is Element of the carrier of (A)

the carrier of (A) is non empty set

Obj (A,(cod F)) is non empty Relation-like the carrier of A -defined the carrier of (A) -valued Function-like V17( the carrier of A) quasi_total Element of K32(K33( the carrier of A, the carrier of (A)))

K33( the carrier of A, the carrier of (A)) is Relation-like set

K32(K33( the carrier of A, the carrier of (A))) is set

(Obj (A,(cod F))) . F2 is Element of the carrier of (A)

(A,(dom F)) . F2 is Element of the carrier of (A)

Obj (A,(dom F)) is non empty Relation-like the carrier of A -defined the carrier of (A) -valued Function-like V17( the carrier of A) quasi_total Element of K32(K33( the carrier of A, the carrier of (A)))

(Obj (A,(dom F))) . F2 is Element of the carrier of (A)

Hom ((cod F),F2) is Element of K32( the carrier' of A)

K32( the carrier' of A) is set

{ b

Hom ((dom F),F2) is Element of K32( the carrier' of A)

{ b

[(Hom ((cod F),F2)),(Hom ((dom F),F2))] is V1() set

{(Hom ((cod F),F2)),(Hom ((dom F),F2))} is non empty set

{(Hom ((cod F),F2))} is non empty set

{{(Hom ((cod F),F2)),(Hom ((dom F),F2))},{(Hom ((cod F),F2))}} is non empty set

id F2 is Morphism of F2,F2

hom (F,(id F2)) is Relation-like Hom ((cod F),(dom (id F2))) -defined Hom ((dom F),(cod (id F2))) -valued Function-like quasi_total Element of K32(K33((Hom ((cod F),(dom (id F2)))),(Hom ((dom F),(cod (id F2))))))

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

the Source of A . (id F2) is Element of the carrier of A

Hom ((cod F),(dom (id F2))) is Element of K32( the carrier' of A)

{ b

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

the Target of A . (id F2) is Element of the carrier of A

Hom ((dom F),(cod (id F2))) is Element of K32( the carrier' of A)

{ b

K33((Hom ((cod F),(dom (id F2)))),(Hom ((dom F),(cod (id F2))))) is Relation-like set

K32(K33((Hom ((cod F),(dom (id F2)))),(Hom ((dom F),(cod (id F2)))))) is set

[[(Hom ((cod F),F2)),(Hom ((dom F),F2))],(hom (F,(id F2)))] is V1() set

{[(Hom ((cod F),F2)),(Hom ((dom F),F2))],(hom (F,(id F2)))} is non empty set

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

{{[(Hom ((cod F),F2)),(Hom ((dom F),F2))],(hom (F,(id F2)))},{[(Hom ((cod F),F2)),(Hom ((dom F),F2))]}} is non empty set

Hom (((A,(cod F)) . F2),((A,(dom F)) . F2)) is Element of K32( the carrier' of (A))

K32( the carrier' of (A)) is set

{ b

F2 is Element of the carrier of A

(A,(cod F)) . F2 is Element of the carrier of (A)

the carrier of (A) is non empty set

Obj (A,(cod F)) is non empty Relation-like the carrier of A -defined the carrier of (A) -valued Function-like V17( the carrier of A) quasi_total Element of K32(K33( the carrier of A, the carrier of (A)))

K33( the carrier of A, the carrier of (A)) is Relation-like set

K32(K33( the carrier of A, the carrier of (A))) is set

(Obj (A,(cod F))) . F2 is Element of the carrier of (A)

(A,(dom F)) . F2 is Element of the carrier of (A)

Obj (A,(dom F)) is non empty Relation-like the carrier of A -defined the carrier of (A) -valued Function-like V17( the carrier of A) quasi_total Element of K32(K33( the carrier of A, the carrier of (A)))

(Obj (A,(dom F))) . F2 is Element of the carrier of (A)

Hom (((A,(cod F)) . F2),((A,(dom F)) . F2)) is Element of K32( the carrier' of (A))

K32( the carrier' of (A)) is set

{ b

F2 is non empty Relation-like the carrier of A -defined the carrier' of (A) -valued Function-like V17( the carrier of A) quasi_total transformation of (A,(cod F)),(A,(dom F))

t is Element of the carrier of A

d1 is Element of the carrier of A

Hom (t,d1) is Element of K32( the carrier' of A)

K32( the carrier' of A) is set

{ b

(A,(cod F)) . t is Element of the carrier of (A)

the carrier of (A) is non empty set

Obj (A,(cod F)) is non empty Relation-like the carrier of A -defined the carrier of (A) -valued Function-like V17( the carrier of A) quasi_total Element of K32(K33( the carrier of A, the carrier of (A)))

K33( the carrier of A, the carrier of (A)) is Relation-like set

K32(K33( the carrier of A, the carrier of (A))) is set

(Obj (A,(cod F))) . t is Element of the carrier of (A)

(A,(cod F)) . d1 is Element of the carrier of (A)

(Obj (A,(cod F))) . d1 is Element of the carrier of (A)

(A,(dom F)) . d1 is Element of the carrier of (A)

Obj (A,(dom F)) is non empty Relation-like the carrier of A -defined the carrier of (A) -valued Function-like V17( the carrier of A) quasi_total Element of K32(K33( the carrier of A, the carrier of (A)))

(Obj (A,(dom F))) . d1 is Element of the carrier of (A)

F2 . d1 is Morphism of (A,(cod F)) . d1,(A,(dom F)) . d1

(A,(dom F)) . t is Element of the carrier of (A)

(Obj (A,(dom F))) . t is Element of the carrier of (A)

F2 . t is Morphism of (A,(cod F)) . t,(A,(dom F)) . t

Hom (((A,(cod F)) . t),((A,(cod F)) . d1)) is Element of K32( the carrier' of (A))

K32( the carrier' of (A)) is set

{ b

d is Morphism of t,d1

(A,(cod F)) /. d is Morphism of (A,(cod F)) . t,(A,(cod F)) . d1

(F2 . d1) * ((A,(cod F)) /. d) is Morphism of (A,(cod F)) . t,(A,(dom F)) . d1

(A,(dom F)) /. d is Morphism of (A,(dom F)) . t,(A,(dom F)) . d1

((A,(dom F)) /. d) * (F2 . t) is Morphism of (A,(cod F)) . t,(A,(dom F)) . d1

dom d is Element of the carrier of A

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

hom ((cod F),d) is Relation-like Hom ((cod F),(dom d)) -defined Hom ((cod F),(cod d)) -valued Function-like quasi_total Element of K32(K33((Hom ((cod F),(dom d))),(Hom ((cod F),(cod d)))))

Hom ((cod F),(dom d)) is Element of K32( the carrier' of A)

{ b

cod d is Element of the carrier of A

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

Hom ((cod F),(cod d)) is Element of K32( the carrier' of A)

{ b

K33((Hom ((cod F),(dom d))),(Hom ((cod F),(cod d)))) is Relation-like set

K32(K33((Hom ((cod F),(dom d))),(Hom ((cod F),(cod d))))) is set

proj2 (hom ((cod F),d)) is set

hom (F,d1) is Relation-like Hom ((cod F),d1) -defined Hom ((dom F),d1) -valued Function-like quasi_total Element of K32(K33((Hom ((cod F),d1)),(Hom ((dom F),d1))))

Hom ((cod F),d1) is Element of K32( the carrier' of A)

{ b

Hom ((dom F),d1) is Element of K32( the carrier' of A)

{ b

K33((Hom ((cod F),d1)),(Hom ((dom F),d1))) is Relation-like set

K32(K33((Hom ((cod F),d1)),(Hom ((dom F),d1)))) is set

proj1 (hom (F,d1)) is set

t is set

hom (F,t) is Relation-like Hom ((cod F),t) -defined Hom ((dom F),t) -valued Function-like quasi_total Element of K32(K33((Hom ((cod F),t)),(Hom ((dom F),t))))

Hom ((cod F),t) is Element of K32( the carrier' of A)

{ b

Hom ((dom F),t) is Element of K32( the carrier' of A)

{ b

K33((Hom ((cod F),t)),(Hom ((dom F),t))) is Relation-like set

K32(K33((Hom ((cod F),t)),(Hom ((dom F),t)))) is set

proj2 (hom (F,t)) is set

hom ((dom F),d) is Relation-like Hom ((dom F),(dom d)) -defined Hom ((dom F),(cod d)) -valued Function-like quasi_total Element of K32(K33((Hom ((dom F),(dom d))),(Hom ((dom F),(cod d)))))

Hom ((dom F),(dom d)) is Element of K32( the carrier' of A)

{ b

Hom ((dom F),(cod d)) is Element of K32( the carrier' of A)

{ b

K33((Hom ((dom F),(dom d))),(Hom ((dom F),(cod d)))) is Relation-like set

K32(K33((Hom ((dom F),(dom d))),(Hom ((dom F),(cod d))))) is set

proj1 (hom ((dom F),d)) is set

t is set

(hom ((cod F),d)) * (hom (F,d1)) is Relation-like Hom ((cod F),(dom d)) -defined Hom ((dom F),d1) -valued Function-like set

proj1 ((hom ((cod F),d)) * (hom (F,d1))) is set

(hom (F,t)) * (hom ((dom F),d)) is Relation-like Hom ((cod F),t) -defined Hom ((dom F),(cod d)) -valued Function-like set

proj1 ((hom (F,t)) * (hom ((dom F),d))) is set

proj1 (hom ((cod F),d)) is set

proj1 (hom (F,t)) is set

proj1 (hom ((cod F),d)) is set

proj1 (hom (F,t)) is set

t is set

((hom ((cod F),d)) * (hom (F,d1))) . t is set

((hom (F,t)) * (hom ((dom F),d))) . t is set

proj1 (hom ((cod F),d)) is set

t1 is Element of the carrier' of A

cod t1 is Element of the carrier of A

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

d (*) t1 is Element of the carrier' of A

cod (d (*) t1) is Element of the carrier of A

the Target of A . (d (*) t1) is Element of the carrier of A

dom (d (*) t1) is Element of the carrier of A

the Source of A . (d (*) t1) is Element of the carrier of A

dom t1 is Element of the carrier of A

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

t1 (*) F is Element of the carrier' of A

dom (t1 (*) F) is Element of the carrier of A

the Source of A . (t1 (*) F) is Element of the carrier of A

(hom (F,t)) . t1 is set

cod (t1 (*) F) is Element of the carrier of A

the Target of A . (t1 (*) F) is Element of the carrier of A

((hom ((cod F),d)) * (hom (F,d1))) . t1 is set

(hom ((cod F),d)) . t1 is set

(hom (F,d1)) . ((hom ((cod F),d)) . t1) is set

(hom (F,d1)) . (d (*) t1) is set

(d (*) t1) (*) F is Element of the carrier' of A

d (*) (t1 (*) F) is Element of the carrier' of A

f is Element of the carrier' of A

d (*) f is Element of the carrier' of A

(hom ((dom F),d)) . ((hom (F,t)) . t1) is