K158() is Element of bool K154()
K154() is set
bool K154() is non empty set
{} is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional set
the empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional set is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional set
1 is non empty set
{{},1} is non empty set
K153() is set
bool K153() is non empty set
bool K158() is non empty set
C is non empty non void V58() 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 Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like V21( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is non empty Relation-like set
bool [: the carrier' of C, 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 V21( the carrier' of C, the carrier of C) 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 non empty Relation-like set
[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is non empty Relation-like set
bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is non empty set
CatStr(# the carrier of C, the carrier' of C, the Source of C, the Target of C, the Comp of C #) is non empty non void V58() strict CatStr
f is non empty non void V58() CatStr
the carrier of f is non empty set
the carrier' of f is non empty set
the Source of f is Relation-like the carrier' of f -defined the carrier of f -valued Function-like V21( the carrier' of f, the carrier of f) Element of bool [: the carrier' of f, the carrier of f:]
[: the carrier' of f, the carrier of f:] is non empty Relation-like set
bool [: the carrier' of f, the carrier of f:] is non empty set
the Target of f is Relation-like the carrier' of f -defined the carrier of f -valued Function-like V21( the carrier' of f, the carrier of f) Element of bool [: the carrier' of f, the carrier of f:]
the Comp of f is Relation-like [: the carrier' of f, the carrier' of f:] -defined the carrier' of f -valued Function-like Element of bool [:[: the carrier' of f, the carrier' of f:], the carrier' of f:]
[: the carrier' of f, the carrier' of f:] is non empty Relation-like set
[:[: the carrier' of f, the carrier' of f:], the carrier' of f:] is non empty Relation-like set
bool [:[: the carrier' of f, the carrier' of f:], the carrier' of f:] is non empty set
CatStr(# the carrier of f, the carrier' of f, the Source of f, the Target of f, the Comp of f #) is non empty non void V58() strict CatStr
dom the Comp of f is Relation-like the carrier' of f -defined the carrier' of f -valued Element of bool [: the carrier' of f, the carrier' of f:]
bool [: the carrier' of f, the carrier' of f:] is non empty set
A1 is Element of the carrier' of f
g is Element of the carrier' of f
[A1,g] is V18() Element of [: the carrier' of f, the carrier' of f:]
{A1,g} is non empty set
{A1} is non empty set
{{A1,g},{A1}} is non empty set
dom A1 is Element of the carrier of f
the Source of f . A1 is Element of the carrier of f
cod g is Element of the carrier of f
the Target of f . g is Element of the carrier of f
A3 is Element of the carrier' of C
A2 is Element of the carrier' of C
[A3,A2] is V18() Element of the carrier' of [:C,C:]
[:C,C:] is non empty non void V58() Category-like transitive associative reflexive with_identities CatStr
[: the carrier of C, the carrier of C:] is non empty Relation-like set
[: the Source of C, the Source of C:] is Relation-like [: the carrier' of C, the carrier' of C:] -defined [: the carrier of C, the carrier of C:] -valued Function-like V21([: the carrier' of C, the carrier' of C:],[: the carrier of C, the carrier of C:]) Element of bool [:[: the carrier' of C, the carrier' of C:],[: the carrier of C, the carrier of C:]:]
[:[: the carrier' of C, the carrier' of C:],[: the carrier of C, the carrier of C:]:] is non empty Relation-like set
bool [:[: the carrier' of C, the carrier' of C:],[: the carrier of C, the carrier of C:]:] is non empty set
[: the Target of C, the Target of C:] is Relation-like [: the carrier' of C, the carrier' of C:] -defined [: the carrier of C, the carrier of C:] -valued Function-like V21([: the carrier' of C, the carrier' of C:],[: the carrier of C, the carrier of C:]) Element of bool [:[: the carrier' of C, the carrier' of C:],[: the carrier of C, the carrier of C:]:]
K222( the carrier' of C, the carrier' of C, the Comp of C, the Comp of C) is Relation-like [:[: the carrier' of C, the carrier' of C:],[: the carrier' of C, the carrier' of C:]:] -defined [: the carrier' of C, the carrier' of C:] -valued Function-like Element of bool [:[:[: the carrier' of C, the carrier' of C:],[: the carrier' of C, the carrier' of C:]:],[: the carrier' of C, the carrier' of C:]:]
[:[: the carrier' of C, the carrier' of C:],[: the carrier' of C, the carrier' of C:]:] is non empty Relation-like set
[:[:[: the carrier' of C, the carrier' of C:],[: the carrier' of C, the carrier' of C:]:],[: the carrier' of C, the carrier' of C:]:] is non empty Relation-like set
bool [:[:[: the carrier' of C, the carrier' of C:],[: the carrier' of C, the carrier' of C:]:],[: the carrier' of C, the carrier' of C:]:] is non empty set
CatStr(# [: the carrier of C, the carrier of C:],[: the carrier' of C, the carrier' of C:],[: the Source of C, the Source of C:],[: the Target of C, the Target of C:],K222( the carrier' of C, the carrier' of C, the Comp of C, the Comp of C) #) is non empty non void V58() strict CatStr
the carrier' of [:C,C:] is non empty set
{A3,A2} is non empty set
{A3} is non empty set
{{A3,A2},{A3}} is non empty set
dom A3 is Element of the carrier of C
the Source of C . A3 is Element of the carrier of C
cod A2 is Element of the carrier of C
the Target of C . A2 is Element of the carrier of C
A1 is Element of the carrier' of f
dom A1 is Element of the carrier of f
the Source of f . A1 is Element of the carrier of f
g is Element of the carrier' of f
cod g is Element of the carrier of f
the Target of f . g is Element of the carrier of f
A1 (*) g is Element of the carrier' of f
dom (A1 (*) g) is Element of the carrier of f
the Source of f . (A1 (*) g) is Element of the carrier of f
dom g is Element of the carrier of f
the Source of f . g is Element of the carrier of f
cod (A1 (*) g) is Element of the carrier of f
the Target of f . (A1 (*) g) is Element of the carrier of f
cod A1 is Element of the carrier of f
the Target of f . A1 is Element of the carrier of f
A3 is Element of the carrier' of C
dom A3 is Element of the carrier of C
the Source of C . A3 is Element of the carrier of C
A2 is Element of the carrier' of C
cod A2 is Element of the carrier of C
the Target of C . A2 is Element of the carrier of C
[A3,A2] is V18() Element of the carrier' of [:C,C:]
[:C,C:] is non empty non void V58() Category-like transitive associative reflexive with_identities CatStr
[: the carrier of C, the carrier of C:] is non empty Relation-like set
[: the Source of C, the Source of C:] is Relation-like [: the carrier' of C, the carrier' of C:] -defined [: the carrier of C, the carrier of C:] -valued Function-like V21([: the carrier' of C, the carrier' of C:],[: the carrier of C, the carrier of C:]) Element of bool [:[: the carrier' of C, the carrier' of C:],[: the carrier of C, the carrier of C:]:]
[:[: the carrier' of C, the carrier' of C:],[: the carrier of C, the carrier of C:]:] is non empty Relation-like set
bool [:[: the carrier' of C, the carrier' of C:],[: the carrier of C, the carrier of C:]:] is non empty set
[: the Target of C, the Target of C:] is Relation-like [: the carrier' of C, the carrier' of C:] -defined [: the carrier of C, the carrier of C:] -valued Function-like V21([: the carrier' of C, the carrier' of C:],[: the carrier of C, the carrier of C:]) Element of bool [:[: the carrier' of C, the carrier' of C:],[: the carrier of C, the carrier of C:]:]
K222( the carrier' of C, the carrier' of C, the Comp of C, the Comp of C) is Relation-like [:[: the carrier' of C, the carrier' of C:],[: the carrier' of C, the carrier' of C:]:] -defined [: the carrier' of C, the carrier' of C:] -valued Function-like Element of bool [:[:[: the carrier' of C, the carrier' of C:],[: the carrier' of C, the carrier' of C:]:],[: the carrier' of C, the carrier' of C:]:]
[:[: the carrier' of C, the carrier' of C:],[: the carrier' of C, the carrier' of C:]:] is non empty Relation-like set
[:[:[: the carrier' of C, the carrier' of C:],[: the carrier' of C, the carrier' of C:]:],[: the carrier' of C, the carrier' of C:]:] is non empty Relation-like set
bool [:[:[: the carrier' of C, the carrier' of C:],[: the carrier' of C, the carrier' of C:]:],[: the carrier' of C, the carrier' of C:]:] is non empty set
CatStr(# [: the carrier of C, the carrier of C:],[: the carrier' of C, the carrier' of C:],[: the Source of C, the Source of C:],[: the Target of C, the Target of C:],K222( the carrier' of C, the carrier' of C, the Comp of C, the Comp of C) #) is non empty non void V58() strict CatStr
the carrier' of [:C,C:] is non empty set
{A3,A2} is non empty set
{A3} is non empty set
{{A3,A2},{A3}} is non empty set
dom the Comp of C is Relation-like the carrier' of C -defined the carrier' of C -valued Element of bool [: the carrier' of C, the carrier' of C:]
bool [: the carrier' of C, the carrier' of C:] is non empty set
the Comp of C . (A3,A2) is set
[A3,A2] is V18() set
the Comp of C . [A3,A2] is set
A3 (*) A2 is Element of the carrier' of C
dom (A3 (*) A2) is Element of the carrier of C
the Source of C . (A3 (*) A2) is Element of the carrier of C
dom A2 is Element of the carrier of C
the Source of C . A2 is Element of the carrier of C
cod (A3 (*) A2) is Element of the carrier of C
the Target of C . (A3 (*) A2) is Element of the carrier of C
cod A3 is Element of the carrier of C
the Target of C . A3 is Element of the carrier of C
A1 is Element of the carrier' of f
cod A1 is Element of the carrier of f
the Target of f . A1 is Element of the carrier of f
g is Element of the carrier' of f
dom g is Element of the carrier of f
the Source of f . g is Element of the carrier of f
g (*) A1 is Element of the carrier' of f
A2 is Element of the carrier' of C
A3 is Element of the carrier' of C
A2 (*) A3 is Element of the carrier' of C
cod A3 is Element of the carrier of C
the Target of C . A3 is Element of the carrier of C
dom A2 is Element of the carrier of C
the Source of C . A2 is Element of the carrier of C
the Comp of f . (g,A1) is set
[g,A1] is V18() set
{g,A1} is non empty set
{g} is non empty set
{{g,A1},{g}} is non empty set
the Comp of f . [g,A1] is set
the Comp of C . (A2,A3) is set
[A2,A3] is V18() set
{A2,A3} is non empty set
{A2} is non empty set
{{A2,A3},{A2}} is non empty set
the Comp of C . [A2,A3] is set
A2 is Element of the carrier' of f
dom A2 is Element of the carrier of f
the Source of f . A2 is Element of the carrier of f
A1 is Element of the carrier' of f
cod A1 is Element of the carrier of f
the Target of f . A1 is Element of the carrier of f
dom A1 is Element of the carrier of f
the Source of f . A1 is Element of the carrier of f
g is Element of the carrier' of f
cod g is Element of the carrier of f
the Target of f . g is Element of the carrier of f
A1 (*) g is Element of the carrier' of f
A2 (*) (A1 (*) g) is Element of the carrier' of f
A2 (*) A1 is Element of the carrier' of f
(A2 (*) A1) (*) g is Element of the carrier' of f
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
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
dom F is Element of the carrier of C
the Source of C . F is Element of the carrier of C
A3 is Element of the carrier' of C
cod A3 is Element of the carrier of C
the Target of C . A3 is Element of the carrier of C
F (*) A3 is Element of the carrier' of C
G (*) F is Element of the carrier' of C
dom (A2 (*) A1) is Element of the carrier of f
the Source of f . (A2 (*) A1) is Element of the carrier of f
cod (A1 (*) g) is Element of the carrier of f
the Target of f . (A1 (*) g) is Element of the carrier of f
G (*) (F (*) A3) is Element of the carrier' of C
(G (*) F) (*) A3 is Element of the carrier' of C
g is Element of the carrier of f
Hom (g,g) is Element of bool the carrier' of f
bool the carrier' of f is non empty set
{ b1 where b1 is Element of the carrier' of f : ( dom b1 = g & cod b1 = g ) } is set
A1 is Element of the carrier of C
id A1 is Morphism of A1,A1
A2 is Element of the carrier' of f
cod A2 is Element of the carrier of f
the Target of f . A2 is Element of the carrier of f
cod (id A1) is Element of the carrier of C
the Target of C . (id A1) is Element of the carrier of C
dom A2 is Element of the carrier of f
the Source of f . A2 is Element of the carrier of f
dom (id A1) is Element of the carrier of C
the Source of C . (id A1) is Element of the carrier of C
g is Element of the carrier of f
A1 is Element of the carrier of C
id A1 is Morphism of A1,A1
A2 is Element of the carrier' of f
cod A2 is Element of the carrier of f
the Target of f . A2 is Element of the carrier of f
cod (id A1) is Element of the carrier of C
the Target of C . (id A1) is Element of the carrier of C
dom A2 is Element of the carrier of f
the Source of f . A2 is Element of the carrier of f
dom (id A1) is Element of the carrier of C
the Source of C . (id A1) is Element of the carrier of C
A3 is Morphism of g,g
F is Element of the carrier of f
Hom (g,F) is Element of bool the carrier' of f
bool the carrier' of f is non empty set
{ b1 where b1 is Element of the carrier' of f : ( dom b1 = g & cod b1 = F ) } is set
Hom (F,g) is Element of bool the carrier' of f
{ b1 where b1 is Element of the carrier' of f : ( dom b1 = F & cod b1 = g ) } is set
FG is Morphism of g,F
FG (*) A3 is Element of the carrier' of f
m is Element of the carrier' of C
cod m is Element of the carrier of C
the Target of C . m is Element of the carrier of C
cod FG is Element of the carrier of f
the Target of f . FG is Element of the carrier of f
G is Element of the carrier of C
dom m is Element of the carrier of C
the Source of C . m is Element of the carrier of C
dom FG is Element of the carrier of f
the Source of f . FG is Element of the carrier of f
Hom (A1,G) is Element of bool the carrier' of C
bool the carrier' of C is non empty set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = A1 & cod b1 = G ) } is set
g1 is Morphism of A1,G
dom g1 is Element of the carrier of C
the Source of C . g1 is Element of the carrier of C
cod A3 is Element of the carrier of f
the Target of f . A3 is Element of the carrier of f
the Comp of f . (FG,A3) is set
[FG,A3] is V18() set
{FG,A3} is non empty set
{FG} is non empty set
{{FG,A3},{FG}} is non empty set
the Comp of f . [FG,A3] is set
the Comp of C . (g1,(id A1)) is set
[g1,(id A1)] is V18() set
{g1,(id A1)} is non empty set
{g1} is non empty set
{{g1,(id A1)},{g1}} is non empty set
the Comp of C . [g1,(id A1)] is set
g1 (*) (id A1) is Element of the carrier' of C
FG is Morphism of F,g
A3 (*) FG is Element of the carrier' of f
m is Element of the carrier' of C
dom m is Element of the carrier of C
the Source of C . m is Element of the carrier of C
dom FG is Element of the carrier of f
the Source of f . FG is Element of the carrier of f
G is Element of the carrier of C
cod m is Element of the carrier of C
the Target of C . m is Element of the carrier of C
cod FG is Element of the carrier of f
the Target of f . FG is Element of the carrier of f
Hom (G,A1) is Element of bool the carrier' of C
bool the carrier' of C is non empty set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = G & cod b1 = A1 ) } is set
g1 is Morphism of G,A1
cod g1 is Element of the carrier of C
the Target of C . g1 is Element of the carrier of C
dom A3 is Element of the carrier of f
the Source of f . A3 is Element of the carrier of f
the Comp of f . (A3,FG) is set
[A3,FG] is V18() set
{A3,FG} is non empty set
{A3} is non empty set
{{A3,FG},{A3}} is non empty set
the Comp of f . [A3,FG] is set
the Comp of C . ((id A1),g1) is set
[(id A1),g1] is V18() set
{(id A1),g1} is non empty set
{(id A1)} is non empty set
{{(id A1),g1},{(id A1)}} is non empty set
the Comp of C . [(id A1),g1] is set
(id A1) (*) g1 is Element of the carrier' of C
C is non empty non void V58() 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 Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like V21( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is non empty Relation-like set
bool [: the carrier' of C, 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 V21( the carrier' of C, the carrier of C) 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 non empty Relation-like set
[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is non empty Relation-like set
bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is non empty set
CatStr(# the carrier of C, the carrier' of C, the Source of C, the Target of C, the Comp of C #) is non empty non void V58() strict CatStr
f is non empty non void V58() Category-like transitive associative reflexive with_identities CatStr
the carrier of f is non empty set
the carrier' of f is non empty set
the Source of f is Relation-like the carrier' of f -defined the carrier of f -valued Function-like V21( the carrier' of f, the carrier of f) Element of bool [: the carrier' of f, the carrier of f:]
[: the carrier' of f, the carrier of f:] is non empty Relation-like set
bool [: the carrier' of f, the carrier of f:] is non empty set
the Target of f is Relation-like the carrier' of f -defined the carrier of f -valued Function-like V21( the carrier' of f, the carrier of f) Element of bool [: the carrier' of f, the carrier of f:]
the Comp of f is Relation-like [: the carrier' of f, the carrier' of f:] -defined the carrier' of f -valued Function-like Element of bool [:[: the carrier' of f, the carrier' of f:], the carrier' of f:]
[: the carrier' of f, the carrier' of f:] is non empty Relation-like set
[:[: the carrier' of f, the carrier' of f:], the carrier' of f:] is non empty Relation-like set
bool [:[: the carrier' of f, the carrier' of f:], the carrier' of f:] is non empty set
CatStr(# the carrier of f, the carrier' of f, the Source of f, the Target of f, the Comp of f #) is non empty non void V58() strict CatStr
g is Element of the carrier of C
id g is Morphism of g,g
A1 is Element of the carrier of f
id A1 is Morphism of A1,A1
A2 is Element of the carrier' of f
cod A2 is Element of the carrier of f
the Target of f . A2 is Element of the carrier of f
cod (id g) is Element of the carrier of C
the Target of C . (id g) is Element of the carrier of C
dom A2 is Element of the carrier of f
the Source of f . A2 is Element of the carrier of f
dom (id g) is Element of the carrier of C
the Source of C . (id g) is Element of the carrier of C
A3 is Morphism of A1,A1
F is Element of the carrier of f
Hom (A1,F) is Element of bool the carrier' of f
bool the carrier' of f is non empty set
{ b1 where b1 is Element of the carrier' of f : ( dom b1 = A1 & cod b1 = F ) } is set
Hom (F,A1) is Element of bool the carrier' of f
{ b1 where b1 is Element of the carrier' of f : ( dom b1 = F & cod b1 = A1 ) } is set
FG is Morphism of A1,F
FG (*) A3 is Element of the carrier' of f
m is Element of the carrier' of C
dom m is Element of the carrier of C
the Source of C . m is Element of the carrier of C
dom FG is Element of the carrier of f
the Source of f . FG is Element of the carrier of f
cod A3 is Element of the carrier of f
the Target of f . A3 is Element of the carrier of f
the Comp of f . (FG,A3) is set
[FG,A3] is V18() set
{FG,A3} is non empty set
{FG} is non empty set
{{FG,A3},{FG}} is non empty set
the Comp of f . [FG,A3] is set
the Comp of C . (m,(id g)) is set
[m,(id g)] is V18() set
{m,(id g)} is non empty set
{m} is non empty set
{{m,(id g)},{m}} is non empty set
the Comp of C . [m,(id g)] is set
m (*) (id g) is Element of the carrier' of C
FG is Morphism of F,A1
A3 (*) FG is Element of the carrier' of f
m is Element of the carrier' of C
cod m is Element of the carrier of C
the Target of C . m is Element of the carrier of C
cod FG is Element of the carrier of f
the Target of f . FG is Element of the carrier of f
dom A3 is Element of the carrier of f
the Source of f . A3 is Element of the carrier of f
the Comp of f . (A3,FG) is set
[A3,FG] is V18() set
{A3,FG} is non empty set
{A3} is non empty set
{{A3,FG},{A3}} is non empty set
the Comp of f . [A3,FG] is set
the Comp of C . ((id g),m) is set
[(id g),m] is V18() set
{(id g),m} is non empty set
{(id g)} is non empty set
{{(id g),m},{(id g)}} is non empty set
the Comp of C . [(id g),m] is set
(id g) (*) m is Element of the carrier' of C
0 is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Element of K158()
[0,0] is V18() set
{0,0} is non empty functional set
{0} is non empty functional set
{{0,0},{0}} is non empty set
[[0,0],1] is V18() set
{[0,0],1} is non empty set
{[0,0]} is non empty Relation-like Function-like set
{{[0,0],1},{[0,0]}} is non empty set
1Cat (0,[[0,0],1]) is non empty trivial V52() non void 1 -element V58() trivial' strict Category-like transitive associative reflexive with_identities CatStr
{[[0,0],1]} is non empty Relation-like Function-like set
K262([[0,0],1],0) is Relation-like {[[0,0],1]} -defined {0} -valued Function-like V21({[[0,0],1]},{0}) Element of bool [:{[[0,0],1]},{0}:]
[:{[[0,0],1]},{0}:] is non empty Relation-like set
bool [:{[[0,0],1]},{0}:] is non empty set
K261([[0,0],1],[[0,0],1],[[0,0],1]) is Relation-like [:{[[0,0],1]},{[[0,0],1]}:] -defined {[[0,0],1]} -valued Function-like V21([:{[[0,0],1]},{[[0,0],1]}:],{[[0,0],1]}) Element of bool [:[:{[[0,0],1]},{[[0,0],1]}:],{[[0,0],1]}:]
[:{[[0,0],1]},{[[0,0],1]}:] is non empty Relation-like set
[:[:{[[0,0],1]},{[[0,0],1]}:],{[[0,0],1]}:] is non empty Relation-like set
bool [:[:{[[0,0],1]},{[[0,0],1]}:],{[[0,0],1]}:] is non empty set
CatStr(# {0},{[[0,0],1]},K262([[0,0],1],0),K262([[0,0],1],0),K261([[0,0],1],[[0,0],1],[[0,0],1]) #) is non empty non void V58() strict CatStr
C is non empty trivial V52() non void 1 -element V58() trivial' strict Category-like transitive associative reflexive with_identities CatStr
the carrier' of C is non empty trivial set
f is Element of the carrier' of C
the carrier of C is non empty trivial V34() set
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 V21( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is non empty Relation-like set
bool [: the carrier' of C, the carrier of C:] is non empty set
the Source of C . f is Element of the carrier of C
cod 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 V21( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
the Target of C . f is Element of the carrier of C
[(dom f),(cod f)] is V18() Element of [: the carrier of C, the carrier of C:]
[: the carrier of C, the carrier of C:] is non empty Relation-like set
{(dom f),(cod f)} is non empty set
{(dom f)} is non empty set
{{(dom f),(cod f)},{(dom f)}} is non empty set
[[(dom f),(cod f)],1] is V18() set
{[(dom f),(cod f)],1} is non empty set
{[(dom f),(cod f)]} is non empty Relation-like Function-like set
{{[(dom f),(cod f)],1},{[(dom f),(cod f)]}} is non empty set
C is non empty non void V58() () CatStr
the carrier' of C is non empty set
the carrier of C is non empty set
f is Element of the carrier' of C
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 V21( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is non empty Relation-like set
bool [: the carrier' of C, the carrier of C:] is non empty set
the Source of C . f is Element of the carrier of C
f `11 is set
cod 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 V21( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
the Target of C . f is Element of the carrier of C
f `12 is set
[(dom f),(cod f)] is V18() Element of [: the carrier of C, the carrier of C:]
[: the carrier of C, the carrier of C:] is non empty Relation-like set
{(dom f),(cod f)} is non empty set
{(dom f)} is non empty set
{{(dom f),(cod f)},{(dom f)}} is non empty set
f `2 is set
[[(dom f),(cod f)],(f `2)] is V18() set
{[(dom f),(cod f)],(f `2)} is non empty set
{[(dom f),(cod f)]} is non empty Relation-like Function-like set
{{[(dom f),(cod f)],(f `2)},{[(dom f),(cod f)]}} is non empty set
g is set
[[(dom f),(cod f)],g] is V18() set
{[(dom f),(cod f)],g} is non empty set
{{[(dom f),(cod f)],g},{[(dom f),(cod f)]}} is non empty set
C is non empty non void V58() () CatStr
the carrier' of C is non empty set
f is Element of the carrier' of C
f `11 is set
the carrier of C is non empty set
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 V21( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is non empty Relation-like set
bool [: the carrier' of C, the carrier of C:] is non empty set
the Source of C . f is Element of the carrier of C
f `12 is set
cod 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 V21( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is non empty Relation-like set
bool [: the carrier' of C, the carrier of C:] is non empty set
the Target of C . f is Element of the carrier of C
F1() is non empty set
F2() is non empty set
[:F1(),F1():] is non empty Relation-like set
{ [[b1,b2],b3] where b1, b2 is Element of F1(), b3 is Element of F2() : P1[b1,b2,b3] } is set
the Element of F1() is Element of F1()
g is Element of F2()
[ the Element of F1(), the Element of F1()] is V18() Element of [:F1(),F1():]
{ the Element of F1(), the Element of F1()} is non empty set
{ the Element of F1()} is non empty set
{{ the Element of F1(), the Element of F1()},{ the Element of F1()}} is non empty set
[[ the Element of F1(), the Element of F1()],g] is V18() Element of [:[:F1(),F1():],F2():]
[:[:F1(),F1():],F2():] is non empty Relation-like set
{[ the Element of F1(), the Element of F1()],g} is non empty set
{[ the Element of F1(), the Element of F1()]} is non empty Relation-like Function-like set
{{[ the Element of F1(), the Element of F1()],g},{[ the Element of F1(), the Element of F1()]}} is non empty set
A1 is set
A2 is Element of F1()
A3 is Element of F1()
[A2,A3] is V18() Element of [:F1(),F1():]
{A2,A3} is non empty set
{A2} is non empty set
{{A2,A3},{A2}} is non empty set
F is Element of F2()
[[A2,A3],F] is V18() Element of [:[:F1(),F1():],F2():]
{[A2,A3],F} is non empty set
{[A2,A3]} is non empty Relation-like Function-like set
{{[A2,A3],F},{[A2,A3]}} is non empty set
bool [:[:F1(),F1():],F2():] is non empty set
A1 is non empty Relation-like [:F1(),F1():] -defined F2() -valued Element of bool [:[:F1(),F1():],F2():]
A2 is Element of A1
A3 is Element of F1()
F is Element of F1()
[A3,F] is V18() Element of [:F1(),F1():]
{A3,F} is non empty set
{A3} is non empty set
{{A3,F},{A3}} is non empty set
G is Element of F2()
[[A3,F],G] is V18() Element of [:[:F1(),F1():],F2():]
{[A3,F],G} is non empty set
{[A3,F]} is non empty Relation-like Function-like set
{{[A3,F],G},{[A3,F]}} is non empty set
A2 `11 is Element of F1()
A2 `12 is Element of F1()
[(A2 `11),(A2 `12)] is V18() Element of [:F1(),F1():]
{(A2 `11),(A2 `12)} is non empty set
{(A2 `11)} is non empty set
{{(A2 `11),(A2 `12)},{(A2 `11)}} is non empty set
A2 `2 is Element of F2()
[[(A2 `11),(A2 `12)],(A2 `2)] is V18() Element of [:[:F1(),F1():],F2():]
{[(A2 `11),(A2 `12)],(A2 `2)} is non empty set
{[(A2 `11),(A2 `12)]} is non empty Relation-like Function-like set
{{[(A2 `11),(A2 `12)],(A2 `2)},{[(A2 `11),(A2 `12)]}} is non empty set
[:A1,F1():] is non empty Relation-like set
bool [:A1,F1():] is non empty set
A2 is Relation-like A1 -defined F1() -valued Function-like V21(A1,F1()) Element of bool [:A1,F1():]
A3 is Relation-like A1 -defined F1() -valued Function-like V21(A1,F1()) Element of bool [:A1,F1():]
F is set
G is set
F `11 is set
G `12 is set
FG is Element of F1()
m is Element of F1()
[FG,m] is V18() Element of [:F1(),F1():]
{FG,m} is non empty set
{FG} is non empty set
{{FG,m},{FG}} is non empty set
g1 is Element of F2()
[[FG,m],g1] is V18() Element of [:[:F1(),F1():],F2():]
{[FG,m],g1} is non empty set
{[FG,m]} is non empty Relation-like Function-like set
{{[FG,m],g1},{[FG,m]}} is non empty set
a2 is Element of F1()
b2 is Element of F1()
[a2,b2] is V18() Element of [:F1(),F1():]
{a2,b2} is non empty set
{a2} is non empty set
{{a2,b2},{a2}} is non empty set
g2 is Element of F2()
[[a2,b2],g2] is V18() Element of [:[:F1(),F1():],F2():]
{[a2,b2],g2} is non empty set
{[a2,b2]} is non empty Relation-like Function-like set
{{[a2,b2],g2},{[a2,b2]}} is non empty set
F `12 is set
G `11 is set
F `2 is set
G `2 is set
F3(g1,g2) is set
[(G `11),(F `12)] is V18() set
{(G `11),(F `12)} is non empty set
{(G `11)} is non empty set
{{(G `11),(F `12)},{(G `11)}} is non empty set
F3((F `2),(G `2)) is set
[[(G `11),(F `12)],F3((F `2),(G `2))] is V18() set
{[(G `11),(F `12)],F3((F `2),(G `2))} is non empty set
{[(G `11),(F `12)]} is non empty Relation-like Function-like set
{{[(G `11),(F `12)],F3((F `2),(G `2))},{[(G `11),(F `12)]}} is non empty set
[:A1,A1:] is non empty Relation-like [:[:F1(),F1():],F2():] -defined [:[:F1(),F1():],F2():] -valued Element of bool [:[:[:F1(),F1():],F2():],[:[:F1(),F1():],F2():]:]
[:[:[:F1(),F1():],F2():],[:[:F1(),F1():],F2():]:] is non empty Relation-like set
bool [:[:[:F1(),F1():],F2():],[:[:F1(),F1():],F2():]:] is non empty set
[:[:A1,A1:],A1:] is non empty Relation-like set
bool [:[:A1,A1:],A1:] is non empty set
F is Relation-like [:A1,A1:] -defined A1 -valued Function-like Element of bool [:[:A1,A1:],A1:]
dom F is Relation-like [:[:F1(),F1():],F2():] -defined [:[:F1(),F1():],F2():] -valued Element of bool [:A1,A1:]
bool [:A1,A1:] is non empty set
G is Element of F1()
FG is Element of F2()
[G,G] is V18() Element of [:F1(),F1():]
{G,G} is non empty set
{G} is non empty set
{{G,G},{G}} is non empty set
[[G,G],FG] is V18() Element of [:[:F1(),F1():],F2():]
{[G,G],FG} is non empty set
{[G,G]} is non empty Relation-like Function-like set
{{[G,G],FG},{[G,G]}} is non empty set
m is Element of A1
g1 is Element of A1
[:F1(),A1:] is non empty Relation-like set
bool [:F1(),A1:] is non empty set
G is Relation-like F1() -defined A1 -valued Function-like V21(F1(),A1) Element of bool [:F1(),A1:]
CatStr(# F1(),A1,A2,A3,F #) is non empty non void V58() strict CatStr
the carrier' of CatStr(# F1(),A1,A2,A3,F #) is non empty set
g1 is Element of the carrier' of CatStr(# F1(),A1,A2,A3,F #)
m is Element of the carrier' of CatStr(# F1(),A1,A2,A3,F #)
[g1,m] is V18() Element of [: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier' of CatStr(# F1(),A1,A2,A3,F #):]
[: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier' of CatStr(# F1(),A1,A2,A3,F #):] is non empty Relation-like set
{g1,m} is non empty set
{g1} is non empty set
{{g1,m},{g1}} is non empty set
g1 `11 is set
m `12 is set
A2 . g1 is set
the Comp of CatStr(# F1(),A1,A2,A3,F #) is Relation-like [: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier' of CatStr(# F1(),A1,A2,A3,F #):] -defined the carrier' of CatStr(# F1(),A1,A2,A3,F #) -valued Function-like Element of bool [:[: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier' of CatStr(# F1(),A1,A2,A3,F #):], the carrier' of CatStr(# F1(),A1,A2,A3,F #):]
[:[: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier' of CatStr(# F1(),A1,A2,A3,F #):], the carrier' of CatStr(# F1(),A1,A2,A3,F #):] is non empty Relation-like set
bool [:[: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier' of CatStr(# F1(),A1,A2,A3,F #):], the carrier' of CatStr(# F1(),A1,A2,A3,F #):] is non empty set
dom the Comp of CatStr(# F1(),A1,A2,A3,F #) is Relation-like the carrier' of CatStr(# F1(),A1,A2,A3,F #) -defined the carrier' of CatStr(# F1(),A1,A2,A3,F #) -valued Element of bool [: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier' of CatStr(# F1(),A1,A2,A3,F #):]
bool [: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier' of CatStr(# F1(),A1,A2,A3,F #):] is non empty set
dom g1 is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
the carrier of CatStr(# F1(),A1,A2,A3,F #) is non empty set
the Source of CatStr(# F1(),A1,A2,A3,F #) is Relation-like the carrier' of CatStr(# F1(),A1,A2,A3,F #) -defined the carrier of CatStr(# F1(),A1,A2,A3,F #) -valued Function-like V21( the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #)) Element of bool [: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #):]
[: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #):] is non empty Relation-like set
bool [: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #):] is non empty set
the Source of CatStr(# F1(),A1,A2,A3,F #) . g1 is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
cod m is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
the Target of CatStr(# F1(),A1,A2,A3,F #) is Relation-like the carrier' of CatStr(# F1(),A1,A2,A3,F #) -defined the carrier of CatStr(# F1(),A1,A2,A3,F #) -valued Function-like V21( the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #)) Element of bool [: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #):]
the Target of CatStr(# F1(),A1,A2,A3,F #) . m is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
the carrier' of CatStr(# F1(),A1,A2,A3,F #) is non empty set
[: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier' of CatStr(# F1(),A1,A2,A3,F #):] is non empty Relation-like set
the Comp of CatStr(# F1(),A1,A2,A3,F #) is Relation-like [: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier' of CatStr(# F1(),A1,A2,A3,F #):] -defined the carrier' of CatStr(# F1(),A1,A2,A3,F #) -valued Function-like Element of bool [:[: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier' of CatStr(# F1(),A1,A2,A3,F #):], the carrier' of CatStr(# F1(),A1,A2,A3,F #):]
[:[: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier' of CatStr(# F1(),A1,A2,A3,F #):], the carrier' of CatStr(# F1(),A1,A2,A3,F #):] is non empty Relation-like set
bool [:[: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier' of CatStr(# F1(),A1,A2,A3,F #):], the carrier' of CatStr(# F1(),A1,A2,A3,F #):] is non empty set
dom the Comp of CatStr(# F1(),A1,A2,A3,F #) is Relation-like the carrier' of CatStr(# F1(),A1,A2,A3,F #) -defined the carrier' of CatStr(# F1(),A1,A2,A3,F #) -valued Element of bool [: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier' of CatStr(# F1(),A1,A2,A3,F #):]
bool [: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier' of CatStr(# F1(),A1,A2,A3,F #):] is non empty set
g1 is Element of the carrier' of CatStr(# F1(),A1,A2,A3,F #)
m is Element of the carrier' of CatStr(# F1(),A1,A2,A3,F #)
[g1,m] is V18() Element of [: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier' of CatStr(# F1(),A1,A2,A3,F #):]
{g1,m} is non empty set
{g1} is non empty set
{{g1,m},{g1}} is non empty set
dom g1 is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
the carrier of CatStr(# F1(),A1,A2,A3,F #) is non empty set
the Source of CatStr(# F1(),A1,A2,A3,F #) is Relation-like the carrier' of CatStr(# F1(),A1,A2,A3,F #) -defined the carrier of CatStr(# F1(),A1,A2,A3,F #) -valued Function-like V21( the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #)) Element of bool [: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #):]
[: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #):] is non empty Relation-like set
bool [: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #):] is non empty set
the Source of CatStr(# F1(),A1,A2,A3,F #) . g1 is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
cod m is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
the Target of CatStr(# F1(),A1,A2,A3,F #) is Relation-like the carrier' of CatStr(# F1(),A1,A2,A3,F #) -defined the carrier of CatStr(# F1(),A1,A2,A3,F #) -valued Function-like V21( the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #)) Element of bool [: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #):]
the Target of CatStr(# F1(),A1,A2,A3,F #) . m is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
b2 is Element of the carrier' of CatStr(# F1(),A1,A2,A3,F #)
dom b2 is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
the Source of CatStr(# F1(),A1,A2,A3,F #) . b2 is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
a2 is Element of the carrier' of CatStr(# F1(),A1,A2,A3,F #)
cod a2 is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
the Target of CatStr(# F1(),A1,A2,A3,F #) . a2 is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
[b2,a2] is V18() Element of [: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier' of CatStr(# F1(),A1,A2,A3,F #):]
{b2,a2} is non empty set
{b2} is non empty set
{{b2,a2},{b2}} is non empty set
g1 is Element of the carrier' of CatStr(# F1(),A1,A2,A3,F #)
dom g1 is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
the carrier of CatStr(# F1(),A1,A2,A3,F #) is non empty set
the Source of CatStr(# F1(),A1,A2,A3,F #) is Relation-like the carrier' of CatStr(# F1(),A1,A2,A3,F #) -defined the carrier of CatStr(# F1(),A1,A2,A3,F #) -valued Function-like V21( the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #)) Element of bool [: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #):]
[: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #):] is non empty Relation-like set
bool [: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #):] is non empty set
the Source of CatStr(# F1(),A1,A2,A3,F #) . g1 is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
m is Element of the carrier' of CatStr(# F1(),A1,A2,A3,F #)
cod m is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
the Target of CatStr(# F1(),A1,A2,A3,F #) is Relation-like the carrier' of CatStr(# F1(),A1,A2,A3,F #) -defined the carrier of CatStr(# F1(),A1,A2,A3,F #) -valued Function-like V21( the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #)) Element of bool [: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #):]
the Target of CatStr(# F1(),A1,A2,A3,F #) . m is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
g1 (*) m is Element of the carrier' of CatStr(# F1(),A1,A2,A3,F #)
dom (g1 (*) m) is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
the Source of CatStr(# F1(),A1,A2,A3,F #) . (g1 (*) m) is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
dom m is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
the Source of CatStr(# F1(),A1,A2,A3,F #) . m is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
cod (g1 (*) m) is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
the Target of CatStr(# F1(),A1,A2,A3,F #) . (g1 (*) m) is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
cod g1 is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
the Target of CatStr(# F1(),A1,A2,A3,F #) . g1 is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
m `11 is set
g1 `11 is set
m `12 is set
g1 `12 is set
F . (g1,m) is set
[g1,m] is V18() set
{g1,m} is non empty set
{g1} is non empty set
{{g1,m},{g1}} is non empty set
F . [g1,m] is set
[(m `11),(g1 `12)] is V18() set
{(m `11),(g1 `12)} is non empty set
{(m `11)} is non empty set
{{(m `11),(g1 `12)},{(m `11)}} is non empty set
g1 `2 is set
m `2 is set
F3((g1 `2),(m `2)) is set
[[(m `11),(g1 `12)],F3((g1 `2),(m `2))] is V18() set
{[(m `11),(g1 `12)],F3((g1 `2),(m `2))} is non empty set
{[(m `11),(g1 `12)]} is non empty Relation-like Function-like set
{{[(m `11),(g1 `12)],F3((g1 `2),(m `2))},{[(m `11),(g1 `12)]}} is non empty set
[g1,m] is V18() Element of [: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier' of CatStr(# F1(),A1,A2,A3,F #):]
F . [g1,m] is set
(F . [g1,m]) `11 is set
the Comp of CatStr(# F1(),A1,A2,A3,F #) . (g1,m) is set
the Comp of CatStr(# F1(),A1,A2,A3,F #) . [g1,m] is set
(F . [g1,m]) `12 is set
a2 is Element of the carrier' of CatStr(# F1(),A1,A2,A3,F #)
dom a2 is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
the carrier of CatStr(# F1(),A1,A2,A3,F #) is non empty set
the Source of CatStr(# F1(),A1,A2,A3,F #) is Relation-like the carrier' of CatStr(# F1(),A1,A2,A3,F #) -defined the carrier of CatStr(# F1(),A1,A2,A3,F #) -valued Function-like V21( the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #)) Element of bool [: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #):]
[: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #):] is non empty Relation-like set
bool [: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #):] is non empty set
the Source of CatStr(# F1(),A1,A2,A3,F #) . a2 is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
g1 is Element of the carrier' of CatStr(# F1(),A1,A2,A3,F #)
cod g1 is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
the Target of CatStr(# F1(),A1,A2,A3,F #) is Relation-like the carrier' of CatStr(# F1(),A1,A2,A3,F #) -defined the carrier of CatStr(# F1(),A1,A2,A3,F #) -valued Function-like V21( the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #)) Element of bool [: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #):]
the Target of CatStr(# F1(),A1,A2,A3,F #) . g1 is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
dom g1 is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
the Source of CatStr(# F1(),A1,A2,A3,F #) . g1 is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
m is Element of the carrier' of CatStr(# F1(),A1,A2,A3,F #)
cod m is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
the Target of CatStr(# F1(),A1,A2,A3,F #) . m is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
g1 (*) m is Element of the carrier' of CatStr(# F1(),A1,A2,A3,F #)
a2 (*) (g1 (*) m) is Element of the carrier' of CatStr(# F1(),A1,A2,A3,F #)
a2 (*) g1 is Element of the carrier' of CatStr(# F1(),A1,A2,A3,F #)
(a2 (*) g1) (*) m is Element of the carrier' of CatStr(# F1(),A1,A2,A3,F #)
g1 `11 is set
a2 `11 is set
m `12 is set
g1 `12 is set
[g1,m] is V18() Element of [: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier' of CatStr(# F1(),A1,A2,A3,F #):]
{g1,m} is non empty set
{g1} is non empty set
{{g1,m},{g1}} is non empty set
[a2,g1] is V18() Element of [: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier' of CatStr(# F1(),A1,A2,A3,F #):]
{a2,g1} is non empty set
{a2} is non empty set
{{a2,g1},{a2}} is non empty set
F . [g1,m] is set
rng F is Relation-like [:F1(),F1():] -defined F2() -valued Element of bool A1
bool A1 is non empty set
F . [a2,g1] is set
F . (g1,m) is set
[g1,m] is V18() set
F . [g1,m] is set
F . (a2,g1) is set
[a2,g1] is V18() set
F . [a2,g1] is set
b2 is Element of A1
m `11 is set
[(m `11),(g1 `12)] is V18() set
{(m `11),(g1 `12)} is non empty set
{(m `11)} is non empty set
{{(m `11),(g1 `12)},{(m `11)}} is non empty set
g1 `2 is set
m `2 is set
F3((g1 `2),(m `2)) is set
[[(m `11),(g1 `12)],F3((g1 `2),(m `2))] is V18() set
{[(m `11),(g1 `12)],F3((g1 `2),(m `2))} is non empty set
{[(m `11),(g1 `12)]} is non empty Relation-like Function-like set
{{[(m `11),(g1 `12)],F3((g1 `2),(m `2))},{[(m `11),(g1 `12)]}} is non empty set
g2 is Element of A1
a2 `12 is set
[(g1 `11),(a2 `12)] is V18() set
{(g1 `11),(a2 `12)} is non empty set
{(g1 `11)} is non empty set
{{(g1 `11),(a2 `12)},{(g1 `11)}} is non empty set
a2 `2 is set
F3((a2 `2),(g1 `2)) is set
[[(g1 `11),(a2 `12)],F3((a2 `2),(g1 `2))] is V18() set
{[(g1 `11),(a2 `12)],F3((a2 `2),(g1 `2))} is non empty set
{[(g1 `11),(a2 `12)]} is non empty Relation-like Function-like set
{{[(g1 `11),(a2 `12)],F3((a2 `2),(g1 `2))},{[(g1 `11),(a2 `12)]}} is non empty set
A2 . b2 is Element of F1()
b2 `11 is Element of F1()
A2 . g2 is Element of F1()
g2 `11 is Element of F1()
A3 . b2 is Element of F1()
b2 `12 is Element of F1()
A3 . g2 is Element of F1()
g2 `12 is Element of F1()
[a2,b2] is V18() Element of [: the carrier' of CatStr(# F1(),A1,A2,A3,F #),A1:]
[: the carrier' of CatStr(# F1(),A1,A2,A3,F #),A1:] is non empty Relation-like set
{a2,b2} is non empty set
{{a2,b2},{a2}} is non empty set
[g2,m] is V18() Element of [:A1, the carrier' of CatStr(# F1(),A1,A2,A3,F #):]
[:A1, the carrier' of CatStr(# F1(),A1,A2,A3,F #):] is non empty Relation-like set
{g2,m} is non empty set
{g2} is non empty set
{{g2,m},{g2}} is non empty set
ha1 is Element of A1
ha1 `11 is Element of F1()
ha1 `12 is Element of F1()
ha1 `2 is Element of F2()
ha2 is Element of A1
ha2 `11 is Element of F1()
ha2 `12 is Element of F1()
ha2 `2 is Element of F2()
hb1 is Element of A1
hb1 `11 is Element of F1()
hb1 `12 is Element of F1()
hb1 `2 is Element of F2()
the Comp of CatStr(# F1(),A1,A2,A3,F #) . (a2,g1) is set
the Comp of CatStr(# F1(),A1,A2,A3,F #) . [a2,g1] is set
dom (a2 (*) g1) is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
the Source of CatStr(# F1(),A1,A2,A3,F #) . (a2 (*) g1) is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
the Comp of CatStr(# F1(),A1,A2,A3,F #) . (g1,m) is set
the Comp of CatStr(# F1(),A1,A2,A3,F #) . [g1,m] is set
cod (g1 (*) m) is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
the Target of CatStr(# F1(),A1,A2,A3,F #) . (g1 (*) m) is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
the Comp of CatStr(# F1(),A1,A2,A3,F #) . (a2,( the Comp of CatStr(# F1(),A1,A2,A3,F #) . (g1,m))) is set
[a2,( the Comp of CatStr(# F1(),A1,A2,A3,F #) . (g1,m))] is V18() set
{a2,( the Comp of CatStr(# F1(),A1,A2,A3,F #) . (g1,m))} is non empty set
{{a2,( the Comp of CatStr(# F1(),A1,A2,A3,F #) . (g1,m))},{a2}} is non empty set
the Comp of CatStr(# F1(),A1,A2,A3,F #) . [a2,( the Comp of CatStr(# F1(),A1,A2,A3,F #) . (g1,m))] is set
[(m `11),(a2 `12)] is V18() set
{(m `11),(a2 `12)} is non empty set
{{(m `11),(a2 `12)},{(m `11)}} is non empty set
b2 `2 is Element of F2()
F3((a2 `2),(b2 `2)) is set
[[(m `11),(a2 `12)],F3((a2 `2),(b2 `2))] is V18() set
{[(m `11),(a2 `12)],F3((a2 `2),(b2 `2))} is non empty set
{[(m `11),(a2 `12)]} is non empty Relation-like Function-like set
{{[(m `11),(a2 `12)],F3((a2 `2),(b2 `2))},{[(m `11),(a2 `12)]}} is non empty set
F3((ha2 `2),(ha1 `2)) is set
F3((hb1 `2),F3((ha2 `2),(ha1 `2))) is set
[[(m `11),(a2 `12)],F3((hb1 `2),F3((ha2 `2),(ha1 `2)))] is V18() set
{[(m `11),(a2 `12)],F3((hb1 `2),F3((ha2 `2),(ha1 `2)))} is non empty set
{{[(m `11),(a2 `12)],F3((hb1 `2),F3((ha2 `2),(ha1 `2)))},{[(m `11),(a2 `12)]}} is non empty set
F3((hb1 `2),(ha2 `2)) is set
F3(F3((hb1 `2),(ha2 `2)),(ha1 `2)) is set
[[(m `11),(a2 `12)],F3(F3((hb1 `2),(ha2 `2)),(ha1 `2))] is V18() set
{[(m `11),(a2 `12)],F3(F3((hb1 `2),(ha2 `2)),(ha1 `2))} is non empty set
{{[(m `11),(a2 `12)],F3(F3((hb1 `2),(ha2 `2)),(ha1 `2))},{[(m `11),(a2 `12)]}} is non empty set
g2 `2 is Element of F2()
F3((g2 `2),(m `2)) is set
[[(m `11),(a2 `12)],F3((g2 `2),(m `2))] is V18() set
{[(m `11),(a2 `12)],F3((g2 `2),(m `2))} is non empty set
{{[(m `11),(a2 `12)],F3((g2 `2),(m `2))},{[(m `11),(a2 `12)]}} is non empty set
the Comp of CatStr(# F1(),A1,A2,A3,F #) . (( the Comp of CatStr(# F1(),A1,A2,A3,F #) . (a2,g1)),m) is set
[( the Comp of CatStr(# F1(),A1,A2,A3,F #) . (a2,g1)),m] is V18() set
{( the Comp of CatStr(# F1(),A1,A2,A3,F #) . (a2,g1)),m} is non empty set
{( the Comp of CatStr(# F1(),A1,A2,A3,F #) . (a2,g1))} is non empty set
{{( the Comp of CatStr(# F1(),A1,A2,A3,F #) . (a2,g1)),m},{( the Comp of CatStr(# F1(),A1,A2,A3,F #) . (a2,g1))}} is non empty set
the Comp of CatStr(# F1(),A1,A2,A3,F #) . [( the Comp of CatStr(# F1(),A1,A2,A3,F #) . (a2,g1)),m] is set
the carrier of CatStr(# F1(),A1,A2,A3,F #) is non empty set
m is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
Hom (m,m) is Element of bool the carrier' of CatStr(# F1(),A1,A2,A3,F #)
bool the carrier' of CatStr(# F1(),A1,A2,A3,F #) is non empty set
{ b1 where b1 is Element of the carrier' of CatStr(# F1(),A1,A2,A3,F #) : ( dom b1 = m & cod b1 = m ) } is set
G . m is set
[: the carrier of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #):] is non empty Relation-like set
[m,m] is V18() Element of [: the carrier of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #):]
{m,m} is non empty set
{m} is non empty set
{{m,m},{m}} is non empty set
g1 is Element of F2()
[[m,m],g1] is V18() Element of [:[: the carrier of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #):],F2():]
[:[: the carrier of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #):],F2():] is non empty Relation-like set
{[m,m],g1} is non empty set
{[m,m]} is non empty Relation-like Function-like set
{{[m,m],g1},{[m,m]}} is non empty set
a2 is Element of F1()
G . a2 is Element of A1
g2 is Element of the carrier' of CatStr(# F1(),A1,A2,A3,F #)
cod g2 is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
the Target of CatStr(# F1(),A1,A2,A3,F #) is Relation-like the carrier' of CatStr(# F1(),A1,A2,A3,F #) -defined the carrier of CatStr(# F1(),A1,A2,A3,F #) -valued Function-like V21( the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #)) Element of bool [: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #):]
[: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #):] is non empty Relation-like set
bool [: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #):] is non empty set
the Target of CatStr(# F1(),A1,A2,A3,F #) . g2 is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
(G . m) `12 is set
dom g2 is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
the Source of CatStr(# F1(),A1,A2,A3,F #) is Relation-like the carrier' of CatStr(# F1(),A1,A2,A3,F #) -defined the carrier of CatStr(# F1(),A1,A2,A3,F #) -valued Function-like V21( the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #)) Element of bool [: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #):]
the Source of CatStr(# F1(),A1,A2,A3,F #) . g2 is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
(G . m) `11 is set
the carrier of CatStr(# F1(),A1,A2,A3,F #) is non empty set
m is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
G . m is set
[: the carrier of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #):] is non empty Relation-like set
[m,m] is V18() Element of [: the carrier of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #):]
{m,m} is non empty set
{m} is non empty set
{{m,m},{m}} is non empty set
g1 is Element of F2()
[[m,m],g1] is V18() Element of [:[: the carrier of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #):],F2():]
[:[: the carrier of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #):],F2():] is non empty Relation-like set
{[m,m],g1} is non empty set
{[m,m]} is non empty Relation-like Function-like set
{{[m,m],g1},{[m,m]}} is non empty set
a2 is Element of F1()
G . a2 is Element of A1
g2 is Element of the carrier' of CatStr(# F1(),A1,A2,A3,F #)
cod g2 is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
the Target of CatStr(# F1(),A1,A2,A3,F #) is Relation-like the carrier' of CatStr(# F1(),A1,A2,A3,F #) -defined the carrier of CatStr(# F1(),A1,A2,A3,F #) -valued Function-like V21( the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #)) Element of bool [: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #):]
[: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #):] is non empty Relation-like set
bool [: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #):] is non empty set
the Target of CatStr(# F1(),A1,A2,A3,F #) . g2 is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
(G . m) `12 is set
dom g2 is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
the Source of CatStr(# F1(),A1,A2,A3,F #) is Relation-like the carrier' of CatStr(# F1(),A1,A2,A3,F #) -defined the carrier of CatStr(# F1(),A1,A2,A3,F #) -valued Function-like V21( the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #)) Element of bool [: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier of CatStr(# F1(),A1,A2,A3,F #):]
the Source of CatStr(# F1(),A1,A2,A3,F #) . g2 is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
(G . m) `11 is set
ha1 is Morphism of m,m
ha2 is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
Hom (m,ha2) is Element of bool the carrier' of CatStr(# F1(),A1,A2,A3,F #)
bool the carrier' of CatStr(# F1(),A1,A2,A3,F #) is non empty set
{ b1 where b1 is Element of the carrier' of CatStr(# F1(),A1,A2,A3,F #) : ( dom b1 = m & cod b1 = ha2 ) } is set
Hom (ha2,m) is Element of bool the carrier' of CatStr(# F1(),A1,A2,A3,F #)
{ b1 where b1 is Element of the carrier' of CatStr(# F1(),A1,A2,A3,F #) : ( dom b1 = ha2 & cod b1 = m ) } is set
hb1 is Morphism of m,ha2
hb1 (*) ha1 is Element of the carrier' of CatStr(# F1(),A1,A2,A3,F #)
C is Element of F1()
F is Element of F1()
[C,F] is V18() Element of [:F1(),F1():]
{C,F} is non empty set
{C} is non empty set
{{C,F},{C}} is non empty set
G is Element of F2()
[[C,F],G] is V18() Element of [:[:F1(),F1():],F2():]
{[C,F],G} is non empty set
{[C,F]} is non empty Relation-like Function-like set
{{[C,F],G},{[C,F]}} is non empty set
dom hb1 is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
the Source of CatStr(# F1(),A1,A2,A3,F #) . hb1 is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
A2 . hb1 is set
[[C,F],G] `11 is Element of F1()
F3(G,g1) is set
[[m,m],g1] `11 is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
[[m,m],g1] `2 is Element of F2()
[[C,F],G] `12 is Element of F1()
[[C,F],G] `2 is Element of F2()
hb1 `11 is set
[[m,m],g1] `12 is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
ha1 `12 is set
[hb1,ha1] is V18() Element of [: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier' of CatStr(# F1(),A1,A2,A3,F #):]
{hb1,ha1} is non empty set
{hb1} is non empty set
{{hb1,ha1},{hb1}} is non empty set
the Comp of CatStr(# F1(),A1,A2,A3,F #) . (hb1,ha1) is set
[hb1,ha1] is V18() set
the Comp of CatStr(# F1(),A1,A2,A3,F #) . [hb1,ha1] is set
F . (hb1,ha1) is set
F . [hb1,ha1] is set
ha1 `11 is set
hb1 `12 is set
[(ha1 `11),(hb1 `12)] is V18() set
{(ha1 `11),(hb1 `12)} is non empty set
{(ha1 `11)} is non empty set
{{(ha1 `11),(hb1 `12)},{(ha1 `11)}} is non empty set
hb1 `2 is set
ha1 `2 is set
F3((hb1 `2),(ha1 `2)) is set
[[(ha1 `11),(hb1 `12)],F3((hb1 `2),(ha1 `2))] is V18() set
{[(ha1 `11),(hb1 `12)],F3((hb1 `2),(ha1 `2))} is non empty set
{[(ha1 `11),(hb1 `12)]} is non empty Relation-like Function-like set
{{[(ha1 `11),(hb1 `12)],F3((hb1 `2),(ha1 `2))},{[(ha1 `11),(hb1 `12)]}} is non empty set
hb1 is Morphism of ha2,m
ha1 (*) hb1 is Element of the carrier' of CatStr(# F1(),A1,A2,A3,F #)
C is Element of F1()
F is Element of F1()
[C,F] is V18() Element of [:F1(),F1():]
{C,F} is non empty set
{C} is non empty set
{{C,F},{C}} is non empty set
G is Element of F2()
[[C,F],G] is V18() Element of [:[:F1(),F1():],F2():]
{[C,F],G} is non empty set
{[C,F]} is non empty Relation-like Function-like set
{{[C,F],G},{[C,F]}} is non empty set
cod hb1 is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
the Target of CatStr(# F1(),A1,A2,A3,F #) . hb1 is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
A3 . hb1 is set
[[C,F],G] `12 is Element of F1()
F3(g1,G) is set
[[m,m],g1] `12 is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
[[m,m],g1] `2 is Element of F2()
[[C,F],G] `11 is Element of F1()
[[C,F],G] `2 is Element of F2()
hb1 `12 is set
[[m,m],g1] `11 is Element of the carrier of CatStr(# F1(),A1,A2,A3,F #)
ha1 `11 is set
[ha1,hb1] is V18() Element of [: the carrier' of CatStr(# F1(),A1,A2,A3,F #), the carrier' of CatStr(# F1(),A1,A2,A3,F #):]
{ha1,hb1} is non empty set
{ha1} is non empty set
{{ha1,hb1},{ha1}} is non empty set
the Comp of CatStr(# F1(),A1,A2,A3,F #) . (ha1,hb1) is set
[ha1,hb1] is V18() set
the Comp of CatStr(# F1(),A1,A2,A3,F #) . [ha1,hb1] is set
F . (ha1