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

F

K20(F

K19(K20(F

C is set

F

C is Relation-like F

c is set

C /. c is Element of F

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

F

K20(F

K19(K20(F

C is Relation-like F

c is Relation-like F

i1 is set

C /. i1 is Element of F

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

dom ((C,c) --> (i2,a)) is set

((C,c) --> (i2,a)) . c

( the carrier' of i1,C,i2) . c

((C,c) --> ((dom i2),(dom a))) . c

( the carrier of i1,C,(dom i2)) . c

((C,c) --> (i2,a)) /. c

((C,c) --> ((dom i2),(dom a))) /. c

((C,c) --> (i2,a)) . c

( the carrier' of i1,c,a) . c

((C,c) --> ((dom i2),(dom a))) . c

( the carrier of i1,c,(dom a)) . c

((C,c) --> (i2,a)) /. c

((C,c) --> ((dom i2),(dom a))) /. c

((C,c) --> (i2,a)) /. c

((C,c) --> ((dom i2),(dom a))) /. c

((C,c) --> (i2,a)) /. c

((C,c) --> ((dom i2),(dom a))) /. c

(i1,{C,c},((C,c) --> (i2,a))) /. 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

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

dom ((C,c) --> (i2,a)) is set

((C,c) --> (i2,a)) . c

( the carrier' of i1,C,i2) . c

((C,c) --> ((cod i2),(cod a))) . c

( the carrier of i1,C,(cod i2)) . c

((C,c) --> (i2,a)) /. c

((C,c) --> ((cod i2),(cod a))) /. c

((C,c) --> (i2,a)) . c

( the carrier' of i1,c,a) . c

((C,c) --> ((cod i2),(cod a))) . c

( the carrier of i1,c,(cod a)) . c

((C,c) --> (i2,a)) /. c

((C,c) --> ((cod i2),(cod a))) /. c

((C,c) --> (i2,a)) /. c

((C,c) --> ((cod i2),(cod a))) /. c

((C,c) --> (i2,a)) /. c

((C,c) --> ((cod i2),(cod a))) /. c

(i1,{C,c},((C,c) --> (i2,a))) /. 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

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

Hom (i1,c) is Element of K19( the carrier' of C)

{ b

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

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

Hom (i1,c) is Element of K19( the carrier' of C)

{ b

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

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

Hom (i1,c) is Element of K19( the carrier' of C)

{ b

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

Hom (i2,i1) is Element of K19( the carrier' of C)

{ b

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

Hom (i2,c) is Element of K19( the carrier' of C)

{ b

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

Hom (i1,c) is Element of K19( the carrier' of C)

{ b

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

Hom (i2,i1) is Element of K19( the carrier' of C)

{ b

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

Hom (i2,c) is Element of K19( the carrier' of C)

{ b

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

Hom (i2,i1) is Element of K19( the carrier' of C)

{ b

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

Hom (c,i1) is Element of K19( the carrier' of C)

{ b

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

Hom (c,i2) is Element of K19( the carrier' of C)

{ b

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

Hom (i2,i1) is Element of K19( the carrier' of C)

{ b

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

Hom (i2,c) is Element of K19( the carrier' of C)

{ b

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

Hom (i1,c) is Element of K19( the carrier' of C)

{ b

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

Hom (i1,c) is Element of K19( the carrier' of C)

{ b

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

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

Hom (i1,c) is Element of K19( the carrier' of C)

{ b

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

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

Hom (i1,c) is Element of K19( the carrier' of C)

{ b

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

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

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

b is Element of the carrier of C

Hom (a,b) is Element of K19( the carrier' of C)

{ b

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

(