CAT_3

:: CAT_3 semantic presentation

K99() is Element of K19(K95())
K95() is set
K19(K95()) is set
K94() is set
K19(K94()) is set
K19(K99()) is set
{} is empty set
1 is non empty set
F₂() is non empty set
F₁() is set
K20(F₁(),F₂()) is set
K19(K20(F₁(),F₂())) is set
C is set
F₃(C) is Element of F₂()
C is Relation-like F₁() -defined F₂() -valued Function-like V18(F₁(),F₂()) Element of K19(K20(F₁(),F₂()))
c is set
C /. c is Element of F₂()
F₃(c) is Element of F₂()
C . c is set
C is set
c is non empty set
K20(C,c) is set
K19(K20(C,c)) is set
i1 is Relation-like C -defined c -valued Function-like V18(C,c) Element of K19(K20(C,c))
i2 is Relation-like C -defined c -valued Function-like V18(C,c) Element of K19(K20(C,c))
a is set
i1 . a is set
i1 /. a is Element of c
i2 /. a is Element of c
i2 . a is set
F₂() is non empty set
F₁() is set
K20(F₁(),F₂()) is set
K19(K20(F₁(),F₂())) is set
C is Relation-like F₁() -defined F₂() -valued Function-like V18(F₁(),F₂()) Element of K19(K20(F₁(),F₂()))
c is Relation-like F₁() -defined F₂() -valued Function-like V18(F₁(),F₂()) Element of K19(K20(F₁(),F₂()))
i1 is set
C /. i1 is Element of F₂()
F₃(i1) is Element of F₂()
c /. i1 is Element of F₂()
C is non empty set
c is set
i1 is Element of C
c .--> i1 is set
{c} is non empty set
{c} --> i1 is Relation-like {c} -defined {i1} -valued Function-like V18({c},{i1}) Element of K19(K20({c},{i1}))
{i1} is non empty set
K20({c},{i1}) is set
K19(K20({c},{i1})) is set
K20({c},C) is set
K19(K20({c},C)) is set
C is set
c is set
i1 is non empty set
i2 is Element of i1
C --> i2 is Relation-like C -defined i1 -valued Function-like V18(C,i1) Element of K19(K20(C,i1))
K20(C,i1) is set
K19(K20(C,i1)) is set
{i2} is non empty set
K20(C,{i2}) is set
(C --> i2) /. c is Element of i1
(C --> i2) . c is set
C is set
c is set
{C,c} is non empty set
i1 is non empty set
i2 is Element of i1
a is Element of i1
(C,c) --> (i2,a) is Relation-like {C,c} -defined i1 -valued Function-like V18({C,c},i1) Element of K19(K20({C,c},i1))
K20({C,c},i1) is set
K19(K20({C,c},i1)) is set
((C,c) --> (i2,a)) /. C is Element of i1
((C,c) --> (i2,a)) /. c is Element of i1
((C,c) --> (i2,a)) . c is set
((C,c) --> (i2,a)) . C is set
c is set
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier' of C is non empty set
K20(c, the carrier' of C) is set
K19(K20(c, the carrier' of C)) is set
the carrier of C is non empty set
K20(c, the carrier of C) is set
K19(K20(c, the carrier of C)) is set
i1 is Relation-like c -defined the carrier' of C -valued Function-like V18(c, the carrier' of C) Element of K19(K20(c, the carrier' of C))
C is set
c is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier' of c is non empty set
the carrier of c is non empty set
i1 is Element of the carrier' of c
C --> i1 is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) Element of K19(K20(C, the carrier' of c))
K20(C, the carrier' of c) is set
K19(K20(C, the carrier' of c)) is set
{i1} is non empty set
K20(C,{i1}) is set
(c,C,(C --> i1)) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
K20(C, the carrier of c) is set
K19(K20(C, the carrier of c)) is set
dom i1 is Element of the carrier of c
C --> (dom i1) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
{(dom i1)} is non empty set
K20(C,{(dom i1)}) is set
b is set
(C --> i1) /. b is Element of the carrier' of c
(C --> (dom i1)) /. b is Element of the carrier of c
(c,C,(C --> i1)) /. b is Element of the carrier of c
C is set
c is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier' of c is non empty set
the carrier of c is non empty set
i1 is Element of the carrier' of c
C --> i1 is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) Element of K19(K20(C, the carrier' of c))
K20(C, the carrier' of c) is set
K19(K20(C, the carrier' of c)) is set
{i1} is non empty set
K20(C,{i1}) is set
(c,C,(C --> i1)) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
K20(C, the carrier of c) is set
K19(K20(C, the carrier of c)) is set
cod i1 is Element of the carrier of c
C --> (cod i1) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
{(cod i1)} is non empty set
K20(C,{(cod i1)}) is set
b is set
(C --> i1) /. b is Element of the carrier' of c
(C --> (cod i1)) /. b is Element of the carrier of c
(c,C,(C --> i1)) /. b is Element of the carrier of c
C is set
c is set
{C,c} is non empty set
i1 is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier' of i1 is non empty set
the carrier of i1 is non empty set
i2 is Element of the carrier' of i1
dom i2 is Element of the carrier of i1
a is Element of the carrier' of i1
(C,c) --> (i2,a) is Relation-like {C,c} -defined the carrier' of i1 -valued Function-like V18({C,c}, the carrier' of i1) Element of K19(K20({C,c}, the carrier' of i1))
K20({C,c}, the carrier' of i1) is set
K19(K20({C,c}, the carrier' of i1)) is set
(i1,{C,c},((C,c) --> (i2,a))) is Relation-like {C,c} -defined the carrier of i1 -valued Function-like V18({C,c}, the carrier of i1) Element of K19(K20({C,c}, the carrier of i1))
K20({C,c}, the carrier of i1) is set
K19(K20({C,c}, the carrier of i1)) is set
dom a is Element of the carrier of i1
(C,c) --> ((dom i2),(dom a)) is Relation-like {C,c} -defined the carrier of i1 -valued Function-like V18({C,c}, the carrier of i1) Element of K19(K20({C,c}, the carrier of i1))
( the carrier' of i1,C,i2) is Relation-like {C} -defined the carrier' of i1 -valued Function-like V18({C}, the carrier' of i1) Element of K19(K20({C}, the carrier' of i1))
{C} is non empty set
K20({C}, the carrier' of i1) is set
K19(K20({C}, the carrier' of i1)) is set
{C} --> i2 is Relation-like {C} -defined {i2} -valued Function-like V18({C},{i2}) Element of K19(K20({C},{i2}))
{i2} is non empty set
K20({C},{i2}) is set
K19(K20({C},{i2})) is set
( the carrier' of i1,c,a) is Relation-like {c} -defined the carrier' of i1 -valued Function-like V18({c}, the carrier' of i1) Element of K19(K20({c}, the carrier' of i1))
{c} is non empty set
K20({c}, the carrier' of i1) is set
K19(K20({c}, the carrier' of i1)) is set
{c} --> a is Relation-like {c} -defined {a} -valued Function-like V18({c},{a}) Element of K19(K20({c},{a}))
{a} is non empty set
K20({c},{a}) is set
K19(K20({c},{a})) is set
( the carrier of i1,C,(dom i2)) is Relation-like {C} -defined the carrier of i1 -valued Function-like V18({C}, the carrier of i1) Element of K19(K20({C}, the carrier of i1))
K20({C}, the carrier of i1) is set
K19(K20({C}, the carrier of i1)) is set
{C} --> (dom i2) is Relation-like {C} -defined {(dom i2)} -valued Function-like V18({C},{(dom i2)}) Element of K19(K20({C},{(dom i2)}))
{(dom i2)} is non empty set
K20({C},{(dom i2)}) is set
K19(K20({C},{(dom i2)})) is set
( the carrier of i1,c,(dom a)) is Relation-like {c} -defined the carrier of i1 -valued Function-like V18({c}, the carrier of i1) Element of K19(K20({c}, the carrier of i1))
K20({c}, the carrier of i1) is set
K19(K20({c}, the carrier of i1)) is set
{c} --> (dom a) is Relation-like {c} -defined {(dom a)} -valued Function-like V18({c},{(dom a)}) Element of K19(K20({c},{(dom a)}))
{(dom a)} is non empty set
K20({c},{(dom a)}) is set
K19(K20({c},{(dom a)})) is set
dom ( the carrier' of i1,c,a) is set
dom ( the carrier of i1,c,(dom a)) is set
( the carrier of i1,C,(dom i2)) +* ( the carrier of i1,c,(dom a)) is Relation-like Function-like set
( the carrier' of i1,C,i2) +* ( the carrier' of i1,c,a) is Relation-like Function-like set
dom ( the carrier' of i1,C,i2) is set
c₁₂ is set
dom ((C,c) --> (i2,a)) is set
((C,c) --> (i2,a)) . c₁₂ is set
( the carrier' of i1,C,i2) . c₁₂ is set
((C,c) --> ((dom i2),(dom a))) . c₁₂ is set
( the carrier of i1,C,(dom i2)) . c₁₂ is set
((C,c) --> (i2,a)) /. c₁₂ is Element of the carrier' of i1
((C,c) --> ((dom i2),(dom a))) /. c₁₂ is Element of the carrier of i1
((C,c) --> (i2,a)) . c₁₂ is set
( the carrier' of i1,c,a) . c₁₂ is set
((C,c) --> ((dom i2),(dom a))) . c₁₂ is set
( the carrier of i1,c,(dom a)) . c₁₂ is set
((C,c) --> (i2,a)) /. c₁₂ is Element of the carrier' of i1
((C,c) --> ((dom i2),(dom a))) /. c₁₂ is Element of the carrier of i1
((C,c) --> (i2,a)) /. c₁₂ is Element of the carrier' of i1
((C,c) --> ((dom i2),(dom a))) /. c₁₂ is Element of the carrier of i1
((C,c) --> (i2,a)) /. c₁₂ is Element of the carrier' of i1
((C,c) --> ((dom i2),(dom a))) /. c₁₂ is Element of the carrier of i1
(i1,{C,c},((C,c) --> (i2,a))) /. c₁₂ is Element of the carrier of i1
C is set
c is set
{C,c} is non empty set
i1 is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier' of i1 is non empty set
the carrier of i1 is non empty set
i2 is Element of the carrier' of i1
cod i2 is Element of the carrier of i1
a is Element of the carrier' of i1
(C,c) --> (i2,a) is Relation-like {C,c} -defined the carrier' of i1 -valued Function-like V18({C,c}, the carrier' of i1) Element of K19(K20({C,c}, the carrier' of i1))
K20({C,c}, the carrier' of i1) is set
K19(K20({C,c}, the carrier' of i1)) is set
(i1,{C,c},((C,c) --> (i2,a))) is Relation-like {C,c} -defined the carrier of i1 -valued Function-like V18({C,c}, the carrier of i1) Element of K19(K20({C,c}, the carrier of i1))
K20({C,c}, the carrier of i1) is set
K19(K20({C,c}, the carrier of i1)) is set
cod a is Element of the carrier of i1
(C,c) --> ((cod i2),(cod a)) is Relation-like {C,c} -defined the carrier of i1 -valued Function-like V18({C,c}, the carrier of i1) Element of K19(K20({C,c}, the carrier of i1))
( the carrier' of i1,C,i2) is Relation-like {C} -defined the carrier' of i1 -valued Function-like V18({C}, the carrier' of i1) Element of K19(K20({C}, the carrier' of i1))
{C} is non empty set
K20({C}, the carrier' of i1) is set
K19(K20({C}, the carrier' of i1)) is set
{C} --> i2 is Relation-like {C} -defined {i2} -valued Function-like V18({C},{i2}) Element of K19(K20({C},{i2}))
{i2} is non empty set
K20({C},{i2}) is set
K19(K20({C},{i2})) is set
( the carrier' of i1,c,a) is Relation-like {c} -defined the carrier' of i1 -valued Function-like V18({c}, the carrier' of i1) Element of K19(K20({c}, the carrier' of i1))
{c} is non empty set
K20({c}, the carrier' of i1) is set
K19(K20({c}, the carrier' of i1)) is set
{c} --> a is Relation-like {c} -defined {a} -valued Function-like V18({c},{a}) Element of K19(K20({c},{a}))
{a} is non empty set
K20({c},{a}) is set
K19(K20({c},{a})) is set
( the carrier of i1,C,(cod i2)) is Relation-like {C} -defined the carrier of i1 -valued Function-like V18({C}, the carrier of i1) Element of K19(K20({C}, the carrier of i1))
K20({C}, the carrier of i1) is set
K19(K20({C}, the carrier of i1)) is set
{C} --> (cod i2) is Relation-like {C} -defined {(cod i2)} -valued Function-like V18({C},{(cod i2)}) Element of K19(K20({C},{(cod i2)}))
{(cod i2)} is non empty set
K20({C},{(cod i2)}) is set
K19(K20({C},{(cod i2)})) is set
( the carrier of i1,c,(cod a)) is Relation-like {c} -defined the carrier of i1 -valued Function-like V18({c}, the carrier of i1) Element of K19(K20({c}, the carrier of i1))
K20({c}, the carrier of i1) is set
K19(K20({c}, the carrier of i1)) is set
{c} --> (cod a) is Relation-like {c} -defined {(cod a)} -valued Function-like V18({c},{(cod a)}) Element of K19(K20({c},{(cod a)}))
{(cod a)} is non empty set
K20({c},{(cod a)}) is set
K19(K20({c},{(cod a)})) is set
dom ( the carrier' of i1,c,a) is set
dom ( the carrier of i1,c,(cod a)) is set
( the carrier of i1,C,(cod i2)) +* ( the carrier of i1,c,(cod a)) is Relation-like Function-like set
( the carrier' of i1,C,i2) +* ( the carrier' of i1,c,a) is Relation-like Function-like set
dom ( the carrier' of i1,C,i2) is set
c₁₂ is set
dom ((C,c) --> (i2,a)) is set
((C,c) --> (i2,a)) . c₁₂ is set
( the carrier' of i1,C,i2) . c₁₂ is set
((C,c) --> ((cod i2),(cod a))) . c₁₂ is set
( the carrier of i1,C,(cod i2)) . c₁₂ is set
((C,c) --> (i2,a)) /. c₁₂ is Element of the carrier' of i1
((C,c) --> ((cod i2),(cod a))) /. c₁₂ is Element of the carrier of i1
((C,c) --> (i2,a)) . c₁₂ is set
( the carrier' of i1,c,a) . c₁₂ is set
((C,c) --> ((cod i2),(cod a))) . c₁₂ is set
( the carrier of i1,c,(cod a)) . c₁₂ is set
((C,c) --> (i2,a)) /. c₁₂ is Element of the carrier' of i1
((C,c) --> ((cod i2),(cod a))) /. c₁₂ is Element of the carrier of i1
((C,c) --> (i2,a)) /. c₁₂ is Element of the carrier' of i1
((C,c) --> ((cod i2),(cod a))) /. c₁₂ is Element of the carrier of i1
((C,c) --> (i2,a)) /. c₁₂ is Element of the carrier' of i1
((C,c) --> ((cod i2),(cod a))) /. c₁₂ is Element of the carrier of i1
(i1,{C,c},((C,c) --> (i2,a))) /. c₁₂ is Element of the carrier of i1
c is set
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier' of C is non empty set
K20(c, the carrier' of C) is set
K19(K20(c, the carrier' of C)) is set
C opp is non empty non void V52() strict Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like V18( the carrier' of C, the carrier of C) Element of K19(K20( the carrier' of C, the carrier of C))
K20( the carrier' of C, the carrier of C) is set
K19(K20( the carrier' of C, the carrier of C)) is set
the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like V18( the carrier' of C, the carrier of C) Element of K19(K20( the carrier' of C, the carrier of C))
the Comp of C is Relation-like K20( the carrier' of C, the carrier' of C) -defined the carrier' of C -valued Function-like Element of K19(K20(K20( the carrier' of C, the carrier' of C), the carrier' of C))
K20( the carrier' of C, the carrier' of C) is set
K20(K20( the carrier' of C, the carrier' of C), the carrier' of C) is set
K19(K20(K20( the carrier' of C, the carrier' of C), the carrier' of C)) is set
~ the Comp of C is Relation-like K20( the carrier' of C, the carrier' of C) -defined the carrier' of C -valued Function-like Element of K19(K20(K20( the carrier' of C, the carrier' of C), the carrier' of C))
CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,(~ the Comp of C) #) is strict CatStr
the carrier' of (C opp) is non empty set
K20(c, the carrier' of (C opp)) is set
K19(K20(c, the carrier' of (C opp))) is set
i1 is Relation-like c -defined the carrier' of C -valued Function-like V18(c, the carrier' of C) Element of K19(K20(c, the carrier' of C))
C is set
c is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier' of c is non empty set
c opp is non empty non void V52() strict Category-like V65() V66() V67() with_identities CatStr
the carrier of c is non empty set
the Target of c is Relation-like the carrier' of c -defined the carrier of c -valued Function-like V18( the carrier' of c, the carrier of c) Element of K19(K20( the carrier' of c, the carrier of c))
K20( the carrier' of c, the carrier of c) is set
K19(K20( the carrier' of c, the carrier of c)) is set
the Source of c is Relation-like the carrier' of c -defined the carrier of c -valued Function-like V18( the carrier' of c, the carrier of c) Element of K19(K20( the carrier' of c, the carrier of c))
the Comp of c is Relation-like K20( the carrier' of c, the carrier' of c) -defined the carrier' of c -valued Function-like Element of K19(K20(K20( the carrier' of c, the carrier' of c), the carrier' of c))
K20( the carrier' of c, the carrier' of c) is set
K20(K20( the carrier' of c, the carrier' of c), the carrier' of c) is set
K19(K20(K20( the carrier' of c, the carrier' of c), the carrier' of c)) is set
~ the Comp of c is Relation-like K20( the carrier' of c, the carrier' of c) -defined the carrier' of c -valued Function-like Element of K19(K20(K20( the carrier' of c, the carrier' of c), the carrier' of c))
CatStr(# the carrier of c, the carrier' of c, the Target of c, the Source of c,(~ the Comp of c) #) is strict CatStr
the carrier' of (c opp) is non empty set
i1 is Element of the carrier' of c
C --> i1 is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) Element of K19(K20(C, the carrier' of c))
K20(C, the carrier' of c) is set
K19(K20(C, the carrier' of c)) is set
{i1} is non empty set
K20(C,{i1}) is set
(c,C,(C --> i1)) is Relation-like C -defined the carrier' of (c opp) -valued Function-like V18(C, the carrier' of (c opp)) Element of K19(K20(C, the carrier' of (c opp)))
K20(C, the carrier' of (c opp)) is set
K19(K20(C, the carrier' of (c opp))) is set
i1 opp is Element of the carrier' of (c opp)
C --> (i1 opp) is Relation-like C -defined the carrier' of (c opp) -valued Function-like V18(C, the carrier' of (c opp)) Element of K19(K20(C, the carrier' of (c opp)))
{(i1 opp)} is non empty set
K20(C,{(i1 opp)}) is set
b is set
(C --> i1) /. b is Element of the carrier' of c
(C --> (i1 opp)) /. b is Element of the carrier' of (c opp)
(c,C,(C --> i1)) /. b is Element of the carrier' of (c opp)
C is set
c is set
{C,c} is non empty set
i1 is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier' of i1 is non empty set
i1 opp is non empty non void V52() strict Category-like V65() V66() V67() with_identities CatStr
the carrier of i1 is non empty set
the Target of i1 is Relation-like the carrier' of i1 -defined the carrier of i1 -valued Function-like V18( the carrier' of i1, the carrier of i1) Element of K19(K20( the carrier' of i1, the carrier of i1))
K20( the carrier' of i1, the carrier of i1) is set
K19(K20( the carrier' of i1, the carrier of i1)) is set
the Source of i1 is Relation-like the carrier' of i1 -defined the carrier of i1 -valued Function-like V18( the carrier' of i1, the carrier of i1) Element of K19(K20( the carrier' of i1, the carrier of i1))
the Comp of i1 is Relation-like K20( the carrier' of i1, the carrier' of i1) -defined the carrier' of i1 -valued Function-like Element of K19(K20(K20( the carrier' of i1, the carrier' of i1), the carrier' of i1))
K20( the carrier' of i1, the carrier' of i1) is set
K20(K20( the carrier' of i1, the carrier' of i1), the carrier' of i1) is set
K19(K20(K20( the carrier' of i1, the carrier' of i1), the carrier' of i1)) is set
~ the Comp of i1 is Relation-like K20( the carrier' of i1, the carrier' of i1) -defined the carrier' of i1 -valued Function-like Element of K19(K20(K20( the carrier' of i1, the carrier' of i1), the carrier' of i1))
CatStr(# the carrier of i1, the carrier' of i1, the Target of i1, the Source of i1,(~ the Comp of i1) #) is strict CatStr
the carrier' of (i1 opp) is non empty set
i2 is Element of the carrier' of i1
i2 opp is Element of the carrier' of (i1 opp)
a is Element of the carrier' of i1
(C,c) --> (i2,a) is Relation-like {C,c} -defined the carrier' of i1 -valued Function-like V18({C,c}, the carrier' of i1) Element of K19(K20({C,c}, the carrier' of i1))
K20({C,c}, the carrier' of i1) is set
K19(K20({C,c}, the carrier' of i1)) is set
(i1,{C,c},((C,c) --> (i2,a))) is Relation-like {C,c} -defined the carrier' of (i1 opp) -valued Function-like V18({C,c}, the carrier' of (i1 opp)) Element of K19(K20({C,c}, the carrier' of (i1 opp)))
K20({C,c}, the carrier' of (i1 opp)) is set
K19(K20({C,c}, the carrier' of (i1 opp))) is set
a opp is Element of the carrier' of (i1 opp)
(C,c) --> ((i2 opp),(a opp)) is Relation-like {C,c} -defined the carrier' of (i1 opp) -valued Function-like V18({C,c}, the carrier' of (i1 opp)) Element of K19(K20({C,c}, the carrier' of (i1 opp)))
g is set
((C,c) --> (i2,a)) /. g is Element of the carrier' of i1
((C,c) --> ((i2 opp),(a opp))) /. g is Element of the carrier' of (i1 opp)
(i1,{C,c},((C,c) --> (i2,a))) /. g is Element of the carrier' of (i1 opp)
C is set
c is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier' of c is non empty set
K20(C, the carrier' of c) is set
K19(K20(C, the carrier' of c)) is set
c opp is non empty non void V52() strict Category-like V65() V66() V67() with_identities CatStr
the carrier of c is non empty set
the Target of c is Relation-like the carrier' of c -defined the carrier of c -valued Function-like V18( the carrier' of c, the carrier of c) Element of K19(K20( the carrier' of c, the carrier of c))
K20( the carrier' of c, the carrier of c) is set
K19(K20( the carrier' of c, the carrier of c)) is set
the Source of c is Relation-like the carrier' of c -defined the carrier of c -valued Function-like V18( the carrier' of c, the carrier of c) Element of K19(K20( the carrier' of c, the carrier of c))
the Comp of c is Relation-like K20( the carrier' of c, the carrier' of c) -defined the carrier' of c -valued Function-like Element of K19(K20(K20( the carrier' of c, the carrier' of c), the carrier' of c))
K20( the carrier' of c, the carrier' of c) is set
K20(K20( the carrier' of c, the carrier' of c), the carrier' of c) is set
K19(K20(K20( the carrier' of c, the carrier' of c), the carrier' of c)) is set
~ the Comp of c is Relation-like K20( the carrier' of c, the carrier' of c) -defined the carrier' of c -valued Function-like Element of K19(K20(K20( the carrier' of c, the carrier' of c), the carrier' of c))
CatStr(# the carrier of c, the carrier' of c, the Target of c, the Source of c,(~ the Comp of c) #) is strict CatStr
(c opp) opp is non empty non void V52() strict Category-like V65() V66() V67() with_identities CatStr
the carrier of (c opp) is non empty set
the carrier' of (c opp) is non empty set
the Target of (c opp) is Relation-like the carrier' of (c opp) -defined the carrier of (c opp) -valued Function-like V18( the carrier' of (c opp), the carrier of (c opp)) Element of K19(K20( the carrier' of (c opp), the carrier of (c opp)))
K20( the carrier' of (c opp), the carrier of (c opp)) is set
K19(K20( the carrier' of (c opp), the carrier of (c opp))) is set
the Source of (c opp) is Relation-like the carrier' of (c opp) -defined the carrier of (c opp) -valued Function-like V18( the carrier' of (c opp), the carrier of (c opp)) Element of K19(K20( the carrier' of (c opp), the carrier of (c opp)))
the Comp of (c opp) is Relation-like K20( the carrier' of (c opp), the carrier' of (c opp)) -defined the carrier' of (c opp) -valued Function-like Element of K19(K20(K20( the carrier' of (c opp), the carrier' of (c opp)), the carrier' of (c opp)))
K20( the carrier' of (c opp), the carrier' of (c opp)) is set
K20(K20( the carrier' of (c opp), the carrier' of (c opp)), the carrier' of (c opp)) is set
K19(K20(K20( the carrier' of (c opp), the carrier' of (c opp)), the carrier' of (c opp))) is set
~ the Comp of (c opp) is Relation-like K20( the carrier' of (c opp), the carrier' of (c opp)) -defined the carrier' of (c opp) -valued Function-like Element of K19(K20(K20( the carrier' of (c opp), the carrier' of (c opp)), the carrier' of (c opp)))
CatStr(# the carrier of (c opp), the carrier' of (c opp), the Target of (c opp), the Source of (c opp),(~ the Comp of (c opp)) #) is strict CatStr
the carrier' of ((c opp) opp) is non empty set
i1 is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) Element of K19(K20(C, the carrier' of c))
(c,C,i1) is Relation-like C -defined the carrier' of (c opp) -valued Function-like V18(C, the carrier' of (c opp)) Element of K19(K20(C, the carrier' of (c opp)))
K20(C, the carrier' of (c opp)) is set
K19(K20(C, the carrier' of (c opp))) is set
((c opp),C,(c,C,i1)) is Relation-like C -defined the carrier' of ((c opp) opp) -valued Function-like V18(C, the carrier' of ((c opp) opp)) Element of K19(K20(C, the carrier' of ((c opp) opp)))
K20(C, the carrier' of ((c opp) opp)) is set
K19(K20(C, the carrier' of ((c opp) opp))) is set
i2 is set
((c opp),C,(c,C,i1)) /. i2 is Element of the carrier' of ((c opp) opp)
(c,C,i1) /. i2 is Element of the carrier' of (c opp)
((c,C,i1) /. i2) opp is Element of the carrier' of ((c opp) opp)
i1 /. i2 is Element of the carrier' of c
(i1 /. i2) opp is Element of the carrier' of (c opp)
((i1 /. i2) opp) opp is Element of the carrier' of ((c opp) opp)
c is set
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
C opp is non empty non void V52() strict Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
the carrier' of C is non empty set
the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like V18( the carrier' of C, the carrier of C) Element of K19(K20( the carrier' of C, the carrier of C))
K20( the carrier' of C, the carrier of C) is set
K19(K20( the carrier' of C, the carrier of C)) is set
the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like V18( the carrier' of C, the carrier of C) Element of K19(K20( the carrier' of C, the carrier of C))
the Comp of C is Relation-like K20( the carrier' of C, the carrier' of C) -defined the carrier' of C -valued Function-like Element of K19(K20(K20( the carrier' of C, the carrier' of C), the carrier' of C))
K20( the carrier' of C, the carrier' of C) is set
K20(K20( the carrier' of C, the carrier' of C), the carrier' of C) is set
K19(K20(K20( the carrier' of C, the carrier' of C), the carrier' of C)) is set
~ the Comp of C is Relation-like K20( the carrier' of C, the carrier' of C) -defined the carrier' of C -valued Function-like Element of K19(K20(K20( the carrier' of C, the carrier' of C), the carrier' of C))
CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,(~ the Comp of C) #) is strict CatStr
the carrier' of (C opp) is non empty set
K20(c, the carrier' of (C opp)) is set
K19(K20(c, the carrier' of (C opp))) is set
K20(c, the carrier' of C) is set
K19(K20(c, the carrier' of C)) is set
i1 is Relation-like c -defined the carrier' of (C opp) -valued Function-like V18(c, the carrier' of (C opp)) Element of K19(K20(c, the carrier' of (C opp)))
C is set
c is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
c opp is non empty non void V52() strict Category-like V65() V66() V67() with_identities CatStr
the carrier of c is non empty set
the carrier' of c is non empty set
the Target of c is Relation-like the carrier' of c -defined the carrier of c -valued Function-like V18( the carrier' of c, the carrier of c) Element of K19(K20( the carrier' of c, the carrier of c))
K20( the carrier' of c, the carrier of c) is set
K19(K20( the carrier' of c, the carrier of c)) is set
the Source of c is Relation-like the carrier' of c -defined the carrier of c -valued Function-like V18( the carrier' of c, the carrier of c) Element of K19(K20( the carrier' of c, the carrier of c))
the Comp of c is Relation-like K20( the carrier' of c, the carrier' of c) -defined the carrier' of c -valued Function-like Element of K19(K20(K20( the carrier' of c, the carrier' of c), the carrier' of c))
K20( the carrier' of c, the carrier' of c) is set
K20(K20( the carrier' of c, the carrier' of c), the carrier' of c) is set
K19(K20(K20( the carrier' of c, the carrier' of c), the carrier' of c)) is set
~ the Comp of c is Relation-like K20( the carrier' of c, the carrier' of c) -defined the carrier' of c -valued Function-like Element of K19(K20(K20( the carrier' of c, the carrier' of c), the carrier' of c))
CatStr(# the carrier of c, the carrier' of c, the Target of c, the Source of c,(~ the Comp of c) #) is strict CatStr
the carrier' of (c opp) is non empty set
i1 is Element of the carrier' of (c opp)
C --> i1 is Relation-like C -defined the carrier' of (c opp) -valued Function-like V18(C, the carrier' of (c opp)) Element of K19(K20(C, the carrier' of (c opp)))
K20(C, the carrier' of (c opp)) is set
K19(K20(C, the carrier' of (c opp))) is set
{i1} is non empty set
K20(C,{i1}) is set
(c,C,(C --> i1)) is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) Element of K19(K20(C, the carrier' of c))
K20(C, the carrier' of c) is set
K19(K20(C, the carrier' of c)) is set
opp i1 is Element of the carrier' of c
i1 opp is Element of the carrier' of ((c opp) opp)
(c opp) opp is non empty non void V52() strict Category-like V65() V66() V67() with_identities CatStr
the carrier of (c opp) is non empty set
the Target of (c opp) is Relation-like the carrier' of (c opp) -defined the carrier of (c opp) -valued Function-like V18( the carrier' of (c opp), the carrier of (c opp)) Element of K19(K20( the carrier' of (c opp), the carrier of (c opp)))
K20( the carrier' of (c opp), the carrier of (c opp)) is set
K19(K20( the carrier' of (c opp), the carrier of (c opp))) is set
the Source of (c opp) is Relation-like the carrier' of (c opp) -defined the carrier of (c opp) -valued Function-like V18( the carrier' of (c opp), the carrier of (c opp)) Element of K19(K20( the carrier' of (c opp), the carrier of (c opp)))
the Comp of (c opp) is Relation-like K20( the carrier' of (c opp), the carrier' of (c opp)) -defined the carrier' of (c opp) -valued Function-like Element of K19(K20(K20( the carrier' of (c opp), the carrier' of (c opp)), the carrier' of (c opp)))
K20( the carrier' of (c opp), the carrier' of (c opp)) is set
K20(K20( the carrier' of (c opp), the carrier' of (c opp)), the carrier' of (c opp)) is set
K19(K20(K20( the carrier' of (c opp), the carrier' of (c opp)), the carrier' of (c opp))) is set
~ the Comp of (c opp) is Relation-like K20( the carrier' of (c opp), the carrier' of (c opp)) -defined the carrier' of (c opp) -valued Function-like Element of K19(K20(K20( the carrier' of (c opp), the carrier' of (c opp)), the carrier' of (c opp)))
CatStr(# the carrier of (c opp), the carrier' of (c opp), the Target of (c opp), the Source of (c opp),(~ the Comp of (c opp)) #) is strict CatStr
the carrier' of ((c opp) opp) is non empty set
C --> (opp i1) is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) Element of K19(K20(C, the carrier' of c))
{(opp i1)} is non empty set
K20(C,{(opp i1)}) is set
b is set
(C --> i1) /. b is Element of the carrier' of (c opp)
(C --> (opp i1)) /. b is Element of the carrier' of c
(c,C,(C --> i1)) /. b is Element of the carrier' of c
C is set
c is set
{C,c} is non empty set
i1 is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
i1 opp is non empty non void V52() strict Category-like V65() V66() V67() with_identities CatStr
the carrier of i1 is non empty set
the carrier' of i1 is non empty set
the Target of i1 is Relation-like the carrier' of i1 -defined the carrier of i1 -valued Function-like V18( the carrier' of i1, the carrier of i1) Element of K19(K20( the carrier' of i1, the carrier of i1))
K20( the carrier' of i1, the carrier of i1) is set
K19(K20( the carrier' of i1, the carrier of i1)) is set
the Source of i1 is Relation-like the carrier' of i1 -defined the carrier of i1 -valued Function-like V18( the carrier' of i1, the carrier of i1) Element of K19(K20( the carrier' of i1, the carrier of i1))
the Comp of i1 is Relation-like K20( the carrier' of i1, the carrier' of i1) -defined the carrier' of i1 -valued Function-like Element of K19(K20(K20( the carrier' of i1, the carrier' of i1), the carrier' of i1))
K20( the carrier' of i1, the carrier' of i1) is set
K20(K20( the carrier' of i1, the carrier' of i1), the carrier' of i1) is set
K19(K20(K20( the carrier' of i1, the carrier' of i1), the carrier' of i1)) is set
~ the Comp of i1 is Relation-like K20( the carrier' of i1, the carrier' of i1) -defined the carrier' of i1 -valued Function-like Element of K19(K20(K20( the carrier' of i1, the carrier' of i1), the carrier' of i1))
CatStr(# the carrier of i1, the carrier' of i1, the Target of i1, the Source of i1,(~ the Comp of i1) #) is strict CatStr
the carrier' of (i1 opp) is non empty set
i2 is Element of the carrier' of (i1 opp)
a is Element of the carrier' of (i1 opp)
(C,c) --> (i2,a) is Relation-like {C,c} -defined the carrier' of (i1 opp) -valued Function-like V18({C,c}, the carrier' of (i1 opp)) Element of K19(K20({C,c}, the carrier' of (i1 opp)))
K20({C,c}, the carrier' of (i1 opp)) is set
K19(K20({C,c}, the carrier' of (i1 opp))) is set
(i1,{C,c},((C,c) --> (i2,a))) is Relation-like {C,c} -defined the carrier' of i1 -valued Function-like V18({C,c}, the carrier' of i1) Element of K19(K20({C,c}, the carrier' of i1))
K20({C,c}, the carrier' of i1) is set
K19(K20({C,c}, the carrier' of i1)) is set
opp i2 is Element of the carrier' of i1
i2 opp is Element of the carrier' of ((i1 opp) opp)
(i1 opp) opp is non empty non void V52() strict Category-like V65() V66() V67() with_identities CatStr
the carrier of (i1 opp) is non empty set
the Target of (i1 opp) is Relation-like the carrier' of (i1 opp) -defined the carrier of (i1 opp) -valued Function-like V18( the carrier' of (i1 opp), the carrier of (i1 opp)) Element of K19(K20( the carrier' of (i1 opp), the carrier of (i1 opp)))
K20( the carrier' of (i1 opp), the carrier of (i1 opp)) is set
K19(K20( the carrier' of (i1 opp), the carrier of (i1 opp))) is set
the Source of (i1 opp) is Relation-like the carrier' of (i1 opp) -defined the carrier of (i1 opp) -valued Function-like V18( the carrier' of (i1 opp), the carrier of (i1 opp)) Element of K19(K20( the carrier' of (i1 opp), the carrier of (i1 opp)))
the Comp of (i1 opp) is Relation-like K20( the carrier' of (i1 opp), the carrier' of (i1 opp)) -defined the carrier' of (i1 opp) -valued Function-like Element of K19(K20(K20( the carrier' of (i1 opp), the carrier' of (i1 opp)), the carrier' of (i1 opp)))
K20( the carrier' of (i1 opp), the carrier' of (i1 opp)) is set
K20(K20( the carrier' of (i1 opp), the carrier' of (i1 opp)), the carrier' of (i1 opp)) is set
K19(K20(K20( the carrier' of (i1 opp), the carrier' of (i1 opp)), the carrier' of (i1 opp))) is set
~ the Comp of (i1 opp) is Relation-like K20( the carrier' of (i1 opp), the carrier' of (i1 opp)) -defined the carrier' of (i1 opp) -valued Function-like Element of K19(K20(K20( the carrier' of (i1 opp), the carrier' of (i1 opp)), the carrier' of (i1 opp)))
CatStr(# the carrier of (i1 opp), the carrier' of (i1 opp), the Target of (i1 opp), the Source of (i1 opp),(~ the Comp of (i1 opp)) #) is strict CatStr
the carrier' of ((i1 opp) opp) is non empty set
opp a is Element of the carrier' of i1
a opp is Element of the carrier' of ((i1 opp) opp)
(C,c) --> ((opp i2),(opp a)) is Relation-like {C,c} -defined the carrier' of i1 -valued Function-like V18({C,c}, the carrier' of i1) Element of K19(K20({C,c}, the carrier' of i1))
g is set
((C,c) --> (i2,a)) /. g is Element of the carrier' of (i1 opp)
((C,c) --> ((opp i2),(opp a))) /. g is Element of the carrier' of i1
(i1,{C,c},((C,c) --> (i2,a))) /. g is Element of the carrier' of i1
C is set
c is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier' of c is non empty set
K20(C, the carrier' of c) is set
K19(K20(C, the carrier' of c)) is set
i1 is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) Element of K19(K20(C, the carrier' of c))
(c,C,i1) is Relation-like C -defined the carrier' of (c opp) -valued Function-like V18(C, the carrier' of (c opp)) Element of K19(K20(C, the carrier' of (c opp)))
c opp is non empty non void V52() strict Category-like V65() V66() V67() with_identities CatStr
the carrier of c is non empty set
the Target of c is Relation-like the carrier' of c -defined the carrier of c -valued Function-like V18( the carrier' of c, the carrier of c) Element of K19(K20( the carrier' of c, the carrier of c))
K20( the carrier' of c, the carrier of c) is set
K19(K20( the carrier' of c, the carrier of c)) is set
the Source of c is Relation-like the carrier' of c -defined the carrier of c -valued Function-like V18( the carrier' of c, the carrier of c) Element of K19(K20( the carrier' of c, the carrier of c))
the Comp of c is Relation-like K20( the carrier' of c, the carrier' of c) -defined the carrier' of c -valued Function-like Element of K19(K20(K20( the carrier' of c, the carrier' of c), the carrier' of c))
K20( the carrier' of c, the carrier' of c) is set
K20(K20( the carrier' of c, the carrier' of c), the carrier' of c) is set
K19(K20(K20( the carrier' of c, the carrier' of c), the carrier' of c)) is set
~ the Comp of c is Relation-like K20( the carrier' of c, the carrier' of c) -defined the carrier' of c -valued Function-like Element of K19(K20(K20( the carrier' of c, the carrier' of c), the carrier' of c))
CatStr(# the carrier of c, the carrier' of c, the Target of c, the Source of c,(~ the Comp of c) #) is strict CatStr
the carrier' of (c opp) is non empty set
K20(C, the carrier' of (c opp)) is set
K19(K20(C, the carrier' of (c opp))) is set
(c,C,(c,C,i1)) is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) Element of K19(K20(C, the carrier' of c))
i2 is set
(c,C,(c,C,i1)) /. i2 is Element of the carrier' of c
(c,C,i1) /. i2 is Element of the carrier' of (c opp)
opp ((c,C,i1) /. i2) is Element of the carrier' of c
((c,C,i1) /. i2) opp is Element of the carrier' of ((c opp) opp)
(c opp) opp is non empty non void V52() strict Category-like V65() V66() V67() with_identities CatStr
the carrier of (c opp) is non empty set
the Target of (c opp) is Relation-like the carrier' of (c opp) -defined the carrier of (c opp) -valued Function-like V18( the carrier' of (c opp), the carrier of (c opp)) Element of K19(K20( the carrier' of (c opp), the carrier of (c opp)))
K20( the carrier' of (c opp), the carrier of (c opp)) is set
K19(K20( the carrier' of (c opp), the carrier of (c opp))) is set
the Source of (c opp) is Relation-like the carrier' of (c opp) -defined the carrier of (c opp) -valued Function-like V18( the carrier' of (c opp), the carrier of (c opp)) Element of K19(K20( the carrier' of (c opp), the carrier of (c opp)))
the Comp of (c opp) is Relation-like K20( the carrier' of (c opp), the carrier' of (c opp)) -defined the carrier' of (c opp) -valued Function-like Element of K19(K20(K20( the carrier' of (c opp), the carrier' of (c opp)), the carrier' of (c opp)))
K20( the carrier' of (c opp), the carrier' of (c opp)) is set
K20(K20( the carrier' of (c opp), the carrier' of (c opp)), the carrier' of (c opp)) is set
K19(K20(K20( the carrier' of (c opp), the carrier' of (c opp)), the carrier' of (c opp))) is set
~ the Comp of (c opp) is Relation-like K20( the carrier' of (c opp), the carrier' of (c opp)) -defined the carrier' of (c opp) -valued Function-like Element of K19(K20(K20( the carrier' of (c opp), the carrier' of (c opp)), the carrier' of (c opp)))
CatStr(# the carrier of (c opp), the carrier' of (c opp), the Target of (c opp), the Source of (c opp),(~ the Comp of (c opp)) #) is strict CatStr
the carrier' of ((c opp) opp) is non empty set
i1 /. i2 is Element of the carrier' of c
(i1 /. i2) opp is Element of the carrier' of (c opp)
opp ((i1 /. i2) opp) is Element of the carrier' of c
((i1 /. i2) opp) opp is Element of the carrier' of ((c opp) opp)
c is set
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier' of C is non empty set
K20(c, the carrier' of C) is set
K19(K20(c, the carrier' of C)) is set
i2 is Element of the carrier' of C
i1 is Relation-like c -defined the carrier' of C -valued Function-like V18(c, the carrier' of C) Element of K19(K20(c, the carrier' of C))
C is set
c is set
{C,c} is non empty set
i1 is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier' of i1 is non empty set
i2 is Element of the carrier' of i1
a is Element of the carrier' of i1
(C,c) --> (i2,a) is Relation-like {C,c} -defined the carrier' of i1 -valued Function-like V18({C,c}, the carrier' of i1) Element of K19(K20({C,c}, the carrier' of i1))
K20({C,c}, the carrier' of i1) is set
K19(K20({C,c}, the carrier' of i1)) is set
b is Element of the carrier' of i1
(i1,{C,c},((C,c) --> (i2,a)),b) is Relation-like {C,c} -defined the carrier' of i1 -valued Function-like V18({C,c}, the carrier' of i1) Element of K19(K20({C,c}, the carrier' of i1))
i2 (*) b is Element of the carrier' of i1
a (*) b is Element of the carrier' of i1
(C,c) --> ((i2 (*) b),(a (*) b)) is Relation-like {C,c} -defined the carrier' of i1 -valued Function-like V18({C,c}, the carrier' of i1) Element of K19(K20({C,c}, the carrier' of i1))
h is set
((C,c) --> (i2,a)) /. h is Element of the carrier' of i1
((C,c) --> ((i2 (*) b),(a (*) b))) /. h is Element of the carrier' of i1
(i1,{C,c},((C,c) --> (i2,a)),b) /. h is Element of the carrier' of i1
C is set
c is set
{C,c} is non empty set
i1 is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier' of i1 is non empty set
i2 is Element of the carrier' of i1
a is Element of the carrier' of i1
i2 (*) a is Element of the carrier' of i1
b is Element of the carrier' of i1
(C,c) --> (a,b) is Relation-like {C,c} -defined the carrier' of i1 -valued Function-like V18({C,c}, the carrier' of i1) Element of K19(K20({C,c}, the carrier' of i1))
K20({C,c}, the carrier' of i1) is set
K19(K20({C,c}, the carrier' of i1)) is set
(i1,{C,c},((C,c) --> (a,b)),i2) is Relation-like {C,c} -defined the carrier' of i1 -valued Function-like V18({C,c}, the carrier' of i1) Element of K19(K20({C,c}, the carrier' of i1))
i2 (*) b is Element of the carrier' of i1
(C,c) --> ((i2 (*) a),(i2 (*) b)) is Relation-like {C,c} -defined the carrier' of i1 -valued Function-like V18({C,c}, the carrier' of i1) Element of K19(K20({C,c}, the carrier' of i1))
h is set
((C,c) --> (a,b)) /. h is Element of the carrier' of i1
((C,c) --> ((i2 (*) a),(i2 (*) b))) /. h is Element of the carrier' of i1
(i1,{C,c},((C,c) --> (a,b)),i2) /. h is Element of the carrier' of i1
C is set
c is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier' of c is non empty set
K20(C, the carrier' of c) is set
K19(K20(C, the carrier' of c)) is set
the carrier of c is non empty set
i1 is Element of the carrier' of c
cod i1 is Element of the carrier of c
C --> (cod i1) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
K20(C, the carrier of c) is set
K19(K20(C, the carrier of c)) is set
{(cod i1)} is non empty set
K20(C,{(cod i1)}) is set
dom i1 is Element of the carrier of c
C --> (dom i1) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
{(dom i1)} is non empty set
K20(C,{(dom i1)}) is set
i2 is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) Element of K19(K20(C, the carrier' of c))
(c,C,i2) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
(c,C,i2,i1) is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) Element of K19(K20(C, the carrier' of c))
(c,C,(c,C,i2,i1)) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
(c,C,(c,C,i2,i1)) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
(c,C,i2) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
a is set
i2 /. a is Element of the carrier' of c
dom (i2 /. a) is Element of the carrier of c
(C --> (cod i1)) /. a is Element of the carrier of c
(c,C,(c,C,i2,i1)) /. a is Element of the carrier of c
(c,C,i2,i1) /. a is Element of the carrier' of c
dom ((c,C,i2,i1) /. a) is Element of the carrier of c
(i2 /. a) (*) i1 is Element of the carrier' of c
dom ((i2 /. a) (*) i1) is Element of the carrier of c
(C --> (dom i1)) /. a is Element of the carrier of c
a is set
i2 /. a is Element of the carrier' of c
dom (i2 /. a) is Element of the carrier of c
(C --> (cod i1)) /. a is Element of the carrier of c
(c,C,i2) /. a is Element of the carrier of c
cod (i2 /. a) is Element of the carrier of c
(i2 /. a) (*) i1 is Element of the carrier' of c
cod ((i2 /. a) (*) i1) is Element of the carrier of c
(c,C,i2,i1) /. a is Element of the carrier' of c
cod ((c,C,i2,i1) /. a) is Element of the carrier of c
(c,C,(c,C,i2,i1)) /. a is Element of the carrier of c
C is set
c is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier' of c is non empty set
K20(C, the carrier' of c) is set
K19(K20(C, the carrier' of c)) is set
the carrier of c is non empty set
i1 is Element of the carrier' of c
dom i1 is Element of the carrier of c
C --> (dom i1) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
K20(C, the carrier of c) is set
K19(K20(C, the carrier of c)) is set
{(dom i1)} is non empty set
K20(C,{(dom i1)}) is set
cod i1 is Element of the carrier of c
C --> (cod i1) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
{(cod i1)} is non empty set
K20(C,{(cod i1)}) is set
i2 is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) Element of K19(K20(C, the carrier' of c))
(c,C,i2) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
(c,C,i2,i1) is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) Element of K19(K20(C, the carrier' of c))
(c,C,(c,C,i2,i1)) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
(c,C,i2) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
(c,C,(c,C,i2,i1)) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
a is set
i2 /. a is Element of the carrier' of c
cod (i2 /. a) is Element of the carrier of c
(C --> (dom i1)) /. a is Element of the carrier of c
(c,C,i2) /. a is Element of the carrier of c
dom (i2 /. a) is Element of the carrier of c
i1 (*) (i2 /. a) is Element of the carrier' of c
dom (i1 (*) (i2 /. a)) is Element of the carrier of c
(c,C,i2,i1) /. a is Element of the carrier' of c
dom ((c,C,i2,i1) /. a) is Element of the carrier of c
(c,C,(c,C,i2,i1)) /. a is Element of the carrier of c
a is set
i2 /. a is Element of the carrier' of c
cod (i2 /. a) is Element of the carrier of c
(C --> (dom i1)) /. a is Element of the carrier of c
(c,C,(c,C,i2,i1)) /. a is Element of the carrier of c
(c,C,i2,i1) /. a is Element of the carrier' of c
cod ((c,C,i2,i1) /. a) is Element of the carrier of c
i1 (*) (i2 /. a) is Element of the carrier' of c
cod (i1 (*) (i2 /. a)) is Element of the carrier of c
(C --> (cod i1)) /. a is Element of the carrier of c
c is set
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier' of C is non empty set
K20(c, the carrier' of C) is set
K19(K20(c, the carrier' of C)) is set
i2 is Relation-like c -defined the carrier' of C -valued Function-like V18(c, the carrier' of C) Element of K19(K20(c, the carrier' of C))
i1 is Relation-like c -defined the carrier' of C -valued Function-like V18(c, the carrier' of C) Element of K19(K20(c, the carrier' of C))
C is set
c is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier' of c is non empty set
K20(C, the carrier' of c) is set
K19(K20(C, the carrier' of c)) is set
the carrier of c is non empty set
i1 is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) Element of K19(K20(C, the carrier' of c))
(c,C,i1) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
K20(C, the carrier of c) is set
K19(K20(C, the carrier of c)) is set
i2 is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) Element of K19(K20(C, the carrier' of c))
(c,C,i2) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
(c,C,i1,i2) is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) Element of K19(K20(C, the carrier' of c))
(c,C,(c,C,i1,i2)) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
(c,C,i2) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
(c,C,(c,C,i1,i2)) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
(c,C,i1) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
a is set
i2 /. a is Element of the carrier' of c
cod (i2 /. a) is Element of the carrier of c
(c,C,i1) /. a is Element of the carrier of c
i1 /. a is Element of the carrier' of c
dom (i1 /. a) is Element of the carrier of c
(c,C,(c,C,i1,i2)) /. a is Element of the carrier of c
(c,C,i1,i2) /. a is Element of the carrier' of c
dom ((c,C,i1,i2) /. a) is Element of the carrier of c
(i1 /. a) (*) (i2 /. a) is Element of the carrier' of c
dom ((i1 /. a) (*) (i2 /. a)) is Element of the carrier of c
dom (i2 /. a) is Element of the carrier of c
(c,C,i2) /. a is Element of the carrier of c
a is set
i2 /. a is Element of the carrier' of c
cod (i2 /. a) is Element of the carrier of c
(c,C,i1) /. a is Element of the carrier of c
i1 /. a is Element of the carrier' of c
dom (i1 /. a) is Element of the carrier of c
(c,C,(c,C,i1,i2)) /. a is Element of the carrier of c
(c,C,i1,i2) /. a is Element of the carrier' of c
cod ((c,C,i1,i2) /. a) is Element of the carrier of c
(i1 /. a) (*) (i2 /. a) is Element of the carrier' of c
cod ((i1 /. a) (*) (i2 /. a)) is Element of the carrier of c
cod (i1 /. a) is Element of the carrier of c
(c,C,i1) /. a is Element of the carrier of c
C is set
c is set
{C,c} is non empty set
i1 is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier' of i1 is non empty set
i2 is Element of the carrier' of i1
a is Element of the carrier' of i1
(C,c) --> (i2,a) is Relation-like {C,c} -defined the carrier' of i1 -valued Function-like V18({C,c}, the carrier' of i1) Element of K19(K20({C,c}, the carrier' of i1))
K20({C,c}, the carrier' of i1) is set
K19(K20({C,c}, the carrier' of i1)) is set
b is Element of the carrier' of i1
i2 (*) b is Element of the carrier' of i1
f is Element of the carrier' of i1
(C,c) --> (b,f) is Relation-like {C,c} -defined the carrier' of i1 -valued Function-like V18({C,c}, the carrier' of i1) Element of K19(K20({C,c}, the carrier' of i1))
(i1,{C,c},((C,c) --> (i2,a)),((C,c) --> (b,f))) is Relation-like {C,c} -defined the carrier' of i1 -valued Function-like V18({C,c}, the carrier' of i1) Element of K19(K20({C,c}, the carrier' of i1))
a (*) f is Element of the carrier' of i1
(C,c) --> ((i2 (*) b),(a (*) f)) is Relation-like {C,c} -defined the carrier' of i1 -valued Function-like V18({C,c}, the carrier' of i1) Element of K19(K20({C,c}, the carrier' of i1))
h is set
((C,c) --> (i2,a)) /. h is Element of the carrier' of i1
((C,c) --> (b,f)) /. h is Element of the carrier' of i1
((C,c) --> ((i2 (*) b),(a (*) f))) /. h is Element of the carrier' of i1
(i1,{C,c},((C,c) --> (i2,a)),((C,c) --> (b,f))) /. h is Element of the carrier' of i1
C is set
c is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier' of c is non empty set
K20(C, the carrier' of c) is set
K19(K20(C, the carrier' of c)) is set
i1 is Element of the carrier' of c
C --> i1 is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) Element of K19(K20(C, the carrier' of c))
{i1} is non empty set
K20(C,{i1}) is set
i2 is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) Element of K19(K20(C, the carrier' of c))
(c,C,i2,i1) is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) Element of K19(K20(C, the carrier' of c))
(c,C,i2,(C --> i1)) is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) Element of K19(K20(C, the carrier' of c))
a is set
(c,C,i2,i1) /. a is Element of the carrier' of c
i2 /. a is Element of the carrier' of c
(i2 /. a) (*) i1 is Element of the carrier' of c
(C --> i1) /. a is Element of the carrier' of c
(i2 /. a) (*) ((C --> i1) /. a) is Element of the carrier' of c
(c,C,i2,(C --> i1)) /. a is Element of the carrier' of c
C is set
c is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier' of c is non empty set
K20(C, the carrier' of c) is set
K19(K20(C, the carrier' of c)) is set
i1 is Element of the carrier' of c
C --> i1 is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) Element of K19(K20(C, the carrier' of c))
{i1} is non empty set
K20(C,{i1}) is set
i2 is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) Element of K19(K20(C, the carrier' of c))
(c,C,i2,i1) is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) Element of K19(K20(C, the carrier' of c))
(c,C,(C --> i1),i2) is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) Element of K19(K20(C, the carrier' of c))
a is set
(c,C,i2,i1) /. a is Element of the carrier' of c
i2 /. a is Element of the carrier' of c
i1 (*) (i2 /. a) is Element of the carrier' of c
(C --> i1) /. a is Element of the carrier' of c
((C --> i1) /. a) (*) (i2 /. a) is Element of the carrier' of c
(c,C,(C --> i1),i2) /. a is Element of the carrier' of c
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
c is Element of the carrier of C
i1 is Element of the carrier of C
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
c is Element of the carrier of C
i1 is Element of the carrier of C
i2 is Morphism of c,i1
Hom (c,i1) is Element of K19( the carrier' of C)
the carrier' of C is non empty set
K19( the carrier' of C) is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = i1 ) } is set
Hom (i1,c) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i1 & cod b₁ = c ) } is set
id i1 is Morphism of i1,i1
a is Morphism of i1,c
i2 * a is Morphism of i1,i1
b is Element of the carrier of C
Hom (i1,b) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i1 & cod b₁ = b ) } is set
f is Morphism of i1,b
f * i2 is Morphism of c,b
g is Morphism of i1,b
g * i2 is Morphism of c,b
f * (i2 * a) is Morphism of i1,b
(g * i2) * a is Morphism of i1,b
g * (i2 * a) is Morphism of i1,b
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
c is Element of the carrier of C
i1 is Element of the carrier of C
i2 is Morphism of c,i1
Hom (c,i1) is Element of K19( the carrier' of C)
the carrier' of C is non empty set
K19( the carrier' of C) is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = i1 ) } is set
Hom (i1,c) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i1 & cod b₁ = c ) } is set
id c is Morphism of c,c
a is Morphism of i1,c
a * i2 is Morphism of c,c
b is Element of the carrier of C
Hom (b,c) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = b & cod b₁ = c ) } is set
f is Morphism of b,c
i2 * f is Morphism of b,i1
g is Morphism of b,c
i2 * g is Morphism of b,i1
(a * i2) * f is Morphism of b,c
a * (i2 * g) is Morphism of b,c
(a * i2) * g is Morphism of b,c
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
c is Element of the carrier of C
i1 is Element of the carrier of C
i2 is Element of the carrier of C
a is Morphism of c,i1
b is Morphism of i1,i2
b * a is Morphism of c,i2
Hom (c,i1) is Element of K19( the carrier' of C)
the carrier' of C is non empty set
K19( the carrier' of C) is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = i1 ) } is set
Hom (i1,c) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i1 & cod b₁ = c ) } is set
id i1 is Morphism of i1,i1
f is Morphism of i1,c
a * f is Morphism of i1,i1
Hom (i1,i2) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i1 & cod b₁ = i2 ) } is set
Hom (i2,i1) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i2 & cod b₁ = i1 ) } is set
id i2 is Morphism of i2,i2
g is Morphism of i2,i1
b * g is Morphism of i2,i2
Hom (c,i2) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = i2 ) } is set
Hom (i2,c) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i2 & cod b₁ = c ) } is set
f * g is Morphism of i2,c
(b * a) * (f * g) is Morphism of i2,i2
a * (f * g) is Morphism of i2,i1
b * (a * (f * g)) is Morphism of i2,i2
(a * f) * g is Morphism of i2,i1
b * ((a * f) * g) is Morphism of i2,i2
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
c is Element of the carrier of C
i1 is Element of the carrier of C
i2 is Element of the carrier of C
a is Morphism of c,i1
b is Morphism of i1,i2
b * a is Morphism of c,i2
Hom (c,i1) is Element of K19( the carrier' of C)
the carrier' of C is non empty set
K19( the carrier' of C) is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = i1 ) } is set
Hom (i1,c) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i1 & cod b₁ = c ) } is set
id c is Morphism of c,c
f is Morphism of i1,c
f * a is Morphism of c,c
Hom (i1,i2) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i1 & cod b₁ = i2 ) } is set
Hom (i2,i1) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i2 & cod b₁ = i1 ) } is set
id i1 is Morphism of i1,i1
g is Morphism of i2,i1
g * b is Morphism of i1,i1
Hom (c,i2) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = i2 ) } is set
Hom (i2,c) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i2 & cod b₁ = c ) } is set
f * g is Morphism of i2,c
(f * g) * (b * a) is Morphism of c,c
g * (b * a) is Morphism of c,i1
f * (g * (b * a)) is Morphism of c,c
(g * b) * a is Morphism of c,i1
f * ((g * b) * a) is Morphism of c,c
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
c is Element of the carrier of C
i1 is Element of the carrier of C
i2 is Element of the carrier of C
Hom (i1,i2) is Element of K19( the carrier' of C)
the carrier' of C is non empty set
K19( the carrier' of C) is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i1 & cod b₁ = i2 ) } is set
Hom (i2,i1) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i2 & cod b₁ = i1 ) } is set
a is Morphism of i1,i2
b is Morphism of i2,c
b * a is Morphism of i1,c
Hom (i1,c) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i1 & cod b₁ = c ) } is set
Hom (c,i1) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = i1 ) } is set
id c is Morphism of c,c
f is Morphism of c,i1
(b * a) * f is Morphism of c,c
Hom (i2,c) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i2 & cod b₁ = c ) } is set
Hom (c,i2) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = i2 ) } is set
a * f is Morphism of c,i2
b * (a * f) is Morphism of c,c
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
c is Element of the carrier of C
i1 is Element of the carrier of C
i2 is Element of the carrier of C
Hom (i1,i2) is Element of K19( the carrier' of C)
the carrier' of C is non empty set
K19( the carrier' of C) is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i1 & cod b₁ = i2 ) } is set
Hom (i2,i1) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i2 & cod b₁ = i1 ) } is set
a is Morphism of c,i1
b is Morphism of i1,i2
b * a is Morphism of c,i2
Hom (c,i2) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = i2 ) } is set
Hom (i2,c) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i2 & cod b₁ = c ) } is set
id c is Morphism of c,c
f is Morphism of i2,c
f * (b * a) is Morphism of c,c
Hom (c,i1) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = i1 ) } is set
Hom (i1,c) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i1 & cod b₁ = c ) } is set
f * b is Morphism of i1,c
(f * b) * a is Morphism of c,c
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
c is Element of the carrier of C
i1 is Element of the carrier of C
i2 is Morphism of c,i1
Hom (c,i1) is Element of K19( the carrier' of C)
the carrier' of C is non empty set
K19( the carrier' of C) is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = i1 ) } is set
Hom (i1,c) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i1 & cod b₁ = c ) } is set
id i1 is Morphism of i1,i1
a is Morphism of i1,c
i2 * a is Morphism of i1,i1
id c is Morphism of c,c
a * i2 is Morphism of c,c
i2 * (a * i2) is Morphism of c,i1
(id i1) * i2 is Morphism of c,i1
i2 * (id c) is Morphism of c,i1
Hom (c,c) is non empty Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = c ) } is set
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
c is Element of the carrier of C
i1 is Element of the carrier of C
i2 is Morphism of c,i1
Hom (c,i1) is Element of K19( the carrier' of C)
the carrier' of C is non empty set
K19( the carrier' of C) is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = i1 ) } is set
Hom (i1,c) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i1 & cod b₁ = c ) } is set
id c is Morphism of c,c
a is Morphism of i1,c
a * i2 is Morphism of c,c
id i1 is Morphism of i1,i1
i2 * a is Morphism of i1,i1
(i2 * a) * i2 is Morphism of c,i1
i2 * (id c) is Morphism of c,i1
(id i1) * i2 is Morphism of c,i1
Hom (i1,i1) is non empty Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i1 & cod b₁ = i1 ) } is set
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
c is Element of the carrier of C
i1 is Element of the carrier of C
i2 is Morphism of c,i1
Hom (c,i1) is Element of K19( the carrier' of C)
the carrier' of C is non empty set
K19( the carrier' of C) is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = i1 ) } is set
Hom (i1,c) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i1 & cod b₁ = c ) } is set
id i1 is Morphism of i1,i1
id c is Morphism of c,c
a is Morphism of i1,c
i2 * a is Morphism of i1,i1
a * i2 is Morphism of c,c
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
c is Element of the carrier of C
i1 is Element of the carrier of C
Hom (c,i1) is Element of K19( the carrier' of C)
the carrier' of C is non empty set
K19( the carrier' of C) is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = i1 ) } is set
i2 is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier' of i2 is non empty set
a is Relation-like the carrier' of C -defined the carrier' of i2 -valued Function-like V18( the carrier' of C, the carrier' of i2) Functor of C,i2
b is Morphism of c,i1
a . b is Element of the carrier' of i2
a . c is Element of the carrier of i2
the carrier of i2 is non empty set
Obj a is Relation-like the carrier of C -defined the carrier of i2 -valued Function-like V18( the carrier of C, the carrier of i2) Element of K19(K20( the carrier of C, the carrier of i2))
K20( the carrier of C, the carrier of i2) is set
K19(K20( the carrier of C, the carrier of i2)) is set
(Obj a) . c is Element of the carrier of i2
a . i1 is Element of the carrier of i2
(Obj a) . i1 is Element of the carrier of i2
Hom ((a . c),(a . i1)) is Element of K19( the carrier' of i2)
K19( the carrier' of i2) is set
{ b₁ where b₁ is Element of the carrier' of i2 : ( dom b₁ = a . c & cod b₁ = a . i1 ) } is set
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier' of C is non empty set
the carrier of C is non empty set
c is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier' of c is non empty set
i1 is Relation-like the carrier' of C -defined the carrier' of c -valued Function-like V18( the carrier' of C, the carrier' of c) Functor of C,c
i2 is Element of the carrier of C
a is Element of the carrier of C
Hom (i2,a) is Element of K19( the carrier' of C)
K19( the carrier' of C) is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i2 & cod b₁ = a ) } is set
b is Element of the carrier of C
Hom (a,b) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = a & cod b₁ = b ) } is set
i1 . i2 is Element of the carrier of c
the carrier of c is non empty set
Obj i1 is Relation-like the carrier of C -defined the carrier of c -valued Function-like V18( the carrier of C, the carrier of c) Element of K19(K20( the carrier of C, the carrier of c))
K20( the carrier of C, the carrier of c) is set
K19(K20( the carrier of C, the carrier of c)) is set
(Obj i1) . i2 is Element of the carrier of c
i1 . a is Element of the carrier of c
(Obj i1) . a is Element of the carrier of c
i1 . b is Element of the carrier of c
(Obj i1) . b is Element of the carrier of c
f is Morphism of i2,a
(C,i2,a,c,i1,f) is Morphism of i1 . i2,i1 . a
g is Morphism of a,b
g * f is Morphism of i2,b
(C,i2,b,c,i1,(g * f)) is Morphism of i1 . i2,i1 . b
(C,a,b,c,i1,g) is Morphism of i1 . a,i1 . b
(C,a,b,c,i1,g) * (C,i2,a,c,i1,f) is Morphism of i1 . i2,i1 . b
cod f is Element of the carrier of C
dom g is Element of the carrier of C
Hom (i2,b) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i2 & cod b₁ = b ) } is set
h is Element of the carrier' of C
i1 . h is Element of the carrier' of c
i is Element of the carrier' of C
i1 . i is Element of the carrier' of c
Hom ((i1 . i2),(i1 . a)) is Element of K19( the carrier' of c)
K19( the carrier' of c) is set
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = i1 . i2 & cod b₁ = i1 . a ) } is set
Hom ((i1 . a),(i1 . b)) is Element of K19( the carrier' of c)
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = i1 . a & cod b₁ = i1 . b ) } is set
h (*) i is Element of the carrier' of C
i1 . (h (*) i) is Element of the carrier' of c
(i1 . h) (*) (i1 . i) is Element of the carrier' of c
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier' of C is non empty set
the carrier of C is non empty set
c is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier' of c is non empty set
i1 is Relation-like the carrier' of C -defined the carrier' of c -valued Function-like V18( the carrier' of C, the carrier' of c) Functor of C,c
i2 is Element of the carrier of C
id i2 is Morphism of i2,i2
(C,i2,i2,c,i1,(id i2)) is Morphism of i1 . i2,i1 . i2
i1 . i2 is Element of the carrier of c
the carrier of c is non empty set
Obj i1 is Relation-like the carrier of C -defined the carrier of c -valued Function-like V18( the carrier of C, the carrier of c) Element of K19(K20( the carrier of C, the carrier of c))
K20( the carrier of C, the carrier of c) is set
K19(K20( the carrier of C, the carrier of c)) is set
(Obj i1) . i2 is Element of the carrier of c
id (i1 . i2) is Morphism of i1 . i2,i1 . i2
Hom (i2,i2) is non empty Element of K19( the carrier' of C)
K19( the carrier' of C) is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i2 & cod b₁ = i2 ) } is set
i1 . (id i2) is Element of the carrier' of c
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
the carrier' of C is non empty set
c is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier' of c is non empty set
i1 is Element of the carrier of C
i2 is Element of the carrier of C
a is Morphism of i1,i2
b is Relation-like the carrier' of C -defined the carrier' of c -valued Function-like V18( the carrier' of C, the carrier' of c) Functor of C,c
b . i1 is Element of the carrier of c
the carrier of c is non empty set
Obj b is Relation-like the carrier of C -defined the carrier of c -valued Function-like V18( the carrier of C, the carrier of c) Element of K19(K20( the carrier of C, the carrier of c))
K20( the carrier of C, the carrier of c) is set
K19(K20( the carrier of C, the carrier of c)) is set
(Obj b) . i1 is Element of the carrier of c
b . i2 is Element of the carrier of c
(Obj b) . i2 is Element of the carrier of c
(C,i1,i2,c,b,a) is Morphism of b . i1,b . i2
Hom (i1,i2) is Element of K19( the carrier' of C)
K19( the carrier' of C) is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i1 & cod b₁ = i2 ) } is set
Hom (i2,i1) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i2 & cod b₁ = i1 ) } is set
id i2 is Morphism of i2,i2
f is Morphism of i2,i1
a * f is Morphism of i2,i2
Hom ((b . i1),(b . i2)) is Element of K19( the carrier' of c)
K19( the carrier' of c) is set
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = b . i1 & cod b₁ = b . i2 ) } is set
Hom ((b . i2),(b . i1)) is Element of K19( the carrier' of c)
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = b . i2 & cod b₁ = b . i1 ) } is set
id (b . i2) is Morphism of b . i2,b . i2
(C,i2,i1,c,b,f) is Morphism of b . i2,b . i1
(C,i1,i2,c,b,a) * (C,i2,i1,c,b,f) is Morphism of b . i2,b . i2
(C,i2,i2,c,b,(id i2)) is Morphism of b . i2,b . i2
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
the carrier' of C is non empty set
c is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier' of c is non empty set
i1 is Element of the carrier of C
i2 is Element of the carrier of C
a is Morphism of i1,i2
b is Relation-like the carrier' of C -defined the carrier' of c -valued Function-like V18( the carrier' of C, the carrier' of c) Functor of C,c
b . i1 is Element of the carrier of c
the carrier of c is non empty set
Obj b is Relation-like the carrier of C -defined the carrier of c -valued Function-like V18( the carrier of C, the carrier of c) Element of K19(K20( the carrier of C, the carrier of c))
K20( the carrier of C, the carrier of c) is set
K19(K20( the carrier of C, the carrier of c)) is set
(Obj b) . i1 is Element of the carrier of c
b . i2 is Element of the carrier of c
(Obj b) . i2 is Element of the carrier of c
(C,i1,i2,c,b,a) is Morphism of b . i1,b . i2
Hom (i1,i2) is Element of K19( the carrier' of C)
K19( the carrier' of C) is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i1 & cod b₁ = i2 ) } is set
Hom (i2,i1) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i2 & cod b₁ = i1 ) } is set
id i1 is Morphism of i1,i1
f is Morphism of i2,i1
f * a is Morphism of i1,i1
Hom ((b . i1),(b . i2)) is Element of K19( the carrier' of c)
K19( the carrier' of c) is set
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = b . i1 & cod b₁ = b . i2 ) } is set
Hom ((b . i2),(b . i1)) is Element of K19( the carrier' of c)
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = b . i2 & cod b₁ = b . i1 ) } is set
id (b . i1) is Morphism of b . i1,b . i1
(C,i2,i1,c,b,f) is Morphism of b . i2,b . i1
(C,i2,i1,c,b,f) * (C,i1,i2,c,b,a) is Morphism of b . i1,b . i1
(C,i1,i1,c,b,(id i1)) is Morphism of b . i1,b . i1
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
C opp is non empty non void V52() strict Category-like V65() V66() V67() with_identities CatStr
the carrier' of C is non empty set
the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like V18( the carrier' of C, the carrier of C) Element of K19(K20( the carrier' of C, the carrier of C))
K20( the carrier' of C, the carrier of C) is set
K19(K20( the carrier' of C, the carrier of C)) is set
the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like V18( the carrier' of C, the carrier of C) Element of K19(K20( the carrier' of C, the carrier of C))
the Comp of C is Relation-like K20( the carrier' of C, the carrier' of C) -defined the carrier' of C -valued Function-like Element of K19(K20(K20( the carrier' of C, the carrier' of C), the carrier' of C))
K20( the carrier' of C, the carrier' of C) is set
K20(K20( the carrier' of C, the carrier' of C), the carrier' of C) is set
K19(K20(K20( the carrier' of C, the carrier' of C), the carrier' of C)) is set
~ the Comp of C is Relation-like K20( the carrier' of C, the carrier' of C) -defined the carrier' of C -valued Function-like Element of K19(K20(K20( the carrier' of C, the carrier' of C), the carrier' of C))
CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,(~ the Comp of C) #) is strict CatStr
c is Element of the carrier of C
c opp is Element of the carrier of (C opp)
the carrier of (C opp) is non empty set
i1 is Element of the carrier of C
i1 opp is Element of the carrier of (C opp)
i2 is Morphism of c,i1
i2 opp is Morphism of i1 opp ,c opp
Hom (c,i1) is Element of K19( the carrier' of C)
K19( the carrier' of C) is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = i1 ) } is set
Hom (i1,c) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i1 & cod b₁ = c ) } is set
id i1 is Morphism of i1,i1
a is Morphism of i1,c
i2 * a is Morphism of i1,i1
Hom ((i1 opp),(c opp)) is Element of K19( the carrier' of (C opp))
the carrier' of (C opp) is non empty set
K19( the carrier' of (C opp)) is set
{ b₁ where b₁ is Element of the carrier' of (C opp) : ( dom b₁ = i1 opp & cod b₁ = c opp ) } is set
Hom ((c opp),(i1 opp)) is Element of K19( the carrier' of (C opp))
{ b₁ where b₁ is Element of the carrier' of (C opp) : ( dom b₁ = c opp & cod b₁ = i1 opp ) } is set
id (i1 opp) is Morphism of i1 opp ,i1 opp
a opp is Morphism of c opp ,i1 opp
(a opp) * (i2 opp) is Morphism of i1 opp ,i1 opp
Hom ((i1 opp),(c opp)) is Element of K19( the carrier' of (C opp))
the carrier' of (C opp) is non empty set
K19( the carrier' of (C opp)) is set
{ b₁ where b₁ is Element of the carrier' of (C opp) : ( dom b₁ = i1 opp & cod b₁ = c opp ) } is set
Hom ((c opp),(i1 opp)) is Element of K19( the carrier' of (C opp))
{ b₁ where b₁ is Element of the carrier' of (C opp) : ( dom b₁ = c opp & cod b₁ = i1 opp ) } is set
id (i1 opp) is Morphism of i1 opp ,i1 opp
a is Morphism of c opp ,i1 opp
a * (i2 opp) is Morphism of i1 opp ,i1 opp
Hom (c,i1) is Element of K19( the carrier' of C)
K19( the carrier' of C) is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = i1 ) } is set
Hom (i1,c) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i1 & cod b₁ = c ) } is set
id i1 is Morphism of i1,i1
opp a is Morphism of i1,c
i2 * (opp a) is Morphism of i1,i1
(opp a) opp is Morphism of c opp ,i1 opp
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
C opp is non empty non void V52() strict Category-like V65() V66() V67() with_identities CatStr
the carrier' of C is non empty set
the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like V18( the carrier' of C, the carrier of C) Element of K19(K20( the carrier' of C, the carrier of C))
K20( the carrier' of C, the carrier of C) is set
K19(K20( the carrier' of C, the carrier of C)) is set
the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like V18( the carrier' of C, the carrier of C) Element of K19(K20( the carrier' of C, the carrier of C))
the Comp of C is Relation-like K20( the carrier' of C, the carrier' of C) -defined the carrier' of C -valued Function-like Element of K19(K20(K20( the carrier' of C, the carrier' of C), the carrier' of C))
K20( the carrier' of C, the carrier' of C) is set
K20(K20( the carrier' of C, the carrier' of C), the carrier' of C) is set
K19(K20(K20( the carrier' of C, the carrier' of C), the carrier' of C)) is set
~ the Comp of C is Relation-like K20( the carrier' of C, the carrier' of C) -defined the carrier' of C -valued Function-like Element of K19(K20(K20( the carrier' of C, the carrier' of C), the carrier' of C))
CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,(~ the Comp of C) #) is strict CatStr
c is Element of the carrier of C
c opp is Element of the carrier of (C opp)
the carrier of (C opp) is non empty set
i1 is Element of the carrier of C
i1 opp is Element of the carrier of (C opp)
i2 is Morphism of c,i1
i2 opp is Morphism of i1 opp ,c opp
Hom (c,i1) is Element of K19( the carrier' of C)
K19( the carrier' of C) is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = i1 ) } is set
Hom (i1,c) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i1 & cod b₁ = c ) } is set
id c is Morphism of c,c
a is Morphism of i1,c
a * i2 is Morphism of c,c
Hom ((i1 opp),(c opp)) is Element of K19( the carrier' of (C opp))
the carrier' of (C opp) is non empty set
K19( the carrier' of (C opp)) is set
{ b₁ where b₁ is Element of the carrier' of (C opp) : ( dom b₁ = i1 opp & cod b₁ = c opp ) } is set
Hom ((c opp),(i1 opp)) is Element of K19( the carrier' of (C opp))
{ b₁ where b₁ is Element of the carrier' of (C opp) : ( dom b₁ = c opp & cod b₁ = i1 opp ) } is set
id (c opp) is Morphism of c opp ,c opp
a opp is Morphism of c opp ,i1 opp
(i2 opp) * (a opp) is Morphism of c opp ,c opp
Hom ((i1 opp),(c opp)) is Element of K19( the carrier' of (C opp))
the carrier' of (C opp) is non empty set
K19( the carrier' of (C opp)) is set
{ b₁ where b₁ is Element of the carrier' of (C opp) : ( dom b₁ = i1 opp & cod b₁ = c opp ) } is set
Hom ((c opp),(i1 opp)) is Element of K19( the carrier' of (C opp))
{ b₁ where b₁ is Element of the carrier' of (C opp) : ( dom b₁ = c opp & cod b₁ = i1 opp ) } is set
id (c opp) is Morphism of c opp ,c opp
a is Morphism of c opp ,i1 opp
(i2 opp) * a is Morphism of c opp ,c opp
Hom (c,i1) is Element of K19( the carrier' of C)
K19( the carrier' of C) is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = i1 ) } is set
Hom (i1,c) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i1 & cod b₁ = c ) } is set
id c is Morphism of c,c
opp a is Morphism of i1,c
(opp a) * i2 is Morphism of c,c
(opp a) opp is Morphism of c opp ,i1 opp
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
i1 is Element of the carrier of C
c is Element of the carrier of C
i2 is Morphism of c,i1
a is Morphism of c,i1
b is Morphism of c,i1
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
c is Element of the carrier of C
i1 is Element of the carrier of C
(C,i1,c) is Morphism of i1,c
dom (C,i1,c) is Element of the carrier of C
cod (C,i1,c) is Element of the carrier of C
Hom (i1,c) is Element of K19( the carrier' of C)
the carrier' of C is non empty set
K19( the carrier' of C) is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i1 & cod b₁ = c ) } is set
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
the carrier' of C is non empty set
c is Element of the carrier of C
i1 is Element of the carrier of C
(C,i1,c) is Morphism of i1,c
i2 is Element of the carrier' of C
dom i2 is Element of the carrier of C
cod i2 is Element of the carrier of C
a is Morphism of i1,c
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
c is Element of the carrier of C
i1 is Element of the carrier of C
(C,c,i1) is Morphism of c,i1
i2 is Morphism of c,i1
Hom (c,i1) is Element of K19( the carrier' of C)
the carrier' of C is non empty set
K19( the carrier' of C) is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = i1 ) } is set
dom i2 is Element of the carrier of C
cod i2 is Element of the carrier of C
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
c is Element of the carrier of C
i1 is Element of the carrier of C
i2 is Morphism of c,i1
a is Morphism of c,i1
b is Morphism of c,i1
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
c is Element of the carrier of C
i1 is Element of the carrier of C
(C,c,i1) is Morphism of c,i1
dom (C,c,i1) is Element of the carrier of C
cod (C,c,i1) is Element of the carrier of C
Hom (c,i1) is Element of K19( the carrier' of C)
the carrier' of C is non empty set
K19( the carrier' of C) is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = i1 ) } is set
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
the carrier' of C is non empty set
c is Element of the carrier of C
i1 is Element of the carrier of C
(C,c,i1) is Morphism of c,i1
i2 is Element of the carrier' of C
dom i2 is Element of the carrier of C
cod i2 is Element of the carrier of C
a is Morphism of c,i1
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
c is Element of the carrier of C
i1 is Element of the carrier of C
(C,c,i1) is Morphism of c,i1
i2 is Morphism of c,i1
Hom (c,i1) is Element of K19( the carrier' of C)
the carrier' of C is non empty set
K19( the carrier' of C) is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = i1 ) } is set
dom i2 is Element of the carrier of C
cod i2 is Element of the carrier of C
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
i1 is set
the carrier' of C is non empty set
K20(i1, the carrier' of C) is set
K19(K20(i1, the carrier' of C)) is set
c is Element of the carrier of C
i1 --> c is Relation-like i1 -defined the carrier of C -valued Function-like V18(i1, the carrier of C) Element of K19(K20(i1, the carrier of C))
K20(i1, the carrier of C) is set
K19(K20(i1, the carrier of C)) is set
{c} is non empty set
K20(i1,{c}) is set
id c is Morphism of c,c
i1 --> (id c) is Relation-like i1 -defined the carrier' of C -valued Function-like V18(i1, the carrier' of C) Element of K19(K20(i1, the carrier' of C))
{(id c)} is non empty set
K20(i1,{(id c)}) is set
i2 is Relation-like i1 -defined the carrier' of C -valued Function-like V18(i1, the carrier' of C) Element of K19(K20(i1, the carrier' of C))
(C,i1,i2) is Relation-like i1 -defined the carrier of C -valued Function-like V18(i1, the carrier of C) Element of K19(K20(i1, the carrier of C))
dom (id c) is Element of the carrier of C
i1 --> (dom (id c)) is Relation-like i1 -defined the carrier of C -valued Function-like V18(i1, the carrier of C) Element of K19(K20(i1, the carrier of C))
{(dom (id c))} is non empty set
K20(i1,{(dom (id c))}) is set
C is set
c is set
i1 is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of i1 is non empty set
the carrier' of i1 is non empty set
i2 is Element of the carrier of i1
a is Relation-like C -defined the carrier' of i1 -valued Function-like V18(C, the carrier' of i1) (i1,i2,C)
a /. c is Element of the carrier' of i1
dom (a /. c) is Element of the carrier of i1
(i1,C,a) is Relation-like C -defined the carrier of i1 -valued Function-like V18(C, the carrier of i1) Element of K19(K20(C, the carrier of i1))
K20(C, the carrier of i1) is set
K19(K20(C, the carrier of i1)) is set
(i1,C,a) /. c is Element of the carrier of i1
C --> i2 is Relation-like C -defined the carrier of i1 -valued Function-like V18(C, the carrier of i1) Element of K19(K20(C, the carrier of i1))
{i2} is non empty set
K20(C,{i2}) is set
(C --> i2) /. c is Element of the carrier of i1
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
the carrier' of C is non empty set
K20({}, the carrier' of C) is set
K19(K20({}, the carrier' of C)) is set
c is Element of the carrier of C
i1 is Relation-like {} -defined the carrier' of C -valued Function-like empty V18( {} , the carrier' of C) Element of K19(K20({}, the carrier' of C))
{} --> c is Relation-like {} -defined the carrier of C -valued Function-like empty V18( {} , the carrier of C) Element of K19(K20({}, the carrier of C))
K20({}, the carrier of C) is set
K19(K20({}, the carrier of C)) is set
{c} is non empty set
K20({},{c}) is set
(C,{},i1) is Relation-like {} -defined the carrier of C -valued Function-like empty V18( {} , the carrier of C) Element of K19(K20({}, the carrier of C))
C is set
{C} is non empty set
c is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of c is non empty set
the carrier' of c is non empty set
i1 is Element of the carrier of c
i2 is Element of the carrier' of c
dom i2 is Element of the carrier of c
( the carrier' of c,C,i2) is Relation-like {C} -defined the carrier' of c -valued Function-like V18({C}, the carrier' of c) Element of K19(K20({C}, the carrier' of c))
K20({C}, the carrier' of c) is set
K19(K20({C}, the carrier' of c)) is set
{C} --> i2 is Relation-like {C} -defined {i2} -valued Function-like V18({C},{i2}) Element of K19(K20({C},{i2}))
{i2} is non empty set
K20({C},{i2}) is set
K19(K20({C},{i2})) is set
b is set
(c,{C},( the carrier' of c,C,i2)) is Relation-like {C} -defined the carrier of c -valued Function-like V18({C}, the carrier of c) Element of K19(K20({C}, the carrier of c))
K20({C}, the carrier of c) is set
K19(K20({C}, the carrier of c)) is set
(c,{C},( the carrier' of c,C,i2)) /. b is Element of the carrier of c
( the carrier' of c,C,i2) /. b is Element of the carrier' of c
dom (( the carrier' of c,C,i2) /. b) is Element of the carrier of c
( the carrier of c,C,i1) is Relation-like {C} -defined the carrier of c -valued Function-like V18({C}, the carrier of c) Element of K19(K20({C}, the carrier of c))
{C} --> i1 is Relation-like {C} -defined {i1} -valued Function-like V18({C},{i1}) Element of K19(K20({C},{i1}))
{i1} is non empty set
K20({C},{i1}) is set
K19(K20({C},{i1})) is set
( the carrier of c,C,i1) /. b is Element of the carrier of c
{C} --> i1 is Relation-like {C} -defined the carrier of c -valued Function-like V18({C}, the carrier of c) Element of K19(K20({C}, the carrier of c))
C is set
c is set
{C,c} is non empty set
i1 is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of i1 is non empty set
the carrier' of i1 is non empty set
i2 is Element of the carrier of i1
a is Element of the carrier' of i1
dom a is Element of the carrier of i1
b is Element of the carrier' of i1
dom b is Element of the carrier of i1
(C,c) --> (a,b) is Relation-like {C,c} -defined the carrier' of i1 -valued Function-like V18({C,c}, the carrier' of i1) Element of K19(K20({C,c}, the carrier' of i1))
K20({C,c}, the carrier' of i1) is set
K19(K20({C,c}, the carrier' of i1)) is set
(i1,{C,c},((C,c) --> (a,b))) is Relation-like {C,c} -defined the carrier of i1 -valued Function-like V18({C,c}, the carrier of i1) Element of K19(K20({C,c}, the carrier of i1))
K20({C,c}, the carrier of i1) is set
K19(K20({C,c}, the carrier of i1)) is set
(C,c) --> ((dom a),(dom b)) is Relation-like {C,c} -defined the carrier of i1 -valued Function-like V18({C,c}, the carrier of i1) Element of K19(K20({C,c}, the carrier of i1))
{C,c} --> i2 is Relation-like {C,c} -defined the carrier of i1 -valued Function-like V18({C,c}, the carrier of i1) Element of K19(K20({C,c}, the carrier of i1))
{i2} is non empty set
K20({C,c},{i2}) is set
C is set
c is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of c is non empty set
the carrier' of c is non empty set
i1 is Element of the carrier of c
i2 is Element of the carrier' of c
cod i2 is Element of the carrier of c
dom i2 is Element of the carrier of c
a is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) (c,i1,C)
(c,C,a,i2) is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) Element of K19(K20(C, the carrier' of c))
K20(C, the carrier' of c) is set
K19(K20(C, the carrier' of c)) is set
(c,C,a) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
K20(C, the carrier of c) is set
K19(K20(C, the carrier of c)) is set
C --> (cod i2) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
{(cod i2)} is non empty set
K20(C,{(cod i2)}) is set
(c,C,(c,C,a,i2)) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
C --> (dom i2) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
{(dom i2)} is non empty set
K20(C,{(dom i2)}) is set
C is set
c is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of c is non empty set
the carrier' of c is non empty set
K20(C, the carrier' of c) is set
K19(K20(C, the carrier' of c)) is set
i1 is Element of the carrier of c
i2 is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) Element of K19(K20(C, the carrier' of c))
(c,C,i2) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
K20(C, the carrier of c) is set
K19(K20(C, the carrier of c)) is set
a is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) (c,i1,C)
(c,C,a) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
(c,C,i2,a) is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) Element of K19(K20(C, the carrier' of c))
(c,C,(c,C,i2,a)) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
(c,C,a) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
C --> i1 is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
{i1} is non empty set
K20(C,{i1}) is set
C is set
c is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier' of c is non empty set
c opp is non empty non void V52() strict Category-like V65() V66() V67() with_identities CatStr
the carrier of c is non empty set
the Target of c is Relation-like the carrier' of c -defined the carrier of c -valued Function-like V18( the carrier' of c, the carrier of c) Element of K19(K20( the carrier' of c, the carrier of c))
K20( the carrier' of c, the carrier of c) is set
K19(K20( the carrier' of c, the carrier of c)) is set
the Source of c is Relation-like the carrier' of c -defined the carrier of c -valued Function-like V18( the carrier' of c, the carrier of c) Element of K19(K20( the carrier' of c, the carrier of c))
the Comp of c is Relation-like K20( the carrier' of c, the carrier' of c) -defined the carrier' of c -valued Function-like Element of K19(K20(K20( the carrier' of c, the carrier' of c), the carrier' of c))
K20( the carrier' of c, the carrier' of c) is set
K20(K20( the carrier' of c, the carrier' of c), the carrier' of c) is set
K19(K20(K20( the carrier' of c, the carrier' of c), the carrier' of c)) is set
~ the Comp of c is Relation-like K20( the carrier' of c, the carrier' of c) -defined the carrier' of c -valued Function-like Element of K19(K20(K20( the carrier' of c, the carrier' of c), the carrier' of c))
CatStr(# the carrier of c, the carrier' of c, the Target of c, the Source of c,(~ the Comp of c) #) is strict CatStr
the carrier' of (c opp) is non empty set
i1 is Element of the carrier' of c
cod i1 is Element of the carrier of c
i1 opp is Element of the carrier' of (c opp)
i2 is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) (c, cod i1,C)
(c,C,i2) is Relation-like C -defined the carrier' of (c opp) -valued Function-like V18(C, the carrier' of (c opp)) Element of K19(K20(C, the carrier' of (c opp)))
K20(C, the carrier' of (c opp)) is set
K19(K20(C, the carrier' of (c opp))) is set
((c opp),C,(c,C,i2),(i1 opp)) is Relation-like C -defined the carrier' of (c opp) -valued Function-like V18(C, the carrier' of (c opp)) Element of K19(K20(C, the carrier' of (c opp)))
(c,C,i2,i1) is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) Element of K19(K20(C, the carrier' of c))
K20(C, the carrier' of c) is set
K19(K20(C, the carrier' of c)) is set
(c,C,(c,C,i2,i1)) is Relation-like C -defined the carrier' of (c opp) -valued Function-like V18(C, the carrier' of (c opp)) Element of K19(K20(C, the carrier' of (c opp)))
a is set
i2 /. a is Element of the carrier' of c
dom (i2 /. a) is Element of the carrier of c
(c,C,i2) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
K20(C, the carrier of c) is set
K19(K20(C, the carrier of c)) is set
(c,C,i2) /. a is Element of the carrier of c
C --> (cod i1) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
{(cod i1)} is non empty set
K20(C,{(cod i1)}) is set
(C --> (cod i1)) /. a is Element of the carrier of c
dom i1 is Element of the carrier of c
cod (i2 /. a) is Element of the carrier of c
Hom ((dom i1),(cod i1)) is Element of K19( the carrier' of c)
K19( the carrier' of c) is set
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = dom i1 & cod b₁ = cod i1 ) } is set
Hom ((dom (i2 /. a)),(cod (i2 /. a))) is Element of K19( the carrier' of c)
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = dom (i2 /. a) & cod b₁ = cod (i2 /. a) ) } is set
b is Morphism of dom i1, cod i1
b opp is Morphism of (cod i1) opp ,(dom i1) opp
(cod i1) opp is Element of the carrier of (c opp)
the carrier of (c opp) is non empty set
(dom i1) opp is Element of the carrier of (c opp)
f is Morphism of cod i1, cod (i2 /. a)
f opp is Morphism of (cod (i2 /. a)) opp ,(cod i1) opp
(cod (i2 /. a)) opp is Element of the carrier of (c opp)
(i2 /. a) opp is Element of the carrier' of (c opp)
((c opp),C,(c,C,i2),(i1 opp)) /. a is Element of the carrier' of (c opp)
(c,C,i2) /. a is Element of the carrier' of (c opp)
(i1 opp) (*) ((c,C,i2) /. a) is Element of the carrier' of (c opp)
(i1 opp) (*) ((i2 /. a) opp) is Element of the carrier' of (c opp)
f (*) b is Element of the carrier' of c
(f (*) b) opp is Element of the carrier' of (c opp)
(c,C,i2,i1) /. a is Element of the carrier' of c
((c,C,i2,i1) /. a) opp is Element of the carrier' of (c opp)
(c,C,(c,C,i2,i1)) /. a is Element of the carrier' of (c opp)
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
i1 is set
the carrier' of C is non empty set
K20(i1, the carrier' of C) is set
K19(K20(i1, the carrier' of C)) is set
C is set
c is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of c is non empty set
the carrier' of c is non empty set
i1 is Element of the carrier of c
i2 is Element of the carrier of c
a is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) (c,i1,C)
(c,C,a) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
K20(C, the carrier of c) is set
K19(K20(C, the carrier of c)) is set
b is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) (c,i2,C)
(c,C,b) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
Hom (i2,i2) is non empty Element of K19( the carrier' of c)
K19( the carrier' of c) is set
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = i2 & cod b₁ = i2 ) } is set
f is Element of the carrier' of c
Hom (i2,i1) is Element of K19( the carrier' of c)
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = i2 & cod b₁ = i1 ) } is set
g is Element of the carrier' of c
Hom (i1,i1) is non empty Element of K19( the carrier' of c)
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = i1 & cod b₁ = i1 ) } is set
i is Element of the carrier' of c
Hom (i1,i2) is Element of K19( the carrier' of c)
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = i1 & cod b₁ = i2 ) } is set
h is Element of the carrier' of c
c₁₂ is Morphism of i1,i2
cod c₁₂ is Element of the carrier of c
id i1 is Morphism of i1,i1
k is set
a /. k is Element of the carrier' of c
dom (a /. k) is Element of the carrier of c
(a /. k) (*) (id i1) is Element of the carrier' of c
id i2 is Morphism of i2,i2
k is set
b /. k is Element of the carrier' of c
dom (b /. k) is Element of the carrier of c
(b /. k) (*) (id i2) is Element of the carrier' of c
h is Morphism of i2,i1
c₁₂ * h is Morphism of i2,i2
h * c₁₂ is Morphism of i1,i1
dom c₁₂ is Element of the carrier of c
cod h is Element of the carrier of c
dom h is Element of the carrier of c
c₁₂ (*) h is Element of the carrier' of c
dom (c₁₂ (*) h) is Element of the carrier of c
cod (c₁₂ (*) h) is Element of the carrier of c
k9 is set
b /. k9 is Element of the carrier' of c
dom (b /. k9) is Element of the carrier of c
(b /. k9) (*) (c₁₂ (*) h) is Element of the carrier' of c
(b /. k9) (*) c₁₂ is Element of the carrier' of c
((b /. k9) (*) c₁₂) (*) h is Element of the carrier' of c
a /. k9 is Element of the carrier' of c
(a /. k9) (*) h is Element of the carrier' of c
h (*) c₁₂ is Element of the carrier' of c
dom (h (*) c₁₂) is Element of the carrier of c
cod (h (*) c₁₂) is Element of the carrier of c
k9 is set
a /. k9 is Element of the carrier' of c
dom (a /. k9) is Element of the carrier of c
(a /. k9) (*) (h (*) c₁₂) is Element of the carrier' of c
(a /. k9) (*) h is Element of the carrier' of c
((a /. k9) (*) h) (*) c₁₂ is Element of the carrier' of c
b /. k9 is Element of the carrier' of c
(b /. k9) (*) c₁₂ is Element of the carrier' of c
C is set
c is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of c is non empty set
the carrier' of c is non empty set
i1 is Element of the carrier of c
i2 is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) (c,i1,C)
a is set
i2 /. a is Element of the carrier' of c
cod (i2 /. a) is Element of the carrier of c
b is Element of the carrier of c
Hom (i1,b) is Element of K19( the carrier' of c)
K19( the carrier' of c) is set
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = i1 & cod b₁ = b ) } is set
f is Morphism of i1,b
id b is Morphism of b,b
g is set
i2 /. g is Element of the carrier' of c
cod (i2 /. g) is Element of the carrier of c
Hom (b,(cod (i2 /. g))) is Element of K19( the carrier' of c)
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = b & cod b₁ = cod (i2 /. g) ) } is set
the Element of Hom (b,(cod (i2 /. g))) is Element of Hom (b,(cod (i2 /. g)))
i is Morphism of b,b
g is Relation-like Function-like set
dom g is set
rng g is set
K20(C, the carrier' of c) is set
K19(K20(C, the carrier' of c)) is set
i is set
h is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) Element of K19(K20(C, the carrier' of c))
h . i is set
h /. i is Element of the carrier' of c
i2 /. i is Element of the carrier' of c
cod (i2 /. i) is Element of the carrier of c
Hom (b,(cod (i2 /. i))) is Element of K19( the carrier' of c)
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = b & cod b₁ = cod (i2 /. i) ) } is set
dom (h /. i) is Element of the carrier of c
(c,C,h) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
K20(C, the carrier of c) is set
K19(K20(C, the carrier of c)) is set
(c,C,h) /. i is Element of the carrier of c
C --> b is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
{b} is non empty set
K20(C,{b}) is set
(C --> b) /. i is Element of the carrier of c
i is set
h . i is set
h /. i is Element of the carrier' of c
i2 /. i is Element of the carrier' of c
cod (i2 /. i) is Element of the carrier of c
Hom (b,(cod (i2 /. i))) is Element of K19( the carrier' of c)
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = b & cod b₁ = cod (i2 /. i) ) } is set
cod (h /. i) is Element of the carrier of c
(c,C,h) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
(c,C,h) /. i is Element of the carrier of c
(c,C,i2) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
(c,C,i2) /. i is Element of the carrier of c
Hom (b,i1) is Element of K19( the carrier' of c)
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = b & cod b₁ = i1 ) } is set
i is Element of the carrier' of c
h is Morphism of b,i1
f * h is Morphism of b,b
f (*) h is Element of the carrier' of c
h /. a is Element of the carrier' of c
h . a is set
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
the carrier' of C is non empty set
K20({}, the carrier' of C) is set
K19(K20({}, the carrier' of C)) is set
c is Element of the carrier of C
i1 is Relation-like {} -defined the carrier' of C -valued Function-like empty V18( {} , the carrier' of C) Element of K19(K20({}, the carrier' of C))
i2 is Element of the carrier of C
Hom (i2,c) is Element of K19( the carrier' of C)
K19( the carrier' of C) is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i2 & cod b₁ = c ) } is set
the Relation-like {} -defined the carrier' of C -valued Function-like empty V18( {} , the carrier' of C) (C,i2, {} ) is Relation-like {} -defined the carrier' of C -valued Function-like empty V18( {} , the carrier' of C) (C,i2, {} )
(C,{},i1) is Relation-like {} -defined the carrier of C -valued Function-like empty V18( {} , the carrier of C) Element of K19(K20({}, the carrier of C))
K20({}, the carrier of C) is set
K19(K20({}, the carrier of C)) is set
b is Element of the carrier' of C
f is Morphism of i2,c
g is Morphism of i2,c
h is set
i1 /. h is Element of the carrier' of C
(i1 /. h) (*) g is Element of the carrier' of C
the Relation-like {} -defined the carrier' of C -valued Function-like empty V18( {} , the carrier' of C) (C,i2, {} ) /. h is Element of the carrier' of C
(C,{},i1) is Relation-like {} -defined the carrier of C -valued Function-like empty V18( {} , the carrier of C) Element of K19(K20({}, the carrier of C))
K20({}, the carrier of C) is set
K19(K20({}, the carrier of C)) is set
i2 is Element of the carrier of C
Hom (i2,c) is Element of K19( the carrier' of C)
K19( the carrier' of C) is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i2 & cod b₁ = c ) } is set
a is Morphism of i2,c
b is Relation-like {} -defined the carrier' of C -valued Function-like empty V18( {} , the carrier' of C) (C,i2, {} )
(C,{},b) is Relation-like {} -defined the carrier of C -valued Function-like empty V18( {} , the carrier of C) Element of K19(K20({}, the carrier of C))
f is Element of the carrier' of C
g is set
i1 /. g is Element of the carrier' of C
(i1 /. g) (*) f is Element of the carrier' of C
b /. g is Element of the carrier' of C
C is set
c is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of c is non empty set
the carrier' of c is non empty set
i1 is Element of the carrier of c
i2 is Element of the carrier of c
a is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) (c,i1,C)
b is Morphism of i2,i1
dom b is Element of the carrier of c
cod b is Element of the carrier of c
(c,C,a,b) is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) Element of K19(K20(C, the carrier' of c))
K20(C, the carrier' of c) is set
K19(K20(C, the carrier' of c)) is set
(c,C,(c,C,a,b)) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
K20(C, the carrier of c) is set
K19(K20(C, the carrier of c)) is set
f is Element of the carrier of c
Hom (f,i2) is Element of K19( the carrier' of c)
K19( the carrier' of c) is set
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = f & cod b₁ = i2 ) } is set
(c,C,a) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
C --> (cod b) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
{(cod b)} is non empty set
K20(C,{(cod b)}) is set
g is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) (c,f,C)
(c,C,g) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
(c,C,a) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
Hom (f,i1) is Element of K19( the carrier' of c)
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = f & cod b₁ = i1 ) } is set
h is Element of the carrier' of c
cod h is Element of the carrier of c
id i1 is Morphism of i1,i1
id i2 is Morphism of i2,i2
i is Morphism of i1,i2
b * i is Morphism of i1,i1
i * b is Morphism of i2,i2
Hom (i1,i2) is Element of K19( the carrier' of c)
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = i1 & cod b₁ = i2 ) } is set
Hom (i2,i1) is Element of K19( the carrier' of c)
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = i2 & cod b₁ = i1 ) } is set
dom i is Element of the carrier of c
cod i is Element of the carrier of c
b (*) i is Element of the carrier' of c
id (cod b) is Morphism of cod b, cod b
i (*) b is Element of the carrier' of c
id (dom b) is Morphism of dom b, dom b
dom h is Element of the carrier of c
i (*) h is Element of the carrier' of c
dom (i (*) h) is Element of the carrier of c
h is Element of the carrier' of c
cod (i (*) h) is Element of the carrier of c
c₁₂ is Element of the carrier' of c
cod c₁₂ is Element of the carrier of c
dom c₁₂ is Element of the carrier of c
b (*) c₁₂ is Element of the carrier' of c
dom (b (*) c₁₂) is Element of the carrier of c
cod (b (*) c₁₂) is Element of the carrier of c
k9 is set
a /. k9 is Element of the carrier' of c
dom (a /. k9) is Element of the carrier of c
(a /. k9) (*) (b (*) c₁₂) is Element of the carrier' of c
(a /. k9) (*) b is Element of the carrier' of c
((a /. k9) (*) b) (*) c₁₂ is Element of the carrier' of c
(c,C,a,b) /. k9 is Element of the carrier' of c
((c,C,a,b) /. k9) (*) c₁₂ is Element of the carrier' of c
g /. k9 is Element of the carrier' of c
i (*) (b (*) c₁₂) is Element of the carrier' of c
(id i2) (*) c₁₂ is Element of the carrier' of c
k9 is set
(c,C,a,b) /. k9 is Element of the carrier' of c
((c,C,a,b) /. k9) (*) c₁₂ is Element of the carrier' of c
g /. k9 is Element of the carrier' of c
a /. k9 is Element of the carrier' of c
dom (a /. k9) is Element of the carrier of c
(a /. k9) (*) b is Element of the carrier' of c
((a /. k9) (*) b) (*) c₁₂ is Element of the carrier' of c
b (*) (i (*) h) is Element of the carrier' of c
(a /. k9) (*) (b (*) (i (*) h)) is Element of the carrier' of c
(id (cod b)) (*) h is Element of the carrier' of c
(a /. k9) (*) ((id (cod b)) (*) h) is Element of the carrier' of c
(a /. k9) (*) h is Element of the carrier' of c
C is set
{C} is non empty set
c is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of c is non empty set
the carrier' of c is non empty set
i1 is Element of the carrier of c
id i1 is Morphism of i1,i1
( the carrier' of c,C,(id i1)) is Relation-like {C} -defined the carrier' of c -valued Function-like V18({C}, the carrier' of c) Element of K19(K20({C}, the carrier' of c))
K20({C}, the carrier' of c) is set
K19(K20({C}, the carrier' of c)) is set
{C} --> (id i1) is Relation-like {C} -defined {(id i1)} -valued Function-like V18({C},{(id i1)}) Element of K19(K20({C},{(id i1)}))
{(id i1)} is non empty set
K20({C},{(id i1)}) is set
K19(K20({C},{(id i1)})) is set
dom (id i1) is Element of the carrier of c
(c,{C},( the carrier' of c,C,(id i1))) is Relation-like {C} -defined the carrier of c -valued Function-like V18({C}, the carrier of c) Element of K19(K20({C}, the carrier of c))
K20({C}, the carrier of c) is set
K19(K20({C}, the carrier of c)) is set
a is Element of the carrier of c
Hom (a,i1) is Element of K19( the carrier' of c)
K19( the carrier' of c) is set
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = a & cod b₁ = i1 ) } is set
b is Relation-like {C} -defined the carrier' of c -valued Function-like V18({C}, the carrier' of c) (c,a,{C})
(c,{C},b) is Relation-like {C} -defined the carrier of c -valued Function-like V18({C}, the carrier of c) Element of K19(K20({C}, the carrier of c))
b /. C is Element of the carrier' of c
f is Element of the carrier' of c
dom f is Element of the carrier of c
cod f is Element of the carrier of c
(c,{C},( the carrier' of c,C,(id i1))) /. C is Element of the carrier of c
( the carrier' of c,C,(id i1)) /. C is Element of the carrier' of c
cod (( the carrier' of c,C,(id i1)) /. C) is Element of the carrier of c
cod (id i1) is Element of the carrier of c
g is Element of the carrier' of c
cod g is Element of the carrier of c
(id i1) (*) g is Element of the carrier' of c
(( the carrier' of c,C,(id i1)) /. C) (*) g is Element of the carrier' of c
h is set
( the carrier' of c,C,(id i1)) /. h is Element of the carrier' of c
(( the carrier' of c,C,(id i1)) /. h) (*) g is Element of the carrier' of c
b /. h is Element of the carrier' of c
b /. h is Element of the carrier' of c
(id i1) (*) g is Element of the carrier' of c
( the carrier' of c,C,(id i1)) /. h is Element of the carrier' of c
(( the carrier' of c,C,(id i1)) /. h) (*) g is Element of the carrier' of c
C is set
c is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of c is non empty set
the carrier' of c is non empty set
i1 is Element of the carrier of c
i2 is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) (c,i1,C)
a is Element of the carrier of c
K20(C, the carrier' of c) is set
K19(K20(C, the carrier' of c)) is set
b is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) Element of K19(K20(C, the carrier' of c))
f is set
i2 /. f is Element of the carrier' of c
cod (i2 /. f) is Element of the carrier of c
(c,C,b) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
K20(C, the carrier of c) is set
K19(K20(C, the carrier of c)) is set
(c,C,b) /. f is Element of the carrier of c
b /. f is Element of the carrier' of c
dom (b /. f) is Element of the carrier of c
(c,a,(cod (i2 /. f))) is Morphism of a, cod (i2 /. f)
dom (c,a,(cod (i2 /. f))) is Element of the carrier of c
C --> a is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
{a} is non empty set
K20(C,{a}) is set
(C --> a) /. f is Element of the carrier of c
g is set
i2 /. g is Element of the carrier' of c
cod (i2 /. g) is Element of the carrier of c
(c,C,i2) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
(c,C,i2) /. g is Element of the carrier of c
(c,a,(cod (i2 /. g))) is Morphism of a, cod (i2 /. g)
cod (c,a,(cod (i2 /. g))) is Element of the carrier of c
f is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) (c,a,C)
f /. g is Element of the carrier' of c
cod (f /. g) is Element of the carrier of c
(c,C,f) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
(c,C,f) /. g is Element of the carrier of c
Hom (a,i1) is Element of K19( the carrier' of c)
K19( the carrier' of c) is set
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = a & cod b₁ = i1 ) } is set
g is Element of the carrier' of c
h is Morphism of a,i1
h is Morphism of a,i1
c₁₂ is set
i2 /. c₁₂ is Element of the carrier' of c
cod (i2 /. c₁₂) is Element of the carrier of c
cod h is Element of the carrier of c
k is Morphism of a, cod (i2 /. c₁₂)
dom (i2 /. c₁₂) is Element of the carrier of c
(i2 /. c₁₂) (*) h is Element of the carrier' of c
cod ((i2 /. c₁₂) (*) h) is Element of the carrier of c
dom h is Element of the carrier of c
dom ((i2 /. c₁₂) (*) h) is Element of the carrier of c
Hom (a,(cod (i2 /. c₁₂))) is Element of K19( the carrier' of c)
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = a & cod b₁ = cod (i2 /. c₁₂) ) } is set
f /. c₁₂ is Element of the carrier' of c
(c,a,(cod (i2 /. c₁₂))) is Morphism of a, cod (i2 /. c₁₂)
i is Morphism of a,i1
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
the carrier' of C is non empty set
C is set
c is set
{C,c} is non empty set
i1 is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of i1 is non empty set
the carrier' of i1 is non empty set
i2 is Element of the carrier of i1
a is Element of the carrier' of i1
b is Element of the carrier' of i1
(C,c) --> (a,b) is Relation-like {C,c} -defined the carrier' of i1 -valued Function-like V18({C,c}, the carrier' of i1) Element of K19(K20({C,c}, the carrier' of i1))
K20({C,c}, the carrier' of i1) is set
K19(K20({C,c}, the carrier' of i1)) is set
dom a is Element of the carrier of i1
dom b is Element of the carrier of i1
(i1,{C,c},((C,c) --> (a,b))) is Relation-like {C,c} -defined the carrier of i1 -valued Function-like V18({C,c}, the carrier of i1) Element of K19(K20({C,c}, the carrier of i1))
K20({C,c}, the carrier of i1) is set
K19(K20({C,c}, the carrier of i1)) is set
h is Element of the carrier of i1
Hom (h,i2) is Element of K19( the carrier' of i1)
K19( the carrier' of i1) is set
{ b₁ where b₁ is Element of the carrier' of i1 : ( dom b₁ = h & cod b₁ = i2 ) } is set
i is Relation-like {C,c} -defined the carrier' of i1 -valued Function-like V18({C,c}, the carrier' of i1) (i1,h,{C,c})
(i1,{C,c},i) is Relation-like {C,c} -defined the carrier of i1 -valued Function-like V18({C,c}, the carrier of i1) Element of K19(K20({C,c}, the carrier of i1))
i /. C is Element of the carrier' of i1
i /. c is Element of the carrier' of i1
(i1,{C,c},((C,c) --> (a,b))) /. C is Element of the carrier of i1
((C,c) --> (a,b)) /. C is Element of the carrier' of i1
cod (((C,c) --> (a,b)) /. C) is Element of the carrier of i1
cod (i /. C) is Element of the carrier of i1
cod a is Element of the carrier of i1
(i1,{C,c},((C,c) --> (a,b))) /. c is Element of the carrier of i1
((C,c) --> (a,b)) /. c is Element of the carrier' of i1
cod (((C,c) --> (a,b)) /. c) is Element of the carrier of i1
cod (i /. c) is Element of the carrier of i1
cod b is Element of the carrier of i1
dom (i /. c) is Element of the carrier of i1
Hom (h,(cod b)) is Element of K19( the carrier' of i1)
{ b₁ where b₁ is Element of the carrier' of i1 : ( dom b₁ = h & cod b₁ = cod b ) } is set
dom (i /. C) is Element of the carrier of i1
Hom (h,(cod a)) is Element of K19( the carrier' of i1)
{ b₁ where b₁ is Element of the carrier' of i1 : ( dom b₁ = h & cod b₁ = cod a ) } is set
k9 is Element of the carrier' of i1
k is Element of the carrier' of i1
(((C,c) --> (a,b)) /. c) (*) k is Element of the carrier' of i1
b (*) k is Element of the carrier' of i1
(((C,c) --> (a,b)) /. C) (*) k is Element of the carrier' of i1
a (*) k is Element of the carrier' of i1
a (*) k is Element of the carrier' of i1
b (*) k is Element of the carrier' of i1
x is set
((C,c) --> (a,b)) /. x is Element of the carrier' of i1
(((C,c) --> (a,b)) /. x) (*) k is Element of the carrier' of i1
i /. x is Element of the carrier' of i1
((C,c) --> (a,b)) /. c is Element of the carrier' of i1
dom (((C,c) --> (a,b)) /. c) is Element of the carrier of i1
((C,c) --> (a,b)) /. C is Element of the carrier' of i1
dom (((C,c) --> (a,b)) /. C) is Element of the carrier of i1
dom a is Element of the carrier of i1
dom b is Element of the carrier of i1
cod a is Element of the carrier of i1
cod b is Element of the carrier of i1
h is Element of the carrier of i1
Hom (h,(cod a)) is Element of K19( the carrier' of i1)
K19( the carrier' of i1) is set
{ b₁ where b₁ is Element of the carrier' of i1 : ( dom b₁ = h & cod b₁ = cod a ) } is set
Hom (h,(cod b)) is Element of K19( the carrier' of i1)
{ b₁ where b₁ is Element of the carrier' of i1 : ( dom b₁ = h & cod b₁ = cod b ) } is set
Hom (h,i2) is Element of K19( the carrier' of i1)
{ b₁ where b₁ is Element of the carrier' of i1 : ( dom b₁ = h & cod b₁ = i2 ) } is set
i is Element of the carrier' of i1
h is Element of the carrier' of i1
dom i is Element of the carrier of i1
dom h is Element of the carrier of i1
(C,c) --> (i,h) is Relation-like {C,c} -defined the carrier' of i1 -valued Function-like V18({C,c}, the carrier' of i1) Element of K19(K20({C,c}, the carrier' of i1))
(i1,{C,c},((C,c) --> (a,b))) is Relation-like {C,c} -defined the carrier of i1 -valued Function-like V18({C,c}, the carrier of i1) Element of K19(K20({C,c}, the carrier of i1))
K20({C,c}, the carrier of i1) is set
K19(K20({C,c}, the carrier of i1)) is set
(C,c) --> ((cod a),(cod b)) is Relation-like {C,c} -defined the carrier of i1 -valued Function-like V18({C,c}, the carrier of i1) Element of K19(K20({C,c}, the carrier of i1))
cod i is Element of the carrier of i1
(C,c) --> ((cod i),(cod b)) is Relation-like {C,c} -defined the carrier of i1 -valued Function-like V18({C,c}, the carrier of i1) Element of K19(K20({C,c}, the carrier of i1))
cod h is Element of the carrier of i1
(C,c) --> ((cod i),(cod h)) is Relation-like {C,c} -defined the carrier of i1 -valued Function-like V18({C,c}, the carrier of i1) Element of K19(K20({C,c}, the carrier of i1))
c₁₂ is Relation-like {C,c} -defined the carrier' of i1 -valued Function-like V18({C,c}, the carrier' of i1) (i1,h,{C,c})
(i1,{C,c},c₁₂) is Relation-like {C,c} -defined the carrier of i1 -valued Function-like V18({C,c}, the carrier of i1) Element of K19(K20({C,c}, the carrier of i1))
k9 is Element of the carrier' of i1
k is Element of the carrier' of i1
a (*) k is Element of the carrier' of i1
b (*) k is Element of the carrier' of i1
x is set
((C,c) --> (a,b)) /. x is Element of the carrier' of i1
c₁₂ /. x is Element of the carrier' of i1
(((C,c) --> (a,b)) /. x) (*) k is Element of the carrier' of i1
(((C,c) --> (a,b)) /. c) (*) k is Element of the carrier' of i1
c₁₂ /. c is Element of the carrier' of i1
(((C,c) --> (a,b)) /. C) (*) k is Element of the carrier' of i1
c₁₂ /. C is Element of the carrier' of i1
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
c is Element of the carrier of C
i1 is Element of the carrier of C
Hom (c,i1) is Element of K19( the carrier' of C)
the carrier' of C is non empty set
K19( the carrier' of C) is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = i1 ) } is set
i2 is Element of the carrier of C
Hom (c,i2) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = i2 ) } is set
a is Morphism of c,i1
b is Morphism of c,i2
dom a is Element of the carrier of C
dom b is Element of the carrier of C
cod a is Element of the carrier of C
cod b is Element of the carrier of C
f is Element of the carrier of C
Hom (f,i1) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = f & cod b₁ = i1 ) } is set
Hom (f,i2) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = f & cod b₁ = i2 ) } is set
Hom (f,c) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = f & cod b₁ = c ) } is set
the Morphism of f,i1 is Morphism of f,i1
the Morphism of f,i2 is Morphism of f,i2
Hom (f,(cod b)) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = f & cod b₁ = cod b ) } is set
Hom (f,(cod a)) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = f & cod b₁ = cod a ) } is set
i is Element of the carrier' of C
i is Morphism of f,i1
h is Morphism of f,i2
c₁₂ is Element of the carrier' of C
k9 is Morphism of f,c
k is Morphism of f,c
a * k is Morphism of f,i1
b * k is Morphism of f,i2
x is Element of the carrier' of C
a (*) k is Element of the carrier' of C
b (*) k is Element of the carrier' of C
x is Element of the carrier' of C
dom a is Element of the carrier of C
dom b is Element of the carrier of C
cod a is Element of the carrier of C
cod b is Element of the carrier of C
f is Element of the carrier of C
Hom (f,(cod a)) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = f & cod b₁ = cod a ) } is set
Hom (f,(cod b)) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = f & cod b₁ = cod b ) } is set
Hom (f,c) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = f & cod b₁ = c ) } is set
g is Element of the carrier' of C
h is Element of the carrier' of C
Hom (f,i1) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = f & cod b₁ = i1 ) } is set
i is Morphism of f,c
h is Element of the carrier' of C
c₁₂ is Element of the carrier' of C
a (*) c₁₂ is Element of the carrier' of C
b (*) c₁₂ is Element of the carrier' of C
k9 is Morphism of f,c
a * k9 is Morphism of f,i1
b * k9 is Morphism of f,i2
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
the carrier' of C is non empty set
c is Element of the carrier of C
i1 is Element of the carrier of C
i2 is Element of the carrier' of C
cod i2 is Element of the carrier of C
a is Element of the carrier' of C
cod a is Element of the carrier of C
b is Element of the carrier' of C
cod b is Element of the carrier of C
f is Element of the carrier' of C
cod f is Element of the carrier of C
0 is empty Element of K99()
{0,1} is non empty set
(0,1) --> (i2,a) is Relation-like {0,1} -defined the carrier' of C -valued Function-like V18({0,1}, the carrier' of C) Element of K19(K20({0,1}, the carrier' of C))
K20({0,1}, the carrier' of C) is set
K19(K20({0,1}, the carrier' of C)) is set
(0,1) --> (b,f) is Relation-like {0,1} -defined the carrier' of C -valued Function-like V18({0,1}, the carrier' of C) Element of K19(K20({0,1}, the carrier' of C))
dom b is Element of the carrier of C
dom f is Element of the carrier of C
dom i2 is Element of the carrier of C
dom a is Element of the carrier of C
(C,{0,1},((0,1) --> (i2,a))) is Relation-like {0,1} -defined the carrier of C -valued Function-like V18({0,1}, the carrier of C) Element of K19(K20({0,1}, the carrier of C))
K20({0,1}, the carrier of C) is set
K19(K20({0,1}, the carrier of C)) is set
(0,1) --> ((cod b),(cod f)) is Relation-like {0,1} -defined the carrier of C -valued Function-like V18({0,1}, the carrier of C) Element of K19(K20({0,1}, the carrier of C))
(C,{0,1},((0,1) --> (b,f))) is Relation-like {0,1} -defined the carrier of C -valued Function-like V18({0,1}, the carrier of C) Element of K19(K20({0,1}, the carrier of C))
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
c is Element of the carrier of C
i1 is Element of the carrier of C
Hom (c,i1) is Element of K19( the carrier' of C)
the carrier' of C is non empty set
K19( the carrier' of C) is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = i1 ) } is set
i2 is Element of the carrier of C
Hom (c,i2) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = i2 ) } is set
Hom (i1,i2) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i1 & cod b₁ = i2 ) } is set
Hom (i2,i1) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i2 & cod b₁ = i1 ) } is set
a is Morphism of c,i1
b is Morphism of c,i2
0 is empty Element of K99()
{0,1} is non empty set
dom a is Element of the carrier of C
dom b is Element of the carrier of C
(0,1) --> (a,b) is Relation-like {0,1} -defined the carrier' of C -valued Function-like V18({0,1}, the carrier' of C) Element of K19(K20({0,1}, the carrier' of C))
K20({0,1}, the carrier' of C) is set
K19(K20({0,1}, the carrier' of C)) is set
g is Relation-like {0,1} -defined the carrier' of C -valued Function-like V18({0,1}, the carrier' of C) (C,c,{0,1})
g /. 0 is Element of the carrier' of C
g /. 1 is Element of the carrier' of C
h is set
i is set
g /. h is Element of the carrier' of C
cod (g /. h) is Element of the carrier of C
g /. i is Element of the carrier' of C
cod (g /. i) is Element of the carrier of C
Hom ((cod (g /. h)),(cod (g /. i))) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = cod (g /. h) & cod b₁ = cod (g /. i) ) } is set
cod (g /. 0) is Element of the carrier of C
cod (g /. 1) is Element of the carrier of C
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
the carrier' of C is non empty set
c is Element of the carrier of C
Hom (c,c) is non empty Element of K19( the carrier' of C)
K19( the carrier' of C) is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = c ) } is set
id c is Morphism of c,c
i1 is Element of the carrier' of C
i2 is Element of the carrier' of C
a is Element of the carrier' of C
i1 (*) a is Element of the carrier' of C
i2 (*) a is Element of the carrier' of C
dom i1 is Element of the carrier of C
dom i2 is Element of the carrier of C
cod i1 is Element of the carrier of C
cod i2 is Element of the carrier of C
Hom (c,(cod i1)) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = cod i1 ) } is set
Hom (c,(cod i2)) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = cod i2 ) } is set
b is Element of the carrier' of C
i1 (*) (id c) is Element of the carrier' of C
i2 (*) (id c) is Element of the carrier' of C
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
the carrier' of C is non empty set
c is Element of the carrier of C
i1 is Element of the carrier of C
i2 is Element of the carrier' of C
a is Element of the carrier' of C
b is Morphism of c,i1
dom b is Element of the carrier of C
cod b is Element of the carrier of C
i2 (*) b is Element of the carrier' of C
a (*) b is Element of the carrier' of C
dom i2 is Element of the carrier of C
dom a is Element of the carrier of C
0 is empty Element of K99()
(0,1) --> (i2,a) is Relation-like {0,1} -defined the carrier' of C -valued Function-like V18({0,1}, the carrier' of C) Element of K19(K20({0,1}, the carrier' of C))
{0,1} is non empty set
K20({0,1}, the carrier' of C) is set
K19(K20({0,1}, the carrier' of C)) is set
(C,{0,1},((0,1) --> (i2,a)),b) is Relation-like {0,1} -defined the carrier' of C -valued Function-like V18({0,1}, the carrier' of C) Element of K19(K20({0,1}, the carrier' of C))
(0,1) --> ((i2 (*) b),(a (*) b)) is Relation-like {0,1} -defined the carrier' of C -valued Function-like V18({0,1}, the carrier' of C) Element of K19(K20({0,1}, the carrier' of C))
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
the carrier' of C is non empty set
c is Element of the carrier of C
i1 is Element of the carrier' of C
cod i1 is Element of the carrier of C
i2 is Element of the carrier' of C
cod i2 is Element of the carrier of C
id (cod i1) is Morphism of cod i1, cod i1
(C,(cod i1),(cod i2)) is Morphism of cod i1, cod i2
dom (C,(cod i1),(cod i2)) is Element of the carrier of C
cod (C,(cod i1),(cod i2)) is Element of the carrier of C
Hom ((cod i1),(cod i1)) is non empty Element of K19( the carrier' of C)
K19( the carrier' of C) is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = cod i1 & cod b₁ = cod i1 ) } is set
Hom ((cod i1),(cod i2)) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = cod i1 & cod b₁ = cod i2 ) } is set
Hom ((cod i1),c) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = cod i1 & cod b₁ = c ) } is set
h is Element of the carrier' of C
dom h is Element of the carrier of C
dom i1 is Element of the carrier of C
i is Morphism of cod i1,c
cod i is Element of the carrier of C
h is Morphism of c, cod i1
i (*) h is Element of the carrier' of C
cod (i (*) h) is Element of the carrier of C
dom i2 is Element of the carrier of C
i2 (*) (i (*) h) is Element of the carrier' of C
cod (i2 (*) (i (*) h)) is Element of the carrier of C
dom (i (*) h) is Element of the carrier of C
Hom (c,c) is non empty Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = c ) } is set
dom (i2 (*) (i (*) h)) is Element of the carrier of C
(C,c,(cod i2)) is Morphism of c, cod i2
Hom (c,(cod i1)) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = cod i1 ) } is set
id c is Morphism of c,c
h * i is Morphism of cod i1, cod i1
i * h is Morphism of c,c
h (*) i is Element of the carrier' of C
i1 (*) (i (*) h) is Element of the carrier' of C
i1 (*) i is Element of the carrier' of C
(i1 (*) i) (*) h is Element of the carrier' of C
cod h is Element of the carrier of C
id (cod h) is Morphism of cod h, cod h
(id (cod h)) (*) h is Element of the carrier' of C
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
the carrier' of C is non empty set
c is Element of the carrier of C
i1 is Element of the carrier' of C
cod i1 is Element of the carrier of C
i2 is Element of the carrier' of C
cod i2 is Element of the carrier of C
id (cod i2) is Morphism of cod i2, cod i2
(C,(cod i2),(cod i1)) is Morphism of cod i2, cod i1
dom (C,(cod i2),(cod i1)) is Element of the carrier of C
cod (C,(cod i2),(cod i1)) is Element of the carrier of C
Hom ((cod i2),(cod i2)) is non empty Element of K19( the carrier' of C)
K19( the carrier' of C) is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = cod i2 & cod b₁ = cod i2 ) } is set
Hom ((cod i2),(cod i1)) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = cod i2 & cod b₁ = cod i1 ) } is set
Hom ((cod i2),c) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = cod i2 & cod b₁ = c ) } is set
h is Element of the carrier' of C
dom h is Element of the carrier of C
dom i2 is Element of the carrier of C
cod h is Element of the carrier of C
i is Morphism of c, cod i2
h (*) i is Element of the carrier' of C
cod (h (*) i) is Element of the carrier of C
dom i1 is Element of the carrier of C
i1 (*) (h (*) i) is Element of the carrier' of C
cod (i1 (*) (h (*) i)) is Element of the carrier of C
dom (h (*) i) is Element of the carrier of C
Hom (c,c) is non empty Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = c ) } is set
dom (i1 (*) (h (*) i)) is Element of the carrier of C
(C,c,(cod i1)) is Morphism of c, cod i1
Hom (c,(cod i2)) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = cod i2 ) } is set
id c is Morphism of c,c
h is Morphism of cod i2,c
i * h is Morphism of cod i2, cod i2
h * i is Morphism of c,c
i (*) h is Element of the carrier' of C
cod i is Element of the carrier of C
id (cod i) is Morphism of cod i, cod i
h (*) i is Element of the carrier' of C
i2 (*) (h (*) i) is Element of the carrier' of C
(id (cod i)) (*) i is Element of the carrier' of C
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
i1 is set
the carrier' of C is non empty set
K20(i1, the carrier' of C) is set
K19(K20(i1, the carrier' of C)) is set
c is Element of the carrier of C
i1 --> c is Relation-like i1 -defined the carrier of C -valued Function-like V18(i1, the carrier of C) Element of K19(K20(i1, the carrier of C))
K20(i1, the carrier of C) is set
K19(K20(i1, the carrier of C)) is set
{c} is non empty set
K20(i1,{c}) is set
id c is Morphism of c,c
i1 --> (id c) is Relation-like i1 -defined the carrier' of C -valued Function-like V18(i1, the carrier' of C) Element of K19(K20(i1, the carrier' of C))
{(id c)} is non empty set
K20(i1,{(id c)}) is set
i2 is Relation-like i1 -defined the carrier' of C -valued Function-like V18(i1, the carrier' of C) Element of K19(K20(i1, the carrier' of C))
(C,i1,i2) is Relation-like i1 -defined the carrier of C -valued Function-like V18(i1, the carrier of C) Element of K19(K20(i1, the carrier of C))
cod (id c) is Element of the carrier of C
i1 --> (cod (id c)) is Relation-like i1 -defined the carrier of C -valued Function-like V18(i1, the carrier of C) Element of K19(K20(i1, the carrier of C))
{(cod (id c))} is non empty set
K20(i1,{(cod (id c))}) is set
C is set
c is set
i1 is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of i1 is non empty set
the carrier' of i1 is non empty set
i2 is Element of the carrier of i1
a is Relation-like C -defined the carrier' of i1 -valued Function-like V18(C, the carrier' of i1) (i1,i2,C)
a /. c is Element of the carrier' of i1
cod (a /. c) is Element of the carrier of i1
(i1,C,a) is Relation-like C -defined the carrier of i1 -valued Function-like V18(C, the carrier of i1) Element of K19(K20(C, the carrier of i1))
K20(C, the carrier of i1) is set
K19(K20(C, the carrier of i1)) is set
(i1,C,a) /. c is Element of the carrier of i1
C --> i2 is Relation-like C -defined the carrier of i1 -valued Function-like V18(C, the carrier of i1) Element of K19(K20(C, the carrier of i1))
{i2} is non empty set
K20(C,{i2}) is set
(C --> i2) /. c is Element of the carrier of i1
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
the carrier' of C is non empty set
K20({}, the carrier' of C) is set
K19(K20({}, the carrier' of C)) is set
c is Element of the carrier of C
i1 is Relation-like {} -defined the carrier' of C -valued Function-like empty V18( {} , the carrier' of C) Element of K19(K20({}, the carrier' of C))
{} --> c is Relation-like {} -defined the carrier of C -valued Function-like empty V18( {} , the carrier of C) Element of K19(K20({}, the carrier of C))
K20({}, the carrier of C) is set
K19(K20({}, the carrier of C)) is set
{c} is non empty set
K20({},{c}) is set
(C,{},i1) is Relation-like {} -defined the carrier of C -valued Function-like empty V18( {} , the carrier of C) Element of K19(K20({}, the carrier of C))
C is set
{C} is non empty set
c is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of c is non empty set
the carrier' of c is non empty set
i1 is Element of the carrier of c
i2 is Element of the carrier' of c
cod i2 is Element of the carrier of c
( the carrier' of c,C,i2) is Relation-like {C} -defined the carrier' of c -valued Function-like V18({C}, the carrier' of c) Element of K19(K20({C}, the carrier' of c))
K20({C}, the carrier' of c) is set
K19(K20({C}, the carrier' of c)) is set
{C} --> i2 is Relation-like {C} -defined {i2} -valued Function-like V18({C},{i2}) Element of K19(K20({C},{i2}))
{i2} is non empty set
K20({C},{i2}) is set
K19(K20({C},{i2})) is set
b is set
(c,{C},( the carrier' of c,C,i2)) is Relation-like {C} -defined the carrier of c -valued Function-like V18({C}, the carrier of c) Element of K19(K20({C}, the carrier of c))
K20({C}, the carrier of c) is set
K19(K20({C}, the carrier of c)) is set
(c,{C},( the carrier' of c,C,i2)) /. b is Element of the carrier of c
( the carrier' of c,C,i2) /. b is Element of the carrier' of c
cod (( the carrier' of c,C,i2) /. b) is Element of the carrier of c
( the carrier of c,C,i1) is Relation-like {C} -defined the carrier of c -valued Function-like V18({C}, the carrier of c) Element of K19(K20({C}, the carrier of c))
{C} --> i1 is Relation-like {C} -defined {i1} -valued Function-like V18({C},{i1}) Element of K19(K20({C},{i1}))
{i1} is non empty set
K20({C},{i1}) is set
K19(K20({C},{i1})) is set
( the carrier of c,C,i1) /. b is Element of the carrier of c
{C} --> i1 is Relation-like {C} -defined the carrier of c -valued Function-like V18({C}, the carrier of c) Element of K19(K20({C}, the carrier of c))
C is set
c is set
{C,c} is non empty set
i1 is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of i1 is non empty set
the carrier' of i1 is non empty set
i2 is Element of the carrier of i1
a is Element of the carrier' of i1
cod a is Element of the carrier of i1
b is Element of the carrier' of i1
cod b is Element of the carrier of i1
(C,c) --> (a,b) is Relation-like {C,c} -defined the carrier' of i1 -valued Function-like V18({C,c}, the carrier' of i1) Element of K19(K20({C,c}, the carrier' of i1))
K20({C,c}, the carrier' of i1) is set
K19(K20({C,c}, the carrier' of i1)) is set
(i1,{C,c},((C,c) --> (a,b))) is Relation-like {C,c} -defined the carrier of i1 -valued Function-like V18({C,c}, the carrier of i1) Element of K19(K20({C,c}, the carrier of i1))
K20({C,c}, the carrier of i1) is set
K19(K20({C,c}, the carrier of i1)) is set
(C,c) --> ((cod a),(cod b)) is Relation-like {C,c} -defined the carrier of i1 -valued Function-like V18({C,c}, the carrier of i1) Element of K19(K20({C,c}, the carrier of i1))
{C,c} --> i2 is Relation-like {C,c} -defined the carrier of i1 -valued Function-like V18({C,c}, the carrier of i1) Element of K19(K20({C,c}, the carrier of i1))
{i2} is non empty set
K20({C,c},{i2}) is set
C is set
c is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of c is non empty set
the carrier' of c is non empty set
i1 is Element of the carrier of c
i2 is Element of the carrier' of c
dom i2 is Element of the carrier of c
cod i2 is Element of the carrier of c
a is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) (c,i1,C)
(c,C,a,i2) is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) Element of K19(K20(C, the carrier' of c))
K20(C, the carrier' of c) is set
K19(K20(C, the carrier' of c)) is set
(c,C,a) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
K20(C, the carrier of c) is set
K19(K20(C, the carrier of c)) is set
C --> (dom i2) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
{(dom i2)} is non empty set
K20(C,{(dom i2)}) is set
(c,C,(c,C,a,i2)) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
C --> (cod i2) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
{(cod i2)} is non empty set
K20(C,{(cod i2)}) is set
C is set
c is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of c is non empty set
the carrier' of c is non empty set
K20(C, the carrier' of c) is set
K19(K20(C, the carrier' of c)) is set
i1 is Element of the carrier of c
i2 is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) (c,i1,C)
(c,C,i2) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
K20(C, the carrier of c) is set
K19(K20(C, the carrier of c)) is set
a is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) Element of K19(K20(C, the carrier' of c))
(c,C,a) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
(c,C,i2,a) is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) Element of K19(K20(C, the carrier' of c))
(c,C,(c,C,i2,a)) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
(c,C,i2) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
C --> i1 is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
{i1} is non empty set
K20(C,{i1}) is set
C is set
c is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of c is non empty set
the carrier' of c is non empty set
K20(C, the carrier' of c) is set
K19(K20(C, the carrier' of c)) is set
c opp is non empty non void V52() strict Category-like V65() V66() V67() with_identities CatStr
the Target of c is Relation-like the carrier' of c -defined the carrier of c -valued Function-like V18( the carrier' of c, the carrier of c) Element of K19(K20( the carrier' of c, the carrier of c))
K20( the carrier' of c, the carrier of c) is set
K19(K20( the carrier' of c, the carrier of c)) is set
the Source of c is Relation-like the carrier' of c -defined the carrier of c -valued Function-like V18( the carrier' of c, the carrier of c) Element of K19(K20( the carrier' of c, the carrier of c))
the Comp of c is Relation-like K20( the carrier' of c, the carrier' of c) -defined the carrier' of c -valued Function-like Element of K19(K20(K20( the carrier' of c, the carrier' of c), the carrier' of c))
K20( the carrier' of c, the carrier' of c) is set
K20(K20( the carrier' of c, the carrier' of c), the carrier' of c) is set
K19(K20(K20( the carrier' of c, the carrier' of c), the carrier' of c)) is set
~ the Comp of c is Relation-like K20( the carrier' of c, the carrier' of c) -defined the carrier' of c -valued Function-like Element of K19(K20(K20( the carrier' of c, the carrier' of c), the carrier' of c))
CatStr(# the carrier of c, the carrier' of c, the Target of c, the Source of c,(~ the Comp of c) #) is strict CatStr
the carrier' of (c opp) is non empty set
i1 is Element of the carrier of c
i1 opp is Element of the carrier of (c opp)
the carrier of (c opp) is non empty set
i2 is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) Element of K19(K20(C, the carrier' of c))
(c,C,i2) is Relation-like C -defined the carrier' of (c opp) -valued Function-like V18(C, the carrier' of (c opp)) Element of K19(K20(C, the carrier' of (c opp)))
K20(C, the carrier' of (c opp)) is set
K19(K20(C, the carrier' of (c opp))) is set
(c,C,i2) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
K20(C, the carrier of c) is set
K19(K20(C, the carrier of c)) is set
C --> i1 is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
{i1} is non empty set
K20(C,{i1}) is set
a is set
i2 /. a is Element of the carrier' of c
dom (i2 /. a) is Element of the carrier of c
cod (i2 /. a) is Element of the carrier of c
b is Morphism of dom (i2 /. a), cod (i2 /. a)
dom b is Element of the carrier of c
cod b is Element of the carrier of c
Hom ((dom b),(cod b)) is Element of K19( the carrier' of c)
K19( the carrier' of c) is set
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = dom b & cod b₁ = cod b ) } is set
b opp is Morphism of (cod (i2 /. a)) opp ,(dom (i2 /. a)) opp
(cod (i2 /. a)) opp is Element of the carrier of (c opp)
(dom (i2 /. a)) opp is Element of the carrier of (c opp)
(i2 /. a) opp is Element of the carrier' of (c opp)
((c opp),C,(c,C,i2)) is Relation-like C -defined the carrier of (c opp) -valued Function-like V18(C, the carrier of (c opp)) Element of K19(K20(C, the carrier of (c opp)))
K20(C, the carrier of (c opp)) is set
K19(K20(C, the carrier of (c opp))) is set
((c opp),C,(c,C,i2)) /. a is Element of the carrier of (c opp)
(c,C,i2) /. a is Element of the carrier' of (c opp)
cod ((c,C,i2) /. a) is Element of the carrier of (c opp)
cod ((i2 /. a) opp) is Element of the carrier of (c opp)
C --> (i1 opp) is Relation-like C -defined the carrier of (c opp) -valued Function-like V18(C, the carrier of (c opp)) Element of K19(K20(C, the carrier of (c opp)))
{(i1 opp)} is non empty set
K20(C,{(i1 opp)}) is set
(C --> (i1 opp)) /. a is Element of the carrier of (c opp)
((c opp),C,(c,C,i2)) is Relation-like C -defined the carrier of (c opp) -valued Function-like V18(C, the carrier of (c opp)) Element of K19(K20(C, the carrier of (c opp)))
K20(C, the carrier of (c opp)) is set
K19(K20(C, the carrier of (c opp))) is set
C --> (i1 opp) is Relation-like C -defined the carrier of (c opp) -valued Function-like V18(C, the carrier of (c opp)) Element of K19(K20(C, the carrier of (c opp)))
{(i1 opp)} is non empty set
K20(C,{(i1 opp)}) is set
a is set
i2 /. a is Element of the carrier' of c
dom (i2 /. a) is Element of the carrier of c
cod (i2 /. a) is Element of the carrier of c
b is Morphism of dom (i2 /. a), cod (i2 /. a)
dom b is Element of the carrier of c
cod b is Element of the carrier of c
Hom ((dom b),(cod b)) is Element of K19( the carrier' of c)
K19( the carrier' of c) is set
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = dom b & cod b₁ = cod b ) } is set
b opp is Morphism of (cod (i2 /. a)) opp ,(dom (i2 /. a)) opp
(cod (i2 /. a)) opp is Element of the carrier of (c opp)
(dom (i2 /. a)) opp is Element of the carrier of (c opp)
(i2 /. a) opp is Element of the carrier' of (c opp)
(c,C,i2) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
K20(C, the carrier of c) is set
K19(K20(C, the carrier of c)) is set
(c,C,i2) /. a is Element of the carrier of c
cod (b opp) is Element of the carrier of (c opp)
(c,C,i2) /. a is Element of the carrier' of (c opp)
cod ((c,C,i2) /. a) is Element of the carrier of (c opp)
C --> i1 is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
{i1} is non empty set
K20(C,{i1}) is set
(C --> i1) /. a is Element of the carrier of c
C is set
c is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
c opp is non empty non void V52() strict Category-like V65() V66() V67() with_identities CatStr
the carrier of c is non empty set
the carrier' of c is non empty set
the Target of c is Relation-like the carrier' of c -defined the carrier of c -valued Function-like V18( the carrier' of c, the carrier of c) Element of K19(K20( the carrier' of c, the carrier of c))
K20( the carrier' of c, the carrier of c) is set
K19(K20( the carrier' of c, the carrier of c)) is set
the Source of c is Relation-like the carrier' of c -defined the carrier of c -valued Function-like V18( the carrier' of c, the carrier of c) Element of K19(K20( the carrier' of c, the carrier of c))
the Comp of c is Relation-like K20( the carrier' of c, the carrier' of c) -defined the carrier' of c -valued Function-like Element of K19(K20(K20( the carrier' of c, the carrier' of c), the carrier' of c))
K20( the carrier' of c, the carrier' of c) is set
K20(K20( the carrier' of c, the carrier' of c), the carrier' of c) is set
K19(K20(K20( the carrier' of c, the carrier' of c), the carrier' of c)) is set
~ the Comp of c is Relation-like K20( the carrier' of c, the carrier' of c) -defined the carrier' of c -valued Function-like Element of K19(K20(K20( the carrier' of c, the carrier' of c), the carrier' of c))
CatStr(# the carrier of c, the carrier' of c, the Target of c, the Source of c,(~ the Comp of c) #) is strict CatStr
the carrier' of (c opp) is non empty set
K20(C, the carrier' of (c opp)) is set
K19(K20(C, the carrier' of (c opp))) is set
the carrier of (c opp) is non empty set
i1 is Relation-like C -defined the carrier' of (c opp) -valued Function-like V18(C, the carrier' of (c opp)) Element of K19(K20(C, the carrier' of (c opp)))
(c,C,i1) is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) Element of K19(K20(C, the carrier' of c))
K20(C, the carrier' of c) is set
K19(K20(C, the carrier' of c)) is set
i2 is Element of the carrier of (c opp)
opp i2 is Element of the carrier of c
i2 opp is Element of the carrier of ((c opp) opp)
(c opp) opp is non empty non void V52() strict Category-like V65() V66() V67() with_identities CatStr
the Target of (c opp) is Relation-like the carrier' of (c opp) -defined the carrier of (c opp) -valued Function-like V18( the carrier' of (c opp), the carrier of (c opp)) Element of K19(K20( the carrier' of (c opp), the carrier of (c opp)))
K20( the carrier' of (c opp), the carrier of (c opp)) is set
K19(K20( the carrier' of (c opp), the carrier of (c opp))) is set
the Source of (c opp) is Relation-like the carrier' of (c opp) -defined the carrier of (c opp) -valued Function-like V18( the carrier' of (c opp), the carrier of (c opp)) Element of K19(K20( the carrier' of (c opp), the carrier of (c opp)))
the Comp of (c opp) is Relation-like K20( the carrier' of (c opp), the carrier' of (c opp)) -defined the carrier' of (c opp) -valued Function-like Element of K19(K20(K20( the carrier' of (c opp), the carrier' of (c opp)), the carrier' of (c opp)))
K20( the carrier' of (c opp), the carrier' of (c opp)) is set
K20(K20( the carrier' of (c opp), the carrier' of (c opp)), the carrier' of (c opp)) is set
K19(K20(K20( the carrier' of (c opp), the carrier' of (c opp)), the carrier' of (c opp))) is set
~ the Comp of (c opp) is Relation-like K20( the carrier' of (c opp), the carrier' of (c opp)) -defined the carrier' of (c opp) -valued Function-like Element of K19(K20(K20( the carrier' of (c opp), the carrier' of (c opp)), the carrier' of (c opp)))
CatStr(# the carrier of (c opp), the carrier' of (c opp), the Target of (c opp), the Source of (c opp),(~ the Comp of (c opp)) #) is strict CatStr
the carrier of ((c opp) opp) is non empty set
((c opp),C,i1) is Relation-like C -defined the carrier of (c opp) -valued Function-like V18(C, the carrier of (c opp)) Element of K19(K20(C, the carrier of (c opp)))
K20(C, the carrier of (c opp)) is set
K19(K20(C, the carrier of (c opp))) is set
C --> i2 is Relation-like C -defined the carrier of (c opp) -valued Function-like V18(C, the carrier of (c opp)) Element of K19(K20(C, the carrier of (c opp)))
{i2} is non empty set
K20(C,{i2}) is set
a is set
i1 /. a is Element of the carrier' of (c opp)
dom (i1 /. a) is Element of the carrier of (c opp)
cod (i1 /. a) is Element of the carrier of (c opp)
b is Morphism of dom (i1 /. a), cod (i1 /. a)
dom b is Element of the carrier of (c opp)
cod b is Element of the carrier of (c opp)
Hom ((dom b),(cod b)) is Element of K19( the carrier' of (c opp))
K19( the carrier' of (c opp)) is set
{ b₁ where b₁ is Element of the carrier' of (c opp) : ( dom b₁ = dom b & cod b₁ = cod b ) } is set
(c,C,(c,C,i1)) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
K20(C, the carrier of c) is set
K19(K20(C, the carrier of c)) is set
(c,C,(c,C,i1)) /. a is Element of the carrier of c
(c,C,i1) /. a is Element of the carrier' of c
dom ((c,C,i1) /. a) is Element of the carrier of c
opp (i1 /. a) is Element of the carrier' of c
(i1 /. a) opp is Element of the carrier' of ((c opp) opp)
the carrier' of ((c opp) opp) is non empty set
dom (opp (i1 /. a)) is Element of the carrier of c
opp (cod (i1 /. a)) is Element of the carrier of c
(cod (i1 /. a)) opp is Element of the carrier of ((c opp) opp)
C --> (opp i2) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
{(opp i2)} is non empty set
K20(C,{(opp i2)}) is set
(C --> (opp i2)) /. a is Element of the carrier of c
(c,C,(c,C,i1)) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
K20(C, the carrier of c) is set
K19(K20(C, the carrier of c)) is set
C --> (opp i2) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
{(opp i2)} is non empty set
K20(C,{(opp i2)}) is set
a is set
i1 /. a is Element of the carrier' of (c opp)
dom (i1 /. a) is Element of the carrier of (c opp)
cod (i1 /. a) is Element of the carrier of (c opp)
b is Morphism of dom (i1 /. a), cod (i1 /. a)
dom b is Element of the carrier of (c opp)
cod b is Element of the carrier of (c opp)
Hom ((dom b),(cod b)) is Element of K19( the carrier' of (c opp))
K19( the carrier' of (c opp)) is set
{ b₁ where b₁ is Element of the carrier' of (c opp) : ( dom b₁ = dom b & cod b₁ = cod b ) } is set
b opp is Morphism of (cod (i1 /. a)) opp ,(dom (i1 /. a)) opp
(cod (i1 /. a)) opp is Element of the carrier of ((c opp) opp)
(dom (i1 /. a)) opp is Element of the carrier of ((c opp) opp)
(i1 /. a) opp is Element of the carrier' of ((c opp) opp)
the carrier' of ((c opp) opp) is non empty set
((c opp),C,i1) is Relation-like C -defined the carrier of (c opp) -valued Function-like V18(C, the carrier of (c opp)) Element of K19(K20(C, the carrier of (c opp)))
K20(C, the carrier of (c opp)) is set
K19(K20(C, the carrier of (c opp))) is set
((c opp),C,i1) /. a is Element of the carrier of (c opp)
opp (i1 /. a) is Element of the carrier' of c
dom (opp (i1 /. a)) is Element of the carrier of c
(c,C,i1) /. a is Element of the carrier' of c
dom ((c,C,i1) /. a) is Element of the carrier of c
C --> i2 is Relation-like C -defined the carrier of (c opp) -valued Function-like V18(C, the carrier of (c opp)) Element of K19(K20(C, the carrier of (c opp)))
{i2} is non empty set
K20(C,{i2}) is set
(C --> i2) /. a is Element of the carrier of (c opp)
C is set
c is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier' of c is non empty set
c opp is non empty non void V52() strict Category-like V65() V66() V67() with_identities CatStr
the carrier of c is non empty set
the Target of c is Relation-like the carrier' of c -defined the carrier of c -valued Function-like V18( the carrier' of c, the carrier of c) Element of K19(K20( the carrier' of c, the carrier of c))
K20( the carrier' of c, the carrier of c) is set
K19(K20( the carrier' of c, the carrier of c)) is set
the Source of c is Relation-like the carrier' of c -defined the carrier of c -valued Function-like V18( the carrier' of c, the carrier of c) Element of K19(K20( the carrier' of c, the carrier of c))
the Comp of c is Relation-like K20( the carrier' of c, the carrier' of c) -defined the carrier' of c -valued Function-like Element of K19(K20(K20( the carrier' of c, the carrier' of c), the carrier' of c))
K20( the carrier' of c, the carrier' of c) is set
K20(K20( the carrier' of c, the carrier' of c), the carrier' of c) is set
K19(K20(K20( the carrier' of c, the carrier' of c), the carrier' of c)) is set
~ the Comp of c is Relation-like K20( the carrier' of c, the carrier' of c) -defined the carrier' of c -valued Function-like Element of K19(K20(K20( the carrier' of c, the carrier' of c), the carrier' of c))
CatStr(# the carrier of c, the carrier' of c, the Target of c, the Source of c,(~ the Comp of c) #) is strict CatStr
the carrier' of (c opp) is non empty set
i1 is Element of the carrier' of c
dom i1 is Element of the carrier of c
i1 opp is Element of the carrier' of (c opp)
i2 is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) (c, dom i1,C)
(c,C,i2) is Relation-like C -defined the carrier' of (c opp) -valued Function-like V18(C, the carrier' of (c opp)) Element of K19(K20(C, the carrier' of (c opp)))
K20(C, the carrier' of (c opp)) is set
K19(K20(C, the carrier' of (c opp))) is set
((c opp),C,(c,C,i2),(i1 opp)) is Relation-like C -defined the carrier' of (c opp) -valued Function-like V18(C, the carrier' of (c opp)) Element of K19(K20(C, the carrier' of (c opp)))
(c,C,i2,i1) is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) Element of K19(K20(C, the carrier' of c))
K20(C, the carrier' of c) is set
K19(K20(C, the carrier' of c)) is set
(c,C,(c,C,i2,i1)) is Relation-like C -defined the carrier' of (c opp) -valued Function-like V18(C, the carrier' of (c opp)) Element of K19(K20(C, the carrier' of (c opp)))
a is set
i2 /. a is Element of the carrier' of c
cod (i2 /. a) is Element of the carrier of c
(c,C,i2) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
K20(C, the carrier of c) is set
K19(K20(C, the carrier of c)) is set
(c,C,i2) /. a is Element of the carrier of c
C --> (dom i1) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
{(dom i1)} is non empty set
K20(C,{(dom i1)}) is set
(C --> (dom i1)) /. a is Element of the carrier of c
cod i1 is Element of the carrier of c
dom (i2 /. a) is Element of the carrier of c
Hom ((dom i1),(cod i1)) is Element of K19( the carrier' of c)
K19( the carrier' of c) is set
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = dom i1 & cod b₁ = cod i1 ) } is set
Hom ((dom (i2 /. a)),(cod (i2 /. a))) is Element of K19( the carrier' of c)
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = dom (i2 /. a) & cod b₁ = cod (i2 /. a) ) } is set
b is Morphism of dom i1, cod i1
b opp is Morphism of (cod i1) opp ,(dom i1) opp
(cod i1) opp is Element of the carrier of (c opp)
the carrier of (c opp) is non empty set
(dom i1) opp is Element of the carrier of (c opp)
f is Morphism of dom (i2 /. a), dom i1
f opp is Morphism of (dom i1) opp ,(dom (i2 /. a)) opp
(dom (i2 /. a)) opp is Element of the carrier of (c opp)
(i2 /. a) opp is Element of the carrier' of (c opp)
((c opp),C,(c,C,i2),(i1 opp)) /. a is Element of the carrier' of (c opp)
(c,C,i2) /. a is Element of the carrier' of (c opp)
((c,C,i2) /. a) (*) (i1 opp) is Element of the carrier' of (c opp)
((i2 /. a) opp) (*) (i1 opp) is Element of the carrier' of (c opp)
i1 (*) (i2 /. a) is Element of the carrier' of c
(i1 (*) (i2 /. a)) opp is Element of the carrier' of (c opp)
(c,C,i2,i1) /. a is Element of the carrier' of c
((c,C,i2,i1) /. a) opp is Element of the carrier' of (c opp)
(c,C,(c,C,i2,i1)) /. a is Element of the carrier' of (c opp)
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
i1 is set
the carrier' of C is non empty set
K20(i1, the carrier' of C) is set
K19(K20(i1, the carrier' of C)) is set
C is set
c is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of c is non empty set
the carrier' of c is non empty set
K20(C, the carrier' of c) is set
K19(K20(C, the carrier' of c)) is set
c opp is non empty non void V52() strict Category-like V65() V66() V67() with_identities CatStr
the Target of c is Relation-like the carrier' of c -defined the carrier of c -valued Function-like V18( the carrier' of c, the carrier of c) Element of K19(K20( the carrier' of c, the carrier of c))
K20( the carrier' of c, the carrier of c) is set
K19(K20( the carrier' of c, the carrier of c)) is set
the Source of c is Relation-like the carrier' of c -defined the carrier of c -valued Function-like V18( the carrier' of c, the carrier of c) Element of K19(K20( the carrier' of c, the carrier of c))
the Comp of c is Relation-like K20( the carrier' of c, the carrier' of c) -defined the carrier' of c -valued Function-like Element of K19(K20(K20( the carrier' of c, the carrier' of c), the carrier' of c))
K20( the carrier' of c, the carrier' of c) is set
K20(K20( the carrier' of c, the carrier' of c), the carrier' of c) is set
K19(K20(K20( the carrier' of c, the carrier' of c), the carrier' of c)) is set
~ the Comp of c is Relation-like K20( the carrier' of c, the carrier' of c) -defined the carrier' of c -valued Function-like Element of K19(K20(K20( the carrier' of c, the carrier' of c), the carrier' of c))
CatStr(# the carrier of c, the carrier' of c, the Target of c, the Source of c,(~ the Comp of c) #) is strict CatStr
i1 is Element of the carrier of c
i1 opp is Element of the carrier of (c opp)
the carrier of (c opp) is non empty set
i2 is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) Element of K19(K20(C, the carrier' of c))
(c,C,i2) is Relation-like C -defined the carrier' of (c opp) -valued Function-like V18(C, the carrier' of (c opp)) Element of K19(K20(C, the carrier' of (c opp)))
the carrier' of (c opp) is non empty set
K20(C, the carrier' of (c opp)) is set
K19(K20(C, the carrier' of (c opp))) is set
((c opp),C,(c,C,i2)) is Relation-like C -defined the carrier of (c opp) -valued Function-like V18(C, the carrier of (c opp)) Element of K19(K20(C, the carrier of (c opp)))
K20(C, the carrier of (c opp)) is set
K19(K20(C, the carrier of (c opp))) is set
a is Element of the carrier of (c opp)
Hom ((i1 opp),a) is Element of K19( the carrier' of (c opp))
K19( the carrier' of (c opp)) is set
{ b₁ where b₁ is Element of the carrier' of (c opp) : ( dom b₁ = i1 opp & cod b₁ = a ) } is set
b is Relation-like C -defined the carrier' of (c opp) -valued Function-like V18(C, the carrier' of (c opp)) (c opp ,a,C)
((c opp),C,b) is Relation-like C -defined the carrier of (c opp) -valued Function-like V18(C, the carrier of (c opp)) Element of K19(K20(C, the carrier of (c opp)))
opp a is Element of the carrier of c
a opp is Element of the carrier of ((c opp) opp)
(c opp) opp is non empty non void V52() strict Category-like V65() V66() V67() with_identities CatStr
the Target of (c opp) is Relation-like the carrier' of (c opp) -defined the carrier of (c opp) -valued Function-like V18( the carrier' of (c opp), the carrier of (c opp)) Element of K19(K20( the carrier' of (c opp), the carrier of (c opp)))
K20( the carrier' of (c opp), the carrier of (c opp)) is set
K19(K20( the carrier' of (c opp), the carrier of (c opp))) is set
the Source of (c opp) is Relation-like the carrier' of (c opp) -defined the carrier of (c opp) -valued Function-like V18( the carrier' of (c opp), the carrier of (c opp)) Element of K19(K20( the carrier' of (c opp), the carrier of (c opp)))
the Comp of (c opp) is Relation-like K20( the carrier' of (c opp), the carrier' of (c opp)) -defined the carrier' of (c opp) -valued Function-like Element of K19(K20(K20( the carrier' of (c opp), the carrier' of (c opp)), the carrier' of (c opp)))
K20( the carrier' of (c opp), the carrier' of (c opp)) is set
K20(K20( the carrier' of (c opp), the carrier' of (c opp)), the carrier' of (c opp)) is set
K19(K20(K20( the carrier' of (c opp), the carrier' of (c opp)), the carrier' of (c opp))) is set
~ the Comp of (c opp) is Relation-like K20( the carrier' of (c opp), the carrier' of (c opp)) -defined the carrier' of (c opp) -valued Function-like Element of K19(K20(K20( the carrier' of (c opp), the carrier' of (c opp)), the carrier' of (c opp)))
CatStr(# the carrier of (c opp), the carrier' of (c opp), the Target of (c opp), the Source of (c opp),(~ the Comp of (c opp)) #) is strict CatStr
the carrier of ((c opp) opp) is non empty set
(c,C,b) is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) Element of K19(K20(C, the carrier' of c))
g is set
i2 /. g is Element of the carrier' of c
dom (i2 /. g) is Element of the carrier of c
cod (i2 /. g) is Element of the carrier of c
h is Morphism of dom (i2 /. g), cod (i2 /. g)
dom h is Element of the carrier of c
cod h is Element of the carrier of c
Hom ((dom h),(cod h)) is Element of K19( the carrier' of c)
K19( the carrier' of c) is set
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = dom h & cod b₁ = cod h ) } is set
h opp is Morphism of (cod (i2 /. g)) opp ,(dom (i2 /. g)) opp
(cod (i2 /. g)) opp is Element of the carrier of (c opp)
(dom (i2 /. g)) opp is Element of the carrier of (c opp)
(i2 /. g) opp is Element of the carrier' of (c opp)
b /. g is Element of the carrier' of (c opp)
dom (b /. g) is Element of the carrier of (c opp)
cod (b /. g) is Element of the carrier of (c opp)
i is Morphism of dom (b /. g), cod (b /. g)
dom i is Element of the carrier of (c opp)
cod i is Element of the carrier of (c opp)
Hom ((dom i),(cod i)) is Element of K19( the carrier' of (c opp))
{ b₁ where b₁ is Element of the carrier' of (c opp) : ( dom b₁ = dom i & cod b₁ = cod i ) } is set
i opp is Morphism of (cod (b /. g)) opp ,(dom (b /. g)) opp
(cod (b /. g)) opp is Element of the carrier of ((c opp) opp)
(dom (b /. g)) opp is Element of the carrier of ((c opp) opp)
(b /. g) opp is Element of the carrier' of ((c opp) opp)
the carrier' of ((c opp) opp) is non empty set
(c,C,i2) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
K20(C, the carrier of c) is set
K19(K20(C, the carrier of c)) is set
(c,C,i2) /. g is Element of the carrier of c
dom (h opp) is Element of the carrier of (c opp)
(c,C,i2) /. g is Element of the carrier' of (c opp)
dom ((c,C,i2) /. g) is Element of the carrier of (c opp)
((c opp),C,b) /. g is Element of the carrier of (c opp)
opp (b /. g) is Element of the carrier' of c
cod (opp (b /. g)) is Element of the carrier of c
f is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) (c, opp a,C)
f /. g is Element of the carrier' of c
cod (f /. g) is Element of the carrier of c
(c,C,f) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
(c,C,f) /. g is Element of the carrier of c
Hom ((opp a),i1) is Element of K19( the carrier' of c)
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = opp a & cod b₁ = i1 ) } is set
g is Element of the carrier' of c
g opp is Element of the carrier' of (c opp)
(opp a) opp is Element of the carrier of (c opp)
Hom ((i1 opp),((opp a) opp)) is Element of K19( the carrier' of (c opp))
{ b₁ where b₁ is Element of the carrier' of (c opp) : ( dom b₁ = i1 opp & cod b₁ = (opp a) opp ) } is set
h is Element of the carrier' of (c opp)
opp h is Element of the carrier' of c
h opp is Element of the carrier' of ((c opp) opp)
opp (i1 opp) is Element of the carrier of c
(i1 opp) opp is Element of the carrier of ((c opp) opp)
Hom ((opp a),(opp (i1 opp))) is Element of K19( the carrier' of c)
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = opp a & cod b₁ = opp (i1 opp) ) } is set
i is set
i2 /. i is Element of the carrier' of c
dom (i2 /. i) is Element of the carrier of c
cod (i2 /. i) is Element of the carrier of c
h is Morphism of dom (i2 /. i), cod (i2 /. i)
dom h is Element of the carrier of c
cod h is Element of the carrier of c
Hom ((dom h),(cod h)) is Element of K19( the carrier' of c)
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = dom h & cod b₁ = cod h ) } is set
h opp is Morphism of (cod (i2 /. i)) opp ,(dom (i2 /. i)) opp
(cod (i2 /. i)) opp is Element of the carrier of (c opp)
(dom (i2 /. i)) opp is Element of the carrier of (c opp)
(i2 /. i) opp is Element of the carrier' of (c opp)
cod ((i2 /. i) opp) is Element of the carrier of (c opp)
(c,C,i2) /. i is Element of the carrier' of (c opp)
cod ((c,C,i2) /. i) is Element of the carrier of (c opp)
dom h is Element of the carrier of (c opp)
h (*) ((c,C,i2) /. i) is Element of the carrier' of (c opp)
opp (h (*) ((c,C,i2) /. i)) is Element of the carrier' of c
(h (*) ((c,C,i2) /. i)) opp is Element of the carrier' of ((c opp) opp)
b /. i is Element of the carrier' of (c opp)
opp (b /. i) is Element of the carrier' of c
(b /. i) opp is Element of the carrier' of ((c opp) opp)
f /. i is Element of the carrier' of c
opp ((c,C,i2) /. i) is Element of the carrier' of c
((c,C,i2) /. i) opp is Element of the carrier' of ((c opp) opp)
(opp ((c,C,i2) /. i)) (*) (opp h) is Element of the carrier' of c
opp ((i2 /. i) opp) is Element of the carrier' of c
((i2 /. i) opp) opp is Element of the carrier' of ((c opp) opp)
(opp ((i2 /. i) opp)) (*) (opp h) is Element of the carrier' of c
(i2 /. i) (*) (opp h) is Element of the carrier' of c
i is set
(c,C,i2) /. i is Element of the carrier' of (c opp)
h (*) ((c,C,i2) /. i) is Element of the carrier' of (c opp)
b /. i is Element of the carrier' of (c opp)
i2 /. i is Element of the carrier' of c
dom (i2 /. i) is Element of the carrier of c
cod (opp h) is Element of the carrier of c
dom (opp h) is Element of the carrier of c
cod (i2 /. i) is Element of the carrier of c
Hom ((dom (opp h)),(cod (opp h))) is Element of K19( the carrier' of c)
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = dom (opp h) & cod b₁ = cod (opp h) ) } is set
Hom ((dom (i2 /. i)),(cod (i2 /. i))) is Element of K19( the carrier' of c)
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = dom (i2 /. i) & cod b₁ = cod (i2 /. i) ) } is set
h is Morphism of dom (opp h), cod (opp h)
h opp is Morphism of (cod (opp h)) opp ,(dom (opp h)) opp
(cod (opp h)) opp is Element of the carrier of (c opp)
(dom (opp h)) opp is Element of the carrier of (c opp)
(opp h) opp is Element of the carrier' of (c opp)
c₁₂ is Morphism of cod (opp h), cod (i2 /. i)
c₁₂ opp is Morphism of (cod (i2 /. i)) opp ,(cod (opp h)) opp
(cod (i2 /. i)) opp is Element of the carrier of (c opp)
(i2 /. i) opp is Element of the carrier' of (c opp)
(i2 /. i) (*) (opp h) is Element of the carrier' of c
f /. i is Element of the carrier' of c
((opp h) opp) (*) ((i2 /. i) opp) is Element of the carrier' of (c opp)
(f /. i) opp is Element of the carrier' of (c opp)
opp (b /. i) is Element of the carrier' of c
(b /. i) opp is Element of the carrier' of ((c opp) opp)
(opp (b /. i)) opp is Element of the carrier' of (c opp)
(c,C,i2) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
K20(C, the carrier of c) is set
K19(K20(C, the carrier of c)) is set
a is Element of the carrier of c
Hom (a,i1) is Element of K19( the carrier' of c)
K19( the carrier' of c) is set
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = a & cod b₁ = i1 ) } is set
b is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) (c,a,C)
(c,C,b) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
f is set
i2 /. f is Element of the carrier' of c
dom (i2 /. f) is Element of the carrier of c
cod (i2 /. f) is Element of the carrier of c
g is Morphism of dom (i2 /. f), cod (i2 /. f)
dom g is Element of the carrier of c
cod g is Element of the carrier of c
Hom ((dom g),(cod g)) is Element of K19( the carrier' of c)
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = dom g & cod b₁ = cod g ) } is set
g opp is Morphism of (cod (i2 /. f)) opp ,(dom (i2 /. f)) opp
(cod (i2 /. f)) opp is Element of the carrier of (c opp)
(dom (i2 /. f)) opp is Element of the carrier of (c opp)
(i2 /. f) opp is Element of the carrier' of (c opp)
b /. f is Element of the carrier' of c
dom (b /. f) is Element of the carrier of c
cod (b /. f) is Element of the carrier of c
h is Morphism of dom (b /. f), cod (b /. f)
dom h is Element of the carrier of c
cod h is Element of the carrier of c
Hom ((dom h),(cod h)) is Element of K19( the carrier' of c)
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = dom h & cod b₁ = cod h ) } is set
h opp is Morphism of (cod (b /. f)) opp ,(dom (b /. f)) opp
(cod (b /. f)) opp is Element of the carrier of (c opp)
(dom (b /. f)) opp is Element of the carrier of (c opp)
(b /. f) opp is Element of the carrier' of (c opp)
((c opp),C,(c,C,i2)) is Relation-like C -defined the carrier of (c opp) -valued Function-like V18(C, the carrier of (c opp)) Element of K19(K20(C, the carrier of (c opp)))
K20(C, the carrier of (c opp)) is set
K19(K20(C, the carrier of (c opp))) is set
((c opp),C,(c,C,i2)) /. f is Element of the carrier of (c opp)
(c,C,i2) /. f is Element of the carrier' of (c opp)
dom ((c,C,i2) /. f) is Element of the carrier of (c opp)
dom (g opp) is Element of the carrier of (c opp)
(c,C,b) /. f is Element of the carrier of c
dom (h opp) is Element of the carrier of (c opp)
(c,C,b) is Relation-like C -defined the carrier' of (c opp) -valued Function-like V18(C, the carrier' of (c opp)) Element of K19(K20(C, the carrier' of (c opp)))
(c,C,b) /. f is Element of the carrier' of (c opp)
dom ((c,C,b) /. f) is Element of the carrier of (c opp)
((c opp),C,(c,C,b)) is Relation-like C -defined the carrier of (c opp) -valued Function-like V18(C, the carrier of (c opp)) Element of K19(K20(C, the carrier of (c opp)))
((c opp),C,(c,C,b)) /. f is Element of the carrier of (c opp)
a opp is Element of the carrier of (c opp)
Hom ((i1 opp),(a opp)) is Element of K19( the carrier' of (c opp))
K19( the carrier' of (c opp)) is set
{ b₁ where b₁ is Element of the carrier' of (c opp) : ( dom b₁ = i1 opp & cod b₁ = a opp ) } is set
f is Relation-like C -defined the carrier' of (c opp) -valued Function-like V18(C, the carrier' of (c opp)) (c opp ,a opp ,C)
g is Element of the carrier' of (c opp)
opp g is Element of the carrier' of c
g opp is Element of the carrier' of ((c opp) opp)
(c opp) opp is non empty non void V52() strict Category-like V65() V66() V67() with_identities CatStr
the Target of (c opp) is Relation-like the carrier' of (c opp) -defined the carrier of (c opp) -valued Function-like V18( the carrier' of (c opp), the carrier of (c opp)) Element of K19(K20( the carrier' of (c opp), the carrier of (c opp)))
K20( the carrier' of (c opp), the carrier of (c opp)) is set
K19(K20( the carrier' of (c opp), the carrier of (c opp))) is set
the Source of (c opp) is Relation-like the carrier' of (c opp) -defined the carrier of (c opp) -valued Function-like V18( the carrier' of (c opp), the carrier of (c opp)) Element of K19(K20( the carrier' of (c opp), the carrier of (c opp)))
the Comp of (c opp) is Relation-like K20( the carrier' of (c opp), the carrier' of (c opp)) -defined the carrier' of (c opp) -valued Function-like Element of K19(K20(K20( the carrier' of (c opp), the carrier' of (c opp)), the carrier' of (c opp)))
K20( the carrier' of (c opp), the carrier' of (c opp)) is set
K20(K20( the carrier' of (c opp), the carrier' of (c opp)), the carrier' of (c opp)) is set
K19(K20(K20( the carrier' of (c opp), the carrier' of (c opp)), the carrier' of (c opp))) is set
~ the Comp of (c opp) is Relation-like K20( the carrier' of (c opp), the carrier' of (c opp)) -defined the carrier' of (c opp) -valued Function-like Element of K19(K20(K20( the carrier' of (c opp), the carrier' of (c opp)), the carrier' of (c opp)))
CatStr(# the carrier of (c opp), the carrier' of (c opp), the Target of (c opp), the Source of (c opp),(~ the Comp of (c opp)) #) is strict CatStr
the carrier' of ((c opp) opp) is non empty set
opp (a opp) is Element of the carrier of c
(a opp) opp is Element of the carrier of ((c opp) opp)
the carrier of ((c opp) opp) is non empty set
opp (i1 opp) is Element of the carrier of c
(i1 opp) opp is Element of the carrier of ((c opp) opp)
Hom ((opp (a opp)),(opp (i1 opp))) is Element of K19( the carrier' of c)
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = opp (a opp) & cod b₁ = opp (i1 opp) ) } is set
h is Element of the carrier' of c
h opp is Element of the carrier' of (c opp)
i is set
i2 /. i is Element of the carrier' of c
dom (i2 /. i) is Element of the carrier of c
cod (i2 /. i) is Element of the carrier of c
h is Morphism of dom (i2 /. i), cod (i2 /. i)
dom h is Element of the carrier of c
cod h is Element of the carrier of c
Hom ((dom h),(cod h)) is Element of K19( the carrier' of c)
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = dom h & cod b₁ = cod h ) } is set
h opp is Morphism of (cod (i2 /. i)) opp ,(dom (i2 /. i)) opp
(cod (i2 /. i)) opp is Element of the carrier of (c opp)
(dom (i2 /. i)) opp is Element of the carrier of (c opp)
(i2 /. i) opp is Element of the carrier' of (c opp)
(c,C,i2) /. i is Element of the carrier' of (c opp)
cod ((c,C,i2) /. i) is Element of the carrier of (c opp)
cod (h opp) is Element of the carrier of (c opp)
cod h is Element of the carrier of c
dom h is Element of the carrier of c
Hom ((dom h),(cod h)) is Element of K19( the carrier' of c)
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = dom h & cod b₁ = cod h ) } is set
Hom ((dom (i2 /. i)),(cod (i2 /. i))) is Element of K19( the carrier' of c)
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = dom (i2 /. i) & cod b₁ = cod (i2 /. i) ) } is set
c₁₂ is Morphism of dom h, cod h
c₁₂ opp is Morphism of (cod h) opp ,(dom h) opp
(cod h) opp is Element of the carrier of (c opp)
(dom h) opp is Element of the carrier of (c opp)
k9 is Morphism of cod h, cod (i2 /. i)
k9 opp is Morphism of (cod (i2 /. i)) opp ,(cod h) opp
(i2 /. i) (*) h is Element of the carrier' of c
b /. i is Element of the carrier' of c
(h opp) (*) ((i2 /. i) opp) is Element of the carrier' of (c opp)
(b /. i) opp is Element of the carrier' of (c opp)
f /. i is Element of the carrier' of (c opp)
(h opp) (*) ((c,C,i2) /. i) is Element of the carrier' of (c opp)
i is set
i2 /. i is Element of the carrier' of c
(i2 /. i) (*) h is Element of the carrier' of c
b /. i is Element of the carrier' of c
dom (i2 /. i) is Element of the carrier of c
cod (i2 /. i) is Element of the carrier of c
h is Morphism of dom (i2 /. i), cod (i2 /. i)
dom h is Element of the carrier of c
cod h is Element of the carrier of c
Hom ((dom h),(cod h)) is Element of K19( the carrier' of c)
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = dom h & cod b₁ = cod h ) } is set
h opp is Morphism of (cod (i2 /. i)) opp ,(dom (i2 /. i)) opp
(cod (i2 /. i)) opp is Element of the carrier of (c opp)
(dom (i2 /. i)) opp is Element of the carrier of (c opp)
(i2 /. i) opp is Element of the carrier' of (c opp)
(c,C,i2) /. i is Element of the carrier' of (c opp)
cod ((c,C,i2) /. i) is Element of the carrier of (c opp)
cod (h opp) is Element of the carrier of (c opp)
cod h is Element of the carrier of c
dom h is Element of the carrier of c
Hom ((dom h),(cod h)) is Element of K19( the carrier' of c)
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = dom h & cod b₁ = cod h ) } is set
Hom ((dom (i2 /. i)),(cod (i2 /. i))) is Element of K19( the carrier' of c)
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = dom (i2 /. i) & cod b₁ = cod (i2 /. i) ) } is set
c₁₂ is Morphism of dom h, cod h
c₁₂ opp is Morphism of (cod h) opp ,(dom h) opp
(cod h) opp is Element of the carrier of (c opp)
(dom h) opp is Element of the carrier of (c opp)
k9 is Morphism of cod h, cod (i2 /. i)
k9 opp is Morphism of (cod (i2 /. i)) opp ,(cod h) opp
(h opp) (*) ((c,C,i2) /. i) is Element of the carrier' of (c opp)
f /. i is Element of the carrier' of (c opp)
(b /. i) opp is Element of the carrier' of (c opp)
(h opp) (*) ((i2 /. i) opp) is Element of the carrier' of (c opp)
((i2 /. i) (*) h) opp is Element of the carrier' of (c opp)
C is set
c is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of c is non empty set
the carrier' of c is non empty set
i1 is Element of the carrier of c
i2 is Element of the carrier of c
a is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) (c,i1,C)
(c,C,a) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
K20(C, the carrier of c) is set
K19(K20(C, the carrier of c)) is set
b is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) (c,i2,C)
(c,C,b) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
Hom (i2,i2) is non empty Element of K19( the carrier' of c)
K19( the carrier' of c) is set
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = i2 & cod b₁ = i2 ) } is set
f is Element of the carrier' of c
Hom (i1,i2) is Element of K19( the carrier' of c)
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = i1 & cod b₁ = i2 ) } is set
g is Element of the carrier' of c
h is Morphism of i1,i2
dom h is Element of the carrier of c
id i1 is Morphism of i1,i1
Hom (i1,i1) is non empty Element of K19( the carrier' of c)
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = i1 & cod b₁ = i1 ) } is set
h is set
a /. h is Element of the carrier' of c
cod (a /. h) is Element of the carrier of c
(id i1) (*) (a /. h) is Element of the carrier' of c
id i2 is Morphism of i2,i2
h is set
b /. h is Element of the carrier' of c
cod (b /. h) is Element of the carrier of c
(id i2) (*) (b /. h) is Element of the carrier' of c
i is Element of the carrier' of c
Hom (i2,i1) is Element of K19( the carrier' of c)
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = i2 & cod b₁ = i1 ) } is set
h is Element of the carrier' of c
c₁₂ is Morphism of i2,i1
h * c₁₂ is Morphism of i2,i2
c₁₂ * h is Morphism of i1,i1
cod h is Element of the carrier of c
dom c₁₂ is Element of the carrier of c
cod c₁₂ is Element of the carrier of c
h (*) c₁₂ is Element of the carrier' of c
cod (h (*) c₁₂) is Element of the carrier of c
dom (h (*) c₁₂) is Element of the carrier of c
k9 is set
b /. k9 is Element of the carrier' of c
cod (b /. k9) is Element of the carrier of c
(h (*) c₁₂) (*) (b /. k9) is Element of the carrier' of c
c₁₂ (*) (b /. k9) is Element of the carrier' of c
h (*) (c₁₂ (*) (b /. k9)) is Element of the carrier' of c
a /. k9 is Element of the carrier' of c
h (*) (a /. k9) is Element of the carrier' of c
c₁₂ (*) h is Element of the carrier' of c
cod (c₁₂ (*) h) is Element of the carrier of c
dom (c₁₂ (*) h) is Element of the carrier of c
k9 is set
a /. k9 is Element of the carrier' of c
cod (a /. k9) is Element of the carrier of c
(c₁₂ (*) h) (*) (a /. k9) is Element of the carrier' of c
h (*) (a /. k9) is Element of the carrier' of c
c₁₂ (*) (h (*) (a /. k9)) is Element of the carrier' of c
b /. k9 is Element of the carrier' of c
c₁₂ (*) (b /. k9) is Element of the carrier' of c
C is set
c is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of c is non empty set
the carrier' of c is non empty set
i1 is Element of the carrier of c
i2 is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) (c,i1,C)
a is set
i2 /. a is Element of the carrier' of c
dom (i2 /. a) is Element of the carrier of c
b is Element of the carrier of c
Hom (b,i1) is Element of K19( the carrier' of c)
K19( the carrier' of c) is set
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = b & cod b₁ = i1 ) } is set
f is Morphism of b,i1
id b is Morphism of b,b
g is set
i2 /. g is Element of the carrier' of c
dom (i2 /. g) is Element of the carrier of c
Hom ((dom (i2 /. g)),b) is Element of K19( the carrier' of c)
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = dom (i2 /. g) & cod b₁ = b ) } is set
the Element of Hom ((dom (i2 /. g)),b) is Element of Hom ((dom (i2 /. g)),b)
i is Morphism of b,b
g is Relation-like Function-like set
dom g is set
rng g is set
K20(C, the carrier' of c) is set
K19(K20(C, the carrier' of c)) is set
i is set
h is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) Element of K19(K20(C, the carrier' of c))
h . i is set
h /. i is Element of the carrier' of c
i2 /. i is Element of the carrier' of c
dom (i2 /. i) is Element of the carrier of c
Hom ((dom (i2 /. i)),b) is Element of K19( the carrier' of c)
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = dom (i2 /. i) & cod b₁ = b ) } is set
cod (h /. i) is Element of the carrier of c
(c,C,h) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
K20(C, the carrier of c) is set
K19(K20(C, the carrier of c)) is set
(c,C,h) /. i is Element of the carrier of c
C --> b is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
{b} is non empty set
K20(C,{b}) is set
(C --> b) /. i is Element of the carrier of c
i is set
h . i is set
h /. i is Element of the carrier' of c
i2 /. i is Element of the carrier' of c
dom (i2 /. i) is Element of the carrier of c
Hom ((dom (i2 /. i)),b) is Element of K19( the carrier' of c)
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = dom (i2 /. i) & cod b₁ = b ) } is set
dom (h /. i) is Element of the carrier of c
(c,C,h) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
(c,C,h) /. i is Element of the carrier of c
(c,C,i2) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
(c,C,i2) /. i is Element of the carrier of c
Hom (i1,b) is Element of K19( the carrier' of c)
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = i1 & cod b₁ = b ) } is set
i is Element of the carrier' of c
h is Morphism of i1,b
h * f is Morphism of b,b
h (*) (i2 /. a) is Element of the carrier' of c
h /. a is Element of the carrier' of c
h . a is set
C is set
c is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of c is non empty set
the carrier' of c is non empty set
i1 is Element of the carrier of c
i2 is Element of the carrier of c
a is Morphism of i1,i2
dom a is Element of the carrier of c
cod a is Element of the carrier of c
b is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) (c,i1,C)
(c,C,b,a) is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) Element of K19(K20(C, the carrier' of c))
K20(C, the carrier' of c) is set
K19(K20(C, the carrier' of c)) is set
(c,C,(c,C,b,a)) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
K20(C, the carrier of c) is set
K19(K20(C, the carrier of c)) is set
f is Element of the carrier of c
Hom (i2,f) is Element of K19( the carrier' of c)
K19( the carrier' of c) is set
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = i2 & cod b₁ = f ) } is set
(c,C,b) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
C --> (dom a) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
{(dom a)} is non empty set
K20(C,{(dom a)}) is set
g is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) (c,f,C)
(c,C,g) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
(c,C,b) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
Hom (i1,f) is Element of K19( the carrier' of c)
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = i1 & cod b₁ = f ) } is set
h is Element of the carrier' of c
dom h is Element of the carrier of c
id i2 is Morphism of i2,i2
id i1 is Morphism of i1,i1
i is Morphism of i2,i1
a * i is Morphism of i2,i2
i * a is Morphism of i1,i1
Hom (i2,i1) is Element of K19( the carrier' of c)
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = i2 & cod b₁ = i1 ) } is set
Hom (i1,i2) is Element of K19( the carrier' of c)
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = i1 & cod b₁ = i2 ) } is set
dom i is Element of the carrier of c
cod i is Element of the carrier of c
a (*) i is Element of the carrier' of c
i (*) a is Element of the carrier' of c
cod h is Element of the carrier of c
h (*) i is Element of the carrier' of c
cod (h (*) i) is Element of the carrier of c
h is Element of the carrier' of c
dom (h (*) i) is Element of the carrier of c
c₁₂ is Element of the carrier' of c
dom c₁₂ is Element of the carrier of c
cod c₁₂ is Element of the carrier of c
c₁₂ (*) a is Element of the carrier' of c
cod (c₁₂ (*) a) is Element of the carrier of c
dom (c₁₂ (*) a) is Element of the carrier of c
k9 is set
b /. k9 is Element of the carrier' of c
cod (b /. k9) is Element of the carrier of c
(c₁₂ (*) a) (*) (b /. k9) is Element of the carrier' of c
a (*) (b /. k9) is Element of the carrier' of c
c₁₂ (*) (a (*) (b /. k9)) is Element of the carrier' of c
(c,C,b,a) /. k9 is Element of the carrier' of c
c₁₂ (*) ((c,C,b,a) /. k9) is Element of the carrier' of c
g /. k9 is Element of the carrier' of c
(c₁₂ (*) a) (*) i is Element of the carrier' of c
c₁₂ (*) (id i2) is Element of the carrier' of c
k9 is set
(c,C,b,a) /. k9 is Element of the carrier' of c
c₁₂ (*) ((c,C,b,a) /. k9) is Element of the carrier' of c
g /. k9 is Element of the carrier' of c
b /. k9 is Element of the carrier' of c
cod (b /. k9) is Element of the carrier of c
a (*) (b /. k9) is Element of the carrier' of c
cod (a (*) (b /. k9)) is Element of the carrier of c
c₁₂ (*) (a (*) (b /. k9)) is Element of the carrier' of c
i (*) (a (*) (b /. k9)) is Element of the carrier' of c
h (*) (i (*) (a (*) (b /. k9))) is Element of the carrier' of c
id (dom a) is Morphism of dom a, dom a
(id (dom a)) (*) (b /. k9) is Element of the carrier' of c
h (*) ((id (dom a)) (*) (b /. k9)) is Element of the carrier' of c
h (*) (b /. k9) is Element of the carrier' of c
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
the carrier' of C is non empty set
c is Element of the carrier of C
i1 is Relation-like {} -defined the carrier' of C -valued Function-like empty V18( {} , the carrier' of C) (C,c, {} )
i2 is Element of the carrier of C
Hom (c,i2) is Element of K19( the carrier' of C)
K19( the carrier' of C) is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = i2 ) } is set
the Relation-like {} -defined the carrier' of C -valued Function-like empty V18( {} , the carrier' of C) (C,i2, {} ) is Relation-like {} -defined the carrier' of C -valued Function-like empty V18( {} , the carrier' of C) (C,i2, {} )
(C,{},i1) is Relation-like {} -defined the carrier of C -valued Function-like empty V18( {} , the carrier of C) Element of K19(K20({}, the carrier of C))
K20({}, the carrier of C) is set
K19(K20({}, the carrier of C)) is set
b is Element of the carrier' of C
f is Morphism of c,i2
g is Morphism of c,i2
h is set
i1 /. h is Element of the carrier' of C
g (*) (i1 /. h) is Element of the carrier' of C
the Relation-like {} -defined the carrier' of C -valued Function-like empty V18( {} , the carrier' of C) (C,i2, {} ) /. h is Element of the carrier' of C
(C,{},i1) is Relation-like {} -defined the carrier of C -valued Function-like empty V18( {} , the carrier of C) Element of K19(K20({}, the carrier of C))
K20({}, the carrier of C) is set
K19(K20({}, the carrier of C)) is set
i2 is Element of the carrier of C
Hom (c,i2) is Element of K19( the carrier' of C)
K19( the carrier' of C) is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = i2 ) } is set
a is Morphism of c,i2
b is Relation-like {} -defined the carrier' of C -valued Function-like empty V18( {} , the carrier' of C) (C,i2, {} )
(C,{},b) is Relation-like {} -defined the carrier of C -valued Function-like empty V18( {} , the carrier of C) Element of K19(K20({}, the carrier of C))
f is Element of the carrier' of C
g is set
i1 /. g is Element of the carrier' of C
f (*) (i1 /. g) is Element of the carrier' of C
b /. g is Element of the carrier' of C
C is set
{C} is non empty set
c is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of c is non empty set
the carrier' of c is non empty set
i1 is Element of the carrier of c
id i1 is Morphism of i1,i1
( the carrier' of c,C,(id i1)) is Relation-like {C} -defined the carrier' of c -valued Function-like V18({C}, the carrier' of c) Element of K19(K20({C}, the carrier' of c))
K20({C}, the carrier' of c) is set
K19(K20({C}, the carrier' of c)) is set
{C} --> (id i1) is Relation-like {C} -defined {(id i1)} -valued Function-like V18({C},{(id i1)}) Element of K19(K20({C},{(id i1)}))
{(id i1)} is non empty set
K20({C},{(id i1)}) is set
K19(K20({C},{(id i1)})) is set
cod (id i1) is Element of the carrier of c
(c,{C},( the carrier' of c,C,(id i1))) is Relation-like {C} -defined the carrier of c -valued Function-like V18({C}, the carrier of c) Element of K19(K20({C}, the carrier of c))
K20({C}, the carrier of c) is set
K19(K20({C}, the carrier of c)) is set
a is Element of the carrier of c
Hom (i1,a) is Element of K19( the carrier' of c)
K19( the carrier' of c) is set
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = i1 & cod b₁ = a ) } is set
b is Relation-like {C} -defined the carrier' of c -valued Function-like V18({C}, the carrier' of c) (c,a,{C})
(c,{C},b) is Relation-like {C} -defined the carrier of c -valued Function-like V18({C}, the carrier of c) Element of K19(K20({C}, the carrier of c))
b /. C is Element of the carrier' of c
f is Element of the carrier' of c
cod f is Element of the carrier of c
dom f is Element of the carrier of c
(c,{C},( the carrier' of c,C,(id i1))) /. C is Element of the carrier of c
( the carrier' of c,C,(id i1)) /. C is Element of the carrier' of c
dom (( the carrier' of c,C,(id i1)) /. C) is Element of the carrier of c
dom (id i1) is Element of the carrier of c
g is Element of the carrier' of c
dom g is Element of the carrier of c
g (*) (id i1) is Element of the carrier' of c
g (*) (( the carrier' of c,C,(id i1)) /. C) is Element of the carrier' of c
h is set
( the carrier' of c,C,(id i1)) /. h is Element of the carrier' of c
g (*) (( the carrier' of c,C,(id i1)) /. h) is Element of the carrier' of c
b /. h is Element of the carrier' of c
b /. h is Element of the carrier' of c
g (*) (id i1) is Element of the carrier' of c
( the carrier' of c,C,(id i1)) /. h is Element of the carrier' of c
g (*) (( the carrier' of c,C,(id i1)) /. h) is Element of the carrier' of c
C is set
c is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of c is non empty set
the carrier' of c is non empty set
i1 is Element of the carrier of c
i2 is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) (c,i1,C)
a is Element of the carrier of c
K20(C, the carrier' of c) is set
K19(K20(C, the carrier' of c)) is set
b is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) Element of K19(K20(C, the carrier' of c))
f is set
i2 /. f is Element of the carrier' of c
dom (i2 /. f) is Element of the carrier of c
(c,C,b) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
K20(C, the carrier of c) is set
K19(K20(C, the carrier of c)) is set
(c,C,b) /. f is Element of the carrier of c
b /. f is Element of the carrier' of c
cod (b /. f) is Element of the carrier of c
(c,(dom (i2 /. f)),a) is Morphism of dom (i2 /. f),a
cod (c,(dom (i2 /. f)),a) is Element of the carrier of c
C --> a is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
{a} is non empty set
K20(C,{a}) is set
(C --> a) /. f is Element of the carrier of c
g is set
i2 /. g is Element of the carrier' of c
dom (i2 /. g) is Element of the carrier of c
(c,C,i2) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
(c,C,i2) /. g is Element of the carrier of c
(c,(dom (i2 /. g)),a) is Morphism of dom (i2 /. g),a
dom (c,(dom (i2 /. g)),a) is Element of the carrier of c
f is Relation-like C -defined the carrier' of c -valued Function-like V18(C, the carrier' of c) (c,a,C)
f /. g is Element of the carrier' of c
dom (f /. g) is Element of the carrier of c
(c,C,f) is Relation-like C -defined the carrier of c -valued Function-like V18(C, the carrier of c) Element of K19(K20(C, the carrier of c))
(c,C,f) /. g is Element of the carrier of c
Hom (i1,a) is Element of K19( the carrier' of c)
K19( the carrier' of c) is set
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = i1 & cod b₁ = a ) } is set
g is Element of the carrier' of c
h is Morphism of i1,a
h is Morphism of i1,a
c₁₂ is set
i2 /. c₁₂ is Element of the carrier' of c
dom (i2 /. c₁₂) is Element of the carrier of c
dom h is Element of the carrier of c
k is Morphism of dom (i2 /. c₁₂),a
cod (i2 /. c₁₂) is Element of the carrier of c
h (*) (i2 /. c₁₂) is Element of the carrier' of c
dom (h (*) (i2 /. c₁₂)) is Element of the carrier of c
cod h is Element of the carrier of c
cod (h (*) (i2 /. c₁₂)) is Element of the carrier of c
Hom ((dom (i2 /. c₁₂)),a) is Element of K19( the carrier' of c)
{ b₁ where b₁ is Element of the carrier' of c : ( dom b₁ = dom (i2 /. c₁₂) & cod b₁ = a ) } is set
f /. c₁₂ is Element of the carrier' of c
(c,(dom (i2 /. c₁₂)),a) is Morphism of dom (i2 /. c₁₂),a
i is Morphism of i1,a
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
the carrier' of C is non empty set
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
the carrier' of C is non empty set
C opp is non empty non void V52() strict Category-like V65() V66() V67() with_identities CatStr
the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like V18( the carrier' of C, the carrier of C) Element of K19(K20( the carrier' of C, the carrier of C))
K20( the carrier' of C, the carrier of C) is set
K19(K20( the carrier' of C, the carrier of C)) is set
the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like V18( the carrier' of C, the carrier of C) Element of K19(K20( the carrier' of C, the carrier of C))
the Comp of C is Relation-like K20( the carrier' of C, the carrier' of C) -defined the carrier' of C -valued Function-like Element of K19(K20(K20( the carrier' of C, the carrier' of C), the carrier' of C))
K20( the carrier' of C, the carrier' of C) is set
K20(K20( the carrier' of C, the carrier' of C), the carrier' of C) is set
K19(K20(K20( the carrier' of C, the carrier' of C), the carrier' of C)) is set
~ the Comp of C is Relation-like K20( the carrier' of C, the carrier' of C) -defined the carrier' of C -valued Function-like Element of K19(K20(K20( the carrier' of C, the carrier' of C), the carrier' of C))
CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,(~ the Comp of C) #) is strict CatStr
c is Element of the carrier of C
c opp is Element of the carrier of (C opp)
the carrier of (C opp) is non empty set
i1 is Element of the carrier' of C
i1 opp is Element of the carrier' of (C opp)
the carrier' of (C opp) is non empty set
i2 is Element of the carrier' of C
i2 opp is Element of the carrier' of (C opp)
dom i1 is Element of the carrier of C
dom i2 is Element of the carrier of C
cod i1 is Element of the carrier of C
cod i2 is Element of the carrier of C
f is Morphism of dom i1, cod i1
dom f is Element of the carrier of C
cod f is Element of the carrier of C
Hom ((dom f),(cod f)) is Element of K19( the carrier' of C)
K19( the carrier' of C) is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = dom f & cod b₁ = cod f ) } is set
f opp is Morphism of (cod i1) opp ,(dom i1) opp
(cod i1) opp is Element of the carrier of (C opp)
(dom i1) opp is Element of the carrier of (C opp)
cod (i1 opp) is Element of the carrier of (C opp)
cod (i2 opp) is Element of the carrier of (C opp)
dom (i1 opp) is Element of the carrier of (C opp)
dom (i2 opp) is Element of the carrier of (C opp)
g is Morphism of dom i2, cod i2
dom g is Element of the carrier of C
cod g is Element of the carrier of C
Hom ((dom g),(cod g)) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = dom g & cod b₁ = cod g ) } is set
g opp is Morphism of (cod i2) opp ,(dom i2) opp
(cod i2) opp is Element of the carrier of (C opp)
(dom i2) opp is Element of the carrier of (C opp)
h is Element of the carrier of (C opp)
Hom ((dom (i1 opp)),h) is Element of K19( the carrier' of (C opp))
K19( the carrier' of (C opp)) is set
{ b₁ where b₁ is Element of the carrier' of (C opp) : ( dom b₁ = dom (i1 opp) & cod b₁ = h ) } is set
Hom ((dom (i2 opp)),h) is Element of K19( the carrier' of (C opp))
{ b₁ where b₁ is Element of the carrier' of (C opp) : ( dom b₁ = dom (i2 opp) & cod b₁ = h ) } is set
Hom ((c opp),h) is Element of K19( the carrier' of (C opp))
{ b₁ where b₁ is Element of the carrier' of (C opp) : ( dom b₁ = c opp & cod b₁ = h ) } is set
i is Element of the carrier' of (C opp)
h is Element of the carrier' of (C opp)
c₁₂ is Morphism of dom (i2 opp), cod (i2 opp)
dom c₁₂ is Element of the carrier of (C opp)
cod c₁₂ is Element of the carrier of (C opp)
Hom ((dom c₁₂),(cod c₁₂)) is Element of K19( the carrier' of (C opp))
{ b₁ where b₁ is Element of the carrier' of (C opp) : ( dom b₁ = dom c₁₂ & cod b₁ = cod c₁₂ ) } is set
opp h is Element of the carrier' of C
h opp is Element of the carrier' of ((C opp) opp)
(C opp) opp is non empty non void V52() strict Category-like V65() V66() V67() with_identities CatStr
the Target of (C opp) is Relation-like the carrier' of (C opp) -defined the carrier of (C opp) -valued Function-like V18( the carrier' of (C opp), the carrier of (C opp)) Element of K19(K20( the carrier' of (C opp), the carrier of (C opp)))
K20( the carrier' of (C opp), the carrier of (C opp)) is set
K19(K20( the carrier' of (C opp), the carrier of (C opp))) is set
the Source of (C opp) is Relation-like the carrier' of (C opp) -defined the carrier of (C opp) -valued Function-like V18( the carrier' of (C opp), the carrier of (C opp)) Element of K19(K20( the carrier' of (C opp), the carrier of (C opp)))
the Comp of (C opp) is Relation-like K20( the carrier' of (C opp), the carrier' of (C opp)) -defined the carrier' of (C opp) -valued Function-like Element of K19(K20(K20( the carrier' of (C opp), the carrier' of (C opp)), the carrier' of (C opp)))
K20( the carrier' of (C opp), the carrier' of (C opp)) is set
K20(K20( the carrier' of (C opp), the carrier' of (C opp)), the carrier' of (C opp)) is set
K19(K20(K20( the carrier' of (C opp), the carrier' of (C opp)), the carrier' of (C opp))) is set
~ the Comp of (C opp) is Relation-like K20( the carrier' of (C opp), the carrier' of (C opp)) -defined the carrier' of (C opp) -valued Function-like Element of K19(K20(K20( the carrier' of (C opp), the carrier' of (C opp)), the carrier' of (C opp)))
CatStr(# the carrier of (C opp), the carrier' of (C opp), the Target of (C opp), the Source of (C opp),(~ the Comp of (C opp)) #) is strict CatStr
the carrier' of ((C opp) opp) is non empty set
opp h is Element of the carrier of C
h opp is Element of the carrier of ((C opp) opp)
the carrier of ((C opp) opp) is non empty set
opp (dom (i2 opp)) is Element of the carrier of C
(dom (i2 opp)) opp is Element of the carrier of ((C opp) opp)
Hom ((opp h),(opp (dom (i2 opp)))) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = opp h & cod b₁ = opp (dom (i2 opp)) ) } is set
opp (i2 opp) is Element of the carrier' of C
(i2 opp) opp is Element of the carrier' of ((C opp) opp)
cod (opp (i2 opp)) is Element of the carrier of C
Hom ((opp h),(cod (opp (i2 opp)))) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = opp h & cod b₁ = cod (opp (i2 opp)) ) } is set
k9 is Morphism of dom (i1 opp), cod (i1 opp)
dom k9 is Element of the carrier of (C opp)
cod k9 is Element of the carrier of (C opp)
Hom ((dom k9),(cod k9)) is Element of K19( the carrier' of (C opp))
{ b₁ where b₁ is Element of the carrier' of (C opp) : ( dom b₁ = dom k9 & cod b₁ = cod k9 ) } is set
opp i is Element of the carrier' of C
i opp is Element of the carrier' of ((C opp) opp)
opp (dom (i1 opp)) is Element of the carrier of C
(dom (i1 opp)) opp is Element of the carrier of ((C opp) opp)
Hom ((opp h),(opp (dom (i1 opp)))) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = opp h & cod b₁ = opp (dom (i1 opp)) ) } is set
opp (i1 opp) is Element of the carrier' of C
(i1 opp) opp is Element of the carrier' of ((C opp) opp)
cod (opp (i1 opp)) is Element of the carrier of C
Hom ((opp h),(cod (opp (i1 opp)))) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = opp h & cod b₁ = cod (opp (i1 opp)) ) } is set
Hom ((opp h),c) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = opp h & cod b₁ = c ) } is set
k is Element of the carrier' of C
k opp is Element of the carrier' of (C opp)
(opp h) opp is Element of the carrier of (C opp)
Hom ((c opp),((opp h) opp)) is Element of K19( the carrier' of (C opp))
{ b₁ where b₁ is Element of the carrier' of (C opp) : ( dom b₁ = c opp & cod b₁ = (opp h) opp ) } is set
x is Element of the carrier' of (C opp)
x (*) (i1 opp) is Element of the carrier' of (C opp)
x (*) (i2 opp) is Element of the carrier' of (C opp)
opp x is Element of the carrier' of C
x opp is Element of the carrier' of ((C opp) opp)
opp (c opp) is Element of the carrier of C
(c opp) opp is Element of the carrier of ((C opp) opp)
Hom ((opp h),(opp (c opp))) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = opp h & cod b₁ = opp (c opp) ) } is set
(opp (i1 opp)) (*) (opp x) is Element of the carrier' of C
(opp (i2 opp)) (*) (opp x) is Element of the carrier' of C
dom x is Element of the carrier of (C opp)
opp (x (*) (i1 opp)) is Element of the carrier' of C
(x (*) (i1 opp)) opp is Element of the carrier' of ((C opp) opp)
opp (x (*) (i2 opp)) is Element of the carrier' of C
(x (*) (i2 opp)) opp is Element of the carrier' of ((C opp) opp)
cod (i1 opp) is Element of the carrier of (C opp)
cod (i2 opp) is Element of the carrier of (C opp)
dom (i1 opp) is Element of the carrier of (C opp)
dom (i2 opp) is Element of the carrier of (C opp)
dom i1 is Element of the carrier of C
cod i1 is Element of the carrier of C
f is Morphism of dom i1, cod i1
dom f is Element of the carrier of C
cod f is Element of the carrier of C
Hom ((dom f),(cod f)) is Element of K19( the carrier' of C)
K19( the carrier' of C) is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = dom f & cod b₁ = cod f ) } is set
f opp is Morphism of (cod i1) opp ,(dom i1) opp
(cod i1) opp is Element of the carrier of (C opp)
(dom i1) opp is Element of the carrier of (C opp)
dom i2 is Element of the carrier of C
cod i2 is Element of the carrier of C
g is Morphism of dom i2, cod i2
dom g is Element of the carrier of C
cod g is Element of the carrier of C
Hom ((dom g),(cod g)) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = dom g & cod b₁ = cod g ) } is set
g opp is Morphism of (cod i2) opp ,(dom i2) opp
(cod i2) opp is Element of the carrier of (C opp)
(dom i2) opp is Element of the carrier of (C opp)
h is Element of the carrier of C
Hom (h,(cod i1)) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = h & cod b₁ = cod i1 ) } is set
Hom (h,(cod i2)) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = h & cod b₁ = cod i2 ) } is set
Hom (h,c) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = h & cod b₁ = c ) } is set
i is Element of the carrier' of C
h is Element of the carrier' of C
h opp is Element of the carrier' of (C opp)
h opp is Element of the carrier of (C opp)
Hom (((cod i2) opp),(h opp)) is Element of K19( the carrier' of (C opp))
K19( the carrier' of (C opp)) is set
{ b₁ where b₁ is Element of the carrier' of (C opp) : ( dom b₁ = (cod i2) opp & cod b₁ = h opp ) } is set
Hom ((dom (i2 opp)),(h opp)) is Element of K19( the carrier' of (C opp))
{ b₁ where b₁ is Element of the carrier' of (C opp) : ( dom b₁ = dom (i2 opp) & cod b₁ = h opp ) } is set
i opp is Element of the carrier' of (C opp)
Hom (((cod i1) opp),(h opp)) is Element of K19( the carrier' of (C opp))
{ b₁ where b₁ is Element of the carrier' of (C opp) : ( dom b₁ = (cod i1) opp & cod b₁ = h opp ) } is set
Hom ((dom (i1 opp)),(h opp)) is Element of K19( the carrier' of (C opp))
{ b₁ where b₁ is Element of the carrier' of (C opp) : ( dom b₁ = dom (i1 opp) & cod b₁ = h opp ) } is set
Hom ((c opp),(h opp)) is Element of K19( the carrier' of (C opp))
{ b₁ where b₁ is Element of the carrier' of (C opp) : ( dom b₁ = c opp & cod b₁ = h opp ) } is set
c₁₂ is Element of the carrier' of (C opp)
opp c₁₂ is Element of the carrier' of C
c₁₂ opp is Element of the carrier' of ((C opp) opp)
(C opp) opp is non empty non void V52() strict Category-like V65() V66() V67() with_identities CatStr
the Target of (C opp) is Relation-like the carrier' of (C opp) -defined the carrier of (C opp) -valued Function-like V18( the carrier' of (C opp), the carrier of (C opp)) Element of K19(K20( the carrier' of (C opp), the carrier of (C opp)))
K20( the carrier' of (C opp), the carrier of (C opp)) is set
K19(K20( the carrier' of (C opp), the carrier of (C opp))) is set
the Source of (C opp) is Relation-like the carrier' of (C opp) -defined the carrier of (C opp) -valued Function-like V18( the carrier' of (C opp), the carrier of (C opp)) Element of K19(K20( the carrier' of (C opp), the carrier of (C opp)))
the Comp of (C opp) is Relation-like K20( the carrier' of (C opp), the carrier' of (C opp)) -defined the carrier' of (C opp) -valued Function-like Element of K19(K20(K20( the carrier' of (C opp), the carrier' of (C opp)), the carrier' of (C opp)))
K20( the carrier' of (C opp), the carrier' of (C opp)) is set
K20(K20( the carrier' of (C opp), the carrier' of (C opp)), the carrier' of (C opp)) is set
K19(K20(K20( the carrier' of (C opp), the carrier' of (C opp)), the carrier' of (C opp))) is set
~ the Comp of (C opp) is Relation-like K20( the carrier' of (C opp), the carrier' of (C opp)) -defined the carrier' of (C opp) -valued Function-like Element of K19(K20(K20( the carrier' of (C opp), the carrier' of (C opp)), the carrier' of (C opp)))
CatStr(# the carrier of (C opp), the carrier' of (C opp), the Target of (C opp), the Source of (C opp),(~ the Comp of (C opp)) #) is strict CatStr
the carrier' of ((C opp) opp) is non empty set
k9 is Element of the carrier' of C
i1 (*) k9 is Element of the carrier' of C
i2 (*) k9 is Element of the carrier' of C
k9 opp is Element of the carrier' of (C opp)
(k9 opp) (*) (i1 opp) is Element of the carrier' of (C opp)
(k9 opp) (*) (i2 opp) is Element of the carrier' of (C opp)
cod k9 is Element of the carrier of C
dom k9 is Element of the carrier of C
Hom ((dom k9),(cod k9)) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = dom k9 & cod b₁ = cod k9 ) } is set
Hom ((dom i1),(cod i1)) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = dom i1 & cod b₁ = cod i1 ) } is set
k is Morphism of dom i1, cod i1
k opp is Morphism of (cod i1) opp ,(dom i1) opp
x is Morphism of dom k9, dom i1
x opp is Morphism of (dom i1) opp ,(dom k9) opp
(dom k9) opp is Element of the carrier of (C opp)
(i1 (*) k9) opp is Element of the carrier' of (C opp)
Hom ((dom i2),(cod i2)) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = dom i2 & cod b₁ = cod i2 ) } is set
ff is Morphism of dom i2, cod i2
ff opp is Morphism of (cod i2) opp ,(dom i2) opp
gg is Morphism of dom k9, dom i2
gg opp is Morphism of (dom i2) opp ,(dom k9) opp
(i2 (*) k9) opp is Element of the carrier' of (C opp)
C is set
c is set
{C,c} is non empty set
i1 is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of i1 is non empty set
the carrier' of i1 is non empty set
i2 is Element of the carrier of i1
a is Element of the carrier' of i1
b is Element of the carrier' of i1
(C,c) --> (a,b) is Relation-like {C,c} -defined the carrier' of i1 -valued Function-like V18({C,c}, the carrier' of i1) Element of K19(K20({C,c}, the carrier' of i1))
K20({C,c}, the carrier' of i1) is set
K19(K20({C,c}, the carrier' of i1)) is set
cod a is Element of the carrier of i1
cod b is Element of the carrier of i1
(i1,{C,c},((C,c) --> (a,b))) is Relation-like {C,c} -defined the carrier of i1 -valued Function-like V18({C,c}, the carrier of i1) Element of K19(K20({C,c}, the carrier of i1))
K20({C,c}, the carrier of i1) is set
K19(K20({C,c}, the carrier of i1)) is set
h is Element of the carrier of i1
Hom (i2,h) is Element of K19( the carrier' of i1)
K19( the carrier' of i1) is set
{ b₁ where b₁ is Element of the carrier' of i1 : ( dom b₁ = i2 & cod b₁ = h ) } is set
i is Relation-like {C,c} -defined the carrier' of i1 -valued Function-like V18({C,c}, the carrier' of i1) (i1,h,{C,c})
(i1,{C,c},i) is Relation-like {C,c} -defined the carrier of i1 -valued Function-like V18({C,c}, the carrier of i1) Element of K19(K20({C,c}, the carrier of i1))
i /. C is Element of the carrier' of i1
i /. c is Element of the carrier' of i1
(i1,{C,c},((C,c) --> (a,b))) /. C is Element of the carrier of i1
((C,c) --> (a,b)) /. C is Element of the carrier' of i1
dom (((C,c) --> (a,b)) /. C) is Element of the carrier of i1
dom (i /. C) is Element of the carrier of i1
dom a is Element of the carrier of i1
(i1,{C,c},((C,c) --> (a,b))) /. c is Element of the carrier of i1
((C,c) --> (a,b)) /. c is Element of the carrier' of i1
dom (((C,c) --> (a,b)) /. c) is Element of the carrier of i1
dom (i /. c) is Element of the carrier of i1
dom b is Element of the carrier of i1
cod (i /. c) is Element of the carrier of i1
Hom ((dom b),h) is Element of K19( the carrier' of i1)
{ b₁ where b₁ is Element of the carrier' of i1 : ( dom b₁ = dom b & cod b₁ = h ) } is set
cod (i /. C) is Element of the carrier of i1
Hom ((dom a),h) is Element of K19( the carrier' of i1)
{ b₁ where b₁ is Element of the carrier' of i1 : ( dom b₁ = dom a & cod b₁ = h ) } is set
k9 is Element of the carrier' of i1
k is Element of the carrier' of i1
k (*) (((C,c) --> (a,b)) /. c) is Element of the carrier' of i1
k (*) b is Element of the carrier' of i1
k (*) (((C,c) --> (a,b)) /. C) is Element of the carrier' of i1
k (*) a is Element of the carrier' of i1
k (*) a is Element of the carrier' of i1
k (*) b is Element of the carrier' of i1
x is set
((C,c) --> (a,b)) /. x is Element of the carrier' of i1
k (*) (((C,c) --> (a,b)) /. x) is Element of the carrier' of i1
i /. x is Element of the carrier' of i1
((C,c) --> (a,b)) /. c is Element of the carrier' of i1
cod (((C,c) --> (a,b)) /. c) is Element of the carrier of i1
((C,c) --> (a,b)) /. C is Element of the carrier' of i1
cod (((C,c) --> (a,b)) /. C) is Element of the carrier of i1
cod a is Element of the carrier of i1
cod b is Element of the carrier of i1
dom a is Element of the carrier of i1
dom b is Element of the carrier of i1
h is Element of the carrier of i1
Hom ((dom a),h) is Element of K19( the carrier' of i1)
K19( the carrier' of i1) is set
{ b₁ where b₁ is Element of the carrier' of i1 : ( dom b₁ = dom a & cod b₁ = h ) } is set
Hom ((dom b),h) is Element of K19( the carrier' of i1)
{ b₁ where b₁ is Element of the carrier' of i1 : ( dom b₁ = dom b & cod b₁ = h ) } is set
Hom (i2,h) is Element of K19( the carrier' of i1)
{ b₁ where b₁ is Element of the carrier' of i1 : ( dom b₁ = i2 & cod b₁ = h ) } is set
i is Element of the carrier' of i1
h is Element of the carrier' of i1
cod i is Element of the carrier of i1
cod h is Element of the carrier of i1
(C,c) --> (i,h) is Relation-like {C,c} -defined the carrier' of i1 -valued Function-like V18({C,c}, the carrier' of i1) Element of K19(K20({C,c}, the carrier' of i1))
(i1,{C,c},((C,c) --> (a,b))) is Relation-like {C,c} -defined the carrier of i1 -valued Function-like V18({C,c}, the carrier of i1) Element of K19(K20({C,c}, the carrier of i1))
K20({C,c}, the carrier of i1) is set
K19(K20({C,c}, the carrier of i1)) is set
(C,c) --> ((dom a),(dom b)) is Relation-like {C,c} -defined the carrier of i1 -valued Function-like V18({C,c}, the carrier of i1) Element of K19(K20({C,c}, the carrier of i1))
dom i is Element of the carrier of i1
(C,c) --> ((dom i),(dom b)) is Relation-like {C,c} -defined the carrier of i1 -valued Function-like V18({C,c}, the carrier of i1) Element of K19(K20({C,c}, the carrier of i1))
dom h is Element of the carrier of i1
(C,c) --> ((dom i),(dom h)) is Relation-like {C,c} -defined the carrier of i1 -valued Function-like V18({C,c}, the carrier of i1) Element of K19(K20({C,c}, the carrier of i1))
c₁₂ is Relation-like {C,c} -defined the carrier' of i1 -valued Function-like V18({C,c}, the carrier' of i1) (i1,h,{C,c})
(i1,{C,c},c₁₂) is Relation-like {C,c} -defined the carrier of i1 -valued Function-like V18({C,c}, the carrier of i1) Element of K19(K20({C,c}, the carrier of i1))
k9 is Element of the carrier' of i1
k is Element of the carrier' of i1
k (*) a is Element of the carrier' of i1
k (*) b is Element of the carrier' of i1
x is set
((C,c) --> (a,b)) /. x is Element of the carrier' of i1
c₁₂ /. x is Element of the carrier' of i1
k (*) (((C,c) --> (a,b)) /. x) is Element of the carrier' of i1
k (*) (((C,c) --> (a,b)) /. c) is Element of the carrier' of i1
c₁₂ /. c is Element of the carrier' of i1
k (*) (((C,c) --> (a,b)) /. C) is Element of the carrier' of i1
c₁₂ /. C is Element of the carrier' of i1
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
the carrier' of C is non empty set
c is Element of the carrier of C
i1 is Element of the carrier of C
i2 is Element of the carrier' of C
dom i2 is Element of the carrier of C
a is Element of the carrier' of C
dom a is Element of the carrier of C
b is Element of the carrier' of C
dom b is Element of the carrier of C
f is Element of the carrier' of C
dom f is Element of the carrier of C
0 is empty Element of K99()
{0,1} is non empty set
(0,1) --> (i2,a) is Relation-like {0,1} -defined the carrier' of C -valued Function-like V18({0,1}, the carrier' of C) Element of K19(K20({0,1}, the carrier' of C))
K20({0,1}, the carrier' of C) is set
K19(K20({0,1}, the carrier' of C)) is set
(0,1) --> (b,f) is Relation-like {0,1} -defined the carrier' of C -valued Function-like V18({0,1}, the carrier' of C) Element of K19(K20({0,1}, the carrier' of C))
cod b is Element of the carrier of C
cod f is Element of the carrier of C
cod i2 is Element of the carrier of C
cod a is Element of the carrier of C
(C,{0,1},((0,1) --> (i2,a))) is Relation-like {0,1} -defined the carrier of C -valued Function-like V18({0,1}, the carrier of C) Element of K19(K20({0,1}, the carrier of C))
K20({0,1}, the carrier of C) is set
K19(K20({0,1}, the carrier of C)) is set
(0,1) --> ((dom b),(dom f)) is Relation-like {0,1} -defined the carrier of C -valued Function-like V18({0,1}, the carrier of C) Element of K19(K20({0,1}, the carrier of C))
(C,{0,1},((0,1) --> (b,f))) is Relation-like {0,1} -defined the carrier of C -valued Function-like V18({0,1}, the carrier of C) Element of K19(K20({0,1}, the carrier of C))
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
c is Element of the carrier of C
i1 is Element of the carrier of C
Hom (c,i1) is Element of K19( the carrier' of C)
the carrier' of C is non empty set
K19( the carrier' of C) is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = i1 ) } is set
i2 is Element of the carrier of C
Hom (i2,i1) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i2 & cod b₁ = i1 ) } is set
a is Morphism of c,i1
b is Morphism of i2,i1
cod a is Element of the carrier of C
cod b is Element of the carrier of C
dom a is Element of the carrier of C
dom b is Element of the carrier of C
f is Element of the carrier of C
Hom (c,f) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = f ) } is set
Hom (i2,f) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i2 & cod b₁ = f ) } is set
Hom (i1,f) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i1 & cod b₁ = f ) } is set
the Morphism of c,f is Morphism of c,f
the Morphism of i2,f is Morphism of i2,f
Hom ((dom b),f) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = dom b & cod b₁ = f ) } is set
Hom ((dom a),f) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = dom a & cod b₁ = f ) } is set
i is Element of the carrier' of C
i is Morphism of c,f
h is Morphism of i2,f
c₁₂ is Element of the carrier' of C
k9 is Morphism of i1,f
k is Morphism of i1,f
k * a is Morphism of c,f
k * b is Morphism of i2,f
x is Element of the carrier' of C
k (*) a is Element of the carrier' of C
k (*) b is Element of the carrier' of C
x is Element of the carrier' of C
cod a is Element of the carrier of C
cod b is Element of the carrier of C
dom a is Element of the carrier of C
dom b is Element of the carrier of C
f is Element of the carrier of C
Hom ((dom a),f) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = dom a & cod b₁ = f ) } is set
Hom ((dom b),f) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = dom b & cod b₁ = f ) } is set
Hom (i1,f) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i1 & cod b₁ = f ) } is set
g is Element of the carrier' of C
h is Element of the carrier' of C
Hom (c,f) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = f ) } is set
i is Morphism of i1,f
h is Element of the carrier' of C
c₁₂ is Element of the carrier' of C
c₁₂ (*) a is Element of the carrier' of C
c₁₂ (*) b is Element of the carrier' of C
k9 is Morphism of i1,f
k9 * a is Morphism of c,f
k9 * b is Morphism of i2,f
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
c is Element of the carrier of C
i1 is Element of the carrier of C
Hom (c,i1) is Element of K19( the carrier' of C)
the carrier' of C is non empty set
K19( the carrier' of C) is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = i1 ) } is set
i2 is Element of the carrier of C
Hom (i2,i1) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i2 & cod b₁ = i1 ) } is set
Hom (c,i2) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = i2 ) } is set
Hom (i2,c) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = i2 & cod b₁ = c ) } is set
a is Morphism of c,i1
b is Morphism of i2,i1
0 is empty Element of K99()
{0,1} is non empty set
cod a is Element of the carrier of C
cod b is Element of the carrier of C
(0,1) --> (a,b) is Relation-like {0,1} -defined the carrier' of C -valued Function-like V18({0,1}, the carrier' of C) Element of K19(K20({0,1}, the carrier' of C))
K20({0,1}, the carrier' of C) is set
K19(K20({0,1}, the carrier' of C)) is set
g is Relation-like {0,1} -defined the carrier' of C -valued Function-like V18({0,1}, the carrier' of C) (C,i1,{0,1})
g /. 0 is Element of the carrier' of C
g /. 1 is Element of the carrier' of C
h is set
i is set
g /. h is Element of the carrier' of C
dom (g /. h) is Element of the carrier of C
g /. i is Element of the carrier' of C
dom (g /. i) is Element of the carrier of C
Hom ((dom (g /. h)),(dom (g /. i))) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = dom (g /. h) & cod b₁ = dom (g /. i) ) } is set
dom (g /. 0) is Element of the carrier of C
dom (g /. 1) is Element of the carrier of C
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
the carrier' of C is non empty set
c is Element of the carrier of C
Hom (c,c) is non empty Element of K19( the carrier' of C)
K19( the carrier' of C) is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = c ) } is set
id c is Morphism of c,c
i1 is Element of the carrier' of C
i2 is Element of the carrier' of C
a is Element of the carrier' of C
a (*) i1 is Element of the carrier' of C
a (*) i2 is Element of the carrier' of C
cod i1 is Element of the carrier of C
cod i2 is Element of the carrier of C
dom i1 is Element of the carrier of C
dom i2 is Element of the carrier of C
Hom ((dom i1),c) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = dom i1 & cod b₁ = c ) } is set
Hom ((dom i2),c) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = dom i2 & cod b₁ = c ) } is set
b is Element of the carrier' of C
(id c) (*) i1 is Element of the carrier' of C
(id c) (*) i2 is Element of the carrier' of C
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
the carrier' of C is non empty set
c is Element of the carrier of C
i1 is Element of the carrier of C
i2 is Element of the carrier' of C
a is Element of the carrier' of C
b is Morphism of c,i1
dom b is Element of the carrier of C
cod b is Element of the carrier of C
b (*) i2 is Element of the carrier' of C
b (*) a is Element of the carrier' of C
cod i2 is Element of the carrier of C
cod a is Element of the carrier of C
0 is empty Element of K99()
(0,1) --> (i2,a) is Relation-like {0,1} -defined the carrier' of C -valued Function-like V18({0,1}, the carrier' of C) Element of K19(K20({0,1}, the carrier' of C))
{0,1} is non empty set
K20({0,1}, the carrier' of C) is set
K19(K20({0,1}, the carrier' of C)) is set
(C,{0,1},((0,1) --> (i2,a)),b) is Relation-like {0,1} -defined the carrier' of C -valued Function-like V18({0,1}, the carrier' of C) Element of K19(K20({0,1}, the carrier' of C))
(0,1) --> ((b (*) i2),(b (*) a)) is Relation-like {0,1} -defined the carrier' of C -valued Function-like V18({0,1}, the carrier' of C) Element of K19(K20({0,1}, the carrier' of C))
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
the carrier' of C is non empty set
c is Element of the carrier of C
i1 is Element of the carrier' of C
dom i1 is Element of the carrier of C
i2 is Element of the carrier' of C
dom i2 is Element of the carrier of C
id (dom i1) is Morphism of dom i1, dom i1
(C,(dom i2),(dom i1)) is Morphism of dom i2, dom i1
cod (C,(dom i2),(dom i1)) is Element of the carrier of C
dom (C,(dom i2),(dom i1)) is Element of the carrier of C
Hom ((dom i1),(dom i1)) is non empty Element of K19( the carrier' of C)
K19( the carrier' of C) is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = dom i1 & cod b₁ = dom i1 ) } is set
Hom ((dom i2),(dom i1)) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = dom i2 & cod b₁ = dom i1 ) } is set
Hom (c,(dom i1)) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = dom i1 ) } is set
h is Element of the carrier' of C
cod h is Element of the carrier of C
cod i1 is Element of the carrier of C
dom h is Element of the carrier of C
i is Morphism of dom i1,c
i (*) h is Element of the carrier' of C
dom (i (*) h) is Element of the carrier of C
cod i2 is Element of the carrier of C
(i (*) h) (*) i2 is Element of the carrier' of C
dom ((i (*) h) (*) i2) is Element of the carrier of C
cod (i (*) h) is Element of the carrier of C
Hom (c,c) is non empty Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = c ) } is set
cod ((i (*) h) (*) i2) is Element of the carrier of C
(C,(dom i2),c) is Morphism of dom i2,c
Hom ((dom i1),c) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = dom i1 & cod b₁ = c ) } is set
id c is Morphism of c,c
h is Morphism of c, dom i1
i * h is Morphism of c,c
h * i is Morphism of dom i1, dom i1
i (*) h is Element of the carrier' of C
(i (*) h) (*) i1 is Element of the carrier' of C
h (*) i1 is Element of the carrier' of C
i (*) (h (*) i1) is Element of the carrier' of C
dom i is Element of the carrier of C
id (dom i) is Morphism of dom i, dom i
i (*) (id (dom i)) is Element of the carrier' of C
h (*) i is Element of the carrier' of C
C is non empty non void V52() Category-like V65() V66() V67() with_identities CatStr
the carrier of C is non empty set
the carrier' of C is non empty set
c is Element of the carrier of C
i1 is Element of the carrier' of C
dom i1 is Element of the carrier of C
i2 is Element of the carrier' of C
dom i2 is Element of the carrier of C
id (dom i2) is Morphism of dom i2, dom i2
(C,(dom i1),(dom i2)) is Morphism of dom i1, dom i2
cod (C,(dom i1),(dom i2)) is Element of the carrier of C
dom (C,(dom i1),(dom i2)) is Element of the carrier of C
Hom ((dom i2),(dom i2)) is non empty Element of K19( the carrier' of C)
K19( the carrier' of C) is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = dom i2 & cod b₁ = dom i2 ) } is set
Hom ((dom i1),(dom i2)) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = dom i1 & cod b₁ = dom i2 ) } is set
Hom (c,(dom i2)) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = dom i2 ) } is set
h is Element of the carrier' of C
cod h is Element of the carrier of C
cod i2 is Element of the carrier of C
dom h is Element of the carrier of C
i is Morphism of dom i2,c
i (*) h is Element of the carrier' of C
dom (i (*) h) is Element of the carrier of C
cod i1 is Element of the carrier of C
(i (*) h) (*) i1 is Element of the carrier' of C
dom ((i (*) h) (*) i1) is Element of the carrier of C
cod (i (*) h) is Element of the carrier of C
Hom (c,c) is non empty Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = c ) } is set
cod ((i (*) h) (*) i1) is Element of the carrier of C
(C,(dom i1),c) is Morphism of dom i1,c
Hom ((dom i2),c) is Element of K19( the carrier' of C)
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = dom i2 & cod b₁ = c ) } is set
id c is Morphism of c,c
h is Morphism of c, dom i2
i * h is Morphism of c,c
h * i is Morphism of dom i2, dom i2
i (*) h is Element of the carrier' of C
(i (*) h) (*) i2 is Element of the carrier' of C
h (*) i2 is Element of the carrier' of C
i (*) (h (*) i2) is Element of the carrier' of C
dom i is Element of the carrier of C
id (dom i) is Morphism of dom i, dom i
i (*) (id (dom i)) is Element of the carrier' of C
h (*) i is Element of the carrier' of C