:: ISOCAT_2 semantic presentation

K145() is Element of bool K141()
K141() is set
bool K141() is non empty set
{} is empty Relation-like non-empty empty-yielding set
the empty Relation-like non-empty empty-yielding set is empty Relation-like non-empty empty-yielding set
1 is non empty set
{{},1} is non empty set
K140() is set
bool K140() is non empty set
bool K145() is non empty set
[:1,1:] is non empty Relation-like set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty Relation-like set
bool [:[:1,1:],1:] is non empty set
A is non empty set
B is non empty set
C is non empty set
Funcs (B,C) is non empty functional FUNCTION_DOMAIN of B,C
[:A,(Funcs (B,C)):] is non empty Relation-like set
bool [:A,(Funcs (B,C)):] is non empty set
c₄ is non empty Relation-like A -defined Funcs (B,C) -valued Function-like total quasi_total Element of bool [:A,(Funcs (B,C)):]
uncurry c₄ is Relation-like Function-like set
[:A,B:] is non empty Relation-like set
[:[:A,B:],C:] is non empty Relation-like set
bool [:[:A,B:],C:] is non empty set
rng c₄ is non empty Element of bool (Funcs (B,C))
bool (Funcs (B,C)) is non empty set
uncurry c₄ is non empty Relation-like [:A,B:] -defined C -valued Function-like total quasi_total Element of bool [:[:A,B:],C:]
dom (uncurry c₄) is non empty Relation-like A -defined B -valued Element of bool [:A,B:]
bool [:A,B:] is non empty set
dom c₄ is non empty Element of bool A
bool A is non empty set
[:(dom c₄),B:] is non empty Relation-like set
A is non empty set
B is non empty set
C is non empty set
Funcs (B,C) is non empty functional FUNCTION_DOMAIN of B,C
[:A,(Funcs (B,C)):] is non empty Relation-like set
bool [:A,(Funcs (B,C)):] is non empty set
c₄ is non empty Relation-like A -defined Funcs (B,C) -valued Function-like total quasi_total Element of bool [:A,(Funcs (B,C)):]
(A,B,C,c₄) is non empty Relation-like [:A,B:] -defined C -valued Function-like total quasi_total Element of bool [:[:A,B:],C:]
[:A,B:] is non empty Relation-like set
[:[:A,B:],C:] is non empty Relation-like set
bool [:[:A,B:],C:] is non empty set
curry (A,B,C,c₄) is non empty Relation-like A -defined Funcs (B,C) -valued Function-like total quasi_total Element of bool [:A,(Funcs (B,C)):]
rng c₄ is non empty Element of bool (Funcs (B,C))
bool (Funcs (B,C)) is non empty set
A is non empty set
B is non empty set
C is non empty set
Funcs (B,C) is non empty functional FUNCTION_DOMAIN of B,C
[:A,(Funcs (B,C)):] is non empty Relation-like set
bool [:A,(Funcs (B,C)):] is non empty set
c₄ is non empty Relation-like A -defined Funcs (B,C) -valued Function-like total quasi_total Element of bool [:A,(Funcs (B,C)):]
(A,B,C,c₄) is non empty Relation-like [:A,B:] -defined C -valued Function-like total quasi_total Element of bool [:[:A,B:],C:]
[:A,B:] is non empty Relation-like set
[:[:A,B:],C:] is non empty Relation-like set
bool [:[:A,B:],C:] is non empty set
o1 is Element of A
c₄ . o1 is Relation-like B -defined C -valued Function-like total quasi_total Element of Funcs (B,C)
o2 is Element of B
(A,B,C,c₄) . (o1,o2) is Element of C
[o1,o2] is set
{o1,o2} is non empty set
{o1} is non empty set
{{o1,o2},{o1}} is non empty set
(A,B,C,c₄) . [o1,o2] is set
(c₄ . o1) . o2 is Element of C
dom c₄ is non empty Element of bool A
bool A is non empty set
dom (c₄ . o1) is Element of bool B
bool B is non empty set
A is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr
the carrier' of A is non empty set
B is Element of the carrier' of A
cod B is Element of the carrier of A
the carrier of A is non empty set
the Target of A is non empty Relation-like the carrier' of A -defined the carrier of A -valued Function-like total quasi_total Element of bool [: the carrier' of A, the carrier of A:]
[: the carrier' of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier' of A, the carrier of A:] is non empty set
the Target of A . B is Element of the carrier of A
id (cod B) is Morphism of cod B, cod B
(id (cod B)) (*) B is Element of the carrier' of A
dom B is Element of the carrier of A
the Source of A is non empty Relation-like the carrier' of A -defined the carrier of A -valued Function-like total quasi_total Element of bool [: the carrier' of A, the carrier of A:]
the Source of A . B is Element of the carrier of A
Hom ((dom B),(cod B)) is Element of bool the carrier' of A
bool the carrier' of A is non empty set
{ b₁ where b₁ is Element of the carrier' of A : ( dom b₁ = dom B & cod b₁ = cod B ) } is set
Hom ((cod B),(cod B)) is non empty Element of bool the carrier' of A
{ b₁ where b₁ is Element of the carrier' of A : ( dom b₁ = cod B & cod b₁ = cod B ) } is set
C is Morphism of dom B, cod B
(id (cod B)) * C is Morphism of dom B, cod B
A is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr
the carrier' of A is non empty set
B is Element of the carrier' of A
dom B is Element of the carrier of A
the carrier of A is non empty set
the Source of A is non empty Relation-like the carrier' of A -defined the carrier of A -valued Function-like total quasi_total Element of bool [: the carrier' of A, the carrier of A:]
[: the carrier' of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier' of A, the carrier of A:] is non empty set
the Source of A . B is Element of the carrier of A
id (dom B) is Morphism of dom B, dom B
B (*) (id (dom B)) is Element of the carrier' of A
cod B is Element of the carrier of A
the Target of A is non empty Relation-like the carrier' of A -defined the carrier of A -valued Function-like total quasi_total Element of bool [: the carrier' of A, the carrier of A:]
the Target of A . B is Element of the carrier of A
Hom ((dom B),(cod B)) is Element of bool the carrier' of A
bool the carrier' of A is non empty set
{ b₁ where b₁ is Element of the carrier' of A : ( dom b₁ = dom B & cod b₁ = cod B ) } is set
Hom ((dom B),(dom B)) is non empty Element of bool the carrier' of A
{ b₁ where b₁ is Element of the carrier' of A : ( dom b₁ = dom B & cod b₁ = dom B ) } is set
C is Morphism of dom B, cod B
C * (id (dom B)) is Morphism of dom B, cod B
A is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr
the carrier' of A is non empty set
B is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr
Functors (A,B) is non empty non void V55() strict Category-like V68() V69() V70() with_identities CatStr
the carrier of (Functors (A,B)) is non empty set
the carrier' of B is non empty set
C is set
Funct (A,B) is non empty FUNCTOR-DOMAIN of A,B
A is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr
the carrier' of A is non empty set
the carrier of A is non empty set
B is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr
Functors (A,B) is non empty non void V55() strict Category-like V68() V69() V70() with_identities CatStr
the carrier' of (Functors (A,B)) is non empty set
the carrier' of B is non empty set
C is Element of the carrier' of (Functors (A,B))
dom C is Element of the carrier of (Functors (A,B))
the carrier of (Functors (A,B)) is non empty set
the Source of (Functors (A,B)) is non empty Relation-like the carrier' of (Functors (A,B)) -defined the carrier of (Functors (A,B)) -valued Function-like total quasi_total Element of bool [: the carrier' of (Functors (A,B)), the carrier of (Functors (A,B)):]
[: the carrier' of (Functors (A,B)), the carrier of (Functors (A,B)):] is non empty Relation-like set
bool [: the carrier' of (Functors (A,B)), the carrier of (Functors (A,B)):] is non empty set
the Source of (Functors (A,B)) . C is Element of the carrier of (Functors (A,B))
cod C is Element of the carrier of (Functors (A,B))
the Target of (Functors (A,B)) is non empty Relation-like the carrier' of (Functors (A,B)) -defined the carrier of (Functors (A,B)) -valued Function-like total quasi_total Element of bool [: the carrier' of (Functors (A,B)), the carrier of (Functors (A,B)):]
the Target of (Functors (A,B)) . C is Element of the carrier of (Functors (A,B))
Hom ((dom C),(cod C)) is Element of bool the carrier' of (Functors (A,B))
bool the carrier' of (Functors (A,B)) is non empty set
{ b₁ where b₁ is Element of the carrier' of (Functors (A,B)) : ( dom b₁ = dom C & cod b₁ = cod C ) } is set
c₄ is non empty Relation-like the carrier' of A -defined the carrier' of B -valued Function-like total quasi_total Functor of A,B
o1 is non empty Relation-like the carrier' of A -defined the carrier' of B -valued Function-like total quasi_total Functor of A,B
[c₄,o1] is set
{c₄,o1} is non empty set
{c₄} is non empty set
{{c₄,o1},{c₄}} is non empty set
o2 is non empty Relation-like the carrier of A -defined the carrier' of B -valued Function-like total quasi_total natural_transformation of c₄,o1
[[c₄,o1],o2] is set
{[c₄,o1],o2} is non empty set
{[c₄,o1]} is non empty Relation-like set
{{[c₄,o1],o2},{[c₄,o1]}} is non empty set
NatTrans (A,B) is non empty NatTrans-DOMAIN of A,B
A is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr
the carrier of A is non empty set
B is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr
Functors (A,B) is non empty non void V55() strict Category-like V68() V69() V70() with_identities CatStr
the carrier' of (Functors (A,B)) is non empty set
the carrier' of B is non empty set
the carrier' of A is non empty set
C is Element of the carrier of A
NatTrans (A,B) is non empty NatTrans-DOMAIN of A,B
c₄ is Element of NatTrans (A,B)
o1 is non empty Relation-like the carrier' of A -defined the carrier' of B -valued Function-like total quasi_total Functor of A,B
o2 is non empty Relation-like the carrier' of A -defined the carrier' of B -valued Function-like total quasi_total Functor of A,B
[o1,o2] is set
{o1,o2} is non empty set
{o1} is non empty set
{{o1,o2},{o1}} is non empty set
G1 is non empty Relation-like the carrier of A -defined the carrier' of B -valued Function-like total quasi_total natural_transformation of o1,o2
[[o1,o2],G1] is set
{[o1,o2],G1} is non empty set
{[o1,o2]} is non empty Relation-like set
{{[o1,o2],G1},{[o1,o2]}} is non empty set
G1 . C is Morphism of o1 . C,o2 . C
o1 . C is Element of the carrier of B
the carrier of B is non empty set
Obj o1 is non empty Relation-like the carrier of A -defined the carrier of B -valued Function-like total quasi_total Element of bool [: the carrier of A, the carrier of B:]
[: the carrier of A, the carrier of B:] is non empty Relation-like set
bool [: the carrier of A, the carrier of B:] is non empty set
(Obj o1) . C is Element of the carrier of B
o2 . C is Element of the carrier of B
Obj o2 is non empty Relation-like the carrier of A -defined the carrier of B -valued Function-like total quasi_total Element of bool [: the carrier of A, the carrier of B:]
(Obj o2) . C is Element of the carrier of B
G2 is Element of the carrier' of B
t is Element of the carrier' of B
F1 is non empty Relation-like the carrier' of A -defined the carrier' of B -valued Function-like total quasi_total Functor of A,B
F2 is non empty Relation-like the carrier' of A -defined the carrier' of B -valued Function-like total quasi_total Functor of A,B
[F1,F2] is set
{F1,F2} is non empty set
{F1} is non empty set
{{F1,F2},{F1}} is non empty set
s is non empty Relation-like the carrier of A -defined the carrier' of B -valued Function-like total quasi_total natural_transformation of F1,F2
[[F1,F2],s] is set
{[F1,F2],s} is non empty set
{[F1,F2]} is non empty Relation-like set
{{[F1,F2],s},{[F1,F2]}} is non empty set
s . C is Morphism of F1 . C,F2 . C
F1 . C is Element of the carrier of B
Obj F1 is non empty Relation-like the carrier of A -defined the carrier of B -valued Function-like total quasi_total Element of bool [: the carrier of A, the carrier of B:]
(Obj F1) . C is Element of the carrier of B
F2 . C is Element of the carrier of B
Obj F2 is non empty Relation-like the carrier of A -defined the carrier of B -valued Function-like total quasi_total Element of bool [: the carrier of A, the carrier of B:]
(Obj F2) . C is Element of the carrier of B
[:(NatTrans (A,B)), the carrier' of B:] is non empty Relation-like set
bool [:(NatTrans (A,B)), the carrier' of B:] is non empty set
c₄ is non empty Relation-like NatTrans (A,B) -defined the carrier' of B -valued Function-like total quasi_total Element of bool [:(NatTrans (A,B)), the carrier' of B:]
[: the carrier' of (Functors (A,B)), the carrier' of B:] is non empty Relation-like set
bool [: the carrier' of (Functors (A,B)), the carrier' of B:] is non empty set
the carrier of (Functors (A,B)) is non empty set
o2 is Element of the carrier of (Functors (A,B))
G1 is non empty Relation-like the carrier' of A -defined the carrier' of B -valued Function-like total quasi_total Functor of A,B
G1 . C is Element of the carrier of B
Obj G1 is non empty Relation-like the carrier of A -defined the carrier of B -valued Function-like total quasi_total Element of bool [: the carrier of A, the carrier of B:]
(Obj G1) . C is Element of the carrier of B
[G1,G1] is set
{G1,G1} is non empty set
{G1} is non empty set
{{G1,G1},{G1}} is non empty set
id G1 is non empty Relation-like the carrier of A -defined the carrier' of B -valued Function-like total quasi_total natural_transformation of G1,G1
[[G1,G1],(id G1)] is set
{[G1,G1],(id G1)} is non empty set
{[G1,G1]} is non empty Relation-like set
{{[G1,G1],(id G1)},{[G1,G1]}} is non empty set
id o2 is Morphism of o2,o2
c₄ . (id o2) is set
c₄ . [[G1,G1],(id G1)] is set
(id G1) . C is Morphism of G1 . C,G1 . C
G2 is Element of the carrier of B
id G2 is Morphism of G2,G2
G1 is Element of the carrier' of (Functors (A,B))
o2 is Element of the carrier' of (Functors (A,B))
[G1,o2] is Element of the carrier' of [:(Functors (A,B)),(Functors (A,B)):]
[:(Functors (A,B)),(Functors (A,B)):] is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr
[: the carrier of (Functors (A,B)), the carrier of (Functors (A,B)):] is non empty Relation-like set
[: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):] is non empty Relation-like set
the Source of (Functors (A,B)) is non empty Relation-like the carrier' of (Functors (A,B)) -defined the carrier of (Functors (A,B)) -valued Function-like total quasi_total Element of bool [: the carrier' of (Functors (A,B)), the carrier of (Functors (A,B)):]
[: the carrier' of (Functors (A,B)), the carrier of (Functors (A,B)):] is non empty Relation-like set
bool [: the carrier' of (Functors (A,B)), the carrier of (Functors (A,B)):] is non empty set
[: the Source of (Functors (A,B)), the Source of (Functors (A,B)):] is non empty Relation-like [: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):] -defined [: the carrier of (Functors (A,B)), the carrier of (Functors (A,B)):] -valued Function-like total quasi_total Element of bool [:[: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):],[: the carrier of (Functors (A,B)), the carrier of (Functors (A,B)):]:]
[:[: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):],[: the carrier of (Functors (A,B)), the carrier of (Functors (A,B)):]:] is non empty Relation-like set
bool [:[: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):],[: the carrier of (Functors (A,B)), the carrier of (Functors (A,B)):]:] is non empty set
the Target of (Functors (A,B)) is non empty Relation-like the carrier' of (Functors (A,B)) -defined the carrier of (Functors (A,B)) -valued Function-like total quasi_total Element of bool [: the carrier' of (Functors (A,B)), the carrier of (Functors (A,B)):]
[: the Target of (Functors (A,B)), the Target of (Functors (A,B)):] is non empty Relation-like [: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):] -defined [: the carrier of (Functors (A,B)), the carrier of (Functors (A,B)):] -valued Function-like total quasi_total Element of bool [:[: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):],[: the carrier of (Functors (A,B)), the carrier of (Functors (A,B)):]:]
the Comp of (Functors (A,B)) is Relation-like [: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):] -defined the carrier' of (Functors (A,B)) -valued Function-like Element of bool [:[: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):], the carrier' of (Functors (A,B)):]
[:[: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):], the carrier' of (Functors (A,B)):] is non empty Relation-like set
bool [:[: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):], the carrier' of (Functors (A,B)):] is non empty set
K209( the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)), the Comp of (Functors (A,B)), the Comp of (Functors (A,B))) is Relation-like [:[: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):],[: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):]:] -defined [: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):] -valued Function-like Element of bool [:[:[: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):],[: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):]:],[: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):]:]
[:[: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):],[: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):]:] is non empty Relation-like set
[:[:[: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):],[: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):]:],[: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):]:] is non empty Relation-like set
bool [:[:[: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):],[: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):]:],[: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):]:] is non empty set
CatStr(# [: the carrier of (Functors (A,B)), the carrier of (Functors (A,B)):],[: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):],[: the Source of (Functors (A,B)), the Source of (Functors (A,B)):],[: the Target of (Functors (A,B)), the Target of (Functors (A,B)):],K209( the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)), the Comp of (Functors (A,B)), the Comp of (Functors (A,B))) #) is strict CatStr
the carrier' of [:(Functors (A,B)),(Functors (A,B)):] is non empty set
{G1,o2} is non empty set
{G1} is non empty set
{{G1,o2},{G1}} is non empty set
dom the Comp of (Functors (A,B)) is Relation-like the carrier' of (Functors (A,B)) -defined the carrier' of (Functors (A,B)) -valued Element of bool [: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):]
bool [: the carrier' of (Functors (A,B)), the carrier' of (Functors (A,B)):] is non empty set
dom o2 is Element of the carrier of (Functors (A,B))
the Source of (Functors (A,B)) . o2 is Element of the carrier of (Functors (A,B))
cod o2 is Element of the carrier of (Functors (A,B))
the Target of (Functors (A,B)) . o2 is Element of the carrier of (Functors (A,B))
F1 is non empty Relation-like the carrier' of A -defined the carrier' of B -valued Function-like total quasi_total Functor of A,B
F2 is non empty Relation-like the carrier' of A -defined the carrier' of B -valued Function-like total quasi_total Functor of A,B
[F1,F2] is set
{F1,F2} is non empty set
{F1} is non empty set
{{F1,F2},{F1}} is non empty set
s is non empty Relation-like the carrier of A -defined the carrier' of B -valued Function-like total quasi_total natural_transformation of F1,F2
[[F1,F2],s] is set
{[F1,F2],s} is non empty set
{[F1,F2]} is non empty Relation-like set
{{[F1,F2],s},{[F1,F2]}} is non empty set
F1 . C is Element of the carrier of B
Obj F1 is non empty Relation-like the carrier of A -defined the carrier of B -valued Function-like total quasi_total Element of bool [: the carrier of A, the carrier of B:]
(Obj F1) . C is Element of the carrier of B
F2 . C is Element of the carrier of B
Obj F2 is non empty Relation-like the carrier of A -defined the carrier of B -valued Function-like total quasi_total Element of bool [: the carrier of A, the carrier of B:]
(Obj F2) . C is Element of the carrier of B
Hom ((F1 . C),(F2 . C)) is Element of bool the carrier' of B
bool the carrier' of B is non empty set
{ b₁ where b₁ is Element of the carrier' of B : ( dom b₁ = F1 . C & cod b₁ = F2 . C ) } is set
G2 is Element of NatTrans (A,B)
c₄ . G2 is Element of the carrier' of B
s . C is Morphism of F1 . C,F2 . C
dom G1 is Element of the carrier of (Functors (A,B))
the Source of (Functors (A,B)) . G1 is Element of the carrier of (Functors (A,B))
cod G1 is Element of the carrier of (Functors (A,B))
the Target of (Functors (A,B)) . G1 is Element of the carrier of (Functors (A,B))
f is non empty Relation-like the carrier' of A -defined the carrier' of B -valued Function-like total quasi_total Functor of A,B
f is non empty Relation-like the carrier' of A -defined the carrier' of B -valued Function-like total quasi_total Functor of A,B
[f,f] is set
{f,f} is non empty set
{f} is non empty set
{{f,f},{f}} is non empty set
f2 is non empty Relation-like the carrier of A -defined the carrier' of B -valued Function-like total quasi_total natural_transformation of f,f
[[f,f],f2] is set
{[f,f],f2} is non empty set
{[f,f]} is non empty Relation-like set
{{[f,f],f2},{[f,f]}} is non empty set
f . C is Element of the carrier of B
Obj f is non empty Relation-like the carrier of A -defined the carrier of B -valued Function-like total quasi_total Element of bool [: the carrier of A, the carrier of B:]
(Obj f) . C is Element of the carrier of B
Hom ((F2 . C),(f . C)) is Element of bool the carrier' of B
{ b₁ where b₁ is Element of the carrier' of B : ( dom b₁ = F2 . C & cod b₁ = f . C ) } is set
t is Element of NatTrans (A,B)
c₄ . t is Element of the carrier' of B
g1 is non empty Relation-like the carrier of A -defined the carrier' of B -valued Function-like total quasi_total natural_transformation of F2,f
g1 . C is Morphism of F2 . C,f . C
G1 (*) o2 is Element of the carrier' of (Functors (A,B))
[F1,f] is set
{F1,f} is non empty set
{{F1,f},{F1}} is non empty set
g1 `*` s is non empty Relation-like the carrier of A -defined the carrier' of B -valued Function-like total quasi_total natural_transformation of F1,f
[[F1,f],(g1 `*` s)] is set
{[F1,f],(g1 `*` s)} is non empty set
{[F1,f]} is non empty Relation-like set
{{[F1,f],(g1 `*` s)},{[F1,f]}} is non empty set
o1 is non empty Relation-like the carrier' of (Functors (A,B)) -defined the carrier' of B -valued Function-like total quasi_total Element of bool [: the carrier' of (Functors (A,B)), the carrier' of B:]
o1 . (G1 (*) o2) is Element of the carrier' of B
(g1 `*` s) . C is Morphism of F1 . C,f . C
(g1 . C) * (s . C) is Morphism of F1 . C,f . C
(g1 . C) (*) (s . C) is Element of the carrier' of B
o1 . o2 is Element of the carrier' of B
o1 . G1 is Element of the carrier' of B
(o1 . G1) (*) (o1 . o2) is Element of the carrier' of B
o2 is Element of the carrier' of (Functors (A,B))
dom o2 is Element of the carrier of (Functors (A,B))
the Source of (Functors (A,B)) . o2 is Element of the carrier of (Functors (A,B))
cod o2 is Element of the carrier of (Functors (A,B))
the Target of (Functors (A,B)) . o2 is Element of the carrier of (Functors (A,B))
G2 is non empty Relation-like the carrier' of A -defined the carrier' of B -valued Function-like total quasi_total Functor of A,B
t is non empty Relation-like the carrier' of A -defined the carrier' of B -valued Function-like total quasi_total Functor of A,B
[G2,t] is set
{G2,t} is non empty set
{G2} is non empty set
{{G2,t},{G2}} is non empty set
F1 is non empty Relation-like the carrier of A -defined the carrier' of B -valued Function-like total quasi_total natural_transformation of G2,t
[[G2,t],F1] is set
{[G2,t],F1} is non empty set
{[G2,t]} is non empty Relation-like set
{{[G2,t],F1},{[G2,t]}} is non empty set
G2 . C is Element of the carrier of B
Obj G2 is non empty Relation-like the carrier of A -defined the carrier of B -valued Function-like total quasi_total Element of bool [: the carrier of A, the carrier of B:]
(Obj G2) . C is Element of the carrier of B
t . C is Element of the carrier of B
Obj t is non empty Relation-like the carrier of A -defined the carrier of B -valued Function-like total quasi_total Element of bool [: the carrier of A, the carrier of B:]
(Obj t) . C is Element of the carrier of B
Hom ((G2 . C),(t . C)) is Element of bool the carrier' of B
{ b₁ where b₁ is Element of the carrier' of B : ( dom b₁ = G2 . C & cod b₁ = t . C ) } is set
[G2,G2] is set
{G2,G2} is non empty set
{{G2,G2},{G2}} is non empty set
id G2 is non empty Relation-like the carrier of A -defined the carrier' of B -valued Function-like total quasi_total natural_transformation of G2,G2
[[G2,G2],(id G2)] is set
{[G2,G2],(id G2)} is non empty set
{[G2,G2]} is non empty Relation-like set
{{[G2,G2],(id G2)},{[G2,G2]}} is non empty set
id (dom o2) is Morphism of dom o2, dom o2
c₄ . (id (dom o2)) is set
c₄ . [[G2,G2],(id G2)] is set
(id G2) . C is Morphism of G2 . C,G2 . C
id (G2 . C) is Morphism of G2 . C,G2 . C
F1 . C is Morphism of G2 . C,t . C
dom (F1 . C) is Element of the carrier of B
the Source of B is non empty Relation-like the carrier' of B -defined the carrier of B -valued Function-like total quasi_total Element of bool [: the carrier' of B, the carrier of B:]
[: the carrier' of B, the carrier of B:] is non empty Relation-like set
bool [: the carrier' of B, the carrier of B:] is non empty set
the Source of B . (F1 . C) is Element of the carrier of B
id (dom (F1 . C)) is Morphism of dom (F1 . C), dom (F1 . C)
G1 is Element of NatTrans (A,B)
c₄ . G1 is Element of the carrier' of B
dom (c₄ . G1) is Element of the carrier of B
the Source of B . (c₄ . G1) is Element of the carrier of B
id (dom (c₄ . G1)) is Morphism of dom (c₄ . G1), dom (c₄ . G1)
o1 . o2 is Element of the carrier' of B
dom (o1 . o2) is Element of the carrier of B
the Source of B . (o1 . o2) is Element of the carrier of B
id (dom (o1 . o2)) is Morphism of dom (o1 . o2), dom (o1 . o2)
[t,t] is set
{t,t} is non empty set
{t} is non empty set
{{t,t},{t}} is non empty set
id t is non empty Relation-like the carrier of A -defined the carrier' of B -valued Function-like total quasi_total natural_transformation of t,t
[[t,t],(id t)] is set
{[t,t],(id t)} is non empty set
{[t,t]} is non empty Relation-like set
{{[t,t],(id t)},{[t,t]}} is non empty set
id (cod o2) is Morphism of cod o2, cod o2
c₄ . (id (cod o2)) is set
c₄ . [[t,t],(id t)] is set
(id t) . C is Morphism of t . C,t . C
id (t . C) is Morphism of t . C,t . C
cod (F1 . C) is Element of the carrier of B
the Target of B is non empty Relation-like the carrier' of B -defined the carrier of B -valued Function-like total quasi_total Element of bool [: the carrier' of B, the carrier of B:]
the Target of B . (F1 . C) is Element of the carrier of B
id (cod (F1 . C)) is Morphism of cod (F1 . C), cod (F1 . C)
cod (c₄ . G1) is Element of the carrier of B
the Target of B . (c₄ . G1) is Element of the carrier of B
id (cod (c₄ . G1)) is Morphism of cod (c₄ . G1), cod (c₄ . G1)
cod (o1 . o2) is Element of the carrier of B
the Target of B . (o1 . o2) is Element of the carrier of B
id (cod (o1 . o2)) is Morphism of cod (o1 . o2), cod (o1 . o2)
o2 is non empty Relation-like the carrier' of (Functors (A,B)) -defined the carrier' of B -valued Function-like total quasi_total Functor of Functors (A,B),B
G1 is non empty Relation-like the carrier' of A -defined the carrier' of B -valued Function-like total quasi_total Functor of A,B
G2 is non empty Relation-like the carrier' of A -defined the carrier' of B -valued Function-like total quasi_total Functor of A,B
[G1,G2] is set
{G1,G2} is non empty set
{G1} is non empty set
{{G1,G2},{G1}} is non empty set
t is non empty Relation-like the carrier of A -defined the carrier' of B -valued Function-like total quasi_total natural_transformation of G1,G2
[[G1,G2],t] is set
{[G1,G2],t} is non empty set
{[G1,G2]} is non empty Relation-like set
{{[G1,G2],t},{[G1,G2]}} is non empty set
o2 . [[G1,G2],t] is set
t . C is Morphism of G1 . C,G2 . C
G1 . C is Element of the carrier of B
Obj G1 is non empty Relation-like the carrier of A -defined the carrier of B -valued Function-like total quasi_total Element of bool [: the carrier of A, the carrier of B:]
(Obj G1) . C is Element of the carrier of B
G2 . C is Element of the carrier of B
Obj G2 is non empty Relation-like the carrier of A -defined the carrier of B -valued Function-like total quasi_total Element of bool [: the carrier of A, the carrier of B:]
(Obj G2) . C is Element of the carrier of B
c₄ is non empty Relation-like the carrier' of (Functors (A,B)) -defined the carrier' of B -valued Function-like total quasi_total Functor of Functors (A,B),B
o1 is non empty Relation-like the carrier' of (Functors (A,B)) -defined the carrier' of B -valued Function-like total quasi_total Functor of Functors (A,B),B
NatTrans (A,B) is non empty NatTrans-DOMAIN of A,B
o2 is Element of the carrier' of (Functors (A,B))
G1 is non empty Relation-like the carrier' of A -defined the carrier' of B -valued Function-like total quasi_total Functor of A,B
G2 is non empty Relation-like the carrier' of A -defined the carrier' of B -valued Function-like total quasi_total Functor of A,B
[G1,G2] is set
{G1,G2} is non empty set
{G1} is non empty set
{{G1,G2},{G1}} is non empty set
t is non empty Relation-like the carrier of A -defined the carrier' of B -valued Function-like total quasi_total natural_transformation of G1,G2
[[G1,G2],t] is set
{[G1,G2],t} is non empty set
{[G1,G2]} is non empty Relation-like set
{{[G1,G2],t},{[G1,G2]}} is non empty set
c₄ . o2 is Element of the carrier' of B
t . C is Morphism of G1 . C,G2 . C
G1 . C is Element of the carrier of B
the carrier of B is non empty set
Obj G1 is non empty Relation-like the carrier of A -defined the carrier of B -valued Function-like total quasi_total Element of bool [: the carrier of A, the carrier of B:]
[: the carrier of A, the carrier of B:] is non empty Relation-like set
bool [: the carrier of A, the carrier of B:] is non empty set
(Obj G1) . C is Element of the carrier of B
G2 . C is Element of the carrier of B
Obj G2 is non empty Relation-like the carrier of A -defined the carrier of B -valued Function-like total quasi_total Element of bool [: the carrier of A, the carrier of B:]
(Obj G2) . C is Element of the carrier of B
o1 . o2 is Element of the carrier' of B
A is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr
B is set
C is set
1Cat (B,C) is non empty trivial V49() non void V54(1) V55() trivial' strict Category-like V68() V69() V70() with_identities CatStr
{B} is non empty set
{C} is non empty set
C :-> B is non empty Relation-like {C} -defined {B} -valued Function-like total quasi_total Element of bool [:{C},{B}:]
[:{C},{B}:] is non empty Relation-like set
bool [:{C},{B}:] is non empty set
(C,C) :-> C is non empty Relation-like [:{C},{C}:] -defined {C} -valued Function-like total quasi_total Element of bool [:[:{C},{C}:],{C}:]
[:{C},{C}:] is non empty Relation-like set
[:[:{C},{C}:],{C}:] is non empty Relation-like set
bool [:[:{C},{C}:],{C}:] is non empty set
CatStr(# {B},{C},(C :-> B),(C :-> B),((C,C) :-> C) #) is strict CatStr
Functors ((1Cat (B,C)),A) is non empty non void V55() strict Category-like V68() V69() V70() with_identities CatStr
the carrier of (1Cat (B,C)) is non empty trivial V31() set
the carrier' of (Functors ((1Cat (B,C)),A)) is non empty set
the carrier' of A is non empty set
c₄ is Element of the carrier of (1Cat (B,C))
((1Cat (B,C)),A,c₄) is non empty Relation-like the carrier' of (Functors ((1Cat (B,C)),A)) -defined the carrier' of A -valued Function-like total quasi_total Functor of Functors ((1Cat (B,C)),A),A
o1 is non empty Relation-like the carrier' of (Functors ((1Cat (B,C)),A)) -defined the carrier' of A -valued Function-like total quasi_total Functor of Functors ((1Cat (B,C)),A),A
NatTrans ((1Cat (B,C)),A) is non empty NatTrans-DOMAIN of 1Cat (B,C),A
o2 is set
the carrier' of (1Cat (B,C)) is non empty trivial set
G2 is non empty Relation-like the carrier' of (1Cat (B,C)) -defined the carrier' of A -valued Function-like total quasi_total Functor of 1Cat (B,C),A
t is non empty Relation-like the carrier' of (1Cat (B,C)) -defined the carrier' of A -valued Function-like total quasi_total Functor of 1Cat (B,C),A
[G2,t] is set
{G2,t} is non empty set
{G2} is non empty set
{{G2,t},{G2}} is non empty set
F1 is non empty Relation-like the carrier of (1Cat (B,C)) -defined the carrier' of A -valued Function-like total quasi_total natural_transformation of G2,t
[[G2,t],F1] is set
{[G2,t],F1} is non empty set
{[G2,t]} is non empty Relation-like set
{{[G2,t],F1},{[G2,t]}} is non empty set
G1 is set
F2 is non empty Relation-like the carrier' of (1Cat (B,C)) -defined the carrier' of A -valued Function-like total quasi_total Functor of 1Cat (B,C),A
s is non empty Relation-like the carrier' of (1Cat (B,C)) -defined the carrier' of A -valued Function-like total quasi_total Functor of 1Cat (B,C),A
[F2,s] is set
{F2,s} is non empty set
{F2} is non empty set
{{F2,s},{F2}} is non empty set
f is non empty Relation-like the carrier of (1Cat (B,C)) -defined the carrier' of A -valued Function-like total quasi_total natural_transformation of F2,s
[[F2,s],f] is set
{[F2,s],f} is non empty set
{[F2,s]} is non empty Relation-like set
{{[F2,s],f},{[F2,s]}} is non empty set
o1 . o2 is set
o1 . G1 is set
F1 . c₄ is Morphism of G2 . c₄,t . c₄
G2 . c₄ is Element of the carrier of A
the carrier of A is non empty set
Obj G2 is non empty Relation-like the carrier of (1Cat (B,C)) -defined the carrier of A -valued Function-like total quasi_total Element of bool [: the carrier of (1Cat (B,C)), the carrier of A:]
[: the carrier of (1Cat (B,C)), the carrier of A:] is non empty Relation-like set
bool [: the carrier of (1Cat (B,C)), the carrier of A:] is non empty set
(Obj G2) . c₄ is Element of the carrier of A
t . c₄ is Element of the carrier of A
Obj t is non empty Relation-like the carrier of (1Cat (B,C)) -defined the carrier of A -valued Function-like total quasi_total Element of bool [: the carrier of (1Cat (B,C)), the carrier of A:]
(Obj t) . c₄ is Element of the carrier of A
f . c₄ is Morphism of F2 . c₄,s . c₄
F2 . c₄ is Element of the carrier of A
Obj F2 is non empty Relation-like the carrier of (1Cat (B,C)) -defined the carrier of A -valued Function-like total quasi_total Element of bool [: the carrier of (1Cat (B,C)), the carrier of A:]
(Obj F2) . c₄ is Element of the carrier of A
s . c₄ is Element of the carrier of A
Obj s is non empty Relation-like the carrier of (1Cat (B,C)) -defined the carrier of A -valued Function-like total quasi_total Element of bool [: the carrier of (1Cat (B,C)), the carrier of A:]
(Obj s) . c₄ is Element of the carrier of A
[:{C}, the carrier' of A:] is non empty Relation-like set
bool [:{C}, the carrier' of A:] is non empty set
{c₄} is non empty set
[:{c₄}, the carrier' of A:] is non empty Relation-like set
bool [:{c₄}, the carrier' of A:] is non empty set
id c₄ is Morphism of c₄,c₄
Hom ((G2 . c₄),(t . c₄)) is Element of bool the carrier' of A
bool the carrier' of A is non empty set
{ b₁ where b₁ is Element of the carrier' of A : ( dom b₁ = G2 . c₄ & cod b₁ = t . c₄ ) } is set
Hom ((F2 . c₄),(s . c₄)) is Element of bool the carrier' of A
{ b₁ where b₁ is Element of the carrier' of A : ( dom b₁ = F2 . c₄ & cod b₁ = s . c₄ ) } is set
f is non empty Relation-like {C} -defined the carrier' of A -valued Function-like total quasi_total Element of bool [:{C}, the carrier' of A:]
f . (id c₄) is set
id (F2 . c₄) is Morphism of F2 . c₄,F2 . c₄
f2 is non empty Relation-like {C} -defined the carrier' of A -valued Function-like total quasi_total Element of bool [:{C}, the carrier' of A:]
f2 . (id c₄) is set
g1 is non empty Relation-like {C} -defined the carrier' of A -valued Function-like total quasi_total Element of bool [:{C}, the carrier' of A:]
g1 . (id c₄) is set
id (s . c₄) is Morphism of s . c₄,s . c₄
f1 is non empty Relation-like {C} -defined the carrier' of A -valued Function-like total quasi_total Element of bool [:{C}, the carrier' of A:]
f1 . (id c₄) is set
t2 is non empty Relation-like {c₄} -defined the carrier' of A -valued Function-like total quasi_total Element of bool [:{c₄}, the carrier' of A:]
t2 . c₄ is set
a1 is non empty Relation-like {c₄} -defined the carrier' of A -valued Function-like total quasi_total Element of bool [:{c₄}, the carrier' of A:]
a1 . c₄ is set
rng o1 is non empty Element of bool the carrier' of A
o2 is set
[: the carrier' of (1Cat (B,C)), the carrier' of A:] is non empty Relation-like set
bool [: the carrier' of (1Cat (B,C)), the carrier' of A:] is non empty set
G1 is Element of the carrier' of A
dom G1 is Element of the carrier of A
the Source of A is non empty Relation-like the carrier' of A -defined the carrier of A -valued Function-like total quasi_total Element of bool [: the carrier' of A, the carrier of A:]
[: the carrier' of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier' of A, the carrier of A:] is non empty set
the Source of A . G1 is Element of the carrier of A
id (dom G1) is Morphism of dom G1, dom G1
{C} --> (id (dom G1)) is non empty Relation-like {C} -defined the carrier' of A -valued Function-like total quasi_total Element of bool [:{C}, the carrier' of A:]
cod G1 is Element of the carrier of A
the Target of A is non empty Relation-like the carrier' of A -defined the carrier of A -valued Function-like total quasi_total Element of bool [: the carrier' of A, the carrier of A:]
the Target of A . G1 is Element of the carrier of A
id (cod G1) is Morphism of cod G1, cod G1
{C} --> (id (cod G1)) is non empty Relation-like {C} -defined the carrier' of A -valued Function-like total quasi_total Element of bool [:{C}, the carrier' of A:]
G2 is non empty Relation-like the carrier' of (1Cat (B,C)) -defined the carrier' of A -valued Function-like total quasi_total Element of bool [: the carrier' of (1Cat (B,C)), the carrier' of A:]
F1 is Element of the carrier' of (1Cat (B,C))
dom F1 is Element of the carrier of (1Cat (B,C))
the Source of (1Cat (B,C)) is non empty Relation-like the carrier' of (1Cat (B,C)) -defined the carrier of (1Cat (B,C)) -valued Function-like total quasi_total Element of bool [: the carrier' of (1Cat (B,C)), the carrier of (1Cat (B,C)):]
[: the carrier' of (1Cat (B,C)), the carrier of (1Cat (B,C)):] is non empty Relation-like set
bool [: the carrier' of (1Cat (B,C)), the carrier of (1Cat (B,C)):] is non empty set
the Source of (1Cat (B,C)) . F1 is Element of the carrier of (1Cat (B,C))
id (dom F1) is Morphism of dom F1, dom F1
G2 . (id (dom F1)) is Element of the carrier' of A
dom (id (dom G1)) is Element of the carrier of A
the Source of A . (id (dom G1)) is Element of the carrier of A
id (dom (id (dom G1))) is Morphism of dom (id (dom G1)), dom (id (dom G1))
G2 . F1 is Element of the carrier' of A
dom (G2 . F1) is Element of the carrier of A
the Source of A . (G2 . F1) is Element of the carrier of A
id (dom (G2 . F1)) is Morphism of dom (G2 . F1), dom (G2 . F1)
cod F1 is Element of the carrier of (1Cat (B,C))
the Target of (1Cat (B,C)) is non empty Relation-like the carrier' of (1Cat (B,C)) -defined the carrier of (1Cat (B,C)) -valued Function-like total quasi_total Element of bool [: the carrier' of (1Cat (B,C)), the carrier of (1Cat (B,C)):]
the Target of (1Cat (B,C)) . F1 is Element of the carrier of (1Cat (B,C))
id (cod F1) is Morphism of cod F1, cod F1
G2 . (id (cod F1)) is Element of the carrier' of A
cod (id (dom G1)) is Element of the carrier of A
the Target of A . (id (dom G1)) is Element of the carrier of A
id (cod (id (dom G1))) is Morphism of cod (id (dom G1)), cod (id (dom G1))
cod (G2 . F1) is Element of the carrier of A
the Target of A . (G2 . F1) is Element of the carrier of A
id (cod (G2 . F1)) is Morphism of cod (G2 . F1), cod (G2 . F1)
F2 is Element of the carrier' of (1Cat (B,C))
dom F2 is Element of the carrier of (1Cat (B,C))
the Source of (1Cat (B,C)) . F2 is Element of the carrier of (1Cat (B,C))
F1 is Element of the carrier' of (1Cat (B,C))
cod F1 is Element of the carrier of (1Cat (B,C))
the Target of (1Cat (B,C)) . F1 is Element of the carrier of (1Cat (B,C))
Hom ((dom G1),(dom G1)) is non empty Element of bool the carrier' of A
{ b₁ where b₁ is Element of the carrier' of A : ( dom b₁ = dom G1 & cod b₁ = dom G1 ) } is set
F2 (*) F1 is Element of the carrier' of (1Cat (B,C))
G2 . (F2 (*) F1) is Element of the carrier' of A
(id (dom G1)) * (id (dom G1)) is Morphism of dom G1, dom G1
(id (dom G1)) (*) (id (dom G1)) is Element of the carrier' of A
G2 . F1 is Element of the carrier' of A
(id (dom G1)) (*) (G2 . F1) is Element of the carrier' of A
G2 . F2 is Element of the carrier' of A
(G2 . F2) (*) (G2 . F1) is Element of the carrier' of A
F2 is Element of the carrier' of (1Cat (B,C))
dom F2 is Element of the carrier of (1Cat (B,C))
the Source of (1Cat (B,C)) . F2 is Element of the carrier of (1Cat (B,C))
F1 is Element of the carrier' of (1Cat (B,C))
cod F1 is Element of the carrier of (1Cat (B,C))
the Target of (1Cat (B,C)) . F1 is Element of the carrier of (1Cat (B,C))
Hom ((cod G1),(cod G1)) is non empty Element of bool the carrier' of A
{ b₁ where b₁ is Element of the carrier' of A : ( dom b₁ = cod G1 & cod b₁ = cod G1 ) } is set
t is non empty Relation-like the carrier' of (1Cat (B,C)) -defined the carrier' of A -valued Function-like total quasi_total Element of bool [: the carrier' of (1Cat (B,C)), the carrier' of A:]
F2 (*) F1 is Element of the carrier' of (1Cat (B,C))
t . (F2 (*) F1) is Element of the carrier' of A
(id (cod G1)) * (id (cod G1)) is Morphism of cod G1, cod G1
(id (cod G1)) (*) (id (cod G1)) is Element of the carrier' of A
t . F1 is Element of the carrier' of A
(id (cod G1)) (*) (t . F1) is Element of the carrier' of A
t . F2 is Element of the carrier' of A
(t . F2) (*) (t . F1) is Element of the carrier' of A
F1 is Element of the carrier' of (1Cat (B,C))
dom F1 is Element of the carrier of (1Cat (B,C))
the Source of (1Cat (B,C)) . F1 is Element of the carrier of (1Cat (B,C))
id (dom F1) is Morphism of dom F1, dom F1
t . (id (dom F1)) is Element of the carrier' of A
dom (id (cod G1)) is Element of the carrier of A
the Source of A . (id (cod G1)) is Element of the carrier of A
id (dom (id (cod G1))) is Morphism of dom (id (cod G1)), dom (id (cod G1))
t . F1 is Element of the carrier' of A
dom (t . F1) is Element of the carrier of A
the Source of A . (t . F1) is Element of the carrier of A
id (dom (t . F1)) is Morphism of dom (t . F1), dom (t . F1)
cod F1 is Element of the carrier of (1Cat (B,C))
the Target of (1Cat (B,C)) . F1 is Element of the carrier of (1Cat (B,C))
id (cod F1) is Morphism of cod F1, cod F1
t . (id (cod F1)) is Element of the carrier' of A
cod (id (cod G1)) is Element of the carrier of A
the Target of A . (id (cod G1)) is Element of the carrier of A
id (cod (id (cod G1))) is Morphism of cod (id (cod G1)), cod (id (cod G1))
cod (t . F1) is Element of the carrier of A
the Target of A . (t . F1) is Element of the carrier of A
id (cod (t . F1)) is Morphism of cod (t . F1), cod (t . F1)
F1 is Element of the carrier of (1Cat (B,C))
id F1 is Morphism of F1,F1
G2 . (id F1) is Element of the carrier' of A
F2 is Element of the carrier of (1Cat (B,C))
id F2 is Morphism of F2,F2
t . (id F2) is Element of the carrier' of A
[: the carrier of (1Cat (B,C)), the carrier' of A:] is non empty Relation-like set
bool [: the carrier of (1Cat (B,C)), the carrier' of A:] is non empty set
{c₄} --> G1 is non empty Relation-like {c₄} -defined the carrier' of A -valued Function-like total quasi_total Element of bool [:{c₄}, the carrier' of A:]
F1 is non empty Relation-like the carrier' of (1Cat (B,C)) -defined the carrier' of A -valued Function-like total quasi_total Functor of 1Cat (B,C),A
F2 is non empty Relation-like the carrier' of (1Cat (B,C)) -defined the carrier' of A -valued Function-like total quasi_total Functor of 1Cat (B,C),A
f is Element of the carrier of (1Cat (B,C))
F1 . f is Element of the carrier of A
Obj F1 is non empty Relation-like the carrier of (1Cat (B,C)) -defined the carrier of A -valued Function-like total quasi_total Element of bool [: the carrier of (1Cat (B,C)), the carrier of A:]
(Obj F1) . f is Element of the carrier of A
F2 . f is Element of the carrier of A
Obj F2 is non empty Relation-like the carrier of (1Cat (B,C)) -defined the carrier of A -valued Function-like total quasi_total Element of bool [: the carrier of (1Cat (B,C)), the carrier of A:]
(Obj F2) . f is Element of the carrier of A
id f is Morphism of f,f
F2 . (id f) is Element of the carrier' of A
id (F2 . f) is Morphism of F2 . f,F2 . f
F1 . (id f) is Element of the carrier' of A
id (F1 . f) is Morphism of F1 . f,F1 . f
f is Element of the carrier of (1Cat (B,C))
F2 . f is Element of the carrier of A
Obj F2 is non empty Relation-like the carrier of (1Cat (B,C)) -defined the carrier of A -valued Function-like total quasi_total Element of bool [: the carrier of (1Cat (B,C)), the carrier of A:]
(Obj F2) . f is Element of the carrier of A
s is non empty Relation-like the carrier of (1Cat (B,C)) -defined the carrier' of A -valued Function-like total quasi_total Element of bool [: the carrier of (1Cat (B,C)), the carrier' of A:]
s . f is Element of the carrier' of A
F1 . f is Element of the carrier of A
Obj F1 is non empty Relation-like the carrier of (1Cat (B,C)) -defined the carrier of A -valued Function-like total quasi_total Element of bool [: the carrier of (1Cat (B,C)), the carrier of A:]
(Obj F1) . f is Element of the carrier of A
Hom ((F1 . f),(F2 . f)) is Element of bool the carrier' of A
{ b₁ where b₁ is Element of the carrier' of A : ( dom b₁ = F1 . f & cod b₁ = F2 . f ) } is set
f is Element of the carrier of (1Cat (B,C))
F1 . f is Element of the carrier of A
(Obj F1) . f is Element of the carrier of A
F2 . f is Element of the carrier of A
(Obj F2) . f is Element of the carrier of A
Hom ((F1 . f),(F2 . f)) is Element of bool the carrier' of A
{ b₁ where b₁ is Element of the carrier' of A : ( dom b₁ = F1 . f & cod b₁ = F2 . f ) } is set
f is non empty Relation-like the carrier of (1Cat (B,C)) -defined the carrier' of A -valued Function-like total quasi_total transformation of F1,F2
f is Element of the carrier of (1Cat (B,C))
f . f is Morphism of F1 . f,F2 . f
F1 . f is Element of the carrier of A
(Obj F1) . f is Element of the carrier of A
F2 . f is Element of the carrier of A
(Obj F2) . f is Element of the carrier of A
({c₄} --> G1) . f is set
f is Element of the carrier of (1Cat (B,C))
f2 is Element of the carrier of (1Cat (B,C))
Hom (f,f2) is trivial Element of bool the carrier' of (1Cat (B,C))
bool the carrier' of (1Cat (B,C)) is non empty set
{ b₁ where b₁ is Element of the carrier' of (1Cat (B,C)) : ( dom b₁ = f & cod b₁ = f2 ) } is set
F2 . f is Element of the carrier of A
(Obj F2) . f is Element of the carrier of A
F2 . f2 is Element of the carrier of A
(Obj F2) . f2 is Element of the carrier of A
Hom ((F2 . f),(F2 . f2)) is Element of bool the carrier' of A
{ b₁ where b₁ is Element of the carrier' of A : ( dom b₁ = F2 . f & cod b₁ = F2 . f2 ) } is set
f . f is Morphism of F1 . f,F2 . f
F1 . f is Element of the carrier of A
(Obj F1) . f is Element of the carrier of A
Hom ((F1 . f),(F2 . f)) is Element of bool the carrier' of A
{ b₁ where b₁ is Element of the carrier' of A : ( dom b₁ = F1 . f & cod b₁ = F2 . f ) } is set
F1 . f2 is Element of the carrier of A
(Obj F1) . f2 is Element of the carrier of A
Hom ((F1 . f),(F1 . f2)) is Element of bool the carrier' of A
{ b₁ where b₁ is Element of the carrier' of A : ( dom b₁ = F1 . f & cod b₁ = F1 . f2 ) } is set
g1 is Morphism of f,f2
F2 /. g1 is Morphism of F2 . f,F2 . f2
F2 . C is set
F1 /. g1 is Morphism of F1 . f,F1 . f2
F1 . C is set
f . f2 is Morphism of F1 . f2,F2 . f2
Hom ((F1 . f2),(F2 . f2)) is Element of bool the carrier' of A
{ b₁ where b₁ is Element of the carrier' of A : ( dom b₁ = F1 . f2 & cod b₁ = F2 . f2 ) } is set
(f . f2) * (F1 /. g1) is Morphism of F1 . f,F2 . f2
G1 (*) (F1 /. g1) is Element of the carrier' of A
(F2 /. g1) (*) G1 is Element of the carrier' of A
(F2 /. g1) * (f . f) is Morphism of F1 . f,F2 . f2
[F1,F2] is set
{F1,F2} is non empty set
{F1} is non empty set
{{F1,F2},{F1}} is non empty set
f is non empty Relation-like the carrier of (1Cat (B,C)) -defined the carrier' of A -valued Function-like total quasi_total natural_transformation of F1,F2
[[F1,F2],f] is set
{[F1,F2],f} is non empty set
{[F1,F2]} is non empty Relation-like set
{{[F1,F2],f},{[F1,F2]}} is non empty set
o1 . [[F1,F2],f] is set
f . c₄ is Morphism of F1 . c₄,F2 . c₄
F1 . c₄ is Element of the carrier of A
(Obj F1) . c₄ is Element of the carrier of A
F2 . c₄ is Element of the carrier of A
(Obj F2) . c₄ is Element of the carrier of A
A is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr
the carrier of A is non empty set
B is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr
[:A,B:] is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr
the carrier of B is non empty set
[: the carrier of A, the carrier of B:] is non empty Relation-like set
the carrier' of A is non empty set
the carrier' of B is non empty set
[: the carrier' of A, the carrier' of B:] is non empty Relation-like set
the Source of A is non empty Relation-like the carrier' of A -defined the carrier of A -valued Function-like total quasi_total Element of bool [: the carrier' of A, the carrier of A:]
[: the carrier' of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier' of A, the carrier of A:] is non empty set
the Source of B is non empty Relation-like the carrier' of B -defined the carrier of B -valued Function-like total quasi_total Element of bool [: the carrier' of B, the carrier of B:]
[: the carrier' of B, the carrier of B:] is non empty Relation-like set
bool [: the carrier' of B, the carrier of B:] is non empty set
[: the Source of A, the Source of B:] is non empty Relation-like [: the carrier' of A, the carrier' of B:] -defined [: the carrier of A, the carrier of B:] -valued Function-like total quasi_total Element of bool [:[: the carrier' of A, the carrier' of B:],[: the carrier of A, the carrier of B:]:]
[:[: the carrier' of A, the carrier' of B:],[: the carrier of A, the carrier of B:]:] is non empty Relation-like set
bool [:[: the carrier' of A, the carrier' of B:],[: the carrier of A, the carrier of B:]:] is non empty set
the Target of A is non empty Relation-like the carrier' of A -defined the carrier of A -valued Function-like total quasi_total Element of bool [: the carrier' of A, the carrier of A:]
the Target of B is non empty Relation-like the carrier' of B -defined the carrier of B -valued Function-like total quasi_total Element of bool [: the carrier' of B, the carrier of B:]
[: the Target of A, the Target of B:] is non empty Relation-like [: the carrier' of A, the carrier' of B:] -defined [: the carrier of A, the carrier of B:] -valued Function-like total quasi_total Element of bool [:[: the carrier' of A, the carrier' of B:],[: the carrier of A, the carrier of B:]:]
the Comp of A is Relation-like [: the carrier' of A, the carrier' of A:] -defined the carrier' of A -valued Function-like Element of bool [:[: the carrier' of A, the carrier' of A:], the carrier' of A:]
[: the carrier' of A, the carrier' of A:] is non empty Relation-like set
[:[: the carrier' of A, the carrier' of A:], the carrier' of A:] is non empty Relation-like set
bool [:[: the carrier' of A, the carrier' of A:], the carrier' of A:] is non empty set
the Comp of B is Relation-like [: the carrier' of B, the carrier' of B:] -defined the carrier' of B -valued Function-like Element of bool [:[: the carrier' of B, the carrier' of B:], the carrier' of B:]
[: the carrier' of B, the carrier' of B:] is non empty Relation-like set
[:[: the carrier' of B, the carrier' of B:], the carrier' of B:] is non empty Relation-like set
bool [:[: the carrier' of B, the carrier' of B:], the carrier' of B:] is non empty set
K209( the carrier' of A, the carrier' of B, the Comp of A, the Comp of B) is Relation-like [:[: the carrier' of A, the carrier' of B:],[: the carrier' of A, the carrier' of B:]:] -defined [: the carrier' of A, the carrier' of B:] -valued Function-like Element of bool [:[:[: the carrier' of A, the carrier' of B:],[: the carrier' of A, the carrier' of B:]:],[: the carrier' of A, the carrier' of B:]:]
[:[: the carrier' of A, the carrier' of B:],[: the carrier' of A, the carrier' of B:]:] is non empty Relation-like set
[:[:[: the carrier' of A, the carrier' of B:],[: the carrier' of A, the carrier' of B:]:],[: the carrier' of A, the carrier' of B:]:] is non empty Relation-like set
bool [:[:[: the carrier' of A, the carrier' of B:],[: the carrier' of A, the carrier' of B:]:],[: the carrier' of A, the carrier' of B:]:] is non empty set
CatStr(# [: the carrier of A, the carrier of B:],[: the carrier' of A, the carrier' of B:],[: the Source of A, the Source of B:],[: the Target of A, the Target of B:],K209( the carrier' of A, the carrier' of B, the Comp of A, the Comp of B) #) is strict CatStr
the carrier' of [:A,B:] is non empty set
C is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr
the carrier' of C is non empty set
c₄ is non empty Relation-like the carrier' of [:A,B:] -defined the carrier' of C -valued Function-like total quasi_total Functor of [:A,B:],C
o1 is Element of the carrier of A
c₄ ?- o1 is non empty Relation-like the carrier' of B -defined the carrier' of C -valued Function-like total quasi_total Functor of B,C
curry c₄ is Relation-like Function-like set
id o1 is Morphism of o1,o1
(curry c₄) . (id o1) is set
o2 is Element of the carrier of B
(c₄ ?- o1) . o2 is Element of the carrier of C
the carrier of C is non empty set
Obj (c₄ ?- o1) is non empty Relation-like the carrier of B -defined the carrier of C -valued Function-like total quasi_total Element of bool [: the carrier of B, the carrier of C:]
[: the carrier of B, the carrier of C:] is non empty Relation-like set
bool [: the carrier of B, the carrier of C:] is non empty set
(Obj (c₄ ?- o1)) . o2 is Element of the carrier of C
[o1,o2] is Element of the carrier of [:A,B:]
the carrier of [:A,B:] is non empty set
{o1,o2} is non empty set
{o1} is non empty set
{{o1,o2},{o1}} is non empty set
c₄ . [o1,o2] is Element of the carrier of C
Obj c₄ is non empty Relation-like the carrier of [:A,B:] -defined the carrier of C -valued Function-like total quasi_total Element of bool [: the carrier of [:A,B:], the carrier of C:]
[: the carrier of [:A,B:], the carrier of C:] is non empty Relation-like set
bool [: the carrier of [:A,B:], the carrier of C:] is non empty set
(Obj c₄) . [o1,o2] is Element of the carrier of C
(Obj c₄) . (o1,o2) is set
[o1,o2] is set
(Obj c₄) . [o1,o2] is set
A is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr
the carrier of A is non empty set
B is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr
the carrier of B is non empty set
[:A,B:] is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr
[: the carrier of A, the carrier of B:] is non empty Relation-like set
the carrier' of A is non empty set
the carrier' of B is non empty set
[: the carrier' of A, the carrier' of B:] is non empty Relation-like set
the Source of A is non empty Relation-like the carrier' of A -defined the carrier of A -valued Function-like total quasi_total Element of bool [: the carrier' of A, the carrier of A:]
[: the carrier' of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier' of A, the carrier of A:] is non empty set
the Source of B is non empty Relation-like the carrier' of B -defined the carrier of B -valued Function-like total quasi_total Element of bool [: the carrier' of B, the carrier of B:]
[: the carrier' of B, the carrier of B:] is non empty Relation-like set
bool [: the carrier' of B, the carrier of B:] is non empty set
[: the Source of A, the Source of B:] is non empty Relation-like [: the carrier' of A, the carrier' of B:] -defined [: the carrier of A, the carrier of B:] -valued Function-like total quasi_total Element of bool [:[: the carrier' of A, the carrier' of B:],[: the carrier of A, the carrier of B:]:]
[:[: the carrier' of A, the carrier' of B:],[: the carrier of A, the carrier of B:]:] is non empty Relation-like set
bool [:[: the carrier' of A, the carrier' of B:],[: the carrier of A, the carrier of B:]:] is non empty set
the Target of A is non empty Relation-like the carrier' of A -defined the carrier of A -valued Function-like total quasi_total Element of bool [: the carrier' of A, the carrier of A:]
the Target of B is non empty Relation-like the carrier' of B -defined the carrier of B -valued Function-like total quasi_total Element of bool [: the carrier' of B, the carrier of B:]
[: the Target of A, the Target of B:] is non empty Relation-like [: the carrier' of A, the carrier' of B:] -defined [: the carrier of A, the carrier of B:] -valued Function-like total quasi_total Element of bool [:[: the carrier' of A, the carrier' of B:],[: the carrier of A, the carrier of B:]:]
the Comp of A is Relation-like [: the carrier' of A, the carrier' of A:] -defined the carrier' of A -valued Function-like Element of bool [:[: the carrier' of A, the carrier' of A:], the carrier' of A:]
[: the carrier' of A, the carrier' of A:] is non empty Relation-like set
[:[: the carrier' of A, the carrier' of A:], the carrier' of A:] is non empty Relation-like set
bool [:[: the carrier' of A, the carrier' of A:], the carrier' of A:] is non empty set
the Comp of B is Relation-like [: the carrier' of B, the carrier' of B:] -defined the carrier' of B -valued Function-like Element of bool [:[: the carrier' of B, the carrier' of B:], the carrier' of B:]
[: the carrier' of B, the carrier' of B:] is non empty Relation-like set
[:[: the carrier' of B, the carrier' of B:], the carrier' of B:] is non empty Relation-like set
bool [:[: the carrier' of B, the carrier' of B:], the carrier' of B:] is non empty set
K209( the carrier' of A, the carrier' of B, the Comp of A, the Comp of B) is Relation-like [:[: the carrier' of A, the carrier' of B:],[: the carrier' of A, the carrier' of B:]:] -defined [: the carrier' of A, the carrier' of B:] -valued Function-like Element of bool [:[:[: the carrier' of A, the carrier' of B:],[: the carrier' of A, the carrier' of B:]:],[: the carrier' of A, the carrier' of B:]:]
[:[: the carrier' of A, the carrier' of B:],[: the carrier' of A, the carrier' of B:]:] is non empty Relation-like set
[:[:[: the carrier' of A, the carrier' of B:],[: the carrier' of A, the carrier' of B:]:],[: the carrier' of A, the carrier' of B:]:] is non empty Relation-like set
bool [:[:[: the carrier' of A, the carrier' of B:],[: the carrier' of A, the carrier' of B:]:],[: the carrier' of A, the carrier' of B:]:] is non empty set
CatStr(# [: the carrier of A, the carrier of B:],[: the carrier' of A, the carrier' of B:],[: the Source of A, the Source of B:],[: the Target of A, the Target of B:],K209( the carrier' of A, the carrier' of B, the Comp of A, the Comp of B) #) is strict CatStr
C is Element of the carrier of A
c₄ is Element of the carrier of A
Hom (C,c₄) is Element of bool the carrier' of A
bool the carrier' of A is non empty set
{ b₁ where b₁ is Element of the carrier' of A : ( dom b₁ = C & cod b₁ = c₄ ) } is set
o1 is Element of the carrier of B
o2 is Element of the carrier of B
Hom (o1,o2) is Element of bool the carrier' of B
bool the carrier' of B is non empty set
{ b₁ where b₁ is Element of the carrier' of B : ( dom b₁ = o1 & cod b₁ = o2 ) } is set
[C,o1] is Element of the carrier of [:A,B:]
the carrier of [:A,B:] is non empty set
{C,o1} is non empty set
{C} is non empty set
{{C,o1},{C}} is non empty set
[c₄,o2] is Element of the carrier of [:A,B:]
{c₄,o2} is non empty set
{c₄} is non empty set
{{c₄,o2},{c₄}} is non empty set
Hom ([C,o1],[c₄,o2]) is Element of bool the carrier' of [:A,B:]
the carrier' of [:A,B:] is non empty set
bool the carrier' of [:A,B:] is non empty set
{ b₁ where b₁ is Element of the carrier' of [:A,B:] : ( dom b₁ = [C,o1] & cod b₁ = [c₄,o2] ) } is set
[:(Hom (C,c₄)),(Hom (o1,o2)):] is Relation-like set
A is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr
the carrier of A is non empty set
the carrier' of A is non empty set
B is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr
the carrier of B is non empty set
[:A,B:] is non empty non void V55() Category-like V68() V69() V70() with_identities CatStr
[: the carrier of A, the carrier of B:] is non empty Relation-like set
the carrier' of B is non empty set
[: the carrier' of A, the carrier' of B:] is non empty Relation-like set
the Source of A is non empty Relation-like the carrier' of A -defined the carrier of A -valued Function-like total quasi_total Element of bool [: the carrier' of A, the carrier of A:]
[: the carrier' of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier' of A, the carrier of A:] is non empty set
the Source of B is non empty Relation-like the carrier' of B -defined the carrier of B -valued Function-like total quasi_total Element of bool [: the carrier' of B, the carrier of B:]
[: the carrier' of B, the carrier of B:] is non empty Relation-like set
bool [: the carrier' of B, the carrier of B:] is non empty set
[: the Source of A, the Source of B:] is non empty Relation-like [: the carrier' of A, the carrier' of B:] -defined [: the carrier of A, the carrier of B:] -valued Function-like total quasi_total Element of bool [:[: the carrier' of A, the carrier' of B:],[: the carrier of A, the carrier of B:]:]
[:[: the carrier' of A, the carrier' of B:],[: the carrier of A, the carrier of B:]:] is non empty Relation-like set
bool [:[: the carrier' of A, the carrier' of B:],[: the carrier of A, the carrier of B:]:] is non empty set
the Target of A is non empty Relation-like the carrier' of A -defined the carrier of A -valued Function-like total quasi_total Element of bool [: the carrier' of A, the carrier of A:]
the Target of B is non empty Relation-like the carrier' of B -defined the carrier of B -valued Function-like total quasi_total Element of bool [: the carrier' of B, the carrier of B:]
[: the Target of A, the Target of B:] is non empty Relation-like [: the carrier' of A, the carrier' of B:] -defined [: the carrier of A, the carrier of B:] -valued Function-like total quasi_total Element of bool [:[: the carrier' of A, the carrier' of B:],[: the carrier of A, the carrier of B:]:]
the Comp of A is Relation-like [: the carrier' of A, the carrier' of A:] -defined the carrier' of A -valued Function-like Element of bool [:[: the