K139() is Element of bool K135()
K135() is set
bool K135() is non empty set
{} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty Function-yielding V81() set
1 is non empty set
{{},1} is non empty set
K134() is set
bool K134() is non empty set
bool K139() is non empty set
C is set
D is set
[:C,D:] is Relation-like set
o is set
{o} is non empty set
o9 is set
{o9} is non empty set
[:{o},{o9}:] is Relation-like non empty set
[o,o9] is V15() set
{o,o9} is non empty set
{{o,o9},{o}} is non empty set
{[o,o9]} is Relation-like Function-like non empty set
C --> o is Relation-like C -defined {o} -valued Function-like constant total V18(C,{o}) Element of bool [:C,{o}:]
[:C,{o}:] is Relation-like set
bool [:C,{o}:] is non empty set
D --> o9 is Relation-like D -defined {o9} -valued Function-like constant total V18(D,{o9}) Element of bool [:D,{o9}:]
[:D,{o9}:] is Relation-like set
bool [:D,{o9}:] is non empty set
[:(C --> o),(D --> o9):] is Relation-like [:C,D:] -defined [:{o},{o9}:] -valued Function-like V18([:C,D:],[:{o},{o9}:]) Element of bool [:[:C,D:],[:{o},{o9}:]:]
[:[:C,D:],[:{o},{o9}:]:] is Relation-like set
bool [:[:C,D:],[:{o},{o9}:]:] is non empty set
[:C,D:] --> [o,o9] is Relation-like [:C,D:] -defined {[o,o9]} -valued Function-like constant total V18([:C,D:],{[o,o9]}) Element of bool [:[:C,D:],{[o,o9]}:]
[:[:C,D:],{[o,o9]}:] is Relation-like set
bool [:[:C,D:],{[o,o9]}:] is non empty set
dom (C --> o) is set
dom (D --> o9) is set
dom ([:C,D:] --> [o,o9]) is Relation-like set
[:(dom (C --> o)),(dom (D --> o9)):] is Relation-like set
m is set
p is set
[m,p] is V15() set
{m,p} is non empty set
{m} is non empty set
{{m,p},{m}} is non empty set
(C --> o) . m is set
(D --> o9) . p is set
([:C,D:] --> [o,o9]) . (m,p) is set
([:C,D:] --> [o,o9]) . [m,p] is set
[((C --> o) . m),((D --> o9) . p)] is V15() set
{((C --> o) . m),((D --> o9) . p)} is non empty set
{((C --> o) . m)} is non empty set
{{((C --> o) . m),((D --> o9) . p)},{((C --> o) . m)}} is non empty set
C is set
[[0]] C is Relation-like empty-yielding C -defined Function-like total set
C --> {} is Relation-like C -defined {{}} -valued Function-like constant total V18(C,{{}}) Function-yielding V81() Element of bool [:C,{{}}:]
{{}} is functional non empty set
[:C,{{}}:] is Relation-like set
bool [:C,{{}}:] is non empty set
C is Relation-like Function-like set
D is Relation-like Function-like set
C * D is Relation-like Function-like set
~ (C * D) is Relation-like Function-like set
~ C is Relation-like Function-like set
(~ C) * D is Relation-like Function-like set
o is set
dom ((~ C) * D) is set
dom (~ C) is set
dom C is set
m is set
o9 is set
[m,o9] is V15() set
{m,o9} is non empty set
{m} is non empty set
{{m,o9},{m}} is non empty set
[o9,m] is V15() set
{o9,m} is non empty set
{o9} is non empty set
{{o9,m},{o9}} is non empty set
p9 is set
p is set
[p9,p] is V15() set
{p9,p} is non empty set
{p9} is non empty set
{{p9,p},{p9}} is non empty set
(~ C) . (p9,p) is set
(~ C) . [p9,p] is set
dom D is set
C . (p,p9) is set
[p,p9] is V15() set
{p,p9} is non empty set
{p} is non empty set
{{p,p9},{p}} is non empty set
C . [p,p9] is set
dom (C * D) is set
m is set
o9 is set
[m,o9] is V15() set
{m,o9} is non empty set
{m} is non empty set
{{m,o9},{m}} is non empty set
[o9,m] is V15() set
{o9,m} is non empty set
{o9} is non empty set
{{o9,m},{o9}} is non empty set
C . (o9,m) is set
C . [o9,m] is set
(~ C) . (m,o9) is set
(~ C) . [m,o9] is set
o is set
o9 is set
[o,o9] is V15() set
{o,o9} is non empty set
{o} is non empty set
{{o,o9},{o}} is non empty set
[o9,o] is V15() set
{o9,o} is non empty set
{o9} is non empty set
{{o9,o},{o9}} is non empty set
((~ C) * D) . (o9,o) is set
((~ C) * D) . [o9,o] is set
(~ C) . (o9,o) is set
(~ C) . [o9,o] is set
D . ((~ C) . (o9,o)) is set
C . (o,o9) is set
C . [o,o9] is set
D . (C . (o,o9)) is set
(C * D) . (o,o9) is set
(C * D) . [o,o9] is set
D is Relation-like Function-like set
o is Relation-like Function-like set
[:D,o:] is Relation-like Function-like set
C is Relation-like Function-like set
[:D,o:] * C is Relation-like Function-like set
~ ([:D,o:] * C) is Relation-like Function-like set
[:o,D:] is Relation-like Function-like set
~ C is Relation-like Function-like set
[:o,D:] * (~ C) is Relation-like Function-like set
o9 is set
dom ([:o,D:] * (~ C)) is set
dom [:o,D:] is set
dom o is set
dom D is set
[:(dom o),(dom D):] is Relation-like set
m is set
p is set
[m,p] is V15() set
{m,p} is non empty set
{m} is non empty set
{{m,p},{m}} is non empty set
[:o,D:] . (m,p) is set
[:o,D:] . [m,p] is set
o . m is set
D . p is set
[(o . m),(D . p)] is V15() set
{(o . m),(D . p)} is non empty set
{(o . m)} is non empty set
{{(o . m),(D . p)},{(o . m)}} is non empty set
[:D,o:] . (p,m) is set
[p,m] is V15() set
{p,m} is non empty set
{p} is non empty set
{{p,m},{p}} is non empty set
[:D,o:] . [p,m] is set
[(D . p),(o . m)] is V15() set
{(D . p),(o . m)} is non empty set
{(D . p)} is non empty set
{{(D . p),(o . m)},{(D . p)}} is non empty set
dom (~ C) is set
dom C is set
a is set
p9 is set
[a,p9] is V15() set
{a,p9} is non empty set
{a} is non empty set
{{a,p9},{a}} is non empty set
dom [:D,o:] is set
[:(dom D),(dom o):] is Relation-like set
[p9,a] is V15() set
{p9,a} is non empty set
{p9} is non empty set
{{p9,a},{p9}} is non empty set
dom ([:D,o:] * C) is set
p is set
m is set
[p,m] is V15() set
{p,m} is non empty set
{p} is non empty set
{{p,m},{p}} is non empty set
[m,p] is V15() set
{m,p} is non empty set
{m} is non empty set
{{m,p},{m}} is non empty set
[:D,o:] . (m,p) is set
[:D,o:] . [m,p] is set
D . m is set
o . p is set
[(D . m),(o . p)] is V15() set
{(D . m),(o . p)} is non empty set
{(D . m)} is non empty set
{{(D . m),(o . p)},{(D . m)}} is non empty set
[:o,D:] . (p,m) is set
[:o,D:] . [p,m] is set
[(o . p),(D . m)] is V15() set
{(o . p),(D . m)} is non empty set
{(o . p)} is non empty set
{{(o . p),(D . m)},{(o . p)}} is non empty set
[:o,D:] . o9 is set
o9 is set
m is set
[o9,m] is V15() set
{o9,m} is non empty set
{o9} is non empty set
{{o9,m},{o9}} is non empty set
[:D,o:] . (o9,m) is set
[:D,o:] . [o9,m] is set
D . o9 is set
o . m is set
[(D . o9),(o . m)] is V15() set
{(D . o9),(o . m)} is non empty set
{(D . o9)} is non empty set
{{(D . o9),(o . m)},{(D . o9)}} is non empty set
[m,o9] is V15() set
{m,o9} is non empty set
{m} is non empty set
{{m,o9},{m}} is non empty set
([:o,D:] * (~ C)) . (m,o9) is set
([:o,D:] * (~ C)) . [m,o9] is set
[:o,D:] . (m,o9) is set
[:o,D:] . [m,o9] is set
(~ C) . ([:o,D:] . (m,o9)) is set
(~ C) . ((o . m),(D . o9)) is set
[(o . m),(D . o9)] is V15() set
{(o . m),(D . o9)} is non empty set
{(o . m)} is non empty set
{{(o . m),(D . o9)},{(o . m)}} is non empty set
(~ C) . [(o . m),(D . o9)] is set
C . ((D . o9),(o . m)) is set
C . [(D . o9),(o . m)] is set
C . ([:D,o:] . (o9,m)) is set
([:D,o:] * C) . (o9,m) is set
([:D,o:] * C) . [o9,m] is set
C is Relation-like Function-like Function-yielding V81() set
~ C is Relation-like Function-like set
D is set
dom (~ C) is set
(~ C) . D is set
dom C is set
o9 is set
o is set
[o9,o] is V15() set
{o9,o} is non empty set
{o9} is non empty set
{{o9,o},{o9}} is non empty set
[o,o9] is V15() set
{o,o9} is non empty set
{o} is non empty set
{{o,o9},{o}} is non empty set
C . (o,o9) is set
C . [o,o9] is Relation-like Function-like set
(~ C) . (o9,o) is set
(~ C) . [o9,o] is set
C is set
D is Relation-like C -defined Function-like total set
o is Relation-like C -defined Function-like total set
o9 is Relation-like C -defined Function-like total set
m is Relation-like C -defined Function-like total Function-yielding V81() ManySortedFunction of D,o
p is Relation-like C -defined Function-like total Function-yielding V81() ManySortedFunction of o,o9
p ** m is Relation-like Function-like Function-yielding V81() set
p9 is Relation-like C -defined Function-like total Function-yielding V81() set
a is set
p9 . a is Relation-like Function-like set
D . a is set
o9 . a is set
[:(D . a),(o9 . a):] is Relation-like set
bool [:(D . a),(o9 . a):] is non empty set
o . a is set
[:(o . a),(o9 . a):] is Relation-like set
bool [:(o . a),(o9 . a):] is non empty set
p . a is Relation-like Function-like set
[:(D . a),(o . a):] is Relation-like set
bool [:(D . a),(o . a):] is non empty set
m . a is Relation-like Function-like set
dom p9 is set
(p ** m) . a is Relation-like Function-like set
n99 is Relation-like D . a -defined o . a -valued Function-like V18(D . a,o . a) Element of bool [:(D . a),(o . a):]
n is Relation-like o . a -defined o9 . a -valued Function-like V18(o . a,o9 . a) Element of bool [:(o . a),(o9 . a):]
n * n99 is Relation-like D . a -defined o9 . a -valued Function-like Element of bool [:(D . a),(o9 . a):]
C is set
[:C,C:] is Relation-like set
D is Relation-like [:C,C:] -defined Function-like total set
~ D is Relation-like [:C,C:] -defined Function-like total set
C is set
[:C,C:] is Relation-like set
D is Relation-like [:C,C:] -defined Function-like total set
~ D is Relation-like [:C,C:] -defined Function-like total set
o is Relation-like [:C,C:] -defined Function-like set
C is set
D is non empty set
[:C,D:] is Relation-like set
bool [:C,D:] is non empty set
o is Relation-like C -defined D -valued Function-like V18(C,D) Element of bool [:C,D:]
o9 is Relation-like D -defined Function-like non empty total set
m is Relation-like D -defined Function-like non empty total set
o * o9 is Relation-like C -defined Function-like total set
o * m is Relation-like C -defined Function-like total set
p is Relation-like D -defined Function-like non empty total Function-yielding V81() ManySortedFunction of o9,m
o * p is Relation-like C -defined Function-like total Function-yielding V81() set
p9 is set
(o * p) . p9 is Relation-like Function-like set
(o * o9) . p9 is set
(o * m) . p9 is set
[:((o * o9) . p9),((o * m) . p9):] is Relation-like set
bool [:((o * o9) . p9),((o * m) . p9):] is non empty set
o . p9 is set
p . (o . p9) is Relation-like Function-like set
o9 . (o . p9) is set
m . (o . p9) is set
[:(o9 . (o . p9)),(m . (o . p9)):] is Relation-like set
bool [:(o9 . (o . p9)),(m . (o . p9)):] is non empty set
dom o is set
C is set
[:C,C:] is Relation-like set
D is Relation-like [:C,C:] -defined Function-like total set
o is Relation-like [:C,C:] -defined Function-like total set
o9 is Relation-like [:C,C:] -defined Function-like total Function-yielding V81() ManySortedFunction of D,o
~ o9 is Relation-like [:C,C:] -defined Function-like total Function-yielding V81() set
~ D is Relation-like [:C,C:] -defined Function-like total set
~ o is Relation-like [:C,C:] -defined Function-like total set
m is Relation-like [:C,C:] -defined Function-like total set
p is set
m . p is set
(~ D) . p is set
(~ o) . p is set
[:((~ D) . p),((~ o) . p):] is Relation-like set
bool [:((~ D) . p),((~ o) . p):] is non empty set
p9 is set
a is set
[p9,a] is V15() set
{p9,a} is non empty set
{p9} is non empty set
{{p9,a},{p9}} is non empty set
[a,p9] is V15() set
{a,p9} is non empty set
{a} is non empty set
{{a,p9},{a}} is non empty set
dom o is set
o . (a,p9) is set
o . [a,p9] is set
(~ o) . (p9,a) is set
(~ o) . [p9,a] is set
dom D is set
D . (a,p9) is set
D . [a,p9] is set
(~ D) . (p9,a) is set
(~ D) . [p9,a] is set
dom o9 is set
o9 . (a,p9) is set
o9 . [a,p9] is Relation-like Function-like set
m . (p9,a) is set
m . [p9,a] is set
C is non empty set
D is non empty set
[:C,D:] is Relation-like non empty set
o is Relation-like [:C,D:] -defined Function-like non empty total set
~ o is Relation-like [:D,C:] -defined Function-like non empty total set
[:D,C:] is Relation-like non empty set
o9 is Element of C
m is Element of D
(~ o) . (m,o9) is set
[m,o9] is V15() set
{m,o9} is non empty set
{m} is non empty set
{{m,o9},{m}} is non empty set
(~ o) . [m,o9] is set
o . (o9,m) is set
[o9,m] is V15() set
{o9,m} is non empty set
{o9} is non empty set
{{o9,m},{o9}} is non empty set
o . [o9,m] is set
[o9,m] is V15() Element of [:C,D:]
dom o is non empty set
C is set
D is Relation-like C -defined Function-like total Function-yielding V81() set
o is Relation-like C -defined Function-like total Function-yielding V81() set
o ** D is Relation-like Function-like Function-yielding V81() set
dom D is set
dom o is set
dom (o ** D) is set
(dom o) /\ (dom D) is set
C is set
D is Relation-like C -defined Function-like total Function-yielding V81() set
o is Relation-like C -defined Function-like total Function-yielding V81() set
o ** D is Relation-like C -defined Function-like Function-yielding V81() set
dom D is set
dom o is set
dom (o ** D) is set
(dom o) /\ (dom D) is set
o is Relation-like Function-like set
dom o is set
m is set
o9 is Relation-like Function-like set
dom o9 is set
o9 . m is set
C is set
D is set
o is Relation-like C -defined Function-like total set
o9 is Relation-like D -defined Function-like total set
dom o is set
dom o9 is set
m is set
o . m is set
o9 . m is set
m is set
o . m is set
o9 . m is set
C is set
D is set
o is Relation-like C -defined Function-like total set
o9 is Relation-like D -defined Function-like total set
p is set
o . p is set
o9 . p is set
m is Relation-like C -defined Function-like total set
m . p is set
C is set
D is set
o is set
o9 is Relation-like C -defined Function-like total set
m is Relation-like D -defined Function-like total set
p is Relation-like o -defined Function-like total set
p9 is set
o9 . p9 is set
p . p9 is set
m . p9 is set
C is set
D is Relation-like C -defined Function-like total set
o is Relation-like C -defined Function-like total set
o9 is set
D . o9 is set
o . o9 is set
o9 is set
D . o9 is set
o . o9 is set
F1() is non empty set
{ [b1,F2(b1)] where b1 is Element of F1() : P1[b1] } is set
D is set
o is set
[D,o] is V15() set
{D,o} is non empty set
{D} is non empty set
{{D,o},{D}} is non empty set
o9 is set
[D,o9] is V15() set
{D,o9} is non empty set
{{D,o9},{D}} is non empty set
m is Element of F1()
F2(m) is set
[m,F2(m)] is V15() set
{m,F2(m)} is non empty set
{m} is non empty set
{{m,F2(m)},{m}} is non empty set
p is Element of F1()
F2(p) is set
[p,F2(p)] is V15() set
{p,F2(p)} is non empty set
{p} is non empty set
{{p,F2(p)},{p}} is non empty set
D is set
o is Element of F1()
F2(o) is set
[o,F2(o)] is V15() set
{o,F2(o)} is non empty set
{o} is non empty set
{{o,F2(o)},{o}} is non empty set
F2() is Relation-like Function-like set
F1() is non empty set
{ [b1,F3(b1)] where b1 is Element of F1() : P1[b1] } is set
dom F2() is set
{ b1 where b1 is Element of F1() : P1[b1] } is set
D is set
o is Element of F1()
F3(o) is set
o9 is set
[D,o9] is V15() set
{D,o9} is non empty set
{D} is non empty set
{{D,o9},{D}} is non empty set
o is set
[D,o] is V15() set
{D,o} is non empty set
{{D,o},{D}} is non empty set
o9 is Element of F1()
F3(o9) is set
[o9,F3(o9)] is V15() set
{o9,F3(o9)} is non empty set
{o9} is non empty set
{{o9,F3(o9)},{o9}} is non empty set
F1() is non empty set
F2() is Relation-like Function-like set
{ [b1,F4(b1)] where b1 is Element of F1() : P1[b1] } is set
F3() is Element of F1()
F2() . F3() is set
F4(F3()) is set
dom F2() is set
{ b1 where b1 is Element of F1() : P1[b1] } is set
[F3(),F4(F3())] is V15() set
{F3(),F4(F3())} is non empty set
{F3()} is non empty set
{{F3(),F4(F3())},{F3()}} is non empty set
C is non empty non void V52() Category-like transitive associative reflexive with_identities CatStr
the carrier of C is non empty set
the carrier' of C is non empty set
the Comp of C is Relation-like [: the carrier' of C, the carrier' of C:] -defined the carrier' of C -valued Function-like Element of bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:]
[: the carrier' of C, the carrier' of C:] is Relation-like non empty set
[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is Relation-like non empty set
bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is non empty set
dom the Comp of C is Relation-like set
o is Element of the carrier of C
o9 is Element of the carrier of C
Hom (o,o9) is Element of bool the carrier' of C
bool the carrier' of C is non empty set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = o & cod b1 = o9 ) } is set
D is Element of the carrier of C
Hom (D,o) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = o ) } is set
[:(Hom (o,o9)),(Hom (D,o)):] is Relation-like the carrier' of C -defined the carrier' of C -valued Element of bool [: the carrier' of C, the carrier' of C:]
bool [: the carrier' of C, the carrier' of C:] is non empty set
m is set
m `1 is set
m `2 is set
p is Element of the carrier' of C
p9 is Element of the carrier' of C
[p,p9] is V15() Element of [: the carrier' of C, the carrier' of C:]
{p,p9} is non empty set
{p} is non empty set
{{p,p9},{p}} is non empty set
dom p is Element of the carrier of C
cod p9 is Element of the carrier of C
C is non empty non void V52() Category-like transitive associative reflexive with_identities CatStr
the carrier of C is non empty set
the Comp of C is Relation-like [: the carrier' of C, the carrier' of C:] -defined the carrier' of C -valued Function-like Element of bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:]
the carrier' of C is non empty set
[: the carrier' of C, the carrier' of C:] is Relation-like non empty set
[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is Relation-like non empty set
bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is non empty set
o is Element of the carrier of C
o9 is Element of the carrier of C
Hom (o,o9) is Element of bool the carrier' of C
bool the carrier' of C is non empty set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = o & cod b1 = o9 ) } is set
D is Element of the carrier of C
Hom (D,o) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = o ) } is set
[:(Hom (o,o9)),(Hom (D,o)):] is Relation-like the carrier' of C -defined the carrier' of C -valued Element of bool [: the carrier' of C, the carrier' of C:]
bool [: the carrier' of C, the carrier' of C:] is non empty set
the Comp of C .: [:(Hom (o,o9)),(Hom (D,o)):] is set
Hom (D,o9) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = o9 ) } is set
m is set
dom the Comp of C is Relation-like set
p is set
the Comp of C . p is set
p `1 is set
p `2 is set
p9 is Element of the carrier' of C
a is Element of the carrier' of C
[p9,a] is V15() Element of [: the carrier' of C, the carrier' of C:]
{p9,a} is non empty set
{p9} is non empty set
{{p9,a},{p9}} is non empty set
the Comp of C . (p9,a) is set
[p9,a] is V15() set
the Comp of C . [p9,a] is set
p9 (*) a is Element of the carrier' of C
C is non empty non void V52() CatStr
the carrier of C is non empty set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the carrier' of C is non empty set
bool the carrier' of C is non empty set
D is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty total set
o is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty total set
o9 is Element of the carrier of C
m is Element of the carrier of C
D . (o9,m) is set
[o9,m] is V15() set
{o9,m} is non empty set
{o9} is non empty set
{{o9,m},{o9}} is non empty set
D . [o9,m] is set
Hom (o9,m) is Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is non empty set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = o9 & cod b1 = m ) } is set
o . (o9,m) is set
o . [o9,m] is set
C is non empty non void V52() Category-like transitive associative reflexive with_identities CatStr
the carrier of C is non empty set
(C) is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty total set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
D is Element of the carrier of C
id D is Morphism of D,D
(C) . (D,D) is set
[D,D] is V15() set
{D,D} is non empty set
{D} is non empty set
{{D,D},{D}} is non empty set
(C) . [D,D] is set
Hom (D,D) is non empty Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is non empty set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = D ) } is set
C is non empty non void V52() Category-like transitive associative reflexive with_identities CatStr
the carrier of C is non empty set
[: the carrier of C, the carrier of C, the carrier of C:] is non empty set
(C) is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty total set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
{|(C),(C)|} is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like non empty total set
{|(C)|} is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like non empty total set
the carrier' of C is non empty set
[: the carrier' of C, the carrier' of C:] is Relation-like non empty set
the Comp of C is Relation-like [: the carrier' of C, the carrier' of C:] -defined the carrier' of C -valued Function-like Element of bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:]
[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is Relation-like non empty set
bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is non empty set
o9 is Relation-like Function-like set
dom o9 is set
p is set
m is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like non empty total set
dom m is non empty set
m . p is set
p `1 is set
(p `1) `2 is set
p `2 is set
(C) . (((p `1) `2),(p `2)) is set
[((p `1) `2),(p `2)] is V15() set
{((p `1) `2),(p `2)} is non empty set
{((p `1) `2)} is non empty set
{{((p `1) `2),(p `2)},{((p `1) `2)}} is non empty set
(C) . [((p `1) `2),(p `2)] is set
(p `1) `1 is set
(C) . (((p `1) `1),((p `1) `2)) is set
[((p `1) `1),((p `1) `2)] is V15() set
{((p `1) `1),((p `1) `2)} is non empty set
{((p `1) `1)} is non empty set
{{((p `1) `1),((p `1) `2)},{((p `1) `1)}} is non empty set
(C) . [((p `1) `1),((p `1) `2)] is set
[:((C) . (((p `1) `2),(p `2))),((C) . (((p `1) `1),((p `1) `2))):] is Relation-like set
the Comp of C | [:((C) . (((p `1) `2),(p `2))),((C) . (((p `1) `1),((p `1) `2))):] is Relation-like [: the carrier' of C, the carrier' of C:] -defined [:((C) . (((p `1) `2),(p `2))),((C) . (((p `1) `1),((p `1) `2))):] -defined [: the carrier' of C, the carrier' of C:] -defined the carrier' of C -valued Function-like Element of bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:]
p is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like non empty total Function-yielding V81() set
p9 is set
p . p9 is Relation-like Function-like set
n is Element of the carrier of C
n99 is Element of the carrier of C
p4 is Element of the carrier of C
[n,n99,p4] is V15() V16() Element of [: the carrier of C, the carrier of C, the carrier of C:]
[n,n99] is V15() set
{n,n99} is non empty set
{n} is non empty set
{{n,n99},{n}} is non empty set
[[n,n99],p4] is V15() set
{[n,n99],p4} is non empty set
{[n,n99]} is Relation-like Function-like non empty set
{{[n,n99],p4},{[n,n99]}} is non empty set
[n,n99,p4] `1 is set
([n,n99,p4] `1) `2 is set
f is Element of [: the carrier of C, the carrier of C, the carrier of C:]
f `2_3 is Element of the carrier of C
f `1 is set
(f `1) `2 is set
[n,n99,p4] `2 is set
f `3_3 is Element of the carrier of C
([n,n99,p4] `1) `1 is set
f `1_3 is Element of the carrier of C
(f `1) `1 is set
a is Relation-like Function-like set
(C) . (n99,p4) is set
[n99,p4] is V15() set
{n99,p4} is non empty set
{n99} is non empty set
{{n99,p4},{n99}} is non empty set
(C) . [n99,p4] is set
(C) . (n,n99) is set
(C) . [n,n99] is set
[:((C) . (n99,p4)),((C) . (n,n99)):] is Relation-like set
the Comp of C | [:((C) . (n99,p4)),((C) . (n,n99)):] is Relation-like [: the carrier' of C, the carrier' of C:] -defined [:((C) . (n99,p4)),((C) . (n,n99)):] -defined [: the carrier' of C, the carrier' of C:] -defined the carrier' of C -valued Function-like Element of bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:]
Hom (n,n99) is Element of bool the carrier' of C
bool the carrier' of C is non empty set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = n & cod b1 = n99 ) } is set
Hom (n99,p4) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = n99 & cod b1 = p4 ) } is set
{|(C)|} . p9 is set
{|(C)|} . (n,n99,p4) is set
(C) . (n,p4) is set
[n,p4] is V15() set
{n,p4} is non empty set
{{n,p4},{n}} is non empty set
(C) . [n,p4] is set
Hom (n,p4) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = n & cod b1 = p4 ) } is set
{|(C),(C)|} . p9 is set
{|(C),(C)|} . (n,n99,p4) is set
[:(Hom (n99,p4)),(Hom (n,n99)):] is Relation-like the carrier' of C -defined the carrier' of C -valued Element of bool [: the carrier' of C, the carrier' of C:]
bool [: the carrier' of C, the carrier' of C:] is non empty set
the Comp of C .: [:(Hom (n99,p4)),(Hom (n,n99)):] is set
rng a is set
dom the Comp of C is Relation-like set
dom a is set
[:({|(C),(C)|} . p9),({|(C)|} . p9):] is Relation-like set
bool [:({|(C),(C)|} . p9),({|(C)|} . p9):] is non empty set
p9 is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like non empty total Function-yielding V81() ManySortedFunction of {|(C),(C)|},{|(C)|}
a is Element of the carrier of C
n is Element of the carrier of C
n99 is Element of the carrier of C
p9 . (a,n,n99) is Relation-like [:((C) . (n,n99)),((C) . (a,n)):] -defined (C) . (a,n99) -valued Function-like V18([:((C) . (n,n99)),((C) . (a,n)):],(C) . (a,n99)) Element of bool [:[:((C) . (n,n99)),((C) . (a,n)):],((C) . (a,n99)):]
(C) . (n,n99) is set
[n,n99] is V15() set
{n,n99} is non empty set
{n} is non empty set
{{n,n99},{n}} is non empty set
(C) . [n,n99] is set
(C) . (a,n) is set
[a,n] is V15() set
{a,n} is non empty set
{a} is non empty set
{{a,n},{a}} is non empty set
(C) . [a,n] is set
[:((C) . (n,n99)),((C) . (a,n)):] is Relation-like set
(C) . (a,n99) is set
[a,n99] is V15() set
{a,n99} is non empty set
{{a,n99},{a}} is non empty set
(C) . [a,n99] is set
[:[:((C) . (n,n99)),((C) . (a,n)):],((C) . (a,n99)):] is Relation-like set
bool [:[:((C) . (n,n99)),((C) . (a,n)):],((C) . (a,n99)):] is non empty set
the Comp of C | [:((C) . (n,n99)),((C) . (a,n)):] is Relation-like [: the carrier' of C, the carrier' of C:] -defined [:((C) . (n,n99)),((C) . (a,n)):] -defined [: the carrier' of C, the carrier' of C:] -defined the carrier' of C -valued Function-like Element of bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:]
[a,n,n99] is V15() V16() Element of [: the carrier of C, the carrier of C, the carrier of C:]
[[a,n],n99] is V15() set
{[a,n],n99} is non empty set
{[a,n]} is Relation-like Function-like non empty set
{{[a,n],n99},{[a,n]}} is non empty set
[a,n,n99] `1 is set
([a,n,n99] `1) `1 is set
p4 is Element of [: the carrier of C, the carrier of C, the carrier of C:]
p4 `1_3 is Element of the carrier of C
p4 `1 is set
(p4 `1) `1 is set
([a,n,n99] `1) `2 is set
p4 `2_3 is Element of the carrier of C
(p4 `1) `2 is set
[a,n,n99] `2 is set
p4 `3_3 is Element of the carrier of C
p9 . [a,n,n99] is Relation-like Function-like set
D is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like non empty total Function-yielding V81() ManySortedFunction of {|(C),(C)|},{|(C)|}
o is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like non empty total Function-yielding V81() ManySortedFunction of {|(C),(C)|},{|(C)|}
o9 is set
m is Element of the carrier of C
p is Element of the carrier of C
p9 is Element of the carrier of C
[m,p,p9] is V15() V16() Element of [: the carrier of C, the carrier of C, the carrier of C:]
[m,p] is V15() set
{m,p} is non empty set
{m} is non empty set
{{m,p},{m}} is non empty set
[[m,p],p9] is V15() set
{[m,p],p9} is non empty set
{[m,p]} is Relation-like Function-like non empty set
{{[m,p],p9},{[m,p]}} is non empty set
D . o9 is Relation-like Function-like set
D . (m,p,p9) is Relation-like [:((C) . (p,p9)),((C) . (m,p)):] -defined (C) . (m,p9) -valued Function-like V18([:((C) . (p,p9)),((C) . (m,p)):],(C) . (m,p9)) Element of bool [:[:((C) . (p,p9)),((C) . (m,p)):],((C) . (m,p9)):]
(C) . (p,p9) is set
[p,p9] is V15() set
{p,p9} is non empty set
{p} is non empty set
{{p,p9},{p}} is non empty set
(C) . [p,p9] is set
(C) . (m,p) is set
(C) . [m,p] is set
[:((C) . (p,p9)),((C) . (m,p)):] is Relation-like set
(C) . (m,p9) is set
[m,p9] is V15() set
{m,p9} is non empty set
{{m,p9},{m}} is non empty set
(C) . [m,p9] is set
[:[:((C) . (p,p9)),((C) . (m,p)):],((C) . (m,p9)):] is Relation-like set
bool [:[:((C) . (p,p9)),((C) . (m,p)):],((C) . (m,p9)):] is non empty set
the Comp of C | [:((C) . (p,p9)),((C) . (m,p)):] is Relation-like [: the carrier' of C, the carrier' of C:] -defined [:((C) . (p,p9)),((C) . (m,p)):] -defined [: the carrier' of C, the carrier' of C:] -defined the carrier' of C -valued Function-like Element of bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:]
o . (m,p,p9) is Relation-like [:((C) . (p,p9)),((C) . (m,p)):] -defined (C) . (m,p9) -valued Function-like V18([:((C) . (p,p9)),((C) . (m,p)):],(C) . (m,p9)) Element of bool [:[:((C) . (p,p9)),((C) . (m,p)):],((C) . (m,p9)):]
o . o9 is Relation-like Function-like set
C is non empty non void V52() Category-like transitive associative reflexive with_identities CatStr
the carrier of C is non empty set
(C) is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty total set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
(C) is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like non empty total Function-yielding V81() ManySortedFunction of {|(C),(C)|},{|(C)|}
[: the carrier of C, the carrier of C, the carrier of C:] is non empty set
{|(C),(C)|} is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like non empty total set
{|(C)|} is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like non empty total set
D is Element of the carrier of C
o is Element of the carrier of C
Hom (D,o) is Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is non empty set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = o ) } is set
o9 is Element of the carrier of C
Hom (o,o9) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = o & cod b1 = o9 ) } is set
(C) . (D,o,o9) is Relation-like [:((C) . (o,o9)),((C) . (D,o)):] -defined (C) . (D,o9) -valued Function-like V18([:((C) . (o,o9)),((C) . (D,o)):],(C) . (D,o9)) Element of bool [:[:((C) . (o,o9)),((C) . (D,o)):],((C) . (D,o9)):]
(C) . (o,o9) is set
[o,o9] is V15() set
{o,o9} is non empty set
{o} is non empty set
{{o,o9},{o}} is non empty set
(C) . [o,o9] is set
(C) . (D,o) is set
[D,o] is V15() set
{D,o} is non empty set
{D} is non empty set
{{D,o},{D}} is non empty set
(C) . [D,o] is set
[:((C) . (o,o9)),((C) . (D,o)):] is Relation-like set
(C) . (D,o9) is set
[D,o9] is V15() set
{D,o9} is non empty set
{{D,o9},{D}} is non empty set
(C) . [D,o9] is set
[:[:((C) . (o,o9)),((C) . (D,o)):],((C) . (D,o9)):] is Relation-like set
bool [:[:((C) . (o,o9)),((C) . (D,o)):],((C) . (D,o9)):] is non empty set
m is Morphism of D,o
p is Morphism of o,o9
((C) . (D,o,o9)) . (p,m) is set
[p,m] is V15() set
{p,m} is non empty set
{p} is non empty set
{{p,m},{p}} is non empty set
((C) . (D,o,o9)) . [p,m] is set
p * m is Morphism of D,o9
[p,m] is V15() Element of [: the carrier' of C, the carrier' of C:]
[: the carrier' of C, the carrier' of C:] is Relation-like non empty set
dom p is Element of the carrier of C
cod m is Element of the carrier of C
the Comp of C is Relation-like [: the carrier' of C, the carrier' of C:] -defined the carrier' of C -valued Function-like Element of bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:]
[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is Relation-like non empty set
bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is non empty set
the Comp of C | [:((C) . (o,o9)),((C) . (D,o)):] is Relation-like [:((C) . (o,o9)),((C) . (D,o)):] -defined [: the carrier' of C, the carrier' of C:] -defined the carrier' of C -valued Function-like Element of bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:]
( the Comp of C | [:((C) . (o,o9)),((C) . (D,o)):]) . [p,m] is set
the Comp of C . (p,m) is set
the Comp of C . [p,m] is set
p (*) m is Element of the carrier' of C
C is non empty non void V52() Category-like transitive associative reflexive with_identities CatStr
the carrier of C is non empty set
(C) is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty total set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
(C) is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like non empty total Function-yielding V81() ManySortedFunction of {|(C),(C)|},{|(C)|}
[: the carrier of C, the carrier of C, the carrier of C:] is non empty set
{|(C),(C)|} is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like non empty total set
{|(C)|} is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like non empty total set
D is Element of the carrier of C
o is Element of the carrier of C
(C) . (D,o) is set
[D,o] is V15() set
{D,o} is non empty set
{D} is non empty set
{{D,o},{D}} is non empty set
(C) . [D,o] is set
o9 is Element of the carrier of C
(C) . (o,o9) is set
[o,o9] is V15() set
{o,o9} is non empty set
{o} is non empty set
{{o,o9},{o}} is non empty set
(C) . [o,o9] is set
m is Element of the carrier of C
(C) . (o9,m) is set
[o9,m] is V15() set
{o9,m} is non empty set
{o9} is non empty set
{{o9,m},{o9}} is non empty set
(C) . [o9,m] is set
(C) . (D,o9,m) is Relation-like [:((C) . (o9,m)),((C) . (D,o9)):] -defined (C) . (D,m) -valued Function-like V18([:((C) . (o9,m)),((C) . (D,o9)):],(C) . (D,m)) Element of bool [:[:((C) . (o9,m)),((C) . (D,o9)):],((C) . (D,m)):]
(C) . (D,o9) is set
[D,o9] is V15() set
{D,o9} is non empty set
{{D,o9},{D}} is non empty set
(C) . [D,o9] is set
[:((C) . (o9,m)),((C) . (D,o9)):] is Relation-like set
(C) . (D,m) is set
[D,m] is V15() set
{D,m} is non empty set
{{D,m},{D}} is non empty set
(C) . [D,m] is set
[:[:((C) . (o9,m)),((C) . (D,o9)):],((C) . (D,m)):] is Relation-like set
bool [:[:((C) . (o9,m)),((C) . (D,o9)):],((C) . (D,m)):] is non empty set
(C) . (D,o,o9) is Relation-like [:((C) . (o,o9)),((C) . (D,o)):] -defined (C) . (D,o9) -valued Function-like V18([:((C) . (o,o9)),((C) . (D,o)):],(C) . (D,o9)) Element of bool [:[:((C) . (o,o9)),((C) . (D,o)):],((C) . (D,o9)):]
[:((C) . (o,o9)),((C) . (D,o)):] is Relation-like set
[:[:((C) . (o,o9)),((C) . (D,o)):],((C) . (D,o9)):] is Relation-like set
bool [:[:((C) . (o,o9)),((C) . (D,o)):],((C) . (D,o9)):] is non empty set
(C) . (D,o,m) is Relation-like [:((C) . (o,m)),((C) . (D,o)):] -defined (C) . (D,m) -valued Function-like V18([:((C) . (o,m)),((C) . (D,o)):],(C) . (D,m)) Element of bool [:[:((C) . (o,m)),((C) . (D,o)):],((C) . (D,m)):]
(C) . (o,m) is set
[o,m] is V15() set
{o,m} is non empty set
{{o,m},{o}} is non empty set
(C) . [o,m] is set
[:((C) . (o,m)),((C) . (D,o)):] is Relation-like set
[:[:((C) . (o,m)),((C) . (D,o)):],((C) . (D,m)):] is Relation-like set
bool [:[:((C) . (o,m)),((C) . (D,o)):],((C) . (D,m)):] is non empty set
(C) . (o,o9,m) is Relation-like [:((C) . (o9,m)),((C) . (o,o9)):] -defined (C) . (o,m) -valued Function-like V18([:((C) . (o9,m)),((C) . (o,o9)):],(C) . (o,m)) Element of bool [:[:((C) . (o9,m)),((C) . (o,o9)):],((C) . (o,m)):]
[:((C) . (o9,m)),((C) . (o,o9)):] is Relation-like set
[:[:((C) . (o9,m)),((C) . (o,o9)):],((C) . (o,m)):] is Relation-like set
bool [:[:((C) . (o9,m)),((C) . (o,o9)):],((C) . (o,m)):] is non empty set
p is set
p9 is set
a is set
((C) . (D,o,o9)) . (p9,p) is set
[p9,p] is V15() set
{p9,p} is non empty set
{p9} is non empty set
{{p9,p},{p9}} is non empty set
((C) . (D,o,o9)) . [p9,p] is set
((C) . (D,o9,m)) . (a,(((C) . (D,o,o9)) . (p9,p))) is set
[a,(((C) . (D,o,o9)) . (p9,p))] is V15() set
{a,(((C) . (D,o,o9)) . (p9,p))} is non empty set
{a} is non empty set
{{a,(((C) . (D,o,o9)) . (p9,p))},{a}} is non empty set
((C) . (D,o9,m)) . [a,(((C) . (D,o,o9)) . (p9,p))] is set
((C) . (o,o9,m)) . (a,p9) is set
[a,p9] is V15() set
{a,p9} is non empty set
{{a,p9},{a}} is non empty set
((C) . (o,o9,m)) . [a,p9] is set
((C) . (D,o,m)) . ((((C) . (o,o9,m)) . (a,p9)),p) is set
[(((C) . (o,o9,m)) . (a,p9)),p] is V15() set
{(((C) . (o,o9,m)) . (a,p9)),p} is non empty set
{(((C) . (o,o9,m)) . (a,p9))} is non empty set
{{(((C) . (o,o9,m)) . (a,p9)),p},{(((C) . (o,o9,m)) . (a,p9))}} is non empty set
((C) . (D,o,m)) . [(((C) . (o,o9,m)) . (a,p9)),p] is set
Hom (D,o) is Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is non empty set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = o ) } is set
Hom (o,o9) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = o & cod b1 = o9 ) } is set
Hom (o9,m) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = o9 & cod b1 = m ) } is set
Hom (o,m) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = o & cod b1 = m ) } is set
n99 is Morphism of o,o9
p4 is Morphism of o9,m
p4 * n99 is Morphism of o,m
Hom (D,o9) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = o9 ) } is set
n is Morphism of D,o
n99 * n is Morphism of D,o9
p4 * (n99 * n) is Morphism of D,m
(p4 * n99) * n is Morphism of D,m
C is non empty non void V52() Category-like transitive associative reflexive with_identities CatStr
the carrier of C is non empty set
(C) is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty total set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
(C) is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like non empty total Function-yielding V81() ManySortedFunction of {|(C),(C)|},{|(C)|}
[: the carrier of C, the carrier of C, the carrier of C:] is non empty set
{|(C),(C)|} is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like non empty total set
{|(C)|} is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like non empty total set
D is Element of the carrier of C
(C) . (D,D) is set
[D,D] is V15() set
{D,D} is non empty set
{D} is non empty set
{{D,D},{D}} is non empty set
(C) . [D,D] is set
id D is Morphism of D,D
o is Element of the carrier of C
(C) . (o,D) is set
[o,D] is V15() set
{o,D} is non empty set
{o} is non empty set
{{o,D},{o}} is non empty set
(C) . [o,D] is set
(C) . (o,D,D) is Relation-like [:((C) . (D,D)),((C) . (o,D)):] -defined (C) . (o,D) -valued Function-like V18([:((C) . (D,D)),((C) . (o,D)):],(C) . (o,D)) Element of bool [:[:((C) . (D,D)),((C) . (o,D)):],((C) . (o,D)):]
[:((C) . (D,D)),((C) . (o,D)):] is Relation-like set
[:[:((C) . (D,D)),((C) . (o,D)):],((C) . (o,D)):] is Relation-like set
bool [:[:((C) . (D,D)),((C) . (o,D)):],((C) . (o,D)):] is non empty set
o9 is set
((C) . (o,D,D)) . ((id D),o9) is set
[(id D),o9] is V15() set
{(id D),o9} is non empty set
{(id D)} is non empty set
{{(id D),o9},{(id D)}} is non empty set
((C) . (o,D,D)) . [(id D),o9] is set
Hom (o,D) is Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is non empty set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = o & cod b1 = D ) } is set
Hom (D,D) is non empty Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = D ) } is set
m is Morphism of o,D
(id D) * m is Morphism of o,D
D is Element of the carrier of C
(C) . (D,D) is set
[D,D] is V15() set
{D,D} is non empty set
{D} is non empty set
{{D,D},{D}} is non empty set
(C) . [D,D] is set
id D is Morphism of D,D
o is Element of the carrier of C
(C) . (D,o) is set
[D,o] is V15() set
{D,o} is non empty set
{{D,o},{D}} is non empty set
(C) . [D,o] is set
(C) . (D,D,o) is Relation-like [:((C) . (D,o)),((C) . (D,D)):] -defined (C) . (D,o) -valued Function-like V18([:((C) . (D,o)),((C) . (D,D)):],(C) . (D,o)) Element of bool [:[:((C) . (D,o)),((C) . (D,D)):],((C) . (D,o)):]
[:((C) . (D,o)),((C) . (D,D)):] is Relation-like set
[:[:((C) . (D,o)),((C) . (D,D)):],((C) . (D,o)):] is Relation-like set
bool [:[:((C) . (D,o)),((C) . (D,D)):],((C) . (D,o)):] is non empty set
o9 is set
((C) . (D,D,o)) . (o9,(id D)) is set
[o9,(id D)] is V15() set
{o9,(id D)} is non empty set
{o9} is non empty set
{{o9,(id D)},{o9}} is non empty set
((C) . (D,D,o)) . [o9,(id D)] is set
Hom (D,o) is Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is non empty set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = o ) } is set
Hom (D,D) is non empty Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = D ) } is set
m is Morphism of D,o
m * (id D) is Morphism of D,o
C is non empty non void V52() Category-like transitive associative reflexive with_identities CatStr
the carrier of C is non empty set
(C) is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty total set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
(C) is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like non empty total Function-yielding V81() ManySortedFunction of {|(C),(C)|},{|(C)|}
[: the carrier of C, the carrier of C, the carrier of C:] is non empty set
{|(C),(C)|} is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like non empty total set
{|(C)|} is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like non empty total set
AltCatStr(# the carrier of C,(C),(C) #) is non empty strict AltCatStr
C is non empty non void V52() Category-like transitive associative reflexive with_identities CatStr
(C) is non empty strict AltCatStr
the carrier of C is non empty set
(C) is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty total set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
(C) is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like non empty total Function-yielding V81() ManySortedFunction of {|(C),(C)|},{|(C)|}
[: the carrier of C, the carrier of C, the carrier of C:] is non empty set
{|(C),(C)|} is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like non empty total set
{|(C)|} is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like non empty total set
AltCatStr(# the carrier of C,(C),(C) #) is non empty strict AltCatStr
the carrier of (C) is non empty set
the Arrows of (C) is Relation-like [: the carrier of (C), the carrier of (C):] -defined Function-like non empty total set
[: the carrier of (C), the carrier of (C):] is Relation-like non empty set
the Comp of (C) is Relation-like [: the carrier of (C), the carrier of (C), the carrier of (C):] -defined Function-like non empty total Function-yielding V81() ManySortedFunction of {| the Arrows of (C), the Arrows of (C)|},{| the Arrows of (C)|}
[: the carrier of (C), the carrier of (C), the carrier of (C):] is non empty set
{| the Arrows of (C), the Arrows of (C)|} is Relation-like [: the carrier of (C), the carrier of (C), the carrier of (C):] -defined Function-like non empty total set
{| the Arrows of (C)|} is Relation-like [: the carrier of (C), the carrier of (C), the carrier of (C):] -defined Function-like non empty total set
C is non empty non void V52() Category-like transitive associative reflexive with_identities CatStr
(C) is non empty strict AltCatStr
the carrier of C is non empty set
(C) is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty total set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
(C) is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like non empty total Function-yielding V81() ManySortedFunction of {|(C),(C)|},{|(C)|}
[: the carrier of C, the carrier of C, the carrier of C:] is non empty set
{|(C),(C)|} is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like non empty total set
{|(C)|} is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like non empty total set
AltCatStr(# the carrier of C,(C),(C) #) is non empty strict AltCatStr
the carrier of (C) is non empty set
the Arrows of (C) is Relation-like [: the carrier of (C), the carrier of (C):] -defined Function-like non empty total set
[: the carrier of (C), the carrier of (C):] is Relation-like non empty set
the Comp of (C) is Relation-like [: the carrier of (C), the carrier of (C), the carrier of (C):] -defined Function-like non empty total Function-yielding V81() ManySortedFunction of {| the Arrows of (C), the Arrows of (C)|},{| the Arrows of (C)|}
[: the carrier of (C), the carrier of (C), the carrier of (C):] is non empty set
{| the Arrows of (C), the Arrows of (C)|} is Relation-like [: the carrier of (C), the carrier of (C), the carrier of (C):] -defined Function-like non empty total set
{| the Arrows of (C)|} is Relation-like [: the carrier of (C), the carrier of (C), the carrier of (C):] -defined Function-like non empty total set
C is non empty non void V52() Category-like transitive associative reflexive with_identities CatStr
(C) is non empty strict AltCatStr
the carrier of C is non empty set
(C) is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty total set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
(C) is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like non empty total Function-yielding V81() ManySortedFunction of {|(C),(C)|},{|(C)|}
[: the carrier of C, the carrier of C, the carrier of C:] is non empty set
{|(C),(C)|} is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like non empty total set
{|(C)|} is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like non empty total set
AltCatStr(# the carrier of C,(C),(C) #) is non empty strict AltCatStr
the carrier of (C) is non empty set
D is Element of the carrier of (C)
o is Element of the carrier of (C)
<^D,o^> is set
the Arrows of (C) is Relation-like [: the carrier of (C), the carrier of (C):] -defined Function-like non empty total set
[: the carrier of (C), the carrier of (C):] is Relation-like non empty set
the Arrows of (C) . (D,o) is set
[D,o] is V15() set
{D,o} is non empty set
{D} is non empty set
{{D,o},{D}} is non empty set
the Arrows of (C) . [D,o] is set
o9 is Element of the carrier of (C)
<^o,o9^> is set
the Arrows of (C) . (o,o9) is set
[o,o9] is V15() set
{o,o9} is non empty set
{o} is non empty set
{{o,o9},{o}} is non empty set
the Arrows of (C) . [o,o9] is set
<^D,o9^> is set
the Arrows of (C) . (D,o9) is set
[D,o9] is V15() set
{D,o9} is non empty set
{{D,o9},{D}} is non empty set
the Arrows of (C) . [D,o9] is set
m is Element of the carrier of C
p9 is Element of the carrier of C
Hom (m,p9) is Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is non empty set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = m & cod b1 = p9 ) } is set
p is Element of the carrier of C
Hom (m,p) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = m & cod b1 = p ) } is set
Hom (p,p9) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = p & cod b1 = p9 ) } is set
C is non empty non void V52() Category-like transitive associative reflexive with_identities CatStr
(C) is non empty strict AltCatStr
the carrier of C is non empty set
(C) is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty total set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
(C) is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like non empty total Function-yielding V81() ManySortedFunction of {|(C),(C)|},{|(C)|}
[: the carrier of C, the carrier of C, the carrier of C:] is non empty set
{|(C),(C)|} is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like non empty total set
{|(C)|} is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like non empty total set
AltCatStr(# the carrier of C,(C),(C) #) is non empty strict AltCatStr
[:1,1:] is Relation-like non empty set
the Relation-like [:1,1:] -defined Function-like non empty total set is Relation-like [:1,1:] -defined Function-like non empty total set
AltGraph(# 1, the Relation-like [:1,1:] -defined Function-like non empty total set #) is strict AltGraph
D is strict AltGraph
the carrier of D is set
C is non empty AltGraph
the carrier of C is non empty set
D is Element of the carrier of C
<^D,D^> is set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty total set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the Arrows of C . (D,D) is set
[D,D] is V15() set
{D,D} is non empty set
{D} is non empty set
{{D,D},{D}} is non empty set
the Arrows of C . [D,D] is set
D is set
the Arrows of C is Relation-like