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
{ b1 where b1 is Element of the carrier' of A : ( dom b1 = cod F & cod b1 = F1 ) } is set
Hom ((dom F),F1) is Element of K32( the carrier' of A)
{ b1 where b1 is Element of the carrier' of A : ( dom b1 = dom F & cod b1 = F1 ) } is set
[(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
{ b1 where b1 is Element of the carrier' of (A) : ( dom b1 = (A,(cod F)) . F1 & cod b1 = (A,(dom F)) . F1 ) } is 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
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
{ b1 where b1 is Element of the carrier' of A : ( dom b1 = cod F & cod b1 = F1 ) } is set
Hom ((dom F),F1) is Element of K32( the carrier' of A)
{ b1 where b1 is Element of the carrier' of A : ( dom b1 = dom F & cod b1 = F1 ) } is set
[(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
{ b1 where b1 is Element of the carrier' of (A) : ( dom b1 = (A,(cod F)) . F1 & cod b1 = (A,(dom F)) . F1 ) } is set
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
{ b1 where b1 is Element of the carrier' of A : ( dom b1 = cod F & cod b1 = F2 ) } is set
Hom ((dom F),F2) is Element of K32( the carrier' of A)
{ b1 where b1 is Element of the carrier' of A : ( dom b1 = dom F & cod b1 = F2 ) } is set
[(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
{ b1 where b1 is Element of the carrier' of (A) : ( dom b1 = (A,(cod F)) . F2 & cod b1 = (A,(dom F)) . F2 ) } is set
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
{ b1 where b1 is Element of the carrier' of (A) : ( dom b1 = (A,(cod F)) . F2 & cod b1 = (A,(dom F)) . F2 ) } is set
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
{ b1 where b1 is Element of the carrier' of A : ( dom b1 = t & cod b1 = d1 ) } is set
(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
{ b1 where b1 is Element of the carrier' of (A) : ( dom b1 = (A,(cod F)) . t & cod b1 = (A,(cod F)) . d1 ) } is set
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)
{ b1 where b1 is Element of the carrier' of A : ( dom b1 = cod F & cod b1 = dom d ) } is set
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)
{ b1 where b1 is Element of the carrier' of A : ( dom b1 = cod F & cod b1 = cod d ) } is set
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)
{ b1 where b1 is Element of the carrier' of A : ( dom b1 = cod F & cod b1 = d1 ) } is set
Hom ((dom F),d1) is Element of K32( the carrier' of A)
{ b1 where b1 is Element of the carrier' of A : ( dom b1 = dom F & cod b1 = d1 ) } is set
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)
{ b1 where b1 is Element of the carrier' of A : ( dom b1 = cod F & cod b1 = t ) } is set
Hom ((dom F),t) is Element of K32( the carrier' of A)
{ b1 where b1 is Element of the carrier' of A : ( dom b1 = dom F & cod b1 = t ) } is set
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)
{ b1 where b1 is Element of the carrier' of A : ( dom b1 = dom F & cod b1 = dom d ) } is set
Hom ((dom F),(cod d)) is Element of K32( the carrier' of A)
{ b1 where b1 is Element of the carrier' of A : ( dom b1 = dom F & cod b1 = cod d ) } is set
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))
{ b1 where b1 is Element of the carrier' of (A) : ( dom b1 = (A,(dom F)) . t & cod b1 = (A,(dom F)) . d1 ) } is set
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))
{ b1 where b1 is Element of the carrier' of (A) : ( dom b1 = (A,(cod F)) . t & cod b1 = (A,(dom F)) . t ) } is set
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))
{ b1 where b1 is Element of the carrier' of (A) : ( dom b1 = (A,(cod F)) . d1 & cod b1 = (A,(dom F)) . d1 ) } is set
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
{ b1 where b1 is Element of the carrier' of A : ( dom b1 = cod F & cod b1 = F1 ) } is set
Hom ((dom F),F1) is Element of K32( the carrier' of A)
{ b1 where b1 is Element of the carrier' of A : ( dom b1 = dom F & cod b1 = F1 ) } is set
[(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)
{ b1 where b1 is Element of the carrier' of A : ( dom b1 = cod F & cod b1 = dom (id F1) ) } is set
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)
{ b1 where b1 is Element of the carrier' of A : ( dom b1 = dom F & cod b1 = cod (id F1) ) } is set
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
{ b1 where b1 is Element of the carrier' of (A) : ( dom b1 = (A,(cod F)) . F1 & cod b1 = (A,(dom F)) . F1 ) } is 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
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
{ b1 where b1 is Element of the carrier' of A : ( dom b1 = cod F & cod b1 = F1 ) } is set
Hom ((dom F),F1) is Element of K32( the carrier' of A)
{ b1 where b1 is Element of the carrier' of A : ( dom b1 = dom F & cod b1 = F1 ) } is set
[(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)
{ b1 where b1 is Element of the carrier' of A : ( dom b1 = cod F & cod b1 = dom (id F1) ) } is set
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)
{ b1 where b1 is Element of the carrier' of A : ( dom b1 = dom F & cod b1 = cod (id F1) ) } is set
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
{ b1 where b1 is Element of the carrier' of (A) : ( dom b1 = (A,(cod F)) . F1 & cod b1 = (A,(dom F)) . F1 ) } is set
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
{ b1 where b1 is Element of the carrier' of A : ( dom b1 = cod F & cod b1 = F2 ) } is set
Hom ((dom F),F2) is Element of K32( the carrier' of A)
{ b1 where b1 is Element of the carrier' of A : ( dom b1 = dom F & cod b1 = F2 ) } is set
[(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)
{ b1 where b1 is Element of the carrier' of A : ( dom b1 = cod F & cod b1 = dom (id F2) ) } is set
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)
{ b1 where b1 is Element of the carrier' of A : ( dom b1 = dom F & cod b1 = cod (id F2) ) } is set
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
{ b1 where b1 is Element of the carrier' of (A) : ( dom b1 = (A,(cod F)) . F2 & cod b1 = (A,(dom F)) . F2 ) } is set
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
{ b1 where b1 is Element of the carrier' of (A) : ( dom b1 = (A,(cod F)) . F2 & cod b1 = (A,(dom F)) . F2 ) } is set
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
{ b1 where b1 is Element of the carrier' of A : ( dom b1 = t & cod b1 = d1 ) } is set
(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
{ b1 where b1 is Element of the carrier' of (A) : ( dom b1 = (A,(cod F)) . t & cod b1 = (A,(cod F)) . d1 ) } is set
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)
{ b1 where b1 is Element of the carrier' of A : ( dom b1 = cod F & cod b1 = dom d ) } is set
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)
{ b1 where b1 is Element of the carrier' of A : ( dom b1 = cod F & cod b1 = cod d ) } is set
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)
{ b1 where b1 is Element of the carrier' of A : ( dom b1 = cod F & cod b1 = d1 ) } is set
Hom ((dom F),d1) is Element of K32( the carrier' of A)
{ b1 where b1 is Element of the carrier' of A : ( dom b1 = dom F & cod b1 = d1 ) } is set
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)
{ b1 where b1 is Element of the carrier' of A : ( dom b1 = cod F & cod b1 = t ) } is set
Hom ((dom F),t) is Element of K32( the carrier' of A)
{ b1 where b1 is Element of the carrier' of A : ( dom b1 = dom F & cod b1 = t ) } is set
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)
{ b1 where b1 is Element of the carrier' of A : ( dom b1 = dom F & cod b1 = dom d ) } is set
Hom ((dom F),(cod d)) is Element of K32( the carrier' of A)
{ b1 where b1 is Element of the carrier' of A : ( dom b1 = dom F & cod b1 = cod d ) } is set
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