:: 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
(