:: NATTRA_1 semantic presentation

K149() is Element of bool K145()
K145() is set
bool K145() is non empty set
{} is Relation-like non-empty empty-yielding empty trivial finite finite-yielding V35() set
the Relation-like non-empty empty-yielding empty trivial finite finite-yielding V35() set is Relation-like non-empty empty-yielding empty trivial finite finite-yielding V35() 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
OA is Relation-like A -defined B -valued Function-like quasi_total Element of bool [:A,B:]
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 is Relation-like OA -defined A -valued Function-like quasi_total Element of bool [:OA,A:]
MB is Relation-like AB -defined B -valued Function-like quasi_total Element of bool [:AB,B:]
[: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:]
|:MA,MB:| is Relation-like Function-like set
[: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
MA is Relation-like [:A,A:] -defined A -valued Function-like Element of bool [:[:A,A:],A:]
MA || OA is Relation-like Function-like set
[:OA,OA:] is Relation-like non empty set
MA | [:OA,OA:] is Relation-like [:OA,OA:] -defined [:A,A:] -defined A -valued set
MB is Relation-like [:B,B:] -defined B -valued Function-like Element of bool [:[:B,B:],B:]
MB || AB is Relation-like Function-like 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:]
proj1 OB is Relation-like set
proj1 MA is Relation-like set
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 MB is Relation-like set
proj1 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]} is Relation-like non empty trivial 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]} is Relation-like non empty trivial 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]} is Relation-like non empty trivial 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
1Cat (A,B) is non empty trivial finite non void 1 -element V55() trivial' strict Category-like transitive associative reflexive with_identities CatStr
{A} is non empty trivial finite set
{B} is non empty trivial finite set
K241(B,A) is Relation-like {B} -defined {A} -valued Function-like quasi_total finite Element of bool [:{B},{A}:]
[:{B},{A}:] is Relation-like non empty finite set
bool [:{B},{A}:] is non empty finite V35() set
K240(B,B,B) is Relation-like [:{B},{B}:] -defined {B} -valued Function-like quasi_total finite Element of bool [:[:{B},{B}:],{B}:]
[:{B},{B}:] is Relation-like non empty finite set
[:[:{B},{B}:],{B}:] is Relation-like non empty finite 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))
A is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
the carrier of A is non empty set
[:A,A:] is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
[: 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:]
[:[:A,A:],A:] is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
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
1Cat (A,B) is non empty trivial finite non void 1 -element V55() trivial' strict Category-like transitive associative reflexive with_identities CatStr
{A} is non empty trivial finite set
{B} is non empty trivial finite set
K241(B,A) is Relation-like {B} -defined {A} -valued Function-like quasi_total finite Element of bool [:{B},{A}:]
[:{B},{A}:] is Relation-like non empty finite set
bool [:{B},{A}:] is non empty finite V35() set
K240(B,B,B) is Relation-like [:{B},{B}:] -defined {B} -valued Function-like quasi_total finite Element of bool [:[:{B},{B}:],{B}:]
[:{B},{B}:] is Relation-like non empty finite set
[:[:{B},{B}:],{B}:] is Relation-like non empty finite 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]} is Relation-like non empty trivial 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))
A is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
the carrier of A is non empty set
B is Element of the carrier of A
id B is Morphism of B,B
1Cat (B,(id B)) is non empty trivial finite non void 1 -element V55() trivial' strict Category-like transitive associative reflexive with_identities CatStr
{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
{ b₁ where b₁ is Element of the carrier' of (1Cat (B,(id B))) : ( dom b₁ = OA & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of A : ( dom b₁ = MA & cod b₁ = MB ) } is set
OB is set
OA is set
[:A,A:] is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
[: 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:]
[:[:A,A:],A:] is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
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
A is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
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
B is non empty non void V55() Category-like transitive associative reflexive with_identities Subcategory of A
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:]
[:A,A:] is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
[: 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:]
[:B,B:] is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
[: 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
A is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
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
AB is Relation-like OA -defined B -valued Function-like quasi_total Element of bool [:OA,B:]
MA is Relation-like OA -defined B -valued Function-like quasi_total Element of bool [:OA,B:]
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:]
[:A,A:] is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
[: 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