:: NATTRA_1 semantic presentation

K149() is Element of bool K145()
K145() is set
bool K145() is non empty set

1 is non empty set
{{},1} is non empty finite set
K144() is set
bool K144() is non empty set
bool K149() is non empty set
A is set
B is non empty set
[:A,B:] is Relation-like set
bool [:A,B:] is non empty set
bool A is non empty set

AB is Element of bool A
OA | AB is Relation-like AB -defined A -defined B -valued set
[:AB,B:] is Relation-like set
bool [:AB,B:] is non empty set
A is non empty set
B is non empty set
[:A,B:] is Relation-like non empty set
OA is non empty set
[:OA,A:] is Relation-like non empty set
bool [:OA,A:] is non empty set
bool OA is non empty set
AB is non empty set
[:AB,B:] is Relation-like non empty set
bool [:AB,B:] is non empty set
bool AB is non empty set
[:OA,AB:] is Relation-like non empty set

[:MA,MB:] is Relation-like [:OA,AB:] -defined [:A,B:] -valued Function-like quasi_total Element of bool [:[:OA,AB:],[:A,B:]:]
[:[:OA,AB:],[:A,B:]:] is Relation-like non empty set
bool [:[:OA,AB:],[:A,B:]:] is non empty set
OB is non empty Element of bool OA
(OA,A,MA,OB) is Relation-like OB -defined OA -defined A -valued Function-like quasi_total Element of bool [:OB,A:]
[:OB,A:] is Relation-like non empty set
bool [:OB,A:] is non empty set
MB is non empty Element of bool AB
[:OB,MB:] is Relation-like OA -defined AB -valued non empty Element of bool [:OA,AB:]
bool [:OA,AB:] is non empty set
([:OA,AB:],[:A,B:],[:MA,MB:],[:OB,MB:]) is Relation-like [:OB,MB:] -defined [:OA,AB:] -defined [:A,B:] -valued Function-like quasi_total Element of bool [:[:OB,MB:],[:A,B:]:]
[:[:OB,MB:],[:A,B:]:] is Relation-like non empty set
bool [:[:OB,MB:],[:A,B:]:] is non empty set
(AB,B,MB,MB) is Relation-like MB -defined AB -defined B -valued Function-like quasi_total Element of bool [:MB,B:]
[:MB,B:] is Relation-like non empty set
bool [:MB,B:] is non empty set
[:(OA,A,MA,OB),(AB,B,MB,MB):] is Relation-like [:OB,MB:] -defined [:A,B:] -valued Function-like quasi_total Element of bool [:[:OB,MB:],[:A,B:]:]
[:OB,MB:] is Relation-like non empty set
[:[:OB,MB:],[:A,B:]:] is Relation-like non empty set
bool [:[:OB,MB:],[:A,B:]:] is non empty set
MA is Element of [:OB,MB:]
a is Element of OB
b is Element of MB
[a,b] is non empty V15() set
{a,b} is non empty finite set
{a} is non empty trivial finite set
{{a,b},{a}} is non empty finite V35() set
(AB,B,MB,MB) . b is Element of B
MB . b is Element of B
(OA,A,MA,OB) . a is Element of A
MA . a is Element of A
[:(OA,A,MA,OB),(AB,B,MB,MB):] . MA is Element of [:A,B:]
[:(OA,A,MA,OB),(AB,B,MB,MB):] . (a,b) is Element of [:A,B:]
[:(OA,A,MA,OB),(AB,B,MB,MB):] . [a,b] is set
[(MA . a),(MB . b)] is non empty V15() set
{(MA . a),(MB . b)} is non empty finite set
{(MA . a)} is non empty trivial finite set
{{(MA . a),(MB . b)},{(MA . a)}} is non empty finite V35() set
[:MA,MB:] . (a,b) is Element of [:A,B:]
[:MA,MB:] . [a,b] is set
([:OA,AB:],[:A,B:],[:MA,MB:],[:OB,MB:]) . MA is Element of [:A,B:]
A is non empty set
bool A is non empty set
B is non empty set
bool B is non empty set
OA is non empty Element of bool A
[:OA,OA:] is Relation-like A -defined A -valued non empty Element of bool [:A,A:]
[:A,A:] is Relation-like non empty set
bool [:A,A:] is non empty set
[:[:OA,OA:],OA:] is Relation-like non empty set
bool [:[:OA,OA:],OA:] is non empty set
AB is non empty Element of bool B
[:AB,AB:] is Relation-like B -defined B -valued non empty Element of bool [:B,B:]
[:B,B:] is Relation-like non empty set
bool [:B,B:] is non empty set
[:[:AB,AB:],AB:] is Relation-like non empty set
bool [:[:AB,AB:],AB:] is non empty set
MA is Relation-like [:OA,OA:] -defined OA -valued Function-like Element of bool [:[:OA,OA:],OA:]
MB is Relation-like [:AB,AB:] -defined AB -valued Function-like Element of bool [:[:AB,AB:],AB:]

[:A,B:] is Relation-like non empty set
[:OA,AB:] is Relation-like A -defined B -valued non empty Element of bool [:A,B:]
bool [:A,B:] is non empty set
[:[:OA,AB:],[:OA,AB:]:] is Relation-like [:A,B:] -defined [:A,B:] -valued non empty Element of bool [:[:A,B:],[:A,B:]:]
[:[:A,B:],[:A,B:]:] is Relation-like non empty set
bool [:[:A,B:],[:A,B:]:] is non empty set
[:[:[:OA,AB:],[:OA,AB:]:],[:OA,AB:]:] is Relation-like non empty set
bool [:[:[:OA,AB:],[:OA,AB:]:],[:OA,AB:]:] is non empty set
A is non empty set
bool A is non empty set
[:A,A:] is Relation-like non empty set
[:[:A,A:],A:] is Relation-like non empty set
bool [:[:A,A:],A:] is non empty set
B is non empty set
bool B is non empty set
[:B,B:] is Relation-like non empty set
[:[:B,B:],B:] is Relation-like non empty set
bool [:[:B,B:],B:] is non empty set
OA is non empty Element of bool A
[:OA,OA:] is Relation-like A -defined A -valued non empty Element of bool [:A,A:]
bool [:A,A:] is non empty set
[:[:OA,OA:],OA:] is Relation-like non empty set
bool [:[:OA,OA:],OA:] is non empty set
AB is non empty Element of bool B
[:AB,AB:] is Relation-like B -defined B -valued non empty Element of bool [:B,B:]
bool [:B,B:] is non empty set
[:[:AB,AB:],AB:] is Relation-like non empty set
bool [:[:AB,AB:],AB:] is non empty set
[:OA,AB:] is Relation-like A -defined B -valued non empty Element of bool [:A,B:]
[:A,B:] is Relation-like non empty set
bool [:A,B:] is non empty set

[:OA,OA:] is Relation-like non empty set
MA | [:OA,OA:] is Relation-like [:OA,OA:] -defined [:A,A:] -defined A -valued set

[:AB,AB:] is Relation-like non empty set
MB | [:AB,AB:] is Relation-like [:AB,AB:] -defined [:B,B:] -defined B -valued set
|:MA,MB:| is Relation-like [:[:A,B:],[:A,B:]:] -defined [:A,B:] -valued Function-like Element of bool [:[:[:A,B:],[:A,B:]:],[:A,B:]:]
[:[:A,B:],[:A,B:]:] is Relation-like non empty set
[:[:[:A,B:],[:A,B:]:],[:A,B:]:] is Relation-like non empty set
bool [:[:[:A,B:],[:A,B:]:],[:A,B:]:] is non empty set
|:MA,MB:| || [:OA,AB:] is Relation-like Function-like set
[:[:OA,AB:],[:OA,AB:]:] is Relation-like non empty set
|:MA,MB:| | [:[:OA,AB:],[:OA,AB:]:] is Relation-like [:[:OA,AB:],[:OA,AB:]:] -defined [:[:A,B:],[:A,B:]:] -defined [:A,B:] -valued set
OB is Relation-like [:OA,OA:] -defined OA -valued Function-like Element of bool [:[:OA,OA:],OA:]

MB is Relation-like [:AB,AB:] -defined AB -valued Function-like Element of bool [:[:AB,AB:],AB:]
(A,B,OA,AB,OB,MB) is Relation-like [:[:OA,AB:],[:OA,AB:]:] -defined [:OA,AB:] -valued Function-like Element of bool [:[:[:OA,AB:],[:OA,AB:]:],[:OA,AB:]:]
[:[:OA,AB:],[:OA,AB:]:] is Relation-like [:A,B:] -defined [:A,B:] -valued non empty Element of bool [:[:A,B:],[:A,B:]:]
bool [:[:A,B:],[:A,B:]:] is non empty set
[:[:[:OA,AB:],[:OA,AB:]:],[:OA,AB:]:] is Relation-like non empty set
bool [:[:[:OA,AB:],[:OA,AB:]:],[:OA,AB:]:] is non empty set
proj1 (A,B,OA,AB,OB,MB) is Relation-like set

proj1 (|:MA,MB:| || [:OA,AB:]) is set
a is set
b is set
a is set
[b,a] is non empty V15() set
{b,a} is non empty finite set
{b} is non empty trivial finite set
{{b,a},{b}} is non empty finite V35() set
a is set
t19 is set
[a,t19] is non empty V15() set
{a,t19} is non empty finite set
{a} is non empty trivial finite set
{{a,t19},{a}} is non empty finite V35() set
[[b,a],[a,t19]] is non empty V15() set
{[b,a],[a,t19]} is Relation-like non empty finite set

{{[b,a],[a,t19]},{[b,a]}} is non empty finite V35() set
[b,a] is non empty V15() set
{b,a} is non empty finite set
{{b,a},{b}} is non empty finite V35() set
[a,t19] is non empty V15() set
{a,t19} is non empty finite set
{a} is non empty trivial finite set
{{a,t19},{a}} is non empty finite V35() set
proj1 |:MA,MB:| is Relation-like set
(proj1 |:MA,MB:|) /\ [:[:OA,AB:],[:OA,AB:]:] is Relation-like [:A,B:] -defined [:A,B:] -valued Element of bool [:[:A,B:],[:A,B:]:]
a is set
(proj1 MA) /\ [:OA,OA:] is Relation-like A -defined A -valued Element of bool [:A,A:]
proj1 |:MA,MB:| is Relation-like set
(proj1 |:MA,MB:|) /\ [:[:OA,AB:],[:OA,AB:]:] is Relation-like [:A,B:] -defined [:A,B:] -valued Element of bool [:[:A,B:],[:A,B:]:]
(proj1 MB) /\ [:AB,AB:] is Relation-like B -defined B -valued Element of bool [:B,B:]
b is set
a is set
[b,a] is non empty V15() set
{b,a} is non empty finite set
{b} is non empty trivial finite set
{{b,a},{b}} is non empty finite V35() set
a is set
t19 is set
[a,t19] is non empty V15() set
{a,t19} is non empty finite set
{a} is non empty trivial finite set
{{a,t19},{a}} is non empty finite V35() set
[[b,a],[a,t19]] is non empty V15() set
{[b,a],[a,t19]} is Relation-like non empty finite set

{{[b,a],[a,t19]},{[b,a]}} is non empty finite V35() set
[b,a] is non empty V15() set
{b,a} is non empty finite set
{{b,a},{b}} is non empty finite V35() set
[a,t19] is non empty V15() set
{a,t19} is non empty finite set
{a} is non empty trivial finite set
{{a,t19},{a}} is non empty finite V35() set
a is set
b is set
a is set
[b,a] is non empty V15() set
{b,a} is non empty finite set
{b} is non empty trivial finite set
{{b,a},{b}} is non empty finite V35() set
a is set
t19 is set
[a,t19] is non empty V15() set
{a,t19} is non empty finite set
{a} is non empty trivial finite set
{{a,t19},{a}} is non empty finite V35() set
[[b,a],[a,t19]] is non empty V15() set
{[b,a],[a,t19]} is Relation-like non empty finite set

{{[b,a],[a,t19]},{[b,a]}} is non empty finite V35() set
[b,a] is non empty V15() set
{b,a} is non empty finite set
{{b,a},{b}} is non empty finite V35() set
[a,t19] is non empty V15() set
{a,t19} is non empty finite set
{a} is non empty trivial finite set
{{a,t19},{a}} is non empty finite V35() set
(A,B,OA,AB,OB,MB) . a is set
(A,B,OA,AB,OB,MB) . ([b,a],[a,t19]) is set
(A,B,OA,AB,OB,MB) . [[b,a],[a,t19]] is set
OB . (b,a) is set
OB . [b,a] is set
MB . (a,t19) is set
MB . [a,t19] is set
[(OB . (b,a)),(MB . (a,t19))] is non empty V15() set
{(OB . (b,a)),(MB . (a,t19))} is non empty finite set
{(OB . (b,a))} is non empty trivial finite set
{{(OB . (b,a)),(MB . (a,t19))},{(OB . (b,a))}} is non empty finite V35() set
MA . [b,a] is set
[(MA . [b,a]),(MB . [a,t19])] is non empty V15() set
{(MA . [b,a]),(MB . [a,t19])} is non empty finite set
{(MA . [b,a])} is non empty trivial finite set
{{(MA . [b,a]),(MB . [a,t19])},{(MA . [b,a])}} is non empty finite V35() set
MA . (b,a) is set
MB . (a,t19) is set
MB . [a,t19] is set
[(MA . (b,a)),(MB . (a,t19))] is non empty V15() set
{(MA . (b,a)),(MB . (a,t19))} is non empty finite set
{(MA . (b,a))} is non empty trivial finite set
{{(MA . (b,a)),(MB . (a,t19))},{(MA . (b,a))}} is non empty finite V35() set
|:MA,MB:| . ([b,a],[a,t19]) is set
|:MA,MB:| . [[b,a],[a,t19]] is set
(|:MA,MB:| || [:OA,AB:]) . a is set
a is Element of [:[:OA,AB:],[:OA,AB:]:]
(A,B,OA,AB,OB,MB) . a is set
(|:MA,MB:| || [:OA,AB:]) . a is set
proj2 (|:MA,MB:| || [:OA,AB:]) is set
proj2 (A,B,OA,AB,OB,MB) is Relation-like set
a is set
b is set
(|:MA,MB:| || [:OA,AB:]) . b is set
(A,B,OA,AB,OB,MB) . b is set
A is set
B is set

{A} is non empty trivial finite set
{B} is non empty trivial finite set

bool [:{B},{A}:] is non empty finite V35() set

bool [:[:{B},{B}:],{B}:] is non empty finite V35() set
CatStr(# {A},{B},K241(B,A),K241(B,A),K240(B,B,B) #) is non empty non void V55() strict CatStr
the carrier' of (1Cat (A,B)) is non empty trivial finite set
OA is Element of the carrier' of (1Cat (A,B))
AB is Element of the carrier' of (1Cat (A,B))

the carrier of A is non empty set

[: the carrier of A, the carrier of A:] is Relation-like non empty set
the carrier' of A is non empty set
[: the carrier' of A, the carrier' of A:] is Relation-like non empty set
the Source of A is Relation-like the carrier' of A -defined the carrier of A -valued Function-like quasi_total Element of bool [: the carrier' of A, the carrier of A:]
[: the carrier' of A, the carrier of A:] is Relation-like non empty set
bool [: the carrier' of A, the carrier of A:] is non empty set
[: the Source of A, the Source of A:] is Relation-like [: the carrier' of A, the carrier' of A:] -defined [: the carrier of A, the carrier of A:] -valued Function-like quasi_total Element of bool [:[: the carrier' of A, the carrier' of A:],[: the carrier of A, the carrier of A:]:]
[:[: the carrier' of A, the carrier' of A:],[: the carrier of A, the carrier of A:]:] is Relation-like non empty set
bool [:[: the carrier' of A, the carrier' of A:],[: the carrier of A, the carrier of A:]:] is non empty set
the Target of A is Relation-like the carrier' of A -defined the carrier of A -valued Function-like quasi_total Element of bool [: the carrier' of A, the carrier of A:]
[: the Target of A, the Target of A:] is Relation-like [: the carrier' of A, the carrier' of A:] -defined [: the carrier of A, the carrier of A:] -valued Function-like quasi_total Element of bool [:[: the carrier' of A, the carrier' of A:],[: the carrier of A, the carrier of A:]:]
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:], the carrier' of A:] is Relation-like non empty set
bool [:[: the carrier' of A, the carrier' of A:], the carrier' of A:] is non empty set
|: the Comp of A, the Comp of A:| is Relation-like [:[: the carrier' of A, the carrier' of A:],[: the carrier' of A, the carrier' of A:]:] -defined [: the carrier' of A, 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, the carrier' of A:]:]
[:[: the carrier' of A, the carrier' of A:],[: the carrier' of A, the carrier' of A:]:] is Relation-like non empty set
[:[:[: the carrier' of A, the carrier' of A:],[: the carrier' of A, the carrier' of A:]:],[: the carrier' of A, the carrier' of A:]:] is Relation-like non empty set
bool [:[:[: the carrier' of A, the carrier' of A:],[: the carrier' of A, the carrier' of A:]:],[: the carrier' of A, the carrier' of A:]:] is non empty set
CatStr(# [: the carrier of A, the carrier of A:],[: the carrier' of A, the carrier' of A:],[: the Source of A, the Source of A:],[: the Target of A, the Target of A:],|: the Comp of A, the Comp of A:| #) is non empty non void V55() strict CatStr
B is Element of the carrier of A
id B is Morphism of B,B
[(id B),(id B)] is non empty V15() Element of the carrier' of [:A,A:]
the carrier' of [:A,A:] is non empty set
{(id B),(id B)} is non empty finite set
{(id B)} is non empty trivial finite set
{{(id B),(id B)},{(id B)}} is non empty finite V35() set
[[(id B),(id B)],(id B)] is non empty V15() Element of the carrier' of [:[:A,A:],A:]

the carrier of [:A,A:] is non empty set
[: the carrier of [:A,A:], the carrier of A:] is Relation-like non empty set
[: the carrier' of [:A,A:], the carrier' of A:] is Relation-like non empty set
the Source of [:A,A:] is Relation-like the carrier' of [:A,A:] -defined the carrier of [:A,A:] -valued Function-like quasi_total Element of bool [: the carrier' of [:A,A:], the carrier of [:A,A:]:]
[: the carrier' of [:A,A:], the carrier of [:A,A:]:] is Relation-like non empty set
bool [: the carrier' of [:A,A:], the carrier of [:A,A:]:] is non empty set
[: the Source of [:A,A:], the Source of A:] is Relation-like [: the carrier' of [:A,A:], the carrier' of A:] -defined [: the carrier of [:A,A:], the carrier of A:] -valued Function-like quasi_total Element of bool [:[: the carrier' of [:A,A:], the carrier' of A:],[: the carrier of [:A,A:], the carrier of A:]:]
[:[: the carrier' of [:A,A:], the carrier' of A:],[: the carrier of [:A,A:], the carrier of A:]:] is Relation-like non empty set
bool [:[: the carrier' of [:A,A:], the carrier' of A:],[: the carrier of [:A,A:], the carrier of A:]:] is non empty set
the Target of [:A,A:] is Relation-like the carrier' of [:A,A:] -defined the carrier of [:A,A:] -valued Function-like quasi_total Element of bool [: the carrier' of [:A,A:], the carrier of [:A,A:]:]
[: the Target of [:A,A:], the Target of A:] is Relation-like [: the carrier' of [:A,A:], the carrier' of A:] -defined [: the carrier of [:A,A:], the carrier of A:] -valued Function-like quasi_total Element of bool [:[: the carrier' of [:A,A:], the carrier' of A:],[: the carrier of [:A,A:], the carrier of A:]:]
the Comp of [:A,A:] is Relation-like [: the carrier' of [:A,A:], the carrier' of [:A,A:]:] -defined the carrier' of [:A,A:] -valued Function-like Element of bool [:[: the carrier' of [:A,A:], the carrier' of [:A,A:]:], the carrier' of [:A,A:]:]
[: the carrier' of [:A,A:], the carrier' of [:A,A:]:] is Relation-like non empty set
[:[: the carrier' of [:A,A:], the carrier' of [:A,A:]:], the carrier' of [:A,A:]:] is Relation-like non empty set
bool [:[: the carrier' of [:A,A:], the carrier' of [:A,A:]:], the carrier' of [:A,A:]:] is non empty set
|: the Comp of [:A,A:], the Comp of A:| is Relation-like [:[: the carrier' of [:A,A:], the carrier' of A:],[: the carrier' of [:A,A:], the carrier' of A:]:] -defined [: the carrier' of [:A,A:], the carrier' of A:] -valued Function-like Element of bool [:[:[: the carrier' of [:A,A:], the carrier' of A:],[: the carrier' of [:A,A:], the carrier' of A:]:],[: the carrier' of [:A,A:], the carrier' of A:]:]
[:[: the carrier' of [:A,A:], the carrier' of A:],[: the carrier' of [:A,A:], the carrier' of A:]:] is Relation-like non empty set
[:[:[: the carrier' of [:A,A:], the carrier' of A:],[: the carrier' of [:A,A:], the carrier' of A:]:],[: the carrier' of [:A,A:], the carrier' of A:]:] is Relation-like non empty set
bool [:[:[: the carrier' of [:A,A:], the carrier' of A:],[: the carrier' of [:A,A:], the carrier' of A:]:],[: the carrier' of [:A,A:], the carrier' of A:]:] is non empty set
CatStr(# [: the carrier of [:A,A:], the carrier of A:],[: the carrier' of [:A,A:], the carrier' of A:],[: the Source of [:A,A:], the Source of A:],[: the Target of [:A,A:], the Target of A:],|: the Comp of [:A,A:], the Comp of A:| #) is non empty non void V55() strict CatStr
the carrier' of [:[:A,A:],A:] is non empty set
{[(id B),(id B)],(id B)} is non empty finite set
{[(id B),(id B)]} is Relation-like non empty trivial finite set
{{[(id B),(id B)],(id B)},{[(id B),(id B)]}} is non empty finite V35() set
dom (id B) is Element of the carrier of A
the Source of A . (id B) is Element of the carrier of A
cod (id B) is Element of the carrier of A
the Target of A . (id B) is Element of the carrier of A
proj1 the Comp of A is Relation-like set
(id B) (*) (id B) is Element of the carrier' of A
the Comp of A . ((id B),(id B)) is set
[(id B),(id B)] is non empty V15() set
the Comp of A . [(id B),(id B)] is set
A is set
B is set

{A} is non empty trivial finite set
{B} is non empty trivial finite set

bool [:{B},{A}:] is non empty finite V35() set

bool [:[:{B},{B}:],{B}:] is non empty finite V35() set
CatStr(# {A},{B},K241(B,A),K241(B,A),K240(B,B,B) #) is non empty non void V55() strict CatStr
the Comp of (1Cat (A,B)) is Relation-like [: the carrier' of (1Cat (A,B)), the carrier' of (1Cat (A,B)):] -defined the carrier' of (1Cat (A,B)) -valued Function-like finite Element of bool [:[: the carrier' of (1Cat (A,B)), the carrier' of (1Cat (A,B)):], the carrier' of (1Cat (A,B)):]
the carrier' of (1Cat (A,B)) is non empty trivial finite set
[: the carrier' of (1Cat (A,B)), the carrier' of (1Cat (A,B)):] is Relation-like non empty finite set
[:[: the carrier' of (1Cat (A,B)), the carrier' of (1Cat (A,B)):], the carrier' of (1Cat (A,B)):] is Relation-like non empty finite set
bool [:[: the carrier' of (1Cat (A,B)), the carrier' of (1Cat (A,B)):], the carrier' of (1Cat (A,B)):] is non empty finite V35() set
[B,B] is non empty V15() set
{B,B} is non empty finite set
{{B,B},{B}} is non empty finite V35() set
[[B,B],B] is non empty V15() set
{[B,B],B} is non empty finite set

{{[B,B],B},{[B,B]}} is non empty finite V35() set
{[[B,B],B]} is Relation-like non empty trivial finite set
the carrier of (1Cat (A,B)) is non empty trivial finite set
the Element of the carrier of (1Cat (A,B)) is Element of the carrier of (1Cat (A,B))
OB is set
id the Element of the carrier of (1Cat (A,B)) is Morphism of the Element of the carrier of (1Cat (A,B)), the Element of the carrier of (1Cat (A,B))
dom (id the Element of the carrier of (1Cat (A,B))) is Element of the carrier of (1Cat (A,B))
the Source of (1Cat (A,B)) is Relation-like the carrier' of (1Cat (A,B)) -defined the carrier of (1Cat (A,B)) -valued Function-like quasi_total finite Element of bool [: the carrier' of (1Cat (A,B)), the carrier of (1Cat (A,B)):]
[: the carrier' of (1Cat (A,B)), the carrier of (1Cat (A,B)):] is Relation-like non empty finite set
bool [: the carrier' of (1Cat (A,B)), the carrier of (1Cat (A,B)):] is non empty finite V35() set
the Source of (1Cat (A,B)) . (id the Element of the carrier of (1Cat (A,B))) is Element of the carrier of (1Cat (A,B))
cod (id the Element of the carrier of (1Cat (A,B))) is Element of the carrier of (1Cat (A,B))
the Target of (1Cat (A,B)) is Relation-like the carrier' of (1Cat (A,B)) -defined the carrier of (1Cat (A,B)) -valued Function-like quasi_total finite Element of bool [: the carrier' of (1Cat (A,B)), the carrier of (1Cat (A,B)):]
the Target of (1Cat (A,B)) . (id the Element of the carrier of (1Cat (A,B))) is Element of the carrier of (1Cat (A,B))
MB is set
MA is set
[MB,MA] is non empty V15() set
{MB,MA} is non empty finite set
{MB} is non empty trivial finite set
{{MB,MA},{MB}} is non empty finite V35() set
proj1 the Comp of (1Cat (A,B)) is Relation-like finite set
a is set
b is set
[a,b] is non empty V15() set
{a,b} is non empty finite set
{a} is non empty trivial finite set
{{a,b},{a}} is non empty finite V35() set
the Comp of (1Cat (A,B)) . ((id the Element of the carrier of (1Cat (A,B))),(id the Element of the carrier of (1Cat (A,B)))) is set
[(id the Element of the carrier of (1Cat (A,B))),(id the Element of the carrier of (1Cat (A,B)))] is non empty V15() set
{(id the Element of the carrier of (1Cat (A,B))),(id the Element of the carrier of (1Cat (A,B)))} is non empty finite set
{(id the Element of the carrier of (1Cat (A,B)))} is non empty trivial finite set
{{(id the Element of the carrier of (1Cat (A,B))),(id the Element of the carrier of (1Cat (A,B)))},{(id the Element of the carrier of (1Cat (A,B)))}} is non empty finite V35() set
the Comp of (1Cat (A,B)) . [(id the Element of the carrier of (1Cat (A,B))),(id the Element of the carrier of (1Cat (A,B)))] is set
(id the Element of the carrier of (1Cat (A,B))) (*) (id the Element of the carrier of (1Cat (A,B))) is Element of the carrier' of (1Cat (A,B))
MB is set
AB is Element of the carrier' of (1Cat (A,B))
id the Element of the carrier of (1Cat (A,B)) is Morphism of the Element of the carrier of (1Cat (A,B)), the Element of the carrier of (1Cat (A,B))

the carrier of A is non empty set
B is Element of the carrier of A
id B is Morphism of B,B

{B} is non empty trivial finite set
{(id B)} is non empty trivial finite set
K241((id B),B) is Relation-like {(id B)} -defined {B} -valued Function-like quasi_total finite Element of bool [:{(id B)},{B}:]
[:{(id B)},{B}:] is Relation-like non empty finite set
bool [:{(id B)},{B}:] is non empty finite V35() set
K240((id B),(id B),(id B)) is Relation-like [:{(id B)},{(id B)}:] -defined {(id B)} -valued Function-like quasi_total finite Element of bool [:[:{(id B)},{(id B)}:],{(id B)}:]
[:{(id B)},{(id B)}:] is Relation-like non empty finite set
[:[:{(id B)},{(id B)}:],{(id B)}:] is Relation-like non empty finite set
bool [:[:{(id B)},{(id B)}:],{(id B)}:] is non empty finite V35() set
CatStr(# {B},{(id B)},K241((id B),B),K241((id B),B),K240((id B),(id B),(id B)) #) is non empty non void V55() strict CatStr
the carrier of (1Cat (B,(id B))) is non empty trivial finite set
OA is set
the Comp of (1Cat (B,(id B))) is Relation-like [: the carrier' of (1Cat (B,(id B))), the carrier' of (1Cat (B,(id B))):] -defined the carrier' of (1Cat (B,(id B))) -valued Function-like finite Element of bool [:[: the carrier' of (1Cat (B,(id B))), the carrier' of (1Cat (B,(id B))):], the carrier' of (1Cat (B,(id B))):]
the carrier' of (1Cat (B,(id B))) is non empty trivial finite set
[: the carrier' of (1Cat (B,(id B))), the carrier' of (1Cat (B,(id B))):] is Relation-like non empty finite set
[:[: the carrier' of (1Cat (B,(id B))), the carrier' of (1Cat (B,(id B))):], the carrier' of (1Cat (B,(id B))):] is Relation-like non empty finite set
bool [:[: the carrier' of (1Cat (B,(id B))), the carrier' of (1Cat (B,(id B))):], the carrier' of (1Cat (B,(id B))):] is non empty finite V35() set
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 is non empty set
[: the carrier' of A, the carrier' of A:] is Relation-like non empty set
[:[: the carrier' of A, the carrier' of A:], the carrier' of A:] is Relation-like non empty set
bool [:[: the carrier' of A, the carrier' of A:], the carrier' of A:] is non empty set
OA is Element of the carrier of (1Cat (B,(id B)))
AB is Element of the carrier of (1Cat (B,(id B)))
Hom (OA,AB) is trivial finite Element of bool the carrier' of (1Cat (B,(id B)))
bool the carrier' of (1Cat (B,(id B))) is non empty finite V35() set
{ b1 where b1 is Element of the carrier' of (1Cat (B,(id B))) : ( dom b1 = OA & cod b1 = AB ) } is set
MA is Element of the carrier of A
MB is Element of the carrier of A
Hom (MA,MB) is Element of bool the carrier' of A
bool the carrier' of A is non empty set
{ b1 where b1 is Element of the carrier' of A : ( dom b1 = MA & cod b1 = MB ) } is set
OB is set
OA is set

[: the carrier of A, the carrier of A:] is Relation-like non empty set
the Source of A is Relation-like the carrier' of A -defined the carrier of A -valued Function-like quasi_total Element of bool [: the carrier' of A, the carrier of A:]
[: the carrier' of A, the carrier of A:] is Relation-like non empty set
bool [: the carrier' of A, the carrier of A:] is non empty set
[: the Source of A, the Source of A:] is Relation-like [: the carrier' of A, the carrier' of A:] -defined [: the carrier of A, the carrier of A:] -valued Function-like quasi_total Element of bool [:[: the carrier' of A, the carrier' of A:],[: the carrier of A, the carrier of A:]:]
[:[: the carrier' of A, the carrier' of A:],[: the carrier of A, the carrier of A:]:] is Relation-like non empty set
bool [:[: the carrier' of A, the carrier' of A:],[: the carrier of A, the carrier of A:]:] is non empty set
the Target of A is Relation-like the carrier' of A -defined the carrier of A -valued Function-like quasi_total Element of bool [: the carrier' of A, the carrier of A:]
[: the Target of A, the Target of A:] is Relation-like [: the carrier' of A, the carrier' of A:] -defined [: the carrier of A, the carrier of A:] -valued Function-like quasi_total Element of bool [:[: the carrier' of A, the carrier' of A:],[: the carrier of A, the carrier of A:]:]
|: the Comp of A, the Comp of A:| is Relation-like [:[: the carrier' of A, the carrier' of A:],[: the carrier' of A, the carrier' of A:]:] -defined [: the carrier' of A, 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, the carrier' of A:]:]
[:[: the carrier' of A, the carrier' of A:],[: the carrier' of A, the carrier' of A:]:] is Relation-like non empty set
[:[:[: the carrier' of A, the carrier' of A:],[: the carrier' of A, the carrier' of A:]:],[: the carrier' of A, the carrier' of A:]:] is Relation-like non empty set
bool [:[:[: the carrier' of A, the carrier' of A:],[: the carrier' of A, the carrier' of A:]:],[: the carrier' of A, the carrier' of A:]:] is non empty set
CatStr(# [: the carrier of A, the carrier of A:],[: the carrier' of A, the carrier' of A:],[: the Source of A, the Source of A:],[: the Target of A, the Target of A:],|: the Comp of A, the Comp of A:| #) is non empty non void V55() strict CatStr
[(id B),(id B)] is non empty V15() Element of the carrier' of [:A,A:]
the carrier' of [:A,A:] is non empty set
{(id B),(id B)} is non empty finite set
{{(id B),(id B)},{(id B)}} is non empty finite V35() set
[[(id B),(id B)],(id B)] is non empty V15() Element of the carrier' of [:[:A,A:],A:]

the carrier of [:A,A:] is non empty set
[: the carrier of [:A,A:], the carrier of A:] is Relation-like non empty set
[: the carrier' of [:A,A:], the carrier' of A:] is Relation-like non empty set
the Source of [:A,A:] is Relation-like the carrier' of [:A,A:] -defined the carrier of [:A,A:] -valued Function-like quasi_total Element of bool [: the carrier' of [:A,A:], the carrier of [:A,A:]:]
[: the carrier' of [:A,A:], the carrier of [:A,A:]:] is Relation-like non empty set
bool [: the carrier' of [:A,A:], the carrier of [:A,A:]:] is non empty set
[: the Source of [:A,A:], the Source of A:] is Relation-like [: the carrier' of [:A,A:], the carrier' of A:] -defined [: the carrier of [:A,A:], the carrier of A:] -valued Function-like quasi_total Element of bool [:[: the carrier' of [:A,A:], the carrier' of A:],[: the carrier of [:A,A:], the carrier of A:]:]
[:[: the carrier' of [:A,A:], the carrier' of A:],[: the carrier of [:A,A:], the carrier of A:]:] is Relation-like non empty set
bool [:[: the carrier' of [:A,A:], the carrier' of A:],[: the carrier of [:A,A:], the carrier of A:]:] is non empty set
the Target of [:A,A:] is Relation-like the carrier' of [:A,A:] -defined the carrier of [:A,A:] -valued Function-like quasi_total Element of bool [: the carrier' of [:A,A:], the carrier of [:A,A:]:]
[: the Target of [:A,A:], the Target of A:] is Relation-like [: the carrier' of [:A,A:], the carrier' of A:] -defined [: the carrier of [:A,A:], the carrier of A:] -valued Function-like quasi_total Element of bool [:[: the carrier' of [:A,A:], the carrier' of A:],[: the carrier of [:A,A:], the carrier of A:]:]
the Comp of [:A,A:] is Relation-like [: the carrier' of [:A,A:], the carrier' of [:A,A:]:] -defined the carrier' of [:A,A:] -valued Function-like Element of bool [:[: the carrier' of [:A,A:], the carrier' of [:A,A:]:], the carrier' of [:A,A:]:]
[: the carrier' of [:A,A:], the carrier' of [:A,A:]:] is Relation-like non empty set
[:[: the carrier' of [:A,A:], the carrier' of [:A,A:]:], the carrier' of [:A,A:]:] is Relation-like non empty set
bool [:[: the carrier' of [:A,A:], the carrier' of [:A,A:]:], the carrier' of [:A,A:]:] is non empty set
|: the Comp of [:A,A:], the Comp of A:| is Relation-like [:[: the carrier' of [:A,A:], the carrier' of A:],[: the carrier' of [:A,A:], the carrier' of A:]:] -defined [: the carrier' of [:A,A:], the carrier' of A:] -valued Function-like Element of bool [:[:[: the carrier' of [:A,A:], the carrier' of A:],[: the carrier' of [:A,A:], the carrier' of A:]:],[: the carrier' of [:A,A:], the carrier' of A:]:]
[:[: the carrier' of [:A,A:], the carrier' of A:],[: the carrier' of [:A,A:], the carrier' of A:]:] is Relation-like non empty set
[:[:[: the carrier' of [:A,A:], the carrier' of A:],[: the carrier' of [:A,A:], the carrier' of A:]:],[: the carrier' of [:A,A:], the carrier' of A:]:] is Relation-like non empty set
bool [:[:[: the carrier' of [:A,A:], the carrier' of A:],[: the carrier' of [:A,A:], the carrier' of A:]:],[: the carrier' of [:A,A:], the carrier' of A:]:] is non empty set
CatStr(# [: the carrier of [:A,A:], the carrier of A:],[: the carrier' of [:A,A:], the carrier' of A:],[: the Source of [:A,A:], the Source of A:],[: the Target of [:A,A:], the Target of A:],|: the Comp of [:A,A:], the Comp of A:| #) is non empty non void V55() strict CatStr
the carrier' of [:[:A,A:],A:] is non empty set
{[(id B),(id B)],(id B)} is non empty finite set
{[(id B),(id B)]} is Relation-like non empty trivial finite set
{{[(id B),(id B)],(id B)},{[(id B),(id B)]}} is non empty finite V35() set
{[[(id B),(id B)],(id B)]} is Relation-like non empty trivial finite set
OA is Element of the carrier of (1Cat (B,(id B)))
id OA is Morphism of OA,OA
AB is Element of the carrier of A
id AB is Morphism of AB,AB

the Source of A is Relation-like the carrier' of A -defined the carrier of A -valued Function-like quasi_total Element of bool [: the carrier' of A, the carrier of A:]
the carrier' of A is non empty set
the carrier of A is non empty set
[: the carrier' of A, the carrier of A:] is Relation-like non empty set
bool [: the carrier' of A, the carrier of A:] is non empty set
the Target of A is Relation-like the carrier' of A -defined the carrier of A -valued Function-like quasi_total Element of bool [: the carrier' of A, the carrier of A:]
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 Relation-like non empty set
[:[: the carrier' of A, the carrier' of A:], the carrier' of A:] is Relation-like non empty set
bool [:[: the carrier' of A, the carrier' of A:], the carrier' of A:] is non empty set

the Source of B is Relation-like the carrier' of B -defined the carrier of B -valued Function-like quasi_total Element of bool [: the carrier' of B, the carrier of B:]
the carrier' of B is non empty set
the carrier of B is non empty set
[: the carrier' of B, the carrier of B:] is Relation-like non empty set
bool [: the carrier' of B, the carrier of B:] is non empty set
the Source of A | the carrier' of B is Relation-like the carrier' of B -defined the carrier' of A -defined the carrier of A -valued set
the Target of B is Relation-like the carrier' of B -defined the carrier of B -valued Function-like quasi_total Element of bool [: the carrier' of B, the carrier of B:]
the Target of A | the carrier' of B is Relation-like the carrier' of B -defined the carrier' of A -defined the carrier of A -valued 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 Relation-like non empty set
[:[: the carrier' of B, the carrier' of B:], the carrier' of B:] is Relation-like non empty set
bool [:[: the carrier' of B, the carrier' of B:], the carrier' of B:] is non empty set
the Comp of A || the carrier' of B is Relation-like Function-like set
the Comp of A | [: the carrier' of B, the carrier' of B:] is Relation-like [: the carrier' of B, the carrier' of B:] -defined [: the carrier' of A, the carrier' of A:] -defined the carrier' of A -valued set
proj1 the Source of A is set
OA is set
proj1 the Source of B is set
AB is Element of the carrier' of B
the Source of B . OA is set
dom AB is Element of the carrier of B
the Source of B . AB is Element of the carrier of B
MA is Element of the carrier' of A
dom MA is Element of the carrier of A
the Source of A . MA is Element of the carrier of A
the Source of A . OA is set
OA is set
proj1 the Target of B is set
AB is Element of the carrier' of B
the Target of B . OA is set
cod AB is Element of the carrier of B
the Target of B . AB is Element of the carrier of B
MA is Element of the carrier' of A
cod MA is Element of the carrier of A
the Target of A . MA is Element of the carrier of A
the Target of A . OA is set
(proj1 the Source of A) /\ the carrier' of B is set
proj1 the Target of A is set
(proj1 the Target of A) /\ the carrier' of B is set
proj1 the Comp of B is Relation-like set
proj1 the Comp of A is Relation-like set
(proj1 the Comp of A) /\ [: the carrier' of B, the carrier' of B:] is Relation-like set
OA is set
OA `1 is set
OA `2 is set
AB is Element of the carrier' of B
MA is Element of the carrier' of B
MB is Element of the carrier' of A
OB is Element of the carrier' of A
[MB,OB] is non empty V15() Element of the carrier' of [:A,A:]

[: the carrier of A, the carrier of A:] is Relation-like non empty set
[: the Source of A, the Source of A:] is Relation-like [: the carrier' of A, the carrier' of A:] -defined [: the carrier of A, the carrier of A:] -valued Function-like quasi_total Element of bool [:[: the carrier' of A, the carrier' of A:],[: the carrier of A, the carrier of A:]:]
[:[: the carrier' of A, the carrier' of A:],[: the carrier of A, the carrier of A:]:] is Relation-like non empty set
bool [:[: the carrier' of A, the carrier' of A:],[: the carrier of A, the carrier of A:]:] is non empty set
[: the Target of A, the Target of A:] is Relation-like [: the carrier' of A, the carrier' of A:] -defined [: the carrier of A, the carrier of A:] -valued Function-like quasi_total Element of bool [:[: the carrier' of A, the carrier' of A:],[: the carrier of A, the carrier of A:]:]
|: the Comp of A, the Comp of A:| is Relation-like [:[: the carrier' of A, the carrier' of A:],[: the carrier' of A, the carrier' of A:]:] -defined [: the carrier' of A, 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, the carrier' of A:]:]
[:[: the carrier' of A, the carrier' of A:],[: the carrier' of A, the carrier' of A:]:] is Relation-like non empty set
[:[:[: the carrier' of A, the carrier' of A:],[: the carrier' of A, the carrier' of A:]:],[: the carrier' of A, the carrier' of A:]:] is Relation-like non empty set
bool [:[:[: the carrier' of A, the carrier' of A:],[: the carrier' of A, the carrier' of A:]:],[: the carrier' of A, the carrier' of A:]:] is non empty set
CatStr(# [: the carrier of A, the carrier of A:],[: the carrier' of A, the carrier' of A:],[: the Source of A, the Source of A:],[: the Target of A, the Target of A:],|: the Comp of A, the Comp of A:| #) is non empty non void V55() strict CatStr
the carrier' of [:A,A:] is non empty set
{MB,OB} is non empty finite set
{MB} is non empty trivial finite set
{{MB,OB},{MB}} is non empty finite V35() set
dom AB is Element of the carrier of B
the Source of B . AB is Element of the carrier of B
dom MB is Element of the carrier of A
the Source of A . MB is Element of the carrier of A
cod OB is Element of the carrier of A
the Target of A . OB is Element of the carrier of A
cod MA is Element of the carrier of B
the Target of B . MA is Element of the carrier of B
[AB,MA] is non empty V15() Element of the carrier' of [:B,B:]

[: the carrier of B, the carrier of B:] is Relation-like non empty set
[: the Source of B, the Source of B:] is Relation-like [: the carrier' of B, the carrier' of B:] -defined [: the carrier of B, the carrier of B:] -valued Function-like quasi_total Element of bool [:[: the carrier' of B, the carrier' of B:],[: the carrier of B, the carrier of B:]:]
[:[: the carrier' of B, the carrier' of B:],[: the carrier of B, the carrier of B:]:] is Relation-like non empty set
bool [:[: the carrier' of B, the carrier' of B:],[: the carrier of B, the carrier of B:]:] is non empty set
[: the Target of B, the Target of B:] is Relation-like [: the carrier' of B, the carrier' of B:] -defined [: the carrier of B, the carrier of B:] -valued Function-like quasi_total Element of bool [:[: the carrier' of B, the carrier' of B:],[: the carrier of B, the carrier of B:]:]
|: the Comp of B, the Comp of B:| is Relation-like [:[: the carrier' of B, the carrier' of B:],[: the carrier' of B, the carrier' of B:]:] -defined [: the carrier' of B, 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, the carrier' of B:]:]
[:[: the carrier' of B, the carrier' of B:],[: the carrier' of B, the carrier' of B:]:] is Relation-like non empty set
[:[:[: the carrier' of B, the carrier' of B:],[: the carrier' of B, the carrier' of B:]:],[: the carrier' of B, the carrier' of B:]:] is Relation-like non empty set
bool [:[:[: the carrier' of B, the carrier' of B:],[: the carrier' of B, the carrier' of B:]:],[: the carrier' of B, the carrier' of B:]:] is non empty set
CatStr(# [: the carrier of B, the carrier of B:],[: the carrier' of B, the carrier' of B:],[: the Source of B, the Source of B:],[: the Target of B, the Target of B:],|: the Comp of B, the Comp of B:| #) is non empty non void V55() strict CatStr
the carrier' of [:B,B:] is non empty set
{AB,MA} is non empty finite set
{AB} is non empty trivial finite set
{{AB,MA},{AB}} is non empty finite V35() set
the Comp of A | ((proj1 the Comp of A) /\ [: the carrier' of B, the carrier' of B:]) is Relation-like (proj1 the Comp of A) /\ [: the carrier' of B, the carrier' of B:] -defined [: the carrier' of A, the carrier' of A:] -defined the carrier' of A -valued set
the Comp of A | (proj1 the Comp of A) is Relation-like proj1 the Comp of A -defined [: the carrier' of A, the carrier' of A:] -defined the carrier' of A -valued set
( the Comp of A | (proj1 the Comp of A)) | [: the carrier' of B, the carrier' of B:] is Relation-like [: the carrier' of B, the carrier' of B:] -defined [: the carrier' of A, the carrier' of A:] -defined the carrier' of A -valued set

the carrier of A is non empty set
bool the carrier of A is non empty set
the carrier' of A is non empty set
bool the carrier' of A is non empty set
the Source of A is Relation-like the carrier' of A -defined the carrier of A -valued Function-like quasi_total Element of bool [: the carrier' of A, the carrier of A:]
[: the carrier' of A, the carrier of A:] is Relation-like non empty set
bool [: the carrier' of A, the carrier of A:] is non empty set
the Target of A is Relation-like the carrier' of A -defined the carrier of A -valued Function-like quasi_total Element of bool [: the carrier' of A, the carrier of A:]
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 Relation-like non empty set
[:[: the carrier' of A, the carrier' of A:], the carrier' of A:] is Relation-like non empty set
bool [:[: the carrier' of A, the carrier' of A:], the carrier' of A:] is non empty set
B is non empty Element of bool the carrier of A
OA is non empty Element of bool the carrier' of A
[:OA,B:] is Relation-like non empty set
bool [:OA,B:] is non empty set
( the carrier' of A, the carrier of A, the Source of A,OA) is Relation-like OA -defined the carrier' of A -defined the carrier of A -valued Function-like quasi_total Element of bool [:OA, the carrier of A:]
[:OA, the carrier of A:] is Relation-like non empty set
bool [:OA, the carrier of A:] is non empty set
( the carrier' of A, the carrier of A, the Target of A,OA) is Relation-like OA -defined the carrier' of A -defined the carrier of A -valued Function-like quasi_total Element of bool [:OA, the carrier of A:]
[:OA,OA:] is Relation-like non empty set
[:[:OA,OA:],OA:] is Relation-like non empty set
bool [:[:OA,OA:],OA:] is non empty set
the Comp of A || OA is Relation-like Function-like set
the Comp of A | [:OA,OA:] is Relation-like [:OA,OA:] -defined [: the carrier' of A, the carrier' of A:] -defined the carrier' of A -valued set

MB is Relation-like [:OA,OA:] -defined OA -valued Function-like Element of bool [:[:OA,OA:],OA:]
CatStr(# B,OA,AB,MA,MB #) is non empty non void V55() strict CatStr
the carrier' of CatStr(# B,OA,AB,MA,MB #) is non empty set
MB is Element of the carrier' of A
MA is Element of the carrier' of CatStr(# B,OA,AB,MA,MB #)
the Source of CatStr(# B,OA,AB,MA,MB #) is Relation-like the carrier' of CatStr(# B,OA,AB,MA,MB #) -defined the carrier of CatStr(# B,OA,AB,MA,MB #) -valued Function-like quasi_total Element of bool [: the carrier' of CatStr(# B,OA,AB,MA,MB #), the carrier of CatStr(# B,OA,AB,MA,MB #):]
the carrier of CatStr(# B,OA,AB,MA,MB #) is non empty set
[: the carrier' of CatStr(# B,OA,AB,MA,MB #), the carrier of CatStr(# B,OA,AB,MA,MB #):] is Relation-like non empty set
bool [: the carrier' of CatStr(# B,OA,AB,MA,MB #), the carrier of CatStr(# B,OA,AB,MA,MB #):] is non empty set
proj1 the Source of CatStr(# B,OA,AB,MA,MB #) is set
dom MB is Element of the carrier of A
the Source of A . MB is Element of the carrier of A
dom MA is Element of the carrier of CatStr(# B,OA,AB,MA,MB #)
the Source of CatStr(# B,OA,AB,MA,MB #) . MA is Element of the carrier of CatStr(# B,OA,AB,MA,MB #)
the Target of CatStr(# B,OA,AB,MA,MB #) is Relation-like the carrier' of CatStr(# B,OA,AB,MA,MB #) -defined the carrier of CatStr(# B,OA,AB,MA,MB #) -valued Function-like quasi_total Element of bool [: the carrier' of CatStr(# B,OA,AB,MA,MB #), the carrier of CatStr(# B,OA,AB,MA,MB #):]
proj1 the Target of CatStr(# B,OA,AB,MA,MB #) is set
cod MB is Element of the carrier of A
the Target of A . MB is Element of the carrier of A
cod MA is Element of the carrier of CatStr(# B,OA,AB,MA,MB #)
the Target of CatStr(# B,OA,AB,MA,MB #) . MA is Element of the carrier of CatStr(# B,OA,AB,MA,MB #)
the Comp of CatStr(# B,OA,AB,MA,MB #) is Relation-like [: the carrier' of CatStr(# B,OA,AB,MA,MB #), the carrier' of CatStr(# B,OA,AB,MA,MB #):] -defined the carrier' of CatStr(# B,OA,AB,MA,MB #) -valued Function-like Element of bool [:[: the carrier' of CatStr(# B,OA,AB,MA,MB #), the carrier' of CatStr(# B,OA,AB,MA,MB #):], the carrier' of CatStr(# B,OA,AB,MA,MB #):]
[: the carrier' of CatStr(# B,OA,AB,MA,MB #), the carrier' of CatStr(# B,OA,AB,MA,MB #):] is Relation-like non empty set
[:[: the carrier' of CatStr(# B,OA,AB,MA,MB #), the carrier' of CatStr(# B,OA,AB,MA,MB #):], the carrier' of CatStr(# B,OA,AB,MA,MB #):] is Relation-like non empty set
bool [:[: the carrier' of CatStr(# B,OA,AB,MA,MB #), the carrier' of CatStr(# B,OA,AB,MA,MB #):], the carrier' of CatStr(# B,OA,AB,MA,MB #):] is non empty set
proj1 the Comp of CatStr(# B,OA,AB,MA,MB #) is Relation-like set
proj1 the Comp of A is Relation-like set
(proj1 the Comp of A) /\ [: the carrier' of CatStr(# B,OA,AB,MA,MB #), the carrier' of CatStr(# B,OA,AB,MA,MB #):] is Relation-like set
MA is Element of the carrier' of CatStr(# B,OA,AB,MA,MB #)
MB is Element of the carrier' of CatStr(# B,OA,AB,MA,MB #)
dom MA is Element of the carrier of CatStr(# B,OA,AB,MA,MB #)
the Source of CatStr(# B,OA,AB,MA,MB #) . MA is Element of the carrier of CatStr(# B,OA,AB,MA,MB #)
cod MB is Element of the carrier of CatStr(# B,OA,AB,MA,MB #)
the Target of CatStr(# B,OA,AB,MA,MB #) . MB is Element of the carrier of CatStr(# B,OA,AB,MA,MB #)
a is Element of the carrier' of A
dom a is Element of the carrier of A
the Source of A . a is Element of the carrier of A
b is Element of the carrier' of A
cod b is Element of the carrier of A
the Target of A . b is Element of the carrier of A
[a,b] is non empty V15() Element of the carrier' of [:A,A:]

[: the carrier of A, the carrier of A:] is Relation-like non empty set
[: the Source of A, the Source of A:] is Relation-like [: the carrier' of A, the carrier' of A:] -defined [: the carrier of A, the carrier of A:] -valued Function-like quasi_total Element of bool [:[: the carrier' of A, the carrier' of A:],[: the carrier of A, the carrier of A:]:]
[:[: the carrier' of A, the carrier' of A:],[: the carrier of A, the carrier of A:]:] is Relation-like non empty set
bool [:[: the carrier' of A, the carrier' of A:],[: the carrier of A, the carrier of A:]:] is non empty set
[: the Target of A, the Target of A:] is Relation-like [: the carrier' of A, the carrier' of A:] -defined [: the carrier of A, the carrier of A:] -valued Function-like quasi_total Element of bool [:[: the carrier' of A, the carrier' of A:],[: the carrier of A, the carrier of A:]:]
|: the Comp of A, the Comp of A:| is Relation-like [:[: the carrier' of A, the carrier' of A:],[: the carrier' of A, the carrier' of A:]:] -defined [: the carrier' of A, 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, the carrier' of A:]:]
[:[: the carrier' of A, the carrier' of A:],[: the carrier' of A, the carrier' of A:]:] is Relation-like non empty set
[:[:[: the carrier' of A, the carrier' of A:],[: the carrier' of A, the carrier' of A:]:],[: the carrier' of A, the carrier' of A:]:] is Relation-like non empty set
bool [:[:[: the carrier' of A, the carrier' of A:],[: the carrier' of A, the carrier' of A:]:],[: the carrier' of A, the carrier' of A:]:] is non empty set
CatStr(# [: the carrier of A, the carrier of A:],[: the carrier' of A, the carrier' of A:],[: the Source of A, the Source of A:],[: the Target of A, the Target of A:],|: the Comp of A, the Comp of A:| #) is non empty non void V55() strict CatStr
the carrier' of [:A,A:] is non empty set
{a,b} is non empty finite set
{a} is non empty trivial finite set
{{a,b},{a}} is non empty finite V35() set
[MA,MB] is non empty V15() set
{MA,MB} is non empty finite set
{MA} is non empty trivial finite set
{{MA,MB},{MA}} is non empty finite V35() set
MA is Element of the carrier' of CatStr(# B,OA,AB,MA,MB #)
MB is Element of the carrier' of CatStr(# B,OA,AB,MA,MB #)
[MA,MB] is non empty V15() set
{MA,MB} is non empty finite set
{MA} is non empty trivial finite set
{{MA,MB},{MA}} is non empty finite V35() set
dom MA is Element of the carrier of CatStr(# B,OA,AB,MA,MB #)
the Source of CatStr(# B,OA,AB,MA,MB #) . MA is Element of the carrier of CatStr(# B,OA,AB,MA,MB #)
cod MB is Element of the carrier of CatStr(# B,OA,AB,MA,MB #)
the Target of CatStr(# B,OA,AB,MA,MB #) . MB is Element of the carrier of CatStr(# B,OA,AB,MA,MB #)
a is Element of the carrier' of A
dom a is Element of the carrier of A
the Source of A . a is Element of the carrier of A
b is Element of the carrier' of A
cod b is Element of the carrier of A
the Target of A . b is Element of the carrier of A
MA is Element of the carrier' of CatStr(# B,OA,AB,MA,MB #)
dom MA is Element of the carrier of CatStr(# B,OA,AB,MA,MB #)
the Source of CatStr(# B,OA,AB,MA,MB #) . MA is Element of the carrier of CatStr(# B,OA,AB,MA,MB #)
MB is Element of the carrier' of CatStr(# B,OA,AB,MA,MB #)
cod MB is Element of the carrier of CatStr(# B,OA,AB,MA,MB #)
the Target of CatStr(# B,OA,AB,MA,MB #) . MB is Element of the carrier of CatStr(# B,OA,AB,MA,MB #)
MA (*) MB is Element of the carrier' of CatStr(# B,OA,AB,MA,MB #)
dom (MA (*) MB) is Element of the carrier of CatStr(# B,OA,AB,MA,MB #)
the Source of CatStr(# B,OA,AB,MA,MB #) . (MA (*) MB) is Element of the carrier of CatStr(# B,OA,AB,MA,MB #)
dom MB is Element of the carrier of CatStr(# B,OA,AB,MA,MB #)
the Source of CatStr(# B,OA,AB,MA,MB #) . MB is Element of the carrier of CatStr(# B,OA,AB,MA,MB #)
cod (MA (*) MB) is Element of the carrier of CatStr(# B,OA,AB,MA,MB #)
the Target of CatStr(# B,OA,AB,MA,MB #) . (MA (*) MB) is Element of the carrier of CatStr(# B,OA,AB,MA,MB #)
cod MA is Element of the carrier of CatStr(# B,OA,AB,MA,MB #)
the Target of CatStr(# B,OA,AB,MA,MB #) . MA is Element of the carrier of CatStr(# B,OA,AB,MA,MB #)
[MA,MB] is non empty V15() set
{MA,MB} is non empty finite set
{MA} is non empty trivial finite set
{{MA,MB},{MA}} is non empty finite V35() set
the Comp of CatStr(# B,OA,AB,MA,MB #) . (MA,MB) is set
the Comp of CatStr(# B,OA,AB,MA,MB #) . [MA,MB] is set
a is Element of the carrier' of A
dom a is Element of the carrier of A
the Source of A . a is Element of the carrier of A
b is Element of the carrier' of A
cod b is Element of the carrier of A
the Target of A . b is Element of the carrier of A
[a,b] is non empty V15() Element of the carrier' of [:A,A