:: ALTCAT_2 semantic presentation

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
F₁() is non empty set
{ [b₁,F₂(b₁)] where b₁ is Element of F₁() : P₁[b₁] } 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 F₁()
F₂(m) is set
[m,F₂(m)] is V15() set
{m,F₂(m)} is non empty set
{m} is non empty set
{{m,F₂(m)},{m}} is non empty set
p is Element of F₁()
F₂(p) is set
[p,F₂(p)] is V15() set
{p,F₂(p)} is non empty set
{p} is non empty set
{{p,F₂(p)},{p}} is non empty set
D is set
o is Element of F₁()
F₂(o) is set
[o,F₂(o)] is V15() set
{o,F₂(o)} is non empty set
{o} is non empty set
{{o,F₂(o)},{o}} is non empty set
F₂() is Relation-like Function-like set
F₁() is non empty set
{ [b₁,F₃(b₁)] where b₁ is Element of F₁() : P₁[b₁] } is set
dom F₂() is set
{ b₁ where b₁ is Element of F₁() : P₁[b₁] } is set
D is set
o is Element of F₁()
F₃(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 F₁()
F₃(o9) is set
[o9,F₃(o9)] is V15() set
{o9,F₃(o9)} is non empty set
{o9} is non empty set
{{o9,F₃(o9)},{o9}} is non empty set
F₁() is non empty set
F₂() is Relation-like Function-like set
{ [b₁,F₄(b₁)] where b₁ is Element of F₁() : P₁[b₁] } is set
F₃() is Element of F₁()
F₂() . F₃() is set
F₄(F₃()) is set
dom F₂() is set
{ b₁ where b₁ is Element of F₁() : P₁[b₁] } is set
[F₃(),F₄(F₃())] is V15() set
{F₃(),F₄(F₃())} is non empty set
{F₃()} is non empty set
{{F₃(),F₄(F₃())},{F₃()}} 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = o & cod b₁ = o9 ) } is set
D is Element of the carrier of C
Hom (D,o) is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = o & cod b₁ = o9 ) } is set
D is Element of the carrier of C
Hom (D,o) is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = o9 & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = n & cod b₁ = n99 ) } is set
Hom (n99,p4) is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = n99 & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = n & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = o ) } is set
o9 is Element of the carrier of C
Hom (o,o9) is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = o & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = o ) } is set
Hom (o,o9) is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = o & cod b₁ = o9 ) } is set
Hom (o9,m) is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = o9 & cod b₁ = m ) } is set
Hom (o,m) is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = o & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = o & cod b₁ = D ) } is set
Hom (D,D) is non empty Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = o ) } is set
Hom (D,D) is non empty Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = m & cod b₁ = p9 ) } is set
p is Element of the carrier of C
Hom (m,p) is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = m & cod b₁ = p ) } is set
Hom (p,p9) is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = p & cod b₁ = 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 [: 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
o is Element of the carrier of C
<^o,o^> is set
the Arrows of C . (o,o) is set
[o,o] is V15() set
{o,o} is non empty set
{o} is non empty set
{{o,o},{o}} is non empty set
the Arrows of C . [o,o] is set
C is non empty transitive 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
m is Element of the carrier of C
<^o9,m^> is set
the Arrows of 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
the Arrows of C . [o9,m] is set
p is Element of <^D,o^>
p9 is Element of <^o,o9^>
a is Element of <^o9,m^>
a * p9 is Element of <^o,m^>
<^o,m^> is set
the Arrows of C . (o,m) is set
[o,m] is V15() set
{o,m} is non empty set
{{o,m},{o}} is non empty set
the Arrows of C . [o,m] is set
(a * p9) * p is Element of <^D,m^>
<^D,m^> is set
the Arrows of C . (D,m) is set
[D,m] is V15() set
{D,m} is non empty set
{{D,m},{D}} is non empty set
the Arrows of C . [D,m] is set
p9 * p is Element of <^D,o9^>
<^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
a * (p9 * p) is Element of <^D,m^>
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
D is Element of the carrier of C
o is Element of the carrier of C
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
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
m is Element of the carrier of C
the Arrows of 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
the Arrows of C . [o9,m] is 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
the Comp of C . (D,o9,m) is Relation-like [:( the Arrows of C . (o9,m)),( the Arrows of C . (D,o9)):] -defined the Arrows of C . (D,m) -valued Function-like V18([:( the Arrows of C . (o9,m)),( the Arrows of C . (D,o9)):], the Arrows of C . (D,m)) Element of bool [:[:( the Arrows of C . (o9,m)),( the Arrows of C . (D,o9)):],( the Arrows of C . (D,m)):]
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
[:( the Arrows of C . (o9,m)),( the Arrows of C . (D,o9)):] is Relation-like set
the Arrows of C . (D,m) is set
[D,m] is V15() set
{D,m} is non empty set
{{D,m},{D}} is non empty set
the Arrows of C . [D,m] is set
[:[:( the Arrows of C . (o9,m)),( the Arrows of C . (D,o9)):],( the Arrows of C . (D,m)):] is Relation-like set
bool [:[:( the Arrows of C . (o9,m)),( the Arrows of C . (D,o9)):],( the Arrows of C . (D,m)):] is non empty set
the Comp of C . (D,o,o9) is Relation-like [:( the Arrows of C . (o,o9)),( the Arrows of C . (D,o)):] -defined the Arrows of C . (D,o9) -valued Function-like V18([:( the Arrows of C . (o,o9)),( the Arrows of C . (D,o)):], the Arrows of C . (D,o9)) Element of bool [:[:( the Arrows of C . (o,o9)),( the Arrows of C . (D,o)):],( the Arrows of C . (D,o9)):]
[:( the Arrows of C . (o,o9)),( the Arrows of C . (D,o)):] is Relation-like set
[:[:( the Arrows of C . (o,o9)),( the Arrows of C . (D,o)):],( the Arrows of C . (D,o9)):] is Relation-like set
bool [:[:( the Arrows of C . (o,o9)),( the Arrows of C . (D,o)):],( the Arrows of C . (D,o9)):] is non empty set
the Comp of C . (D,o,m) is Relation-like [:( the Arrows of C . (o,m)),( the Arrows of C . (D,o)):] -defined the Arrows of C . (D,m) -valued Function-like V18([:( the Arrows of C . (o,m)),( the Arrows of C . (D,o)):], the Arrows of C . (D,m)) Element of bool [:[:( the Arrows of C . (o,m)),( the Arrows of C . (D,o)):],( the Arrows of C . (D,m)):]
the Arrows of C . (o,m) is set
[o,m] is V15() set
{o,m} is non empty set
{{o,m},{o}} is non empty set
the Arrows of C . [o,m] is set
[:( the Arrows of C . (o,m)),( the Arrows of C . (D,o)):] is Relation-like set
[:[:( the Arrows of C . (o,m)),( the Arrows of C . (D,o)):],( the Arrows of C . (D,m)):] is Relation-like set
bool [:[:( the Arrows of C . (o,m)),( the Arrows of C . (D,o)):],( the Arrows of C . (D,m)):] is non empty set
the Comp of C . (o,o9,m) is Relation-like [:( the Arrows of C . (o9,m)),( the Arrows of C . (o,o9)):] -defined the Arrows of C . (o,m) -valued Function-like V18([:( the Arrows of C . (o9,m)),( the Arrows of C . (o,o9)):], the Arrows of C . (o,m)) Element of bool [:[:( the Arrows of C . (o9,m)),( the Arrows of C . (o,o9)):],( the Arrows of C . (o,m)):]
[:( the Arrows of C . (o9,m)),( the Arrows of C . (o,o9)):] is Relation-like set
[:[:( the Arrows of C . (o9,m)),( the Arrows of C . (o,o9)):],( the Arrows of C . (o,m)):] is Relation-like set
bool [:[:( the Arrows of C . (o9,m)),( the Arrows of C . (o,o9)):],( the Arrows of C . (o,m)):] is non empty set
n99 is set
p4 is set
f is set
( the Comp of C . (D,o,o9)) . (p4,n99) is set
[p4,n99] is V15() set
{p4,n99} is non empty set
{p4} is non empty set
{{p4,n99},{p4}} is non empty set
( the Comp of C . (D,o,o9)) . [p4,n99] is set
( the Comp of C . (D,o9,m)) . (f,(( the Comp of C . (D,o,o9)) . (p4,n99))) is set
[f,(( the Comp of C . (D,o,o9)) . (p4,n99))] is V15() set
{f,(( the Comp of C . (D,o,o9)) . (p4,n99))} is non empty set
{f} is non empty set
{{f,(( the Comp of C . (D,o,o9)) . (p4,n99))},{f}} is non empty set
( the Comp of C . (D,o9,m)) . [f,(( the Comp of C . (D,o,o9)) . (p4,n99))] is set
( the Comp of C . (o,o9,m)) . (f,p4) is set
[f,p4] is V15() set
{f,p4} is non empty set
{{f,p4},{f}} is non empty set
( the Comp of C . (o,o9,m)) . [f,p4] is set
( the Comp of C . (D,o,m)) . ((( the Comp of C . (o,o9,m)) . (f,p4)),n99) is set
[(( the Comp of C . (o,o9,m)) . (f,p4)),n99] is V15() set
{(( the Comp of C . (o,o9,m)) . (f,p4)),n99} is non empty set
{(( the Comp of C . (o,o9,m)) . (f,p4))} is non empty set
{{(( the Comp of C . (o,o9,m)) . (f,p4)),n99},{(( the Comp of C . (o,o9,m)) . (f,p4))}} is non empty set
( the Comp of C . (D,o,m)) . [(( the Comp of C . (o,o9,m)) . (f,p4)),n99] is set
p is Element of the carrier of C
p9 is Element of the carrier of C
<^p,p9^> is set
the Arrows of 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
the Arrows of C . [p,p9] is set
a is Element of the carrier of C
<^p9,a^> is set
the Arrows of C . (p9,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
the Arrows of C . [p9,a] is set
<^p,a^> is set
the Arrows of C . (p,a) is set
[p,a] is V15() set
{p,a} is non empty set
{{p,a},{p}} is non empty set
the Arrows of C . [p,a] is set
n is Element of the carrier of C
<^a,n^> is set
the Arrows of 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
the Arrows of C . [a,n] is set
h is Element of <^p9,a^>
gg is Element of <^a,n^>
gg * h is Element of <^p9,n^>
<^p9,n^> is set
the Arrows of C . (p9,n) is set
[p9,n] is V15() set
{p9,n} is non empty set
{{p9,n},{p9}} is non empty set
the Arrows of C . [p9,n] is set
g is Element of <^p,p9^>
h * g is Element of <^p,a^>
gg * (h * g) is Element of <^p,n^>
<^p,n^> is set
the Arrows of C . (p,n) is set
[p,n] is V15() set
{p,n} is non empty set
{{p,n},{p}} is non empty set
the Arrows of C . [p,n] is set
(gg * h) * g is Element of <^p,n^>
C is non empty AltCatStr
the carrier of C is non empty set
o is Element of the carrier of C
<^o,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 . (o,o) is set
[o,o] is V15() set
{o,o} is non empty set
{o} is non empty set
{{o,o},{o}} is non empty set
the Arrows of C . [o,o] is set
D is non empty with_units AltCatStr
the carrier of D is non empty set
o9 is Element of the carrier of D
idm o9 is Element of <^o9,o9^>
<^o9,o9^> is set
the Arrows of D is Relation-like [: the carrier of D, the carrier of D:] -defined Function-like non empty total set
[: the carrier of D, the carrier of D:] is Relation-like non empty set
the Arrows of D . (o9,o9) is set
[o9,o9] is V15() set
{o9,o9} is non empty set
{o9} is non empty set
{{o9,o9},{o9}} is non empty set
the Arrows of D . [o9,o9] is set
m is Element of <^o,o^>
p9 is Element of the carrier of C
<^p9,o^> is set
the Arrows of C . (p9,o) is set
[p9,o] is V15() set
{p9,o} is non empty set
{p9} is non empty set
{{p9,o},{p9}} is non empty set
the Arrows of C . [p9,o] is set
<^o,p9^> is set
the Arrows of C . (o,p9) is set
[o,p9] is V15() set
{o,p9} is non empty set
{{o,p9},{o}} is non empty set
the Arrows of C . [o,p9] is set
a is Element of <^p9,o^>
p is Element of <^o,o^>
p * a is Element of <^p9,o^>
n is Element of <^o,p9^>
n * p is Element of <^o,p9^>
D is Element of the carrier of C
o is Element of the carrier of C
<^o,o^> is set
the Arrows of C . (o,o) is set
[o,o] is V15() set
{o,o} is non empty set
{o} is non empty set
{{o,o},{o}} is non empty set
the Arrows of C . [o,o] is set
o9 is Element of <^o,o^>
m is set
p is 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
a is set
p9 is Element of the carrier of C
the Arrows of C . (p9,D) is set
[p9,D] is V15() set
{p9,D} is non empty set
{p9} is non empty set
{{p9,D},{p9}} is non empty set
the Arrows of C . [p9,D] is set
n is Element of the carrier of C
<^n,o^> is set
the Arrows of C . (n,o) is set
[n,o] is V15() set
{n,o} is non empty set
{n} is non empty set
{{n,o},{n}} is non empty set
the Arrows of C . [n,o] is 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
the Comp of C . (p9,D,D) is Relation-like [:( the Arrows of C . (D,D)),( the Arrows of C . (p9,D)):] -defined the Arrows of C . (p9,D) -valued Function-like V18([:( the Arrows of C . (D,D)),( the Arrows of C . (p9,D)):], the Arrows of C . (p9,D)) Element of bool [:[:( the Arrows of C . (D,D)),( the Arrows of C . (p9,D)):],( the Arrows of C . (p9,D)):]
[:( the Arrows of C . (D,D)),( the Arrows of C . (p9,D)):] is Relation-like set
[:[:( the Arrows of C . (D,D)),( the Arrows of C . (p9,D)):],( the Arrows of C . (p9,D)):] is Relation-like set
bool [:[:( the Arrows of C . (D,D)),( the Arrows of C . (p9,D)):],( the Arrows of C . (p9,D)):] is non empty set
( the Comp of C . (p9,D,D)) . (p,a) is set
[p,a] is V15() set
{p,a} is non empty set
{p} is non empty set
{{p,a},{p}} is non empty set
( the Comp of C . (p9,D,D)) . [p,a] is set
n99 is Element of <^n,o^>
o9 * n99 is Element of <^n,o^>
D is Element of the carrier of C
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
o is Element of the carrier of C
<^o,o^> is set
the Arrows of C . (o,o) is set
[o,o] is V15() set
{o,o} is non empty set
{o} is non empty set
{{o,o},{o}} is non empty set
the Arrows of C . [o,o] is set
o9 is Element of <^o,o^>
m is Element of <^o,o^>
p is Element of the carrier of C
the Arrows of C . (D,p) is set
[D,p] is V15() set
{D,p} is non empty set
{{D,p},{D}} is non empty set
the Arrows of C . [D,p] is set
the Comp of C . (D,D,p) is Relation-like [:( the Arrows of C . (D,p)),( the Arrows of C . (D,D)):] -defined the Arrows of C . (D,p) -valued Function-like V18([:( the Arrows of C . (D,p)),( the Arrows of C . (D,D)):], the Arrows of C . (D,p)) Element of bool [:[:( the Arrows of C . (D,p)),( the Arrows of C . (D,D)):],( the Arrows of C . (D,p)):]
[:( the Arrows of C . (D,p)),( the Arrows of C . (D,D)):] is Relation-like set
[:[:( the Arrows of C . (D,p)),( the Arrows of C . (D,D)):],( the Arrows of C . (D,p)):] is Relation-like set
bool [:[:( the Arrows of C . (D,p)),( the Arrows of C . (D,D)):],( the Arrows of C . (D,p)):] is non empty set
p9 is set
( the Comp of C . (D,D,p)) . (p9,m) is set
[p9,m] is V15() set
{p9,m} is non empty set
{p9} is non empty set
{{p9,m},{p9}} is non empty set
( the Comp of C . (D,D,p)) . [p9,m] is set
a is Element of the carrier of C
<^o,a^> is set
the Arrows of C . (o,a) is set
[o,a] is V15() set
{o,a} is non empty set
{{o,a},{o}} is non empty set
the Arrows of C . [o,a] is set
n is Element of <^o,a^>
n * o9 is Element of <^o,a^>
C is non empty AltCatStr
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
the non empty with_units () AltCatStr is non empty with_units () AltCatStr
the non empty transitive associative with_units () AltCatStr is non empty transitive associative with_units () AltCatStr
C is strict AltCatStr
the carrier of C is set
D is strict AltCatStr
the carrier of D is set
[: the carrier of D, the carrier of D, the carrier of D:] is set
[: the carrier of C, the carrier of C, the carrier of C:] is set
the Comp of C is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like total Function-yielding V81() ManySortedFunction of {| the Arrows of C, the Arrows of C|},{| the Arrows of C|}
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like total set
[: the carrier of C, the carrier of C:] is Relation-like 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 total set
{| the Arrows of C|} is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like total set
the Comp of D is Relation-like [: the carrier of D, the carrier of D, the carrier of D:] -defined Function-like total Function-yielding V81() ManySortedFunction of {| the Arrows of D, the Arrows of D|},{| the Arrows of D|}
the Arrows of D is Relation-like [: the carrier of D, the carrier of D:] -defined Function-like total set
[: the carrier of D, the carrier of D:] is Relation-like set
{| the Arrows of D, the Arrows of D|} is Relation-like [: the carrier of D, the carrier of D, the carrier of D:] -defined Function-like total set
{| the Arrows of D|} is Relation-like [: the carrier of D, the carrier of D, the carrier of D:] -defined Function-like total set
C is set
[:C,C:] is Relation-like set
the Relation-like [:C,C:] -defined Function-like total set is Relation-like [:C,C:] -defined Function-like total set
[:C,C,C:] is set
{| the Relation-like [:C,C:] -defined Function-like total set , the Relation-like [:C,C:] -defined Function-like total set |} is Relation-like [:C,C,C:] -defined Function-like total set
{| the Relation-like [:C,C:] -defined Function-like total set |} is Relation-like [:C,C,C:] -defined Function-like total set
the Relation-like [:C,C,C:] -defined Function-like total Function-yielding V81() ManySortedFunction of {| the Relation-like [:C,C:] -defined Function-like total set , the Relation-like [:C,C:] -defined Function-like total set |},{| the Relation-like [:C,C:] -defined Function-like total set |} is Relation-like [:C,C,C:] -defined Function-like total Function-yielding V81() ManySortedFunction of {| the Relation-like [:C,C:] -defined Function-like total set , the Relation-like [:C,C:] -defined Function-like total set |},{| the Relation-like [:C,C:] -defined Function-like total set |}
AltCatStr(# C, the Relation-like [:C,C:] -defined Function-like total set , the Relation-like [:C,C,C:] -defined Function-like total Function-yielding V81() ManySortedFunction of {| the Relation-like [:C,C:] -defined Function-like total set , the Relation-like [:C,C:] -defined Function-like total set |},{| the Relation-like [:C,C:] -defined Function-like total set |} #) is strict AltCatStr
the carrier of AltCatStr(# C, the Relation-like [:C,C:] -defined Function-like total set , the Relation-like [:C,C,C:] -defined Function-like total Function-yielding V81() ManySortedFunction of {| the Relation-like [:C,C:] -defined Function-like total set , the Relation-like [:C,C:] -defined Function-like total set |},{| the Relation-like [:C,C:] -defined Function-like total set |} #) is set
C is strict AltCatStr
the carrier of C is set
D is strict AltCatStr
the carrier of D is set
() is strict AltCatStr
C is empty trivial V46() V51( {} ) strict AltCatStr
C is AltCatStr
the carrier of C is set
[: the carrier of C, the carrier of C:] is Relation-like set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like total set
[: the carrier of C, the carrier of C, the carrier of C:] is set
the Comp of C is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like total Function-yielding V81() ManySortedFunction of {| the Arrows of C, the Arrows of C|},{| the Arrows of C|}
{| 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 total set
{| the Arrows of C|} is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like total set
C is AltCatStr
the carrier of C is set
[: the carrier of C, the carrier of C:] is Relation-like set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like total set
[: the carrier of C, the carrier of C, the carrier of C:] is set
the Comp of C is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like total Function-yielding V81() ManySortedFunction of {| the Arrows of C, the Arrows of C|},{| the Arrows of C|}
{| 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 total set
{| the Arrows of C|} is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like total set
C is AltCatStr
D is AltCatStr
o is AltCatStr
the carrier of C is set
the carrier of D is set
[: the carrier of C, the carrier of C:] is Relation-like set
[: the carrier of D, the carrier of D:] is Relation-like set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like total set
the Arrows of D is Relation-like [: the carrier of D, the carrier of D:] -defined Function-like total set
[: the carrier of C, the carrier of C, the carrier of C:] is set
[: the carrier of D, the carrier of D, the carrier of D:] is set
the Comp of C is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like total Function-yielding V81() ManySortedFunction of {| the Arrows of C, the Arrows of C|},{| the Arrows of C|}
{| 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 total set
{| the Arrows of C|} is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like total set
the Comp of D is Relation-like [: the carrier of D, the carrier of D, the carrier of D:] -defined Function-like total Function-yielding V81() ManySortedFunction of {| the Arrows of D, the Arrows of D|},{| the Arrows of D|}
{| the Arrows of D, the Arrows of D|} is Relation-like [: the carrier of D, the carrier of D, the carrier of D:] -defined Function-like total set
{| the Arrows of D|} is Relation-like [: the carrier of D, the carrier of D, the carrier of D:] -defined Function-like total set
the carrier of o is set
[: the carrier of o, the carrier of o:] is Relation-like set
the Arrows of o is Relation-like [: the carrier of o, the carrier of o:] -defined Function-like total set
[: the carrier of o, the carrier of o, the carrier of o:] is set
the Comp of o is Relation-like [: the carrier of o, the carrier of o, the carrier of o:] -defined Function-like total Function-yielding V81() ManySortedFunction of {| the Arrows of o, the Arrows of o|},{| the Arrows of o|}
{| the Arrows of o, the Arrows of o|} is Relation-like [: the carrier of o, the carrier of o, the carrier of o:] -defined Function-like total set
{| the Arrows of o|} is Relation-like [: the carrier of o, the carrier of o, the carrier of o:] -defined Function-like total set
C is AltCatStr
D is AltCatStr
the carrier of C is set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like total set
[: the carrier of C, the carrier of C:] is Relation-like set
the Comp of C is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like 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 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 total set
{| the Arrows of C|} is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like total set
AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) is strict AltCatStr
the carrier of D is set
the Arrows of D is Relation-like [: the carrier of D, the carrier of D:] -defined Function-like total set
[: the carrier of D, the carrier of D:] is Relation-like set
the Comp of D is Relation-like [: the carrier of D, the carrier of D, the carrier of D:] -defined Function-like total Function-yielding V81() ManySortedFunction of {| the Arrows of D, the Arrows of D|},{| the Arrows of D|}
[: the carrier of D, the carrier of D, the carrier of D:] is set
{| the Arrows of D, the Arrows of D|} is Relation-like [: the carrier of D, the carrier of D, the carrier of D:] -defined Function-like total set
{| the Arrows of D|} is Relation-like [: the carrier of D, the carrier of D, the carrier of D:] -defined Function-like total set
AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) is strict AltCatStr
C is AltCatStr
the carrier of C is set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like total set
[: the carrier of C, the carrier of C:] is Relation-like set
the Comp of C is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like 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 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 total set
{| the Arrows of C|} is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like total set
AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) is strict AltCatStr
o is (C)
C is non empty AltCatStr
the carrier of C is non empty set
D is Element of the carrier of C
{D} is non empty Element of bool the carrier of C
bool the carrier of C is non empty set
<^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,D) :-> <^D,D^> is Relation-like [:{D},{D}:] -defined {<^D,D^>} -valued Function-like V18([:{D},{D}:],{<^D,D^>}) Element of bool [:[:{D},{D}:],{<^D,D^>}:]
[:{D},{D}:] is Relation-like non empty set
{<^D,D^>} is non empty set
[:[:{D},{D}:],{<^D,D^>}:] is Relation-like non empty set
bool [:[:{D},{D}:],{<^D,D^>}:] is non empty set
{[D,D]} is Relation-like Function-like non empty set
{[D,D]} --> <^D,D^> is Relation-like {[D,D]} -defined {<^D,D^>} -valued Function-like constant non empty total V18({[D,D]},{<^D,D^>}) Element of bool [:{[D,D]},{<^D,D^>}:]
[:{[D,D]},{<^D,D^>}:] is Relation-like non empty set
bool [:{[D,D]},{<^D,D^>}:] is non empty set
[D,D,D] is V15() V16() Element of [: 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 non empty set
[[D,D],D] is V15() set
{[D,D],D} is non empty set
{{[D,D],D},{[D,D]}} is 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 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
the Comp of C . (D,D,D) is Relation-like [:( the Arrows of C . (D,D)),( the Arrows of C . (D,D)):] -defined the Arrows of C . (D,D) -valued Function-like V18([:( the Arrows of C . (D,D)),( the Arrows of C . (D,D)):], the Arrows of C . (D,D)) Element of bool [:[:( the Arrows of C . (D,D)),( the Arrows of C . (D,D)):],( the Arrows of C . (D,D)):]
[:( the Arrows of C . (D,D)),( the Arrows of C . (D,D)):] is Relation-like set
[:[:( the Arrows of C . (D,D)),( the Arrows of C . (D,D)):],( the Arrows of C . (D,D)):] is Relation-like set
bool [:[:( the Arrows of C . (D,D)),( the Arrows of C . (D,D)):],( the Arrows of C . (D,D)):] is non empty set
[D,D,D] .--> ( the Comp of C . (D,D,D)) is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined {[D,D,D]} -defined bool [:[:( the Arrows of C . (D,D)),( the Arrows of C . (D,D)):],( the Arrows of C . (D,D)):] -valued Function-like one-to-one Function-yielding V81() set
{[D,D,D]} is non empty set
{[D,D,D]} --> ( the Comp of C . (D,D,D)) is Relation-like {[D,D,D]} -defined bool [:[:( the Arrows of C . (D,D)),( the Arrows of C . (D,D)):],( the Arrows of C . (D,D)):] -valued {( the Comp of C . (D,D,D))} -valued Function-like constant non empty total V18({[D,D,D]},{( the Comp of C . (D,D,D))}) Function-yielding V81() Element of bool [:{[D,D,D]},{( the Comp of C . (D,D,D))}:]
{( the Comp of C . (D,D,D))} is functional non empty set
[:{[D,D,D]},{( the Comp of C . (D,D,D))}:] is Relation-like non empty set
bool [:{[D,D,D]},{( the Comp of C . (D,D,D))}:] is non empty set
dom ([D,D,D] .--> ( the Comp of C . (D,D,D))) is set
{[D,D,D]} is non empty Element of bool [: the carrier of C, the carrier of C, the carrier of C:]
bool [: the carrier of C, the carrier of C, the carrier of C:] is non empty set
[:{D},{D},{D}:] is non empty Element of bool [: the carrier of C, the carrier of C, the carrier of C:]
dom ((D,D) :-> <^D,D^>) is Relation-like set
[:{D},{D}:] is Relation-like the carrier of C -defined the carrier of C -valued non empty Element of bool [: the carrier of C, the carrier of C:]
bool [: the carrier of C, the carrier of C:] is non empty set
p is Relation-like [:{D},{D}:] -defined Function-like non empty total set
p . (D,D) is set
p . [D,D] is set
o9 is Relation-like [:{D},{D},{D}:] -defined Function-like non empty total set
[:{D},{D},{D}:] is non empty set
{|p,p|} is Relation-like [:{D},{D},{D}:] -defined Function-like non empty total set
{|p|} is Relation-like [:{D},{D},{D}:] -defined Function-like non empty total set
p9 is set
o9 . p9 is set
{|p,p|} . p9 is set
{|p|} . p9 is set
[:({|p,p|} . p9),({|p|} . p9):] is Relation-like set
bool [:({|p,p|} . p9),({|p|} . p9):] is non empty set
{|p|} . (D,D,D) is set
{|p,p|} . (D,D,D) is set
p9 is Relation-like [:{D},{D},{D}:] -defined Function-like non empty total Function-yielding V81() ManySortedFunction of {|p,p|},{|p|}
AltCatStr(# {D},p,p9 #) is non empty strict AltCatStr
the carrier of AltCatStr(# {D},p,p9 #) is non empty set
[: the carrier of AltCatStr(# {D},p,p9 #), the carrier of AltCatStr(# {D},p,p9 #):] is Relation-like non empty set
the Arrows of AltCatStr(# {D},p,p9 #) is Relation-like [: the carrier of AltCatStr(# {D},p,p9 #), the carrier of AltCatStr(# {D},p,p9 #):] -defined Function-like non empty total set
[: the carrier of AltCatStr(# {D},p,p9 #), the carrier of AltCatStr(# {D},p,p9 #), the carrier of AltCatStr(# {D},p,p9 #):] is non empty set
the Comp of AltCatStr(# {D},p,p9 #) is Relation-like [: the carrier of AltCatStr(# {D},p,p9 #), the carrier of AltCatStr(# {D},p,p9 #), the carrier of AltCatStr(# {D},p,p9 #):] -defined Function-like non empty total Function-yielding V81() ManySortedFunction of {| the Arrows of AltCatStr(# {D},p,p9 #), the Arrows of AltCatStr(# {D},p,p9 #)|},{| the Arrows of AltCatStr(# {D},p,p9 #)|}
{| the Arrows of AltCatStr(# {D},p,p9 #), the Arrows of AltCatStr(# {D},p,p9 #)|} is Relation-like [: the carrier of AltCatStr(# {D},p,p9 #), the carrier of AltCatStr(# {D},p,p9 #), the carrier of AltCatStr(# {D},p,p9 #):] -defined Function-like non empty total set
{| the Arrows of AltCatStr(# {D},p,p9 #)|} is Relation-like [: the carrier of AltCatStr(# {D},p,p9 #), the carrier of AltCatStr(# {D},p,p9 #), the carrier of AltCatStr(# {D},p,p9 #):] -defined Function-like non empty total set
n is set
the Arrows of AltCatStr(# {D},p,p9 #) . n is set
the Arrows of C . n is set
[D,D] is V15() Element of [: the carrier of C, the carrier of C:]
{[D,D]} is Relation-like the carrier of C -defined the carrier of C -valued Function-like non empty Element of bool [: the carrier of C, the carrier of C:]
n is set
the Comp of AltCatStr(# {D},p,p9 #) . n is Relation-like Function-like set
the Comp of C . n is Relation-like Function-like set
n is strict (C)
the carrier of n is set
the Arrows of n is Relation-like [: the carrier of n, the carrier of n:] -defined Function-like total set
[: the carrier of n, the carrier of n:] is Relation-like set
the Comp of n is Relation-like [: the carrier of n, the carrier of n, the carrier of n:] -defined Function-like total Function-yielding V81() ManySortedFunction of {| the Arrows of n, the Arrows of n|},{| the Arrows of n|}
[: the carrier of n, the carrier of n, the carrier of n:] is set
{| the Arrows of n, the Arrows of n|} is Relation-like [: the carrier of n, the carrier of n, the carrier of n:] -defined Function-like total set
{| the Arrows of n|} is Relation-like [: the carrier of n, the carrier of n, the carrier of n:] -defined Function-like total set
o is strict (C)
the carrier of o is set
the Arrows of o is Relation-like [: the carrier of o, the carrier of o:] -defined Function-like total set
[: the carrier of o, the carrier of o:] is Relation-like set
the Comp of o is Relation-like [: the carrier of o, the carrier of o, the carrier of o:] -defined Function-like total Function-yielding V81() ManySortedFunction of {| the Arrows of o, the Arrows of o|},{| the Arrows of o|}
[: the carrier of o, the carrier of o, the carrier of o:] is set
{| the Arrows of o, the Arrows of o|} is Relation-like [: the carrier of o, the carrier of o, the carrier of o:] -defined Function-like total set
{| the Arrows of o|} is Relation-like [: the carrier of o, the carrier of o, the carrier of o:] -defined Function-like total set
o9 is strict (C)
the carrier of o9 is set
the Arrows of o9 is Relation-like [: the carrier of o9, the carrier of o9:] -defined Function-like total set
[: the carrier of o9, the carrier of o9:] is Relation-like set
the Comp of o9 is Relation-like [: the carrier of o9, the carrier of o9, the carrier of o9:] -defined Function-like total Function-yielding V81() ManySortedFunction of {| the Arrows of o9, the Arrows of o9|},{| the Arrows of o9|}
[: the carrier of o9, the carrier of o9, the carrier of o9:] is set
{| the Arrows of o9, the Arrows of o9|} is Relation-like [: the carrier of o9, the carrier of o9, the carrier of o9:] -defined Function-like total set
{| the Arrows of o9|} is Relation-like [: the carrier of o9, the carrier of o9, the carrier of o9:] -defined Function-like total set
C is non empty AltCatStr
the carrier of C is non empty set
D is Element of the carrier of C
(C,D) is strict (C)
the carrier of (C,D) is set
o is Element of the carrier of (C,D)
{D} is non empty Element of bool the carrier of C
bool the carrier of C is non empty set
C is non empty AltCatStr
the carrier of C is non empty set
D is Element of the carrier of C
(C,D) is strict (C)
the carrier of (C,D) is set
o is Element of the carrier of (C,D)
o9 is Element of the carrier of (C,D)
<^o,o9^> is set
the Arrows of (C,D) is Relation-like [: the carrier of (C,D), the carrier of (C,D):] -defined Function-like total set
[: the carrier of (C,D), the carrier of (C,D):] is Relation-like set
the Arrows of (C,D) . (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,D) . [o,o9] is set
m is Element of the carrier of (C,D)
<^o9,m^> is set
the Arrows 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
the Arrows of (C,D) . [o9,m] is set
<^o,m^> is set
the Arrows of (C,D) . (o,m) is set
[o,m] is V15() set
{o,m} is non empty set
{{o,m},{o}} is non empty set
the Arrows of (C,D) . [o,m] is set
the carrier of (C,D) is set
{D} is non empty Element of bool the carrier of C
bool the carrier of C is non empty set
C is non empty AltCatStr
the carrier of C is non empty set
the Element of the carrier of C is Element of the carrier of C
(C, the Element of the carrier of C) is non empty transitive strict (C)
C is non empty transitive AltCatStr
D is non empty transitive (C)
the carrier of D is non empty set
o is non empty transitive (C)
the carrier of o is non empty set
[: the carrier of D, the carrier of D:] is Relation-like non empty set
[: the carrier of o, the carrier of o:] is Relation-like non empty set
the Arrows of D is Relation-like [: the carrier of D, the carrier of D:] -defined Function-like non empty total set
the Arrows of o is Relation-like [: the carrier of o, the carrier of o:] -defined Function-like non empty total set
[: the carrier of D, the carrier of D, the carrier of D:] is non empty set
[: the carrier of o, the carrier of o, the carrier of o:] is non empty set
the Comp of D is Relation-like [: the carrier of D, the carrier of D, the carrier of D:] -defined Function-like non empty total Function-yielding V81() ManySortedFunction of {| the Arrows of D, the Arrows of D|},{| the Arrows of D|}
{| the Arrows of D, the Arrows of D|} is Relation-like [: the carrier of D, the carrier of D, the carrier of D:] -defined Function-like non empty total set
{| the Arrows of D|} is Relation-like [: the carrier of D, the carrier of D, the carrier of D:] -defined Function-like non empty total set
the Comp of o is Relation-like [: the carrier of o, the carrier of o, the carrier of o:] -defined Function-like non empty total Function-yielding V81() ManySortedFunction of {| the Arrows of o, the Arrows of o|},{| the Arrows of o|}
{| the Arrows of o, the Arrows of o|} is Relation-like [: the carrier of o, the carrier of o, the carrier of o:] -defined Function-like non empty total set
{| the Arrows of o|} is Relation-like [: the carrier of o, the carrier of o, the carrier of o:] -defined Function-like non empty total set
o9 is set
the Comp of D . o9 is Relation-like Function-like set
the Comp of o . o9 is Relation-like Function-like set
m is set
p is set
p9 is set
[m,p,p9] is V15() V16() set
[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
a is Element of the carrier of D
n is Element of the carrier of D
n99 is Element of the carrier of D
[n,n99] is V15() Element of [: the carrier of D, the carrier of D:]
{n,n99} is non empty set
{n} is non empty set
{{n,n99},{n}} is non empty set
<^n,n99^> is set
the Arrows of D . (n,n99) is set
[n,n99] is V15() set
the Arrows of D . [n,n99] is set
f is Element of the carrier of o
g is Element of the carrier of o
<^f,g^> is set
the Arrows of o . (f,g) is set
[f,g] is V15() set
{f,g} is non empty set
{f} is non empty set
{{f,g},{f}} is non empty set
the Arrows of o . [f,g] is set
p4 is Element of the carrier of o
<^p4,f^> is set
the Arrows of o . (p4,f) is set
[p4,f] is V15() set
{p4,f} is non empty set
{p4} is non empty set
{{p4,f},{p4}} is non empty set
the Arrows of o . [p4,f] is set
[:<^f,g^>,<^p4,f^>:] is Relation-like set
<^p4,g^> is set
the Arrows of o . (p4,g) is set
[p4,g] is V15() set
{p4,g} is non empty set
{{p4,g},{p4}} is non empty set
the Arrows of o . [p4,g] is set
[:[:<^f,g^>,<^p4,f^>:],<^p4,g^>:] is Relation-like set
bool [:[:<^f,g^>,<^p4,f^>:],<^p4,g^>:] is non empty set
the Comp of o . (p4,f,g) is Relation-like [:( the Arrows of o . (f,g)),( the Arrows of o . (p4,f)):] -defined the Arrows of o . (p4,g) -valued Function-like V18([:( the Arrows of o . (f,g)),( the Arrows of o . (p4,f)):], the Arrows of o . (p4,g)) Element of bool [:[:( the Arrows of o . (f,g)),( the Arrows of o . (p4,f)):],( the Arrows of o . (p4,g)):]
[:( the Arrows of o . (f,g)),( the Arrows of o . (p4,f)):] is Relation-like set
[:[:( the Arrows of o . (f,g)),( the Arrows of o . (p4,f)):],( the Arrows of o . (p4,g)):] is Relation-like set
bool [:[:( the Arrows of o . (f,g)),( the Arrows of o . (p4,f)):],( the Arrows of o . (p4,g)):] is non empty set
<^a,n^> is set
the Arrows of D . (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
the Arrows of D . [a,n] is set
[:<^n,n99^>,<^a,n^>:] is Relation-like set
<^a,n99^> is set
the Arrows of D . (a,n99) is set
[a,n99] is V15() set
{a,n99} is non empty set
{{a,n99},{a}} is non empty set
the Arrows of D . [a,n99] is set
[:[:<^n,n99^>,<^a,n^>:],<^a,n99^>:] is Relation-like set
bool [:[:<^n,n99^>,<^a,n^>:],<^a,n99^>:] is non empty set
the Comp of D . (a,n,n99) is Relation-like [:( the Arrows of D . (n,n99)),( the Arrows of D . (a,n)):] -defined the Arrows of D . (a,n99) -valued Function-like V18([:( the Arrows of D . (n,n99)),( the Arrows of D . (a,n)):], the Arrows of D . (a,n99)) Element of bool [:[:( the Arrows of D . (n,n99)),( the Arrows of D . (a,n)):],( the Arrows of D . (a,n99)):]
[:( the Arrows of D . (n,n99)),( the Arrows of D . (a,n)):] is Relation-like set
[:[:( the Arrows of D . (n,n99)),( the Arrows of D . (a,n)):],( the Arrows of D . (a,n99)):] is Relation-like set
bool [:[:( the Arrows of D . (n,n99)),( the Arrows of D . (a,n)):],( the Arrows of D . (a,n99)):] is non empty set
gg is Relation-like [:<^n,n99^>,<^a,n^>:] -defined <^a,n99^> -valued Function-like V18([:<^n,n99^>,<^a,n^>:],<^a,n99^>) Element of bool [:[:<^n,n99^>,<^a,n^>:],<^a,n99^>:]
dom gg is Relation-like set
h is Relation-like [:<^f,g^>,<^p4,f^>:] -defined <^p4,g^> -valued Function-like V18([:<^f,g^>,<^p4,f^>:],<^p4,g^>) Element of bool [:[:<^f,g^>,<^p4,f^>:],<^p4,g^>:]
dom h is Relation-like set
[a,n] is V15() Element of [: the carrier of D, the carrier of D:]
the carrier of C is non empty set
hh is Element of the carrier of C
o3 is Element of the carrier of C
<^hh,o3^> 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 . (hh,o3) is set
[hh,o3] is V15() set
{hh,o3} is non empty set
{hh} is non empty set
{{hh,o3},{hh}} is non empty set
the Arrows of C . [hh,o3] is set
ff is Element of the carrier of C
<^ff,hh^> is set
the Arrows of C . (ff,hh) is set
[ff,hh] is V15() set
{ff,hh} is non empty set
{ff} is non empty set
{{ff,hh},{ff}} is non empty set
the Arrows of C . [ff,hh] is set
[:<^hh,o3^>,<^ff,hh^>:] is Relation-like set
<^ff,o3^> is set
the Arrows of C . (ff,o3) is set
[ff,o3] is V15() set
{ff,o3} is non empty set
{{ff,o3},{ff}} is non empty set
the Arrows of C . [ff,o3] is set
[:[:<^hh,o3^>,<^ff,hh^>:],<^ff,o3^>:] is Relation-like set
bool [:[:<^hh,o3^>,<^ff,hh^>:],<^ff,o3^>:] is 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
the Comp of C . (ff,hh,o3) is Relation-like [:( the Arrows of C . (hh,o3)),( the Arrows of C . (ff,hh)):] -defined the Arrows of C . (ff,o3) -valued Function-like V18([:( the Arrows of C . (hh,o3)),( the Arrows of C . (ff,hh)):], the Arrows of C . (ff,o3)) Element of bool [:[:( the Arrows of C . (hh,o3)),( the Arrows of C . (ff,hh)):],( the Arrows of C . (ff,o3)):]
[:( the Arrows of C . (hh,o3)),( the Arrows of C . (ff,hh)):] is Relation-like set
[:[:( the Arrows of C . (hh,o3)),( the Arrows of C . (ff,hh)):],( the Arrows of C . (ff,o3)):] is Relation-like set
bool [:[:( the Arrows of C . (hh,o3)),( the Arrows of C . (ff,hh)):],( the Arrows of C . (ff,o3)):] is non empty set
c is Relation-like [:<^hh,o3^>,<^ff,hh^>:] -defined <^ff,o3^> -valued Function-like V18([:<^hh,o3^>,<^ff,hh^>:],<^ff,o3^>) Element of bool [:[:<^hh,o3^>,<^ff,hh^>:],<^ff,o3^>:]
[ff,hh,o3] is V15() V16() Element of [: the carrier of C, the carrier of C, the carrier of C:]
[[ff,hh],o3] is V15() set
{[ff,hh],o3} is non empty set
{[ff,hh]} is Relation-like Function-like non empty set
{{[ff,hh],o3},{[ff,hh]}} is non empty set
the Comp of C . [ff,hh,o3] is Relation-like Function-like set
the Comp of o . [ff,hh,o3] is Relation-like Function-like set
y is set
the Comp of D . [ff,hh,o3] is Relation-like Function-like set
gg . y is set
c . y is set
h . y is set
C is AltCatStr
C is non empty with_units () AltCatStr
C is AltCatStr
the carrier of C is set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like total set
[: the carrier of C, the carrier of C:] is Relation-like set
the Comp of C is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like 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 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 total set
{| the Arrows of C|} is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like total set
AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) is strict AltCatStr
o is (C)
dom the Arrows of C is set
the carrier of o is set
[: the carrier of o, the carrier of o:] is Relation-like set
the Arrows of o is Relation-like [: the carrier of o, the carrier of o:] -defined Function-like total set
the Arrows of C || the carrier of o is Relation-like Function-like set
the Arrows of C | [: the carrier of o, the carrier of o:] is Relation-like [: the carrier of o, the carrier of o:] -defined [: the carrier of C, the carrier of C:] -defined Function-like set
C is non empty 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
AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) is non empty strict AltCatStr
o is (C)
dom the Arrows of C is non empty set
the carrier of o is set
[: the carrier of o, the carrier of o:] is Relation-like set
the Arrows of o is Relation-like [: the carrier of o, the carrier of o:] -defined Function-like total set
the Arrows of C || the carrier of o is Relation-like Function-like set
the Arrows of C | [: the carrier of o, the carrier of o:] is Relation-like [: the carrier of o, the carrier of o:] -defined [: the carrier of C, the carrier of C:] -defined Function-like set
C is non empty transitive associative with_units () AltCatStr
the carrier of C is non empty set
D is Element of the carrier of C
(C,D) is non empty transitive strict (C)
the carrier of (C,D) is non empty set
{D} is non empty Element of bool the carrier of C
bool the carrier of C is non empty set
the Arrows of (C,D) is Relation-like [: the carrier of (C,D), the carrier of (C,D):] -defined Function-like non empty total set
[: the carrier of (C,D), the carrier of (C,D):] is Relation-like non empty set
<^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,D) :-> <^D,D^> is Relation-like [:{D},{D}:] -defined {<^D,D^>} -valued Function-like V18([:{D},{D}:],{<^D,D^>}) Element of bool [:[:{D},{D}:],{<^D,D^>}:]
[:{D},{D}:] is Relation-like non empty set
{<^D,D^>} is non empty set
[:[:{D},{D}:],{<^D,D^>}:] is Relation-like non empty set
bool [:[:{D},{D}:],{<^D,D^>}:] is non empty set
{[D,D]} is Relation-like Function-like non empty set
{[D,D]} --> <^D,D^> is Relation-like {[D,D]} -defined {<^D,D^>} -valued Function-like constant non empty total V18({[D,D]},{<^D,D^>}) Element of bool [:{[D,D]},{<^D,D^>}:]
[:{[D,D]},{<^D,D^>}:] is Relation-like non empty set
bool [:{[D,D]},{<^D,D^>}:] is non empty set
the Arrows of C || the carrier of (C,D) is Relation-like Function-like set
the Arrows of C | [: the carrier of (C,D), the carrier of (C,D):] is Relation-like [: the carrier of (C,D), the carrier of (C,D):] -defined [: the carrier of C, the carrier of C:] -defined Function-like set
o is Element of the carrier of (C,D)
o9 is Element of the carrier of C
<^o,o^> is set
the Arrows of (C,D) . (o,o) is set
[o,o] is V15() set
{o,o} is non empty set
{o} is non empty set
{{o,o},{o}} is non empty set
the Arrows of (C,D) . [o,o] is set
((D,D) :-> <^D,D^>) . (D,D) is set
((D,D) :-> <^D,D^>) . [D,D] is set
<^o9,o9^> is set
the Arrows of C . (o9,o9) is set
[o9,o9] is V15() set
{o9,o9} is non empty set
{o9} is non empty set
{{o9,o9},{o9}} is non empty set
the Arrows of C . [o9,o9] is set
idm o9 is Element of <^o9,o9^>
C is non empty transitive associative with_units () AltCatStr
the carrier of C is non empty set
the Element of the carrier of C is Element of the carrier of C
(C, the Element of the carrier of C) is non empty transitive strict (C) (C) (C)
C is non empty transitive 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
AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) is non empty strict AltCatStr
D is (C)
the carrier of D is set
the Arrows of D is Relation-like [: the carrier of D, the carrier of D:] -defined Function-like total set
[: the carrier of D, the carrier of D:] is Relation-like set
the Comp of D is Relation-like [: the carrier of D, the carrier of D, the carrier of D:] -defined Function-like total Function-yielding V81() ManySortedFunction of {| the Arrows of D, the Arrows of D|},{| the Arrows of D|}
[: the carrier of D, the carrier of D, the carrier of D:] is set
{| the Arrows of D, the Arrows of D|} is Relation-like [: the carrier of D, the carrier of D, the carrier of D:] -defined Function-like total set
{| the Arrows of D|} is Relation-like [: the carrier of D, the carrier of D, the carrier of D:] -defined Function-like total set
AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) is strict AltCatStr
o is Element of the carrier of D
o9 is Element of the carrier of D
<^o,o9^> is set
the Arrows of D . (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 D . [o,o9] is set
m is Element of the carrier of D
<^o9,m^> is set
the Arrows of 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
the Arrows of D . [o9,m] is set
<^o,m^> is set
the Arrows of D . (o,m) is set
[o,m] is V15() set
{o,m} is non empty set
{{o,m},{o}} is non empty set
the Arrows of D . [o,m] is set
p is Element of the carrier of C
a is Element of the carrier of C
<^p,a^> is set
the Arrows of C . (p,a) is set
[p,a] is V15() set
{p,a} is non empty set
{p} is non empty set
{{p,a},{p}} is non empty set
the Arrows of C . [p,a] is set
p9 is Element of the carrier of C
<^p,p9^> is set
the Arrows of C . (p,p9) is set
[p,p9] is V15() set
{p,p9} is non empty set
{{p,p9},{p}} is non empty set
the Arrows of C . [p,p9] is set
<^p9,a^> is set
the Arrows of C . (p9,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
the Arrows of C . [p9,a] is set
C is non empty transitive AltCatStr
D is non empty transitive (C)
the carrier of D is non empty set
o is non empty transitive (C)
the carrier of o is non empty set
the Arrows of D is Relation-like [: the carrier of D, the carrier of D:] -defined Function-like non empty total set
[: the carrier of D, the carrier of D:] is Relation-like non empty set
the Arrows of o is Relation-like [: the carrier of o, the carrier of o:] -defined Function-like non empty total set
[: the carrier of o, the carrier of o:] is Relation-like non empty set
the Comp of D is Relation-like [: the carrier of D, the carrier of D, the carrier of D:] -defined Function-like non empty total Function-yielding V81() ManySortedFunction of {| the Arrows of D, the Arrows of D|},{| the Arrows of D|}
[: the carrier of D, the carrier of D, the carrier of D:] is non empty set
{| the Arrows of D, the Arrows of D|} is Relation-like [: the carrier of D, the carrier of D, the carrier of D:] -defined Function-like non empty total set
{| the Arrows of D|} is Relation-like [: the carrier of D, the carrier of D, the carrier of D:] -defined Function-like non empty total set
AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) is non empty strict AltCatStr
the Comp of o is Relation-like [: the carrier of o, the carrier of o, the carrier of o:] -defined Function-like non empty total Function-yielding V81() ManySortedFunction of {| the Arrows of o, the Arrows of o|},{| the Arrows of o|}
[: the carrier of o, the carrier of o, the carrier of o:] is non empty set
{| the Arrows of o, the Arrows of o|} is Relation-like [: the carrier of o, the carrier of o, the carrier of o:] -defined Function-like non empty total set
{| the Arrows of o|} is Relation-like [: the carrier of o, the carrier of o, the carrier of o:] -defined Function-like non empty total set
AltCatStr(# the carrier of o, the Arrows of o, the Comp of o #) is non empty strict AltCatStr
C is non empty transitive 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
AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) is non empty strict AltCatStr
D is (C) (C)
the carrier of D is set
the Arrows of D is Relation-like [: the carrier of D, the carrier of D:] -defined Function-like total set
[: the carrier of D, the carrier of D:] is Relation-like set
the Comp of D is Relation-like [: the carrier of D, the carrier of D, the carrier of D:] -defined Function-like total Function-yielding V81() ManySortedFunction of {| the Arrows of D, the Arrows of D|},{| the Arrows of D|}
[: the carrier of D, the carrier of D, the carrier of D:] is set
{| the Arrows of D, the Arrows of D|} is Relation-like [: the carrier of D, the carrier of D, the carrier of D:] -defined Function-like total set
{| the Arrows of D|} is Relation-like [: the carrier of D, the carrier of D, the carrier of D:] -defined Function-like total set
AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) is strict AltCatStr
dom the Arrows of C is non empty set
the Arrows of C || the carrier of D is Relation-like Function-like set
the Arrows of C | [: the carrier of D, the carrier of D:] is Relation-like [: the carrier of D, the carrier of D:] -defined [: the carrier of C, the carrier of C:] -defined Function-like set
C is non empty AltCatStr
the carrier of C is non empty set
D is non empty (C) (C)
the carrier of D is non empty set
o is Element of the carrier of C
o9 is Element of the carrier of C
<^o,o9^> 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 . (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
m is Element of the carrier of D
p is Element of the carrier of D
<^m,p^> is set
the Arrows of D is Relation-like [: the carrier of D, the carrier of D:] -defined Function-like non empty total set
[: the carrier of D, the carrier of D:] is Relation-like non empty set
the Arrows of D . (m,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
the Arrows of D . [m,p] is set
[m,p] is V15() Element of [: the carrier of D, the carrier of D:]
the Arrows of C || the carrier of D is Relation-like Function-like set
the Arrows of C | [: the carrier of D, the carrier of D:] is Relation-like [: the carrier of D, the carrier of D:] -defined [: the carrier of C, the carrier of C:] -defined Function-like set
( the Arrows of C || the carrier of D) . (m,p) is set
( the Arrows of C || the carrier of D) . [m,p] is set
C is non empty AltCatStr
the carrier of C is non empty set
D is non empty (C)
the carrier of D is non empty set
o is Element of the carrier of D
C is non empty transitive AltCatStr
D is (C)
the carrier of D is set
o is Element of the carrier of D
o9 is Element of the carrier of D
<^o,o9^> is set
the Arrows of D is Relation-like [: the carrier of D, the carrier of D:] -defined Function-like total set
[: the carrier of D, the carrier of D:] is Relation-like set
the Arrows of D . (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 D . [o,o9] is set
m is Element of the carrier of D
<^o9,m^> is set
the Arrows of 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
the Arrows of D . [o9,m] is set
<^o,m^> is set
the Arrows of D . (o,m) is set
[o,m] is V15() set
{o,m} is non empty set
{{o,m},{o}} is non empty set
the Arrows of D . [o,m] is set
the carrier of C is non empty set
p is Element of the carrier of C
p9 is Element of the carrier of C
<^p,p9^> 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 . (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
the Arrows of C . [p,p9] is set
a is Element of the carrier of C
<^p9,a^> is set
the Arrows of C . (p9,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
the Arrows of C . [p9,a] is set
<^p,a^> is set
the Arrows of C . (p,a) is set
[p,a] is V15() set
{p,a} is non empty set
{{p,a},{p}} is non empty set
the Arrows of C . [p,a] is set
C is non empty transitive AltCatStr
D is non empty transitive (C) (C)
the carrier of D is non empty set
o is non empty transitive (C) (C)
the carrier of o is non empty set
the Arrows of D is Relation-like [: the carrier of D, the carrier of D:] -defined Function-like non empty total set
[: the carrier of D, the carrier of D:] is Relation-like non empty set
the Comp of D is Relation-like [: the carrier of D, the carrier of D, the carrier of D:] -defined Function-like non empty total Function-yielding V81() ManySortedFunction of {| the Arrows of D, the Arrows of D|},{| the Arrows of D|}
[: the carrier of D, the carrier of D, the carrier of D:] is non empty set
{| the Arrows of D, the Arrows of D|} is Relation-like [: the carrier of D, the carrier of D, the carrier of D:] -defined Function-like non empty total set
{| the Arrows of D|} is Relation-like [: the carrier of D, the carrier of D, the carrier of D:] -defined Function-like non empty total set
AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) is non empty strict AltCatStr
the Arrows of o is Relation-like [: the carrier of o, the carrier of o:] -defined Function-like non empty total set
[: the carrier of o, the carrier of o:] is Relation-like non empty set
the Comp of o is Relation-like [: the carrier of o, the carrier of o, the carrier of o:] -defined Function-like non empty total Function-yielding V81() ManySortedFunction of {| the Arrows of o, the Arrows of o|},{| the Arrows of o|}
[: the carrier of o, the carrier of o, the carrier of o:] is non empty set
{| the Arrows of o, the Arrows of o|} is Relation-like [: the carrier of o, the carrier of o, the carrier of o:] -defined Function-like non empty total set
{| the Arrows of o|} is Relation-like [: the carrier of o, the carrier of o, the carrier of o:] -defined Function-like non empty total set
AltCatStr(# the carrier of o, the Arrows of o, the Comp of o #) is non empty strict AltCatStr
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 is non empty set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the Arrows of C || the carrier of o is Relation-like Function-like set
the Arrows of C | [: the carrier of o, the carrier of o:] is Relation-like [: the carrier of o, the carrier of o:] -defined [: the carrier of C, the carrier of C:] -defined Function-like set
C is non empty AltCatStr
the carrier of C is non empty set
D is non empty (C)
the carrier of D is non empty set
o is Element of the carrier of C
o9 is Element of the carrier of C
<^o,o9^> 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 . (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
m is Element of the carrier of D
p is Element of the carrier of D
<^m,p^> is set
the Arrows of D is Relation-like [: the carrier of D, the carrier of D:] -defined Function-like non empty total set
[: the carrier of D, the carrier of D:] is Relation-like non empty set
the Arrows of D . (m,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
the Arrows of D . [m,p] is set
[m,p] is V15() Element of [: the carrier of D, the carrier of D:]
C is non empty transitive AltCatStr
the carrier of C is non empty set
D is non empty transitive (C)
the carrier of D is non empty set
o is Element of the carrier of D
o9 is Element of the carrier of D
<^o,o9^> is set
the Arrows of D is Relation-like [: the carrier of D, the carrier of D:] -defined Function-like non empty total set
[: the carrier of D, the carrier of D:] is Relation-like non empty set
the Arrows of D . (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 D . [o,o9] is set
m is Element of the carrier of D
<^o9,m^> is set
the Arrows of 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
the Arrows of D . [o9,m] is set
p is Element of the carrier of C
p9 is Element of the carrier of C
a is Element of the carrier of C
<^p,p9^> 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 . (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
the Arrows of C . [p,p9] is set
<^p9,a^> is set
the Arrows of C . (p9,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
the Arrows of C . [p9,a] is set
n is Element of <^p,p9^>
n99 is Element of <^p9,a^>
n99 * n is Element of <^p,a^>
<^p,a^> is set
the Arrows of C . (p,a) is set
[p,a] is V15() set
{p,a} is non empty set
{{p,a},{p}} is non empty set
the Arrows of C . [p,a] is set
p4 is Element of <^o,o9^>
f is Element of <^o9,m^>
f * p4 is Element of <^o,m^>
<^o,m^> is set
the Arrows of D . (o,m) is set
[o,m] is V15() set
{o,m} is non empty set
{{o,m},{o}} is non empty set
the Arrows of D . [o,m] is set
the Comp of D is Relation-like [: the carrier of D, the carrier of D, the carrier of D:] -defined Function-like non empty total Function-yielding V81() ManySortedFunction of {| the Arrows of D, the Arrows of D|},{| the Arrows of D|}
[: the carrier of D, the carrier of D, the carrier of D:] is non empty set
{| the Arrows of D, the Arrows of D|} is Relation-like [: the carrier of D, the carrier of D, the carrier of D:] -defined Function-like non empty total set
{| the Arrows of D|} is Relation-like [: the carrier of D, the carrier of D, the carrier of D:] -defined Function-like non empty total set
the Comp of D . (o,o9,m) is Relation-like [:( the Arrows of D . (o9,m)),( the Arrows of D . (o,o9)):] -defined the Arrows of D . (o,m) -valued Function-like V18([:( the Arrows of D . (o9,m)),( the Arrows of D . (o,o9)):], the Arrows of D . (o,m)) Element of bool [:[:( the Arrows of D . (o9,m)),( the Arrows of D . (o,o9)):],( the Arrows of D . (o,m)):]
[:( the Arrows of D . (o9,m)),( the Arrows of D . (o,o9)):] is Relation-like set
[:[:( the Arrows of D . (o9,m)),( the Arrows of D . (o,o9)):],( the Arrows of D . (o,m)):] is Relation-like set
bool [:[:( the Arrows of D . (o9,m)),( the Arrows of D . (o,o9)):],( the Arrows of D . (o,m)):] is non empty set
dom ( the Comp of D . (o,o9,m)) is Relation-like set
[:<^o9,m^>,<^o,o9^>:] is Relation-like set
[f,p4] is V15() set
{f,p4} is non empty set
{f} is non empty set
{{f,p4},{f}} is non empty set
[: the carrier of C, the carrier of C, the carrier of C:] is 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 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
[o,o9,m] is V15() V16() Element of [: the carrier of D, the carrier of D, the carrier of D:]
[[o,o9],m] is V15() set
{[o,o9],m} is non empty set
{[o,o9]} is Relation-like Function-like non empty set
{{[o,o9],m},{[o,o9]}} is non empty set
the Comp of D . [o,o9,m] is Relation-like Function-like set
the Comp of C . (p,p9,a) is Relation-like [:( the Arrows of C . (p9,a)),( the Arrows of C . (p,p9)):] -defined the Arrows of C . (p,a) -valued Function-like V18([:( the Arrows of C . (p9,a)),( the Arrows of C . (p,p9)):], the Arrows of C . (p,a)) Element of bool [:[:( the Arrows of C . (p9,a)),( the Arrows of C . (p,p9)):],( the Arrows of C . (p,a)):]
[:( the Arrows of C . (p9,a)),( the Arrows of C . (p,p9)):] is Relation-like set
[:[:( the Arrows of C . (p9,a)),( the Arrows of C . (p,p9)):],( the Arrows of C . (p,a)):] is Relation-like set
bool [:[:( the Arrows of C . (p9,a)),( the Arrows of C . (p,p9)):],( the Arrows of C . (p,a)):] is non empty set
[p,p9,a] is V15() V16() Element of [: the carrier of C, the carrier of C, the carrier of C:]
[[p,p9],a] is V15() set
{[p,p9],a} is non empty set
{[p,p9]} is Relation-like Function-like non empty set
{{[p,p9],a},{[p,p9]}} is non empty set
the Comp of C . [p,p9,a] is Relation-like Function-like set
( the Comp of C . (p,p9,a)) . (n99,n) is set
[n99,n] is V15() set
{n99,n} is non empty set
{n99} is non empty set
{{n99,n},{n99}} is non empty set
( the Comp of C . (p,p9,a)) . [n99,n] is set
( the Comp of D . (o,o9,m)) . (f,p4) is set
( the Comp of D . (o,o9,m)) . [f,p4] is set
C is non empty transitive associative AltCatStr
D is non empty (C)
o is non empty transitive (C)
the carrier of o is non empty set
o9 is Element of the carrier of o
m is Element of the carrier of o
<^o9,m^> is set
the Arrows of o is Relation-like [: the carrier of o, the carrier of o:] -defined Function-like non empty total set
[: the carrier of o, the carrier of o:] is Relation-like non empty set
the Arrows of 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
the Arrows of o . [o9,m] is set
p is Element of the carrier of o
<^m,p^> is set
the Arrows of o . (m,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
the Arrows of o . [m,p] is set
p9 is Element of the carrier of o
<^p,p9^> is set
the Arrows of o . (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
the Arrows of o . [p,p9] is set
the carrier of C is non empty set
f is Element of <^o9,m^>
g is Element of <^m,p^>
g * f is Element of <^o9,p^>
<^o9,p^> is set
the Arrows of o . (o9,p) is set
[o9,p] is V15() set
{o9,p} is non empty set
{{o9,p},{o9}} is non empty set
the Arrows of o . [o9,p] is set
h is Element of <^p,p9^>
h * g is Element of <^m,p9^>
<^m,p9^> is set
the Arrows of o . (m,p9) is set
[m,p9] is V15() set
{m,p9} is non empty set
{{m,p9},{m}} is non empty set
the Arrows of o . [m,p9] is set
(h * g) * f is Element of <^o9,p9^>
<^o9,p9^> is set
the Arrows of o . (o9,p9) is set
[o9,p9] is V15() set
{o9,p9} is non empty set
{{o9,p9},{o9}} is non empty set
the Arrows of o . [o9,p9] is set
h * (g * f) is Element of <^o9,p9^>
n is Element of the carrier of C
n99 is Element of the carrier of C
<^n,n99^> 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 . (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
the Arrows of C . [n,n99] is set
a is Element of the carrier of C
<^a,n^> is set
the Arrows of 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
the Arrows of C . [a,n] is set
ff is Element of <^a,n^>
gg is Element of <^n,n99^>
gg * ff is Element of <^a,n99^>
<^a,n99^> is set
the Arrows of C . (a,n99) is set
[a,n99] is V15() set
{a,n99} is non empty set
{{a,n99},{a}} is non empty set
the Arrows of C . [a,n99] is set
p4 is Element of the carrier of C
<^n99,p4^> is set
the Arrows of 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
the Arrows of C . [n99,p4] is set
hh is Element of <^n99,p4^>
hh * gg is Element of <^n,p4^>
<^n,p4^> is set
the Arrows of C . (n,p4) is set
[n,p4] is V15() set
{n,p4} is non empty set
{{n,p4},{n}} is non empty set
the Arrows of C . [n,p4] is set
(hh * gg) * ff is Element of <^a,p4^>
<^a,p4^> is set
the Arrows of C . (a,p4) is set
[a,p4] is V15() set
{a,p4} is non empty set
{{a,p4},{a}} is non empty set
the Arrows of C . [a,p4] is set
hh * (gg * ff) is Element of <^a,p4^>
C is non empty AltCatStr
the carrier of C is non empty set
D is non empty (C)
the carrier of D is non empty set
o is Element of the carrier of C
o9 is Element of the carrier of C
<^o,o9^> 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 . (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
m is Element of the carrier of D
p is Element of the carrier of D
<^m,p^> is set
the Arrows of D is Relation-like [: the carrier of D, the carrier of D:] -defined Function-like non empty total set
[: the carrier of D, the carrier of D:] is Relation-like non empty set
the Arrows of D . (m,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
the Arrows of D . [m,p] is set
p9 is Element of <^m,p^>
C is non empty transitive with_units () AltCatStr
D is non empty (C)
the carrier of D is non empty set
o is Element of the carrier of D
<^o,o^> is set
the Arrows of D is Relation-like [: the carrier of D, the carrier of D:] -defined Function-like non empty total set
[: the carrier of D, the carrier of D:] is Relation-like non empty set
the Arrows of D . (o,o) is set
[o,o] is V15() set
{o,o} is non empty set
{o} is non empty set
{{o,o},{o}} is non empty set
the Arrows of D . [o,o] is set
the carrier of C is non empty set
o9 is Element of the carrier of C
idm o9 is Element of <^o9,o9^>
<^o9,o9^> 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 . (o9,o9) is set
[o9,o9] is V15() set
{o9,o9} is non empty set
{o9} is non empty set
{{o9,o9},{o9}} is non empty set
the Arrows of C . [o9,o9] is set
m is Element of <^o,o^>
p is Element of the carrier of D
<^p,o^> is set
the Arrows of D . (p,o) is set
[p,o] is V15() set
{p,o} is non empty set
{p} is non empty set
{{p,o},{p}} is non empty set
the Arrows of D . [p,o] is set
<^o,p^> is set
the Arrows of D . (o,p) is set
[o,p] is V15() set
{o,p} is non empty set
{{o,p},{o}} is non empty set
the Arrows of D . [o,p] is set
p9 is Element of <^p,o^>
m * p9 is Element of <^p,o^>
a is Element of <^o,p^>
a * m is Element of <^o,p^>
n is Element of the carrier of C
<^n,o9^> is set
the Arrows of C . (n,o9) is set
[n,o9] is V15() set
{n,o9} is non empty set
{n} is non empty set
{{n,o9},{n}} is non empty set
the Arrows of C . [n,o9] is set
n99 is Element of <^n,o9^>
(idm o9) * n99 is Element of <^n,o9^>
n is Element of the carrier of C
<^o9,n^> is set
the Arrows of C . (o9,n) is set
[o9,n] is V15() set
{o9,n} is non empty set
{{o9,n},{o9}} is non empty set
the Arrows of C . [o9,n] is set
n99 is Element of <^o9,n^>
n99 * (idm o9) is Element of <^o9,n^>
C is non empty transitive associative with_units () AltCatStr
the carrier of C is non empty set
the Element of the carrier of C is Element of the carrier of C
(C, the Element of the carrier of C) is non empty transitive strict associative with_units () (C) (C) (C)
C is non empty transitive associative with_units () AltCatStr
the carrier of C is non empty set
D is non empty transitive associative with_units () (C) (C)
the carrier of D is non empty set
o is Element of the carrier of D
idm o is Element of <^o,o^>
<^o,o^> is set
the Arrows of D is Relation-like [: the carrier of D, the carrier of D:] -defined Function-like non empty total set
[: the carrier of D, the carrier of D:] is Relation-like non empty set
the Arrows of D . (o,o) is set
[o,o] is V15() set
{o,o} is non empty set
{o} is non empty set
{{o,o},{o}} is non empty set
the Arrows of D . [o,o] is set
o9 is Element of the carrier of C
idm o9 is Element of <^o9,o9^>
<^o9,o9^> 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 . (o9,o9) is set
[o9,o9] is V15() set
{o9,o9} is non empty set
{o9} is non empty set
{{o9,o9},{o9}} is non empty set
the Arrows of C . [o9,o9] is set
p is Element of the carrier of D
<^o,p^> is set
the Arrows of D . (o,p) is set
[o,p] is V15() set
{o,p} is non empty set
{{o,p},{o}} is non empty set
the Arrows of D . [o,p] is set
p9 is Element of the carrier of C
<^o9,p9^> is set
the Arrows of C . (o9,p9) is set
[o9,p9] is V15() set
{o9,p9} is non empty set
{{o9,p9},{o9}} is non empty set
the Arrows of C . [o9,p9] is set
a is Element of <^o,p^>
m is Element of <^o,o^>
a * m is Element of <^o,p^>
n is Element of <^o9,p9^>
n * (idm o9) is Element of <^o9,p9^>