:: OPPCAT_1 semantic presentation

K104() is Element of bool K100()
K100() is set
bool K100() is set
K99() is set
bool K99() is set
bool K104() is set
{} is empty set
the empty set is empty set
1 is non empty set
C is non empty set
a is non empty set
[:C,a:] is set
S is non empty set
[:[:C,a:],S:] is set
bool [:[:C,a:],S:] is set
f is Relation-like [:C,a:] -defined S -valued Function-like Element of bool [:[:C,a:],S:]
~ f is Relation-like Function-like set
[:a,C:] is set
[:[:a,C:],S:] is set
bool [:[:a,C:],S:] is set
C is non empty non void V55() 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 Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is set
bool [: the carrier' of C, the carrier of C:] is set
the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, 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:] is set
[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set
bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set
( the carrier' of C, the carrier' of C, 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:]
CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) #) is strict CatStr
C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
the carrier of C is non empty set
a is Element of the carrier of C
(C) is non empty non void V55() strict CatStr
the carrier' of C is non empty set
the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is set
bool [: the carrier' of C, the carrier of C:] is set
the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, 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:] is set
[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set
bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set
( the carrier' of C, the carrier' of C, 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:]
CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) #) is strict CatStr
the carrier of (C) is non empty set
C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
(C) is non empty non void V55() strict CatStr
the carrier of C is non empty set
the carrier' of C is non empty set
the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is set
bool [: the carrier' of C, the carrier of C:] is set
the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, 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:] is set
[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set
bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set
( the carrier' of C, the carrier' of C, 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:]
CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) #) is strict CatStr
the carrier' of (C) is non empty set
g is Element of the carrier' of (C)
Sgg is Element of the carrier' of (C)
[g,Sgg] is set
{g,Sgg} is non empty set
{g} is non empty set
{{g,Sgg},{g}} 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 set
[:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set
bool [:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set
dom the Comp of (C) is Relation-like set
dom g is Element of the carrier of (C)
the carrier of (C) is non empty set
the Source of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]
[: the carrier' of (C), the carrier of (C):] is set
bool [: the carrier' of (C), the carrier of (C):] is set
the Source of (C) . g is Element of the carrier of (C)
cod Sgg is Element of the carrier of (C)
the Target of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]
the Target of (C) . Sgg is Element of the carrier of (C)
d is Element of the carrier' of C
c₁₀ is Element of the carrier' of C
[d,c₁₀] is set
{d,c₁₀} is non empty set
{d} is non empty set
{{d,c₁₀},{d}} is non empty set
dom the Comp of C is Relation-like set
dom d is Element of the carrier of C
the Source of C . d is Element of the carrier of C
cod c₁₀ is Element of the carrier of C
the Target of C . c₁₀ is Element of the carrier of C
c₁₀ is Element of the carrier' of C
cod c₁₀ is Element of the carrier of C
the Target of C . c₁₀ is Element of the carrier of C
d is Element of the carrier' of C
dom d is Element of the carrier of C
the Source of C . d is Element of the carrier of C
[d,c₁₀] is set
{d,c₁₀} is non empty set
{d} is non empty set
{{d,c₁₀},{d}} is non empty set
dom the Comp of C is Relation-like set
g is Element of the carrier' of C
the Target of C . g is Element of the carrier of C
Sgg is Element of the carrier' of C
the Source of C . Sgg is Element of the carrier of C
( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . (g,Sgg) is set
[g,Sgg] is set
{g,Sgg} is non empty set
{g} is non empty set
{{g,Sgg},{g}} is non empty set
( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . [g,Sgg] is set
the Comp of C . (Sgg,g) is set
[Sgg,g] is set
{Sgg,g} is non empty set
{Sgg} is non empty set
{{Sgg,g},{Sgg}} is non empty set
the Comp of C . [Sgg,g] is set
the carrier' of (C) is non empty set
c₁₀ is Element of the carrier' of (C)
dom c₁₀ is Element of the carrier of (C)
the carrier of (C) is non empty set
the Source of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]
[: the carrier' of (C), the carrier of (C):] is set
bool [: the carrier' of (C), the carrier of (C):] is set
the Source of (C) . c₁₀ is Element of the carrier of (C)
d is Element of the carrier' of (C)
cod d is Element of the carrier of (C)
the Target of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]
the Target of (C) . d is Element of the carrier of (C)
[c₁₀,d] is set
{c₁₀,d} is non empty set
{c₁₀} is non empty set
{{c₁₀,d},{c₁₀}} is non empty set
dom ( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) is Relation-like set
the carrier' of (C) is non empty set
g is Element of the carrier' of (C)
dom g is Element of the carrier of (C)
the carrier of (C) is non empty set
the Source of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]
[: the carrier' of (C), the carrier of (C):] is set
bool [: the carrier' of (C), the carrier of (C):] is set
the Source of (C) . g is Element of the carrier of (C)
Sgg is Element of the carrier' of (C)
cod Sgg is Element of the carrier of (C)
the Target of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]
the Target of (C) . Sgg is Element of the carrier of (C)
g (*) Sgg is Element of the carrier' of (C)
dom (g (*) Sgg) is Element of the carrier of (C)
the Source of (C) . (g (*) Sgg) is Element of the carrier of (C)
dom Sgg is Element of the carrier of (C)
the Source of (C) . Sgg is Element of the carrier of (C)
cod (g (*) Sgg) is Element of the carrier of (C)
the Target of (C) . (g (*) Sgg) is Element of the carrier of (C)
cod g is Element of the carrier of (C)
the Target of (C) . g is Element of the carrier of (C)
c₁₀ is Element of the carrier' of C
cod c₁₀ is Element of the carrier of C
the Target of C . c₁₀ is Element of the carrier of C
d is Element of the carrier' of C
dom d is Element of the carrier of C
the Source of C . d is Element of the carrier of C
[d,c₁₀] is set
{d,c₁₀} is non empty set
{d} is non empty set
{{d,c₁₀},{d}} is non empty set
dom the Comp of C is Relation-like set
[g,Sgg] is set
{g,Sgg} is non empty set
{g} is non empty set
{{g,Sgg},{g}} 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 set
[:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set
bool [:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set
dom the Comp of (C) is Relation-like set
( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . (c₁₀,d) is set
[c₁₀,d] is set
{c₁₀,d} is non empty set
{c₁₀} is non empty set
{{c₁₀,d},{c₁₀}} is non empty set
( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . [c₁₀,d] is set
the Comp of C . (d,c₁₀) is set
the Comp of C . [d,c₁₀] is set
d (*) c₁₀ is Element of the carrier' of C
cod (d (*) c₁₀) is Element of the carrier of C
the Target of C . (d (*) c₁₀) is Element of the carrier of C
cod d is Element of the carrier of C
the Target of C . d is Element of the carrier of C
dom (d (*) c₁₀) is Element of the carrier of C
the Source of C . (d (*) c₁₀) is Element of the carrier of C
dom c₁₀ is Element of the carrier of C
the Source of C . c₁₀ is Element of the carrier of C
the carrier' of (C) is non empty set
d is Element of the carrier' of (C)
dom d is Element of the carrier of (C)
the carrier of (C) is non empty set
the Source of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]
[: the carrier' of (C), the carrier of (C):] is set
bool [: the carrier' of (C), the carrier of (C):] is set
the Source of (C) . d is Element of the carrier of (C)
g is Element of the carrier' of (C)
cod g is Element of the carrier of (C)
the Target of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]
the Target of (C) . g is Element of the carrier of (C)
dom g is Element of the carrier of (C)
the Source of (C) . g is Element of the carrier of (C)
Sgg is Element of the carrier' of (C)
cod Sgg is Element of the carrier of (C)
the Target of (C) . Sgg is Element of the carrier of (C)
g (*) Sgg is Element of the carrier' of (C)
d (*) (g (*) Sgg) is Element of the carrier' of (C)
d (*) g is Element of the carrier' of (C)
(d (*) g) (*) Sgg is Element of the carrier' of (C)
bb is Element of the carrier' of C
b is Element of the carrier' of C
[bb,b] is set
{bb,b} is non empty set
{bb} is non empty set
{{bb,b},{bb}} is non empty set
dom ( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) is Relation-like set
( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . (bb,b) is set
( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . [bb,b] is set
c₁₀ is Element of the carrier' of C
[b,c₁₀] is set
{b,c₁₀} is non empty set
{b} is non empty set
{{b,c₁₀},{b}} is non empty set
( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . (b,c₁₀) is set
( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . [b,c₁₀] is set
the Comp of C . (b,bb) is set
[b,bb] is set
{b,bb} is non empty set
{{b,bb},{b}} is non empty set
the Comp of C . [b,bb] is set
the Target of C . (( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . (bb,b)) is set
dom (d (*) g) is Element of the carrier of (C)
the Source of (C) . (d (*) g) is Element of the carrier of (C)
( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . ((( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . (bb,b)),c₁₀) is set
[(( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . (bb,b)),c₁₀] is set
{(( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . (bb,b)),c₁₀} is non empty set
{(( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . (bb,b))} is non empty set
{{(( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . (bb,b)),c₁₀},{(( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . (bb,b))}} is non empty set
( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . [(( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . (bb,b)),c₁₀] is set
the Comp of C . (c₁₀,( the Comp of C . (b,bb))) is set
[c₁₀,( the Comp of C . (b,bb))] is set
{c₁₀,( the Comp of C . (b,bb))} is non empty set
{c₁₀} is non empty set
{{c₁₀,( the Comp of C . (b,bb))},{c₁₀}} is non empty set
the Comp of C . [c₁₀,( the Comp of C . (b,bb))] is set
cod bb is Element of the carrier of C
the Target of C . bb is Element of the carrier of C
dom b is Element of the carrier of C
the Source of C . b is Element of the carrier of C
cod b is Element of the carrier of C
the Target of C . b is Element of the carrier of C
dom c₁₀ is Element of the carrier of C
the Source of C . c₁₀ is Element of the carrier of C
the Comp of C . (c₁₀,b) is set
[c₁₀,b] is set
{c₁₀,b} is non empty set
{{c₁₀,b},{c₁₀}} is non empty set
the Comp of C . [c₁₀,b] is set
the Source of C . (( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . (b,c₁₀)) is set
cod (g (*) Sgg) is Element of the carrier of (C)
the Target of (C) . (g (*) Sgg) is Element of the carrier of (C)
[(d (*) g),Sgg] is set
{(d (*) g),Sgg} is non empty set
{(d (*) g)} is non empty set
{{(d (*) g),Sgg},{(d (*) g)}} 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 set
[:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set
bool [:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set
dom the Comp of (C) is Relation-like set
[d,(g (*) Sgg)] is set
{d,(g (*) Sgg)} is non empty set
{d} is non empty set
{{d,(g (*) Sgg)},{d}} is non empty set
[d,g] is set
{d,g} is non empty set
{{d,g},{d}} is non empty set
c₁₀ (*) b is Element of the carrier' of C
dom (c₁₀ (*) b) is Element of the carrier of C
the Source of C . (c₁₀ (*) b) is Element of the carrier of C
b (*) bb is Element of the carrier' of C
cod (b (*) bb) is Element of the carrier of C
the Target of C . (b (*) bb) is Element of the carrier of C
[g,Sgg] is set
{g,Sgg} is non empty set
{g} is non empty set
{{g,Sgg},{g}} is non empty set
( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . (bb,(( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . (b,c₁₀))) is set
[bb,(( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . (b,c₁₀))] is set
{bb,(( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . (b,c₁₀))} is non empty set
{{bb,(( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . (b,c₁₀))},{bb}} is non empty set
( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . [bb,(( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . (b,c₁₀))] is set
the Comp of C . (( the Comp of C . (c₁₀,b)),bb) is set
[( the Comp of C . (c₁₀,b)),bb] is set
{( the Comp of C . (c₁₀,b)),bb} is non empty set
{( the Comp of C . (c₁₀,b))} is non empty set
{{( the Comp of C . (c₁₀,b)),bb},{( the Comp of C . (c₁₀,b))}} is non empty set
the Comp of C . [( the Comp of C . (c₁₀,b)),bb] is set
(c₁₀ (*) b) (*) bb is Element of the carrier' of C
c₁₀ (*) (b (*) bb) is Element of the carrier' of C
the carrier of (C) is non empty set
Sgg is Element of the carrier of (C)
Hom (Sgg,Sgg) is Element of bool the carrier' of (C)
the carrier' of (C) is non empty set
bool the carrier' of (C) is set
{ b₁ where b₁ is Element of the carrier' of (C) : ( dom b₁ = Sgg & cod b₁ = Sgg ) } is set
g is Element of the carrier of C
Hom (g,g) is non empty Element of bool the carrier' of C
bool the carrier' of C is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = g & cod b₁ = g ) } is set
d is Element of the carrier' of C
c₁₀ is Element of the carrier' of (C)
dom c₁₀ is Element of the carrier of (C)
the Source of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]
[: the carrier' of (C), the carrier of (C):] is set
bool [: the carrier' of (C), the carrier of (C):] is set
the Source of (C) . c₁₀ is Element of the carrier of (C)
cod d is Element of the carrier of C
the Target of C . d is Element of the carrier of C
cod c₁₀ is Element of the carrier of (C)
the Target of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]
the Target of (C) . c₁₀ is Element of the carrier of (C)
dom d is Element of the carrier of C
the Source of C . d is Element of the carrier of C
the carrier of (C) is non empty set
Sgg is Element of the carrier of (C)
the carrier' of (C) is non empty set
g is Element of the carrier of C
id g is Morphism of g,g
d is Element of the carrier' of (C)
dom d is Element of the carrier of (C)
the Source of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]
[: the carrier' of (C), the carrier of (C):] is set
bool [: the carrier' of (C), the carrier of (C):] is set
the Source of (C) . d is Element of the carrier of (C)
cod (id g) is Element of the carrier of C
the Target of C . (id g) is Element of the carrier of C
cod d is Element of the carrier of (C)
the Target of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]
the Target of (C) . d is Element of the carrier of (C)
dom (id g) is Element of the carrier of C
the Source of C . (id g) is Element of the carrier of C
c₁₀ is Morphism of Sgg,Sgg
b is Element of the carrier of (C)
Hom (Sgg,b) is Element of bool the carrier' of (C)
bool the carrier' of (C) is set
{ b₁ where b₁ is Element of the carrier' of (C) : ( dom b₁ = Sgg & cod b₁ = b ) } is set
Hom (b,Sgg) is Element of bool the carrier' of (C)
{ b₁ where b₁ is Element of the carrier' of (C) : ( dom b₁ = b & cod b₁ = Sgg ) } is set
g is Morphism of Sgg,b
g (*) c₁₀ is Element of the carrier' of (C)
gg is Element of the carrier' of C
dom gg is Element of the carrier of C
the Source of C . gg is Element of the carrier of C
cod g is Element of the carrier of (C)
the Target of (C) . g is Element of the carrier of (C)
bb is Element of the carrier of C
cod gg is Element of the carrier of C
the Target of C . gg is Element of the carrier of C
dom g is Element of the carrier of (C)
the Source of (C) . g is Element of the carrier of (C)
the Source of C . c₁₀ is set
the Target of C . g is set
cod c₁₀ is Element of the carrier of (C)
the Target of (C) . c₁₀ is Element of the carrier of (C)
[g,c₁₀] is set
{g,c₁₀} is non empty set
{g} is non empty set
{{g,c₁₀},{g}} 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 set
[:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set
bool [:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set
dom the Comp of (C) is Relation-like set
( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . (g,c₁₀) is set
( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . [g,c₁₀] is set
the Comp of C . (c₁₀,g) is set
[c₁₀,g] is set
{c₁₀,g} is non empty set
{c₁₀} is non empty set
{{c₁₀,g},{c₁₀}} is non empty set
the Comp of C . [c₁₀,g] is set
gg is Morphism of bb,g
(id g) (*) gg is Element of the carrier' of C
g is Morphism of b,Sgg
c₁₀ (*) g is Element of the carrier' of (C)
gg is Element of the carrier' of C
cod gg is Element of the carrier of C
the Target of C . gg is Element of the carrier of C
dom g is Element of the carrier of (C)
the Source of (C) . g is Element of the carrier of (C)
bb is Element of the carrier of C
dom gg is Element of the carrier of C
the Source of C . gg is Element of the carrier of C
cod g is Element of the carrier of (C)
the Target of (C) . g is Element of the carrier of (C)
the Target of C . c₁₀ is set
the Source of C . g is set
dom c₁₀ is Element of the carrier of (C)
the Source of (C) . c₁₀ is Element of the carrier of (C)
[c₁₀,g] is set
{c₁₀,g} is non empty set
{c₁₀} is non empty set
{{c₁₀,g},{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 set
[:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set
bool [:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set
dom the Comp of (C) is Relation-like set
( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . (c₁₀,g) is set
( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) . [c₁₀,g] is set
the Comp of C . (g,c₁₀) is set
[g,c₁₀] is set
{g,c₁₀} is non empty set
{g} is non empty set
{{g,c₁₀},{g}} is non empty set
the Comp of C . [g,c₁₀] is set
gg is Morphism of g,bb
gg (*) (id g) is Element of the carrier' of C
C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
(C) is non empty non void V55() strict 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 Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is set
bool [: the carrier' of C, the carrier of C:] is set
the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, 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:] is set
[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set
bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set
( the carrier' of C, the carrier' of C, 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:]
CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) #) is strict CatStr
the carrier of (C) is non empty set
a is Element of the carrier of (C)
((C),a) is Element of the carrier of ((C))
((C)) is non empty non void V55() strict Category-like transitive associative reflexive with_identities CatStr
the carrier' of (C) is non empty set
the Target of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]
[: the carrier' of (C), the carrier of (C):] is set
bool [: the carrier' of (C), the carrier of (C):] is set
the Source of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), 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):] is set
[:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set
bool [:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set
( the carrier' of (C), the carrier' of (C), 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):]
CatStr(# the carrier of (C), the carrier' of (C), the Target of (C), the Source of (C),( the carrier' of (C), the carrier' of (C), the carrier' of (C), the Comp of (C)) #) is strict CatStr
the carrier of ((C)) is non empty set
C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
the carrier of C is non empty set
(C) is non empty non void V55() strict Category-like transitive associative reflexive with_identities CatStr
the carrier' of C is non empty set
the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is set
bool [: the carrier' of C, the carrier of C:] is set
the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, 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:] is set
[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set
bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set
( the carrier' of C, the carrier' of C, 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:]
CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) #) is strict CatStr
a is Element of the carrier of C
(C,a) is Element of the carrier of (C)
the carrier of (C) is non empty set
((C),(C,a)) is Element of the carrier of ((C))
((C)) is non empty non void V55() strict Category-like transitive associative reflexive with_identities CatStr
the carrier' of (C) is non empty set
the Target of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]
[: the carrier' of (C), the carrier of (C):] is set
bool [: the carrier' of (C), the carrier of (C):] is set
the Source of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), 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):] is set
[:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set
bool [:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set
( the carrier' of (C), the carrier' of (C), 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):]
CatStr(# the carrier of (C), the carrier' of (C), the Target of (C), the Source of (C),( the carrier' of (C), the carrier' of (C), the carrier' of (C), the Comp of (C)) #) is strict CatStr
the carrier of ((C)) is non empty set
C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
the carrier of C is non empty set
a is Element of the carrier of C
(C,a) is Element of the carrier of (C)
(C) is non empty non void V55() strict Category-like transitive associative reflexive with_identities CatStr
the carrier' of C is non empty set
the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is set
bool [: the carrier' of C, the carrier of C:] is set
the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, 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:] is set
[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set
bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set
( the carrier' of C, the carrier' of C, 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:]
CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) #) is strict CatStr
the carrier of (C) is non empty set
(C,(C,a)) is Element of the carrier of C
((C),(C,a)) is Element of the carrier of ((C))
((C)) is non empty non void V55() strict Category-like transitive associative reflexive with_identities CatStr
the carrier' of (C) is non empty set
the Target of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]
[: the carrier' of (C), the carrier of (C):] is set
bool [: the carrier' of (C), the carrier of (C):] is set
the Source of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), 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):] is set
[:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set
bool [:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set
( the carrier' of (C), the carrier' of (C), 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):]
CatStr(# the carrier of (C), the carrier' of (C), the Target of (C), the Source of (C),( the carrier' of (C), the carrier' of (C), the carrier' of (C), the Comp of (C)) #) is strict CatStr
the carrier of ((C)) is non empty set
C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
(C) is non empty non void V55() strict 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 Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is set
bool [: the carrier' of C, the carrier of C:] is set
the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, 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:] is set
[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set
bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set
( the carrier' of C, the carrier' of C, 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:]
CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) #) is strict CatStr
the carrier of (C) is non empty set
a is Element of the carrier of (C)
(C,a) is Element of the carrier of C
((C),a) is Element of the carrier of ((C))
((C)) is non empty non void V55() strict Category-like transitive associative reflexive with_identities CatStr
the carrier' of (C) is non empty set
the Target of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]
[: the carrier' of (C), the carrier of (C):] is set
bool [: the carrier' of (C), the carrier of (C):] is set
the Source of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), 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):] is set
[:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set
bool [:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set
( the carrier' of (C), the carrier' of (C), 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):]
CatStr(# the carrier of (C), the carrier' of (C), the Target of (C), the Source of (C),( the carrier' of (C), the carrier' of (C), the carrier' of (C), the Comp of (C)) #) is strict CatStr
the carrier of ((C)) is non empty set
(C,(C,a)) is Element of the carrier of (C)
C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
the carrier of C is non empty set
(C) is non empty non void V55() strict Category-like transitive associative reflexive with_identities CatStr
the carrier' of C is non empty set
the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is set
bool [: the carrier' of C, the carrier of C:] is set
the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, 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:] is set
[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set
bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set
( the carrier' of C, the carrier' of C, 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:]
CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) #) is strict CatStr
a is Element of the carrier of C
S is Element of the carrier of C
Hom (a,S) is Element of bool the carrier' of C
bool the carrier' of C is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = a & cod b₁ = S ) } is set
(C,S) is Element of the carrier of (C)
the carrier of (C) is non empty set
(C,a) is Element of the carrier of (C)
Hom ((C,S),(C,a)) is Element of bool the carrier' of (C)
the carrier' of (C) is non empty set
bool the carrier' of (C) is set
{ b₁ where b₁ is Element of the carrier' of (C) : ( dom b₁ = (C,S) & cod b₁ = (C,a) ) } is set
f is set
S2 is Element of the carrier' of C
dom S2 is Element of the carrier of C
the Source of C . S2 is Element of the carrier of C
cod S2 is Element of the carrier of C
the Target of C . S2 is Element of the carrier of C
Sff is Element of the carrier' of (C)
dom Sff is Element of the carrier of (C)
the Source of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]
[: the carrier' of (C), the carrier of (C):] is set
bool [: the carrier' of (C), the carrier of (C):] is set
the Source of (C) . Sff is Element of the carrier of (C)
cod Sff is Element of the carrier of (C)
the Target of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]
the Target of (C) . Sff is Element of the carrier of (C)
f is set
S2 is Element of the carrier' of (C)
dom S2 is Element of the carrier of (C)
the Source of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]
[: the carrier' of (C), the carrier of (C):] is set
bool [: the carrier' of (C), the carrier of (C):] is set
the Source of (C) . S2 is Element of the carrier of (C)
cod S2 is Element of the carrier of (C)
the Target of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]
the Target of (C) . S2 is Element of the carrier of (C)
Sff is Element of the carrier' of C
dom Sff is Element of the carrier of C
the Source of C . Sff is Element of the carrier of C
cod Sff is Element of the carrier of C
the Target of C . Sff is Element of the carrier of C
C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
(C) is non empty non void V55() strict 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 Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is set
bool [: the carrier' of C, the carrier of C:] is set
the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, 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:] is set
[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set
bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set
( the carrier' of C, the carrier' of C, 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:]
CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) #) is strict CatStr
the carrier of (C) is non empty set
a is Element of the carrier of (C)
S is Element of the carrier of (C)
Hom (a,S) is Element of bool the carrier' of (C)
the carrier' of (C) is non empty set
bool the carrier' of (C) is set
{ b₁ where b₁ is Element of the carrier' of (C) : ( dom b₁ = a & cod b₁ = S ) } is set
(C,S) is Element of the carrier of C
((C),S) is Element of the carrier of ((C))
((C)) is non empty non void V55() strict Category-like transitive associative reflexive with_identities CatStr
the Target of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]
[: the carrier' of (C), the carrier of (C):] is set
bool [: the carrier' of (C), the carrier of (C):] is set
the Source of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), 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):] is set
[:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set
bool [:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set
( the carrier' of (C), the carrier' of (C), 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):]
CatStr(# the carrier of (C), the carrier' of (C), the Target of (C), the Source of (C),( the carrier' of (C), the carrier' of (C), the carrier' of (C), the Comp of (C)) #) is strict CatStr
the carrier of ((C)) is non empty set
(C,a) is Element of the carrier of C
((C),a) is Element of the carrier of ((C))
Hom ((C,S),(C,a)) is Element of bool the carrier' of C
bool the carrier' of C is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = (C,S) & cod b₁ = (C,a) ) } is set
(C,(C,a)) is Element of the carrier of (C)
(C,(C,S)) is Element of the carrier of (C)
Hom ((C,(C,a)),(C,(C,S))) is Element of bool the carrier' of (C)
{ b₁ where b₁ is Element of the carrier' of (C) : ( dom b₁ = (C,(C,a)) & cod b₁ = (C,(C,S)) ) } is set
C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
the carrier' of C is non empty set
a is Element of the carrier' of C
(C) is non empty non void V55() strict Category-like transitive associative reflexive with_identities CatStr
the carrier of C is non empty set
the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is set
bool [: the carrier' of C, the carrier of C:] is set
the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, 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:] is set
[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set
bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set
( the carrier' of C, the carrier' of C, 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:]
CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) #) is strict CatStr
the carrier' of (C) is non empty set
C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
(C) is non empty non void V55() strict 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 Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is set
bool [: the carrier' of C, the carrier of C:] is set
the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, 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:] is set
[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set
bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set
( the carrier' of C, the carrier' of C, 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:]
CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) #) is strict CatStr
the carrier' of (C) is non empty set
a is Element of the carrier' of (C)
((C),a) is Element of the carrier' of ((C))
((C)) is non empty non void V55() strict Category-like transitive associative reflexive with_identities CatStr
the carrier of (C) is non empty set
the Target of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]
[: the carrier' of (C), the carrier of (C):] is set
bool [: the carrier' of (C), the carrier of (C):] is set
the Source of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), 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):] is set
[:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set
bool [:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set
( the carrier' of (C), the carrier' of (C), 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):]
CatStr(# the carrier of (C), the carrier' of (C), the Target of (C), the Source of (C),( the carrier' of (C), the carrier' of (C), the carrier' of (C), the Comp of (C)) #) is strict CatStr
the carrier' of ((C)) is non empty set
C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
the carrier of C is non empty set
a is Element of the carrier of C
S is Element of the carrier of C
Hom (a,S) is Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = a & cod b₁ = S ) } is set
f is Morphism of a,S
(C) is non empty non void V55() strict Category-like transitive associative reflexive with_identities CatStr
the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is set
bool [: the carrier' of C, the carrier of C:] is set
the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, 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:] is set
[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set
bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set
( the carrier' of C, the carrier' of C, 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:]
CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) #) is strict CatStr
(C,S) is Element of the carrier of (C)
the carrier of (C) is non empty set
(C,a) is Element of the carrier of (C)
Hom ((C,S),(C,a)) is Element of bool the carrier' of (C)
the carrier' of (C) is non empty set
bool the carrier' of (C) is set
{ b₁ where b₁ is Element of the carrier' of (C) : ( dom b₁ = (C,S) & cod b₁ = (C,a) ) } is set
C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
the carrier of C is non empty set
(C) is non empty non void V55() strict Category-like transitive associative reflexive with_identities CatStr
the carrier' of C is non empty set
the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is set
bool [: the carrier' of C, the carrier of C:] is set
the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, 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:] is set
[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set
bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set
( the carrier' of C, the carrier' of C, 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:]
CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) #) is strict CatStr
a is Element of the carrier of C
(C,a) is Element of the carrier of (C)
the carrier of (C) is non empty set
S is Element of the carrier of C
(C,S) is Element of the carrier of (C)
Hom ((C,a),(C,S)) is Element of bool the carrier' of (C)
the carrier' of (C) is non empty set
bool the carrier' of (C) is set
{ b₁ where b₁ is Element of the carrier' of (C) : ( dom b₁ = (C,a) & cod b₁ = (C,S) ) } is set
f is Morphism of (C,a),(C,S)
Hom (S,a) is Element of bool the carrier' of C
bool the carrier' of C is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = S & cod b₁ = a ) } is set
C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
the carrier of C is non empty set
(C) is non empty non void V55() strict Category-like transitive associative reflexive with_identities CatStr
the carrier' of C is non empty set
the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is set
bool [: the carrier' of C, the carrier of C:] is set
the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, 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:] is set
[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set
bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set
( the carrier' of C, the carrier' of C, 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:]
CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) #) is strict CatStr
a is Element of the carrier of C
S is Element of the carrier of C
Hom (a,S) is Element of bool the carrier' of C
bool the carrier' of C is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = a & cod b₁ = S ) } is set
(C,S) is Element of the carrier of (C)
the carrier of (C) is non empty set
(C,a) is Element of the carrier of (C)
Hom ((C,S),(C,a)) is Element of bool the carrier' of (C)
the carrier' of (C) is non empty set
bool the carrier' of (C) is set
{ b₁ where b₁ is Element of the carrier' of (C) : ( dom b₁ = (C,S) & cod b₁ = (C,a) ) } is set
f is Morphism of a,S
(C,a,S,f) is Morphism of (C,S),(C,a)
((C),(C,S),(C,a),(C,a,S,f)) is Morphism of ((C),(C,a)),((C),(C,S))
((C)) is non empty non void V55() strict Category-like transitive associative reflexive with_identities CatStr
the Target of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]
[: the carrier' of (C), the carrier of (C):] is set
bool [: the carrier' of (C), the carrier of (C):] is set
the Source of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), 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):] is set
[:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set
bool [:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set
( the carrier' of (C), the carrier' of (C), 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):]
CatStr(# the carrier of (C), the carrier' of (C), the Target of (C), the Source of (C),( the carrier' of (C), the carrier' of (C), the carrier' of (C), the Comp of (C)) #) is strict CatStr
((C),(C,a)) is Element of the carrier of ((C))
the carrier of ((C)) is non empty set
((C),(C,S)) is Element of the carrier of ((C))
C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
the carrier of C is non empty set
a is Element of the carrier of C
S is Element of the carrier of C
Hom (a,S) is Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = a & cod b₁ = S ) } is set
(C) is non empty non void V55() strict Category-like transitive associative reflexive with_identities CatStr
the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is set
bool [: the carrier' of C, the carrier of C:] is set
the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, 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:] is set
[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set
bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set
( the carrier' of C, the carrier' of C, 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:]
CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) #) is strict CatStr
(C,S) is Element of the carrier of (C)
the carrier of (C) is non empty set
(C,a) is Element of the carrier of (C)
Hom ((C,S),(C,a)) is Element of bool the carrier' of (C)
the carrier' of (C) is non empty set
bool the carrier' of (C) is set
{ b₁ where b₁ is Element of the carrier' of (C) : ( dom b₁ = (C,S) & cod b₁ = (C,a) ) } is set
f is Morphism of a,S
(C,a,S,f) is Morphism of (C,S),(C,a)
(C,S,a,(C,a,S,f)) is Morphism of a,S
C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
(C) is non empty non void V55() strict 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 Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is set
bool [: the carrier' of C, the carrier of C:] is set
the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, 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:] is set
[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set
bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set
( the carrier' of C, the carrier' of C, 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:]
CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) #) is strict CatStr
the carrier of (C) is non empty set
a is Element of the carrier of (C)
S is Element of the carrier of (C)
f is Morphism of a,S
(C,f) is Element of the carrier' of C
((C),f) is Element of the carrier' of ((C))
((C)) is non empty non void V55() strict Category-like transitive associative reflexive with_identities CatStr
the carrier' of (C) is non empty set
the Target of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]
[: the carrier' of (C), the carrier of (C):] is set
bool [: the carrier' of (C), the carrier of (C):] is set
the Source of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), 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):] is set
[:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set
bool [:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set
( the carrier' of (C), the carrier' of (C), 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):]
CatStr(# the carrier of (C), the carrier' of (C), the Target of (C), the Source of (C),( the carrier' of (C), the carrier' of (C), the carrier' of (C), the Comp of (C)) #) is strict CatStr
the carrier' of ((C)) is non empty set
(C,(C,f)) is Element of the carrier' of (C)
C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
the carrier of C is non empty set
(C) is non empty non void V55() strict Category-like transitive associative reflexive with_identities CatStr
the carrier' of C is non empty set
the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is set
bool [: the carrier' of C, the carrier of C:] is set
the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, 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:] is set
[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set
bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set
( the carrier' of C, the carrier' of C, 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:]
CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) #) is strict CatStr
a is Element of the carrier of C
S is Element of the carrier of C
Hom (a,S) is Element of bool the carrier' of C
bool the carrier' of C is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = a & cod b₁ = S ) } is set
(C,S) is Element of the carrier of (C)
the carrier of (C) is non empty set
(C,a) is Element of the carrier of (C)
Hom ((C,S),(C,a)) is Element of bool the carrier' of (C)
the carrier' of (C) is non empty set
bool the carrier' of (C) is set
{ b₁ where b₁ is Element of the carrier' of (C) : ( dom b₁ = (C,S) & cod b₁ = (C,a) ) } is set
f is Morphism of a,S
(C,a,S,f) is Morphism of (C,S),(C,a)
dom (C,a,S,f) is Element of the carrier of (C)
the Source of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]
[: the carrier' of (C), the carrier of (C):] is set
bool [: the carrier' of (C), the carrier of (C):] is set
the Source of (C) . (C,a,S,f) is Element of the carrier of (C)
cod f is Element of the carrier of C
the Target of C . f is Element of the carrier of C
cod (C,a,S,f) is Element of the carrier of (C)
the Target of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]
the Target of (C) . (C,a,S,f) is Element of the carrier of (C)
dom f is Element of the carrier of C
the Source of C . f is Element of the carrier of C
C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
(C) is non empty non void V55() strict 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 Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is set
bool [: the carrier' of C, the carrier of C:] is set
the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, 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:] is set
[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set
bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set
( the carrier' of C, the carrier' of C, 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:]
CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,( the carrier' of C, the carrier' of C, the carrier' of C, the Comp of C) #) is strict CatStr
the carrier of (C) is non empty set
a is Element of the carrier of (C)
S is Element of the carrier of (C)
S2 is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
(S2) is non empty non void V55() strict Category-like transitive associative reflexive with_identities CatStr
the carrier of S2 is non empty set
the carrier' of S2 is non empty set
the Target of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like non empty total quasi_total Element of bool [: the carrier' of S2, the carrier of S2:]
[: the carrier' of S2, the carrier of S2:] is set
bool [: the carrier' of S2, the carrier of S2:] is set
the Source of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like non empty total quasi_total Element of bool [: the carrier' of S2, the carrier of S2:]
the Comp of S2 is Relation-like [: the carrier' of S2, the carrier' of S2:] -defined the carrier' of S2 -valued Function-like Element of bool [:[: the carrier' of S2, the carrier' of S2:], the carrier' of S2:]
[: the carrier' of S2, the carrier' of S2:] is set
[:[: the carrier' of S2, the carrier' of S2:], the carrier' of S2:] is set
bool [:[: the carrier' of S2, the carrier' of S2:], the carrier' of S2:] is set
( the carrier' of S2, the carrier' of S2, the carrier' of S2, the Comp of S2) is Relation-like [: the carrier' of S2, the carrier' of S2:] -defined the carrier' of S2 -valued Function-like Element of bool [:[: the carrier' of S2, the carrier' of S2:], the carrier' of S2:]
CatStr(# the carrier of S2, the carrier' of S2, the Target of S2, the Source of S2,( the carrier' of S2, the carrier' of S2, the carrier' of S2, the Comp of S2) #) is strict CatStr
the carrier of (S2) is non empty set
Sff is Element of the carrier of (S2)
Sgg is Element of the carrier of (S2)
f is Morphism of a,S
(C,f) is Element of the carrier' of C
((C),f) is Element of the carrier' of ((C))
((C)) is non empty non void V55() strict Category-like transitive associative reflexive with_identities CatStr
the carrier' of (C) is non empty set
the Target of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), the carrier of (C):]
[: the carrier' of (C), the carrier of (C):] is set
bool [: the carrier' of (C), the carrier of (C):] is set
the Source of (C) is Relation-like the carrier' of (C) -defined the carrier of (C) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (C), 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):] is set
[:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set
bool [:[: the carrier' of (C), the carrier' of (C):], the carrier' of (C):] is set
( the carrier' of (C), the carrier' of (C), 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):]
CatStr(# the carrier of (C), the carrier' of (C), the Target of (C), the Source of (C),( the carrier' of (C), the carrier' of (C), the carrier' of (C), the Comp of (C)) #) is strict CatStr
the carrier' of ((C)) is non empty set
dom (C,f) is Element of the carrier of C
the Source of C . (C,f) is Element of the carrier of C
cod f is Element of the carrier of (C)
the Target of (C) . f is Element of the carrier of (C)
g is Morphism of Sff,Sgg
(S2,g) is Element of the carrier' of S2
((S2),g) is Element of the carrier' of ((S2))
((S2)) is non empty non void V55() strict Category-like transitive associative reflexive with_identities CatStr
the carrier' of (S2) is non empty set
the Target of (S2) is Relation-like the carrier' of (S2) -defined the carrier of (S2) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (S2), the carrier of (S2):]
[: the carrier' of (S2), the carrier of (S2):] is set
bool [: the carrier' of (S2), the carrier of (S2):] is set
the Source of (S2) is Relation-like the carrier' of (S2) -defined the carrier of (S2) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (S2), the carrier of (S2):]
the Comp of (S2) is Relation-like [: the carrier' of (S2), the carrier' of (S2):] -defined the carrier' of (S2) -valued Function-like Element of bool [:[: the carrier' of (S2), the carrier' of (S2):], the carrier' of (S2):]
[: the carrier' of (S2), the carrier' of (S2):] is set
[:[: the carrier' of (S2), the carrier' of (S2):], the carrier' of (S2):] is set
bool [:[: the carrier' of (S2), the carrier' of (S2):], the carrier' of (S2):] is set
( the carrier' of (S2), the carrier' of (S2), the carrier' of (S2), the Comp of (S2)) is Relation-like [: the carrier' of (S2), the carrier' of (S2):] -defined the carrier' of (S2) -valued Function-like Element of bool [:[: the carrier' of (S2), the carrier' of (S2):], the carrier' of (S2):]
CatStr(# the carrier of (S2), the carrier' of (S2), the Target of (S2), the Source of (S2),( the carrier' of (S2), the carrier' of (S2), the carrier' of (S2), the Comp of (S2)) #) is strict CatStr
the carrier' of ((S2)) is non empty set
cod (S2,g) is Element of the carrier of S2
the Target of S2 . (S2,g) is Element of the carrier of S2
dom g is Element of the carrier of (S2)
the Source of (S2) . g is Element of the carrier of (S2)
C is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
the carrier of C is non empty set
a is Element of the carrier of C
S is Element of the carrier of C
Hom (a,S) is Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is set
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = a & cod b₁ = S ) } is set
f is Morphism of a,S
dom f is Element of the carrier of C
the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is set
bool [: the carrier' of