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

{ [b

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,F

{m,F

{m} is non empty set

{{m,F

p is Element of F

F

[p,F

{p,F

{p} is non empty set

{{p,F

D is set

o is Element of F

F

[o,F

{o,F

{o} is non empty set

{{o,F

F

F

{ [b

dom F

{ b

D is set

o is Element of F

F

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,F

{o9,F

{o9} is non empty set

{{o9,F

F

F

{ [b

F

F

F

dom F

{ b

[F

{F

{F

{{F

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

D is Element of the carrier of C

Hom (D,o) is Element of bool the carrier' of C

{ b

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

D is Element of the carrier of C

Hom (D,o) is Element of bool the carrier' of C

{ b

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

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

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

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

Hom (n99,p4) is Element of bool the carrier' of C

{ b

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

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

o9 is Element of the carrier of C

Hom (o,o9) is Element of bool the carrier' of C

{ b

(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

Hom (o,o9) is Element of bool the carrier' of C

{ b

Hom (o9,m) is Element of bool the carrier' of C

{ b

Hom (o,m) is Element of bool the carrier' of C

{ b

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

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

Hom (D,D) is non empty Element of bool the carrier' of C

{ b

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

Hom (D,D) is non empty Element of bool the carrier' of C

{ b

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

p is Element of the carrier of C

Hom (m,p) is Element of bool the carrier' of C

{ b

Hom (p,p9) is Element of bool the carrier' of C

{ b

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