:: 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

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

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