:: YELLOW21 semantic presentation

K143() is non empty epsilon-transitive epsilon-connected ordinal V33() cardinal limit_cardinal Element of bool K139()

K139() is set

bool K139() is non empty set

omega is non empty epsilon-transitive epsilon-connected ordinal V33() cardinal limit_cardinal set

bool omega is non empty V33() set

{} is set

the Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() cardinal {} -element set is Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() cardinal {} -element set

1 is non empty set

{{},1} is set

bool K143() is non empty V33() set

W is set

1-sorted(# W #) is strict 1-sorted

W is set

a is set

b is set

a is Relation-like Function-like set

dom a is set

b is set

f is set

b1 is strict V57() reflexive transitive antisymmetric RelStr

the InternalRel of b1 is Relation-like the carrier of b1 -defined the carrier of b1 -valued V16( the carrier of b1) quasi_total reflexive antisymmetric transitive Element of bool [: the carrier of b1, the carrier of b1:]

the carrier of b1 is set

[: the carrier of b1, the carrier of b1:] is set

bool [: the carrier of b1, the carrier of b1:] is non empty set

b1 is strict V57() reflexive transitive antisymmetric RelStr

the InternalRel of b1 is Relation-like the carrier of b1 -defined the carrier of b1 -valued V16( the carrier of b1) quasi_total reflexive antisymmetric transitive Element of bool [: the carrier of b1, the carrier of b1:]

the carrier of b1 is set

[: the carrier of b1, the carrier of b1:] is set

bool [: the carrier of b1, the carrier of b1:] is non empty set

dom the InternalRel of b1 is Element of bool the carrier of b1

bool the carrier of b1 is non empty set

a1 is set

b9 is strict V57() reflexive transitive antisymmetric RelStr

the InternalRel of b9 is Relation-like the carrier of b9 -defined the carrier of b9 -valued V16( the carrier of b9) quasi_total reflexive antisymmetric transitive Element of bool [: the carrier of b9, the carrier of b9:]

the carrier of b9 is set

[: the carrier of b9, the carrier of b9:] is set

bool [: the carrier of b9, the carrier of b9:] is non empty set

Union a is set

b is set

f is set

(f) is 1-sorted

the carrier of (f) is set

a1 is set

b1 is strict V57() reflexive transitive antisymmetric RelStr

the InternalRel of b1 is Relation-like the carrier of b1 -defined the carrier of b1 -valued V16( the carrier of b1) quasi_total reflexive antisymmetric transitive Element of bool [: the carrier of b1, the carrier of b1:]

the carrier of b1 is set

[: the carrier of b1, the carrier of b1:] is set

bool [: the carrier of b1, the carrier of b1:] is non empty set

b1 is strict V57() reflexive transitive antisymmetric RelStr

the InternalRel of b1 is Relation-like the carrier of b1 -defined the carrier of b1 -valued V16( the carrier of b1) quasi_total reflexive antisymmetric transitive Element of bool [: the carrier of b1, the carrier of b1:]

the carrier of b1 is set

[: the carrier of b1, the carrier of b1:] is set

bool [: the carrier of b1, the carrier of b1:] is non empty set

b9 is set

a . b9 is set

[:b9,b9:] is set

bool [:b9,b9:] is non empty set

B is Relation-like b9 -defined b9 -valued V16(b9) quasi_total reflexive antisymmetric transitive Element of bool [:b9,b9:]

dom B is Element of bool b9

bool b9 is non empty set

a1 is strict V57() reflexive transitive antisymmetric RelStr

the InternalRel of a1 is Relation-like the carrier of a1 -defined the carrier of a1 -valued V16( the carrier of a1) quasi_total reflexive antisymmetric transitive Element of bool [: the carrier of a1, the carrier of a1:]

the carrier of a1 is set

[: the carrier of a1, the carrier of a1:] is set

bool [: the carrier of a1, the carrier of a1:] is non empty set

a . the carrier of a1 is set

W is non empty set

(W) is set

the Element of W is Element of W

[: the Element of W, the Element of W:] is set

bool [: the Element of W, the Element of W:] is non empty set

the Relation-like the Element of W -defined the Element of W -valued V16( the Element of W) quasi_total reflexive antisymmetric transitive Element of bool [: the Element of W, the Element of W:] is Relation-like the Element of W -defined the Element of W -valued V16( the Element of W) quasi_total reflexive antisymmetric transitive Element of bool [: the Element of W, the Element of W:]

RelStr(# the Element of W, the Relation-like the Element of W -defined the Element of W -valued V16( the Element of W) quasi_total reflexive antisymmetric transitive Element of bool [: the Element of W, the Element of W:] #) is strict V57() reflexive transitive antisymmetric RelStr

(RelStr(# the Element of W, the Relation-like the Element of W -defined the Element of W -valued V16( the Element of W) quasi_total reflexive antisymmetric transitive Element of bool [: the Element of W, the Element of W:] #)) is 1-sorted

W is with_non-empty_elements set

(W) is set

a is set

(a) is 1-sorted

the carrier of (a) is set

b is V57() reflexive transitive antisymmetric RelStr

(b) is 1-sorted

W is non empty transitive V110() with_units reflexive AltCatStr

W is non empty transitive V110() with_units reflexive AltCatStr

the carrier of W is non empty set

a is Relation-like the carrier of W -defined Function-like V16( the carrier of W) set

b is Element of the carrier of W

f is Element of the carrier of W

<^b,f^> is set

the Arrows of W is Relation-like [: the carrier of W, the carrier of W:] -defined Function-like V16([: the carrier of W, the carrier of W:]) set

[: the carrier of W, the carrier of W:] is non empty set

the Arrows of W . (b,f) is set

[b,f] is set

{b,f} is set

{b} is non empty trivial 1 -element set

{{b,f},{b}} is set

the Arrows of W . [b,f] is set

a . b is set

a . f is set

Funcs ((a . b),(a . f)) is functional set

a1 is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

b1 is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

MonFuncs (a1,b1) is set

(f) is 1-sorted

the carrier of b1 is non empty set

(b) is 1-sorted

the carrier of a1 is non empty set

b is Element of the carrier of W

W -carrier_of b is set

idm b is retraction coretraction iso mono epi Element of <^b,b^>

<^b,b^> is non empty set

the Arrows of W is Relation-like [: the carrier of W, the carrier of W:] -defined Function-like V16([: the carrier of W, the carrier of W:]) set

[: the carrier of W, the carrier of W:] is non empty set

the Arrows of W . (b,b) is set

[b,b] is set

{b,b} is set

{b} is non empty trivial 1 -element set

{{b,b},{b}} is set

the Arrows of W . [b,b] is set

dom (idm b) is set

f is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

MonFuncs (f,f) is set

the carrier of f is non empty set

[: the carrier of f, the carrier of f:] is non empty set

bool [: the carrier of f, the carrier of f:] is non empty set

Funcs ( the carrier of f, the carrier of f) is functional non empty FUNCTION_DOMAIN of the carrier of f, the carrier of f

a1 is Relation-like the carrier of f -defined the carrier of f -valued Function-like non empty V16( the carrier of f) quasi_total Element of bool [: the carrier of f, the carrier of f:]

id (W -carrier_of b) is Relation-like W -carrier_of b -defined W -carrier_of b -valued Function-like one-to-one V16(W -carrier_of b) quasi_total Element of bool [:(W -carrier_of b),(W -carrier_of b):]

[:(W -carrier_of b),(W -carrier_of b):] is set

bool [:(W -carrier_of b),(W -carrier_of b):] is non empty set

dom (id (W -carrier_of b)) is Element of bool (W -carrier_of b)

bool (W -carrier_of b) is non empty set

dom a1 is Element of bool the carrier of f

bool the carrier of f is non empty set

F

a is set

[:F

b is set

f is set

[b,f] is set

{b,f} is set

{b} is non empty trivial 1 -element set

{{b,f},{b}} is set

a1 is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

b1 is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

MonFuncs (a1,b1) is set

b9 is set

B is set

a is Relation-like Function-like set

dom a is set

b is set

f is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of f is non empty set

a1 is set

b1 is set

b9 is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of b9 is non empty set

b is Relation-like Function-like set

dom b is set

f is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

a1 is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

[f,a1] is set

{f,a1} is set

{f} is non empty trivial 1 -element set

{{f,a1},{f}} is set

a . [f,a1] is set

b1 is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

b9 is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

[b1,b9] is set

{b1,b9} is set

{b1} is non empty trivial 1 -element set

{{b1,b9},{b1}} is set

MonFuncs (b1,b9) is set

B is set

MonFuncs (f,a1) is set

the carrier of f is non empty set

the carrier of a1 is non empty set

[: the carrier of f, the carrier of a1:] is non empty set

bool [: the carrier of f, the carrier of a1:] is non empty set

Funcs ( the carrier of f, the carrier of a1) is functional non empty FUNCTION_DOMAIN of the carrier of f, the carrier of a1

f1 is Relation-like the carrier of f -defined the carrier of a1 -valued Function-like non empty V16( the carrier of f) quasi_total Element of bool [: the carrier of f, the carrier of a1:]

f1 is Relation-like the carrier of f -defined the carrier of a1 -valued Function-like non empty V16( the carrier of f) quasi_total monotone Element of bool [: the carrier of f, the carrier of a1:]

dom f1 is Element of bool the carrier of f

bool the carrier of f is non empty set

rng f1 is Element of bool the carrier of a1

bool the carrier of a1 is non empty set

f is Element of F

a1 is Element of F

[f,a1] is set

{f,a1} is set

{f} is non empty trivial 1 -element set

{{f,a1},{f}} is set

a . [f,a1] is set

b1 is Element of F

[a1,b1] is set

{a1,b1} is set

{a1} is non empty trivial 1 -element set

{{a1,b1},{a1}} is set

a . [a1,b1] is set

[f,b1] is set

{f,b1} is set

{{f,b1},{f}} is set

a . [f,b1] is set

b9 is Relation-like Function-like set

B is Relation-like Function-like set

b9 * B is Relation-like Function-like set

f2 is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of f2 is non empty set

g2 is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of g2 is non empty set

[: the carrier of f2, the carrier of g2:] is non empty set

bool [: the carrier of f2, the carrier of g2:] is non empty set

f1 is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of f1 is non empty set

[: the carrier of f1, the carrier of f2:] is non empty set

bool [: the carrier of f1, the carrier of f2:] is non empty set

f9 is Relation-like the carrier of f1 -defined the carrier of f2 -valued Function-like non empty V16( the carrier of f1) quasi_total monotone Element of bool [: the carrier of f1, the carrier of f2:]

g1 is Relation-like the carrier of f2 -defined the carrier of g2 -valued Function-like non empty V16( the carrier of f2) quasi_total monotone Element of bool [: the carrier of f2, the carrier of g2:]

g1 * f9 is Relation-like the carrier of f1 -defined the carrier of g2 -valued Function-like non empty V16( the carrier of f1) quasi_total Element of bool [: the carrier of f1, the carrier of g2:]

[: the carrier of f1, the carrier of g2:] is non empty set

bool [: the carrier of f1, the carrier of g2:] is non empty set

[f1,g2] is set

{f1,g2} is set

{f1} is non empty trivial 1 -element set

{{f1,g2},{f1}} is set

a . [f1,g2] is set

f is Element of F

a1 is Element of F

[f,a1] is set

{f,a1} is set

{f} is non empty trivial 1 -element set

{{f,a1},{f}} is set

a . [f,a1] is set

b . f is set

b . a1 is set

Funcs (H

b1 is set

b9 is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of b9 is non empty set

B is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of B is non empty set

Funcs ( the carrier of b9, the carrier of B) is functional non empty FUNCTION_DOMAIN of the carrier of b9, the carrier of B

Funcs ((b . f), the carrier of B) is functional non empty FUNCTION_DOMAIN of b . f, the carrier of B

f is Element of F

b . f is set

id (b . f) is Relation-like b . f -defined b . f -valued Function-like one-to-one V16(b . f) quasi_total Element of bool [:(b . f),(b . f):]

[:(b . f),(b . f):] is set

bool [:(b . f),(b . f):] is non empty set

a1 is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

id a1 is Relation-like the carrier of a1 -defined the carrier of a1 -valued Function-like non empty V16( the carrier of a1) quasi_total monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving Element of bool [: the carrier of a1, the carrier of a1:]

the carrier of a1 is non empty set

[: the carrier of a1, the carrier of a1:] is non empty set

bool [: the carrier of a1, the carrier of a1:] is non empty set

id the carrier of a1 is Relation-like the carrier of a1 -defined the carrier of a1 -valued Function-like one-to-one non empty V16( the carrier of a1) quasi_total Element of bool [: the carrier of a1, the carrier of a1:]

id H

[:H

bool [:H

[f,f] is set

{f,f} is set

{f} is non empty trivial 1 -element set

{{f,f},{f}} is set

a . [f,f] is set

f is non empty transitive strict semi-functional V110() with_units reflexive para-functional set-id-inheriting concrete AltCatStr

the carrier of f is non empty set

the Arrows of f is Relation-like [: the carrier of f, the carrier of f:] -defined Function-like V16([: the carrier of f, the carrier of f:]) set

[: the carrier of f, the carrier of f:] is non empty set

a1 is Element of the carrier of f

a1 is Element of the carrier of f

b1 is Element of the carrier of f

<^a1,b1^> is set

the Arrows of f . (a1,b1) is set

[a1,b1] is set

{a1,b1} is set

{a1} is non empty trivial 1 -element set

{{a1,b1},{a1}} is set

the Arrows of f . [a1,b1] is set

b9 is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

B is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

MonFuncs (b9,B) is set

f1 is set

[b9,B] is set

{b9,B} is set

{b9} is non empty trivial 1 -element set

{{b9,B},{b9}} is set

a . [b9,B] is set

a1 is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of a1 is non empty set

b1 is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of b1 is non empty set

[: the carrier of a1, the carrier of b1:] is non empty set

bool [: the carrier of a1, the carrier of b1:] is non empty set

the Arrows of f . (a1,b1) is set

[a1,b1] is set

{a1,b1} is set

{a1} is non empty trivial 1 -element set

{{a1,b1},{a1}} is set

the Arrows of f . [a1,b1] is set

b9 is Relation-like the carrier of a1 -defined the carrier of b1 -valued Function-like non empty V16( the carrier of a1) quasi_total monotone Element of bool [: the carrier of a1, the carrier of b1:]

dom the Arrows of f is Relation-like the carrier of f -defined the carrier of f -valued Element of bool [: the carrier of f, the carrier of f:]

bool [: the carrier of f, the carrier of f:] is non empty set

B is Element of the carrier of f

f1 is Element of the carrier of f

<^B,f1^> is set

the Arrows of f . (B,f1) is set

[B,f1] is set

{B,f1} is set

{B} is non empty trivial 1 -element set

{{B,f1},{B}} is set

the Arrows of f . [B,f1] is set

a . [B,f1] is set

B is Element of the carrier of f

f1 is Element of the carrier of f

<^B,f1^> is set

the Arrows of f . (B,f1) is set

[B,f1] is set

{B,f1} is set

{B} is non empty trivial 1 -element set

{{B,f1},{B}} is set

the Arrows of f . [B,f1] is set

a . [B,f1] is set

the non empty V57() reflexive transitive antisymmetric lower-bounded upper-bounded V121() with_suprema with_infima complete up-complete /\-complete RelStr is non empty V57() reflexive transitive antisymmetric lower-bounded upper-bounded V121() with_suprema with_infima complete up-complete /\-complete RelStr

{ the non empty V57() reflexive transitive antisymmetric lower-bounded upper-bounded V121() with_suprema with_infima complete up-complete /\-complete RelStr } is non empty trivial 1 -element set

a is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of a is non empty set

b is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of b is non empty set

[: the carrier of a, the carrier of b:] is non empty set

bool [: the carrier of a, the carrier of b:] is non empty set

f is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of f is non empty set

[: the carrier of b, the carrier of f:] is non empty set

bool [: the carrier of b, the carrier of f:] is non empty set

a1 is Relation-like the carrier of a -defined the carrier of b -valued Function-like non empty V16( the carrier of a) quasi_total Element of bool [: the carrier of a, the carrier of b:]

b1 is Relation-like the carrier of b -defined the carrier of f -valued Function-like non empty V16( the carrier of b) quasi_total Element of bool [: the carrier of b, the carrier of f:]

b1 * a1 is Relation-like the carrier of a -defined the carrier of f -valued Function-like non empty V16( the carrier of a) quasi_total Element of bool [: the carrier of a, the carrier of f:]

[: the carrier of a, the carrier of f:] is non empty set

bool [: the carrier of a, the carrier of f:] is non empty set

a is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

id a is Relation-like the carrier of a -defined the carrier of a -valued Function-like non empty V16( the carrier of a) quasi_total monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving Element of bool [: 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 non empty set

bool [: the carrier of a, the carrier of a:] is non empty set

id the carrier of a is Relation-like the carrier of a -defined the carrier of a -valued Function-like one-to-one non empty V16( the carrier of a) quasi_total Element of bool [: the carrier of a, the carrier of a:]

a is Element of { the non empty V57() reflexive transitive antisymmetric lower-bounded upper-bounded V121() with_suprema with_infima complete up-complete /\-complete RelStr }

a is non empty transitive strict V110() with_units reflexive AltCatStr

the carrier of a is non empty set

the Arrows of a is Relation-like [: the carrier of a, the carrier of a:] -defined Function-like V16([: the carrier of a, the carrier of a:]) set

[: the carrier of a, the carrier of a:] is non empty set

b is Element of the carrier of a

W is non empty transitive V110() with_units reflexive () AltCatStr

the carrier of W is non empty set

a is Element of the carrier of W

W -carrier_of a is set

idm a is retraction coretraction iso mono epi Element of <^a,a^>

<^a,a^> is non empty set

the Arrows of W is Relation-like [: the carrier of W, the carrier of W:] -defined Function-like V16([: the carrier of W, the carrier of W:]) set

[: the carrier of W, the carrier of W:] is non empty set

the Arrows of W . (a,a) is set

[a,a] is set

{a,a} is set

{a} is non empty trivial 1 -element set

{{a,a},{a}} is set

the Arrows of W . [a,a] is set

dom (idm a) is set

(a) is 1-sorted

the carrier of (a) is set

b is 1-sorted

the carrier of b is set

W is non empty transitive V110() with_units reflexive set-id-inheriting () AltCatStr

the carrier of W is non empty set

a is Element of the carrier of W

idm a is retraction coretraction iso mono epi Element of <^a,a^>

<^a,a^> is non empty set

the Arrows of W is Relation-like [: the carrier of W, the carrier of W:] -defined Function-like V16([: the carrier of W, the carrier of W:]) set

[: the carrier of W, the carrier of W:] is non empty set

the Arrows of W . (a,a) is set

[a,a] is set

{a,a} is set

{a} is non empty trivial 1 -element set

{{a,a},{a}} is set

the Arrows of W . [a,a] is set

(a) is 1-sorted

id (a) is Relation-like the carrier of (a) -defined the carrier of (a) -valued Function-like V16( the carrier of (a)) quasi_total Element of bool [: the carrier of (a), the carrier of (a):]

the carrier of (a) is set

[: the carrier of (a), the carrier of (a):] is set

bool [: the carrier of (a), the carrier of (a):] is non empty set

id the carrier of (a) is Relation-like the carrier of (a) -defined the carrier of (a) -valued Function-like one-to-one V16( the carrier of (a)) quasi_total Element of bool [: the carrier of (a), the carrier of (a):]

W -carrier_of a is set

dom (idm a) is set

b is 1-sorted

the carrier of b is set

W is non empty transitive semi-functional V110() with_units reflexive para-functional set-id-inheriting concrete () () AltCatStr

the carrier of W is non empty set

W is non empty transitive semi-functional V110() with_units reflexive para-functional set-id-inheriting concrete () () AltCatStr

the carrier of W is non empty set

a is Element of the carrier of W

(a) is 1-sorted

b is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

f is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

W is non empty transitive semi-functional V110() with_units reflexive para-functional set-id-inheriting concrete () () () AltCatStr

the carrier of W is non empty set

W is non empty transitive semi-functional V110() with_units reflexive para-functional set-id-inheriting concrete () () () AltCatStr

the carrier of W is non empty set

a is Element of the carrier of W

(a) is 1-sorted

W is non empty transitive semi-functional V110() with_units reflexive para-functional set-id-inheriting concrete () () AltCatStr

the carrier of W is non empty set

a is Element of the carrier of W

b is Element of the carrier of W

<^a,b^> is set

the Arrows of W is Relation-like [: the carrier of W, the carrier of W:] -defined Function-like V16([: the carrier of W, the carrier of W:]) set

[: the carrier of W, the carrier of W:] is non empty set

the Arrows of W . (a,b) is set

[a,b] is set

{a,b} is set

{a} is non empty trivial 1 -element set

{{a,b},{a}} is set

the Arrows of W . [a,b] is set

f is Relation-like Function-like Element of <^a,b^>

(W,a) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of (W,a) is non empty set

(W,b) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of (W,b) is non empty set

[: the carrier of (W,a), the carrier of (W,b):] is non empty set

bool [: the carrier of (W,a), the carrier of (W,b):] is non empty set

MonFuncs ((W,a),(W,b)) is set

Funcs ( the carrier of (W,a), the carrier of (W,b)) is functional non empty FUNCTION_DOMAIN of the carrier of (W,a), the carrier of (W,b)

a1 is Relation-like the carrier of (W,a) -defined the carrier of (W,b) -valued Function-like non empty V16( the carrier of (W,a)) quasi_total Element of bool [: the carrier of (W,a), the carrier of (W,b):]

W is non empty transitive semi-functional V110() with_units reflexive para-functional set-id-inheriting concrete () () AltCatStr

the carrier of W is non empty set

a is Element of the carrier of W

b is Element of the carrier of W

<^a,b^> is set

the Arrows of W is Relation-like [: the carrier of W, the carrier of W:] -defined Function-like V16([: the carrier of W, the carrier of W:]) set

[: the carrier of W, the carrier of W:] is non empty set

the Arrows of W . (a,b) is set

[a,b] is set

{a,b} is set

{a} is non empty trivial 1 -element set

{{a,b},{a}} is set

the Arrows of W . [a,b] is set

f is Element of the carrier of W

<^b,f^> is set

the Arrows of W . (b,f) is set

[b,f] is set

{b,f} is set

{b} is non empty trivial 1 -element set

{{b,f},{b}} is set

the Arrows of W . [b,f] is set

(W,a) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of (W,a) is non empty set

(W,b) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of (W,b) is non empty set

(W,f) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of (W,f) is non empty set

a1 is Relation-like Function-like Element of <^a,b^>

(W,a,b,a1) is Relation-like the carrier of (W,a) -defined the carrier of (W,b) -valued Function-like non empty V16( the carrier of (W,a)) quasi_total monotone Element of bool [: the carrier of (W,a), the carrier of (W,b):]

[: the carrier of (W,a), the carrier of (W,b):] is non empty set

bool [: the carrier of (W,a), the carrier of (W,b):] is non empty set

b1 is Relation-like Function-like Element of <^b,f^>

b1 * a1 is Relation-like Function-like Element of <^a,f^>

<^a,f^> is set

the Arrows of W . (a,f) is set

[a,f] is set

{a,f} is set

{{a,f},{a}} is set

the Arrows of W . [a,f] is set

(W,b,f,b1) is Relation-like the carrier of (W,b) -defined the carrier of (W,f) -valued Function-like non empty V16( the carrier of (W,b)) quasi_total monotone Element of bool [: the carrier of (W,b), the carrier of (W,f):]

[: the carrier of (W,b), the carrier of (W,f):] is non empty set

bool [: the carrier of (W,b), the carrier of (W,f):] is non empty set

(W,b,f,b1) * (W,a,b,a1) is Relation-like the carrier of (W,a) -defined the carrier of (W,f) -valued Function-like non empty V16( the carrier of (W,a)) quasi_total Element of bool [: the carrier of (W,a), the carrier of (W,f):]

[: the carrier of (W,a), the carrier of (W,f):] is non empty set

bool [: the carrier of (W,a), the carrier of (W,f):] is non empty set

F

W is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

id W is Relation-like the carrier of W -defined the carrier of W -valued Function-like non empty V16( the carrier of W) quasi_total monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving Element of bool [: the carrier of W, the carrier of W:]

the carrier of W is non empty set

[: the carrier of W, the carrier of W:] is non empty set

bool [: the carrier of W, the carrier of W:] is non empty set

id the carrier of W is Relation-like the carrier of W -defined the carrier of W -valued Function-like one-to-one non empty V16( the carrier of W) quasi_total Element of bool [: the carrier of W, the carrier of W:]

W is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of W is non empty set

a is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of a is non empty set

[: the carrier of W, the carrier of a:] is non empty set

bool [: the carrier of W, the carrier of a:] is non empty set

b is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of b is non empty set

[: the carrier of a, the carrier of b:] is non empty set

bool [: the carrier of a, the carrier of b:] is non empty set

f is Relation-like the carrier of W -defined the carrier of a -valued Function-like non empty V16( the carrier of W) quasi_total Element of bool [: the carrier of W, the carrier of a:]

a1 is Relation-like the carrier of a -defined the carrier of b -valued Function-like non empty V16( the carrier of a) quasi_total Element of bool [: the carrier of a, the carrier of b:]

a1 * f is Relation-like the carrier of W -defined the carrier of b -valued Function-like non empty V16( the carrier of W) quasi_total Element of bool [: the carrier of W, the carrier of b:]

[: the carrier of W, the carrier of b:] is non empty set

bool [: the carrier of W, the carrier of b:] is non empty set

W is non empty transitive strict V110() with_units reflexive AltCatStr

the carrier of W is non empty set

the Arrows of W is Relation-like [: the carrier of W, the carrier of W:] -defined Function-like V16([: the carrier of W, the carrier of W:]) set

[: the carrier of W, the carrier of W:] is non empty set

a is non empty transitive strict semi-functional V110() with_units reflexive para-functional set-id-inheriting concrete () () AltCatStr

the carrier of a is non empty set

b is Element of the carrier of a

(a,b) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of (a,b) is non empty set

f is Element of the carrier of a

(a,f) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of (a,f) is non empty set

[: the carrier of (a,b), the carrier of (a,f):] is non empty set

bool [: the carrier of (a,b), the carrier of (a,f):] is non empty set

<^b,f^> is set

the Arrows of a is Relation-like [: the carrier of a, the carrier of a:] -defined Function-like V16([: the carrier of a, the carrier of a:]) set

[: the carrier of a, the carrier of a:] is non empty set

the Arrows of a . (b,f) is set

[b,f] is set

{b,f} is set

{b} is non empty trivial 1 -element set

{{b,f},{b}} is set

the Arrows of a . [b,f] is set

a1 is Relation-like the carrier of (a,b) -defined the carrier of (a,f) -valued Function-like non empty V16( the carrier of (a,b)) quasi_total monotone Element of bool [: the carrier of (a,b), the carrier of (a,f):]

b1 is Relation-like the carrier of (a,b) -defined the carrier of (a,f) -valued Function-like non empty V16( the carrier of (a,b)) quasi_total monotone Element of bool [: the carrier of (a,b), the carrier of (a,f):]

F

(F

W is set

a is non empty strict V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of a is non empty set

a is non empty strict V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of a is non empty set

(a) is 1-sorted

f is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

b is non empty set

a1 is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

b1 is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of f is non empty set

the carrier of a1 is non empty set

[: the carrier of f, the carrier of a1:] is non empty set

bool [: the carrier of f, the carrier of a1:] is non empty set

the carrier of b1 is non empty set

[: the carrier of a1, the carrier of b1:] is non empty set

bool [: the carrier of a1, the carrier of b1:] is non empty set

b9 is Relation-like the carrier of f -defined the carrier of a1 -valued Function-like non empty V16( the carrier of f) quasi_total Element of bool [: the carrier of f, the carrier of a1:]

B is Relation-like the carrier of a1 -defined the carrier of b1 -valued Function-like non empty V16( the carrier of a1) quasi_total Element of bool [: the carrier of a1, the carrier of b1:]

B * b9 is Relation-like the carrier of f -defined the carrier of b1 -valued Function-like non empty V16( the carrier of f) quasi_total Element of bool [: the carrier of f, the carrier of b1:]

[: the carrier of f, the carrier of b1:] is non empty set

bool [: the carrier of f, the carrier of b1:] is non empty set

f is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

id f is Relation-like the carrier of f -defined the carrier of f -valued Function-like non empty V16( the carrier of f) quasi_total monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving Element of bool [: the carrier of f, the carrier of f:]

the carrier of f is non empty set

[: the carrier of f, the carrier of f:] is non empty set

bool [: the carrier of f, the carrier of f:] is non empty set

id the carrier of f is Relation-like the carrier of f -defined the carrier of f -valued Function-like one-to-one non empty V16( the carrier of f) quasi_total Element of bool [: the carrier of f, the carrier of f:]

f is Element of b

f is non empty transitive strict semi-functional V110() with_units reflexive para-functional set-id-inheriting concrete () () AltCatStr

the carrier of f is non empty set

a1 is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

(a1) is 1-sorted

the carrier of a1 is non empty set

a1 is Element of the carrier of f

(f,a1) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of (f,a1) is non empty set

b1 is Element of the carrier of f

(f,b1) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of (f,b1) is non empty set

[: the carrier of (f,a1), the carrier of (f,b1):] is non empty set

bool [: the carrier of (f,a1), the carrier of (f,b1):] is non empty set

B is Element of the carrier of f

(f,B) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of (f,B) is non empty set

f1 is Element of the carrier of f

(f,f1) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of (f,f1) is non empty set

[: the carrier of (f,B), the carrier of (f,f1):] is non empty set

bool [: the carrier of (f,B), the carrier of (f,f1):] is non empty set

b9 is Relation-like the carrier of (f,a1) -defined the carrier of (f,b1) -valued Function-like non empty V16( the carrier of (f,a1)) quasi_total monotone Element of bool [: the carrier of (f,a1), the carrier of (f,b1):]

<^a1,b1^> is set

the Arrows of f is Relation-like [: the carrier of f, the carrier of f:] -defined Function-like V16([: the carrier of f, the carrier of f:]) set

[: the carrier of f, the carrier of f:] is non empty set

the Arrows of f . (a1,b1) is set

[a1,b1] is set

{a1,b1} is set

{a1} is non empty trivial 1 -element set

{{a1,b1},{a1}} is set

the Arrows of f . [a1,b1] is set

f2 is Relation-like the carrier of (f,B) -defined the carrier of (f,f1) -valued Function-like non empty V16( the carrier of (f,B)) quasi_total monotone Element of bool [: the carrier of (f,B), the carrier of (f,f1):]

<^B,f1^> is set

the Arrows of f . (B,f1) is set

[B,f1] is set

{B,f1} is set

{B} is non empty trivial 1 -element set

{{B,f1},{B}} is set

the Arrows of f . [B,f1] is set

F

W is non empty transitive semi-functional V110() with_units reflexive para-functional set-id-inheriting concrete () () AltCatStr

the carrier of W is non empty set

a is non empty transitive semi-functional V110() with_units reflexive para-functional set-id-inheriting concrete () () AltCatStr

the carrier of a is non empty set

the Arrows of W is Relation-like [: the carrier of W, the carrier of W:] -defined Function-like V16([: the carrier of W, the carrier of W:]) set

[: the carrier of W, the carrier of W:] is non empty set

the Comp of W is Relation-like [: the carrier of W, the carrier of W, the carrier of W:] -defined Function-like V16([: the carrier of W, the carrier of W, the carrier of W:]) M21([: the carrier of W, the carrier of W, the carrier of W:],{| the Arrows of W, the Arrows of W|},{| the Arrows of W|})

[: the carrier of W, the carrier of W, the carrier of W:] is non empty set

{| the Arrows of W, the Arrows of W|} is Relation-like [: the carrier of W, the carrier of W, the carrier of W:] -defined Function-like V16([: the carrier of W, the carrier of W, the carrier of W:]) set

{| the Arrows of W|} is Relation-like [: the carrier of W, the carrier of W, the carrier of W:] -defined Function-like V16([: the carrier of W, the carrier of W, the carrier of W:]) set

AltCatStr(# the carrier of W, the Arrows of W, the Comp of W #) is strict AltCatStr

the Arrows of a is Relation-like [: the carrier of a, the carrier of a:] -defined Function-like V16([: the carrier of a, the carrier of a:]) set

[: the carrier of a, the carrier of a:] is non empty set

the Comp of a is Relation-like [: the carrier of a, the carrier of a, the carrier of a:] -defined Function-like V16([: the carrier of a, the carrier of a, the carrier of a:]) M21([: the carrier of a, the carrier of a, the carrier of a:],{| the Arrows of a, the Arrows of a|},{| the Arrows of a|})

[: the carrier of a, the carrier of a, the carrier of a:] is non empty set

{| the Arrows of a, the Arrows of a|} is Relation-like [: the carrier of a, the carrier of a, the carrier of a:] -defined Function-like V16([: the carrier of a, the carrier of a, the carrier of a:]) set

{| the Arrows of a|} is Relation-like [: the carrier of a, the carrier of a, the carrier of a:] -defined Function-like V16([: the carrier of a, the carrier of a, the carrier of a:]) set

AltCatStr(# the carrier of a, the Arrows of a, the Comp of a #) is strict AltCatStr

b is Element of the carrier of a

f is Element of the carrier of a

a1 is Element of the carrier of W

b1 is Element of the carrier of W

<^a1,b1^> is set

the Arrows of W . (a1,b1) is set

[a1,b1] is set

{a1,b1} is set

{a1} is non empty trivial 1 -element set

{{a1,b1},{a1}} is set

the Arrows of W . [a1,b1] is set

<^b,f^> is set

the Arrows of a . (b,f) is set

[b,f] is set

{b,f} is set

{b} is non empty trivial 1 -element set

{{b,f},{b}} is set

the Arrows of a . [b,f] is set

the Arrows of W . (b,f) is set

the Arrows of W . [b,f] is set

b9 is set

B is Relation-like Function-like Element of <^b,f^>

(a,b,f,B) is Relation-like the carrier of (a,b) -defined the carrier of (a,f) -valued Function-like non empty V16( the carrier of (a,b)) quasi_total monotone Element of bool [: the carrier of (a,b), the carrier of (a,f):]

(a,b) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of (a,b) is non empty set

(a,f) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of (a,f) is non empty set

[: the carrier of (a,b), the carrier of (a,f):] is non empty set

bool [: the carrier of (a,b), the carrier of (a,f):] is non empty set

(W,a1) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

(W,b1) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr

b9 is set

B is Relation-like Function-like Element of <^a1,b1^>

(W,a1,b1,B) is Relation-like the carrier of (W,a1) -defined the carrier of (W,b1) -valued Function-like non empty V16( the carrier of (W,a1)) quasi_total monotone Element of bool [: the carrier of (W,a1), the carrier of (W,b1):]

the carrier of (W,a1) is non empty set

the carrier of (W,b1) is non empty set

[: the carrier of (W,a1), the carrier of (W,b1):] is non empty set

bool [: the carrier of (W,a1), the carrier of (W,b1):] is non empty set

b is Element of the carrier of W

f is Element of the carrier of W

<^b,f^> is set

the Arrows of W . (b,f) is set

[b,f] is set

{b,f} is set

{b} is non empty trivial 1 -element set

{{b,f},{b}} is set

the Arrows of W . [b,f] is set

F

W is non empty transitive semi-functional V110() with_units reflexive para-functional set-id-inheriting concrete () () AltCatStr

the carrier of W is non empty set

a is non empty transitive semi-functional V110() with_units reflexive para-functional set-id-inheriting concrete () () AltCatStr

the carrier of a is non empty set

the Arrows of W is Relation-like [: the carrier of W, the carrier of W:] -defined Function-like V16([: the carrier of W, the carrier of W:]) set

[: the carrier of W, the carrier of W:] is non empty set

the Comp of W is Relation-like [: the carrier of W, the carrier of W, the carrier of W:] -defined Function-like V16([: the carrier of W, the carrier of W, the carrier of W:]) M21([: the carrier of W, the carrier of W, the carrier of W:],{| the Arrows of W, the Arrows of W|},{| the Arrows of W|})

[: the carrier of W, the carrier of W, the carrier of W:] is non empty set

{| the Arrows of W, the Arrows of W|} is Relation-like [: the carrier of W, the carrier of W, the carrier of W:] -defined Function-like V16([: the carrier of W, the carrier of W, the carrier of W:]) set

{| the Arrows of W|} is Relation-like [: the carrier of W, the carrier of W, the carrier of W:] -defined Function-like V16([: the carrier of W, the carrier of W, the carrier of W:]) set

AltCatStr(# the carrier of W, the Arrows of W, the Comp of W #) is strict AltCatStr

the Arrows of a is Relation-like [: the carrier of a, the carrier of a:] -defined Function-like V16([: the carrier of a, the carrier of a:]) set

[: the carrier of a, the carrier of a:] is non empty set

the Comp of a is Relation-like [: the carrier of a, the carrier of a, the carrier of a:] -defined Function-like V16([: the carrier of a, the carrier of a, the carrier of a:]) M21([: the carrier of a, the carrier of a, the carrier of a:],{| the Arrows of a, the Arrows of a|},{| the Arrows of a|})

[: the carrier of a, the carrier of a, the carrier of a:] is non empty set

{| the Arrows of a, the Arrows of a|} is Relation-like [: the carrier of a, the carrier of a, the carrier of a:] -defined Function-like V16([: the carrier of a, the carrier of a, the carrier of a:]) set

{| the Arrows of a|} is Relation-like [: the carrier of a, the carrier of a, the carrier of a:] -defined Function-like V16([: the carrier of a, the carrier of a, the carrier of a:]) set

AltCatStr(# the carrier of a, the Arrows of a, the Comp of a #) is strict AltCatStr

b is set

(b) is 1-sorted

the carrier of (b) is set

b is set

(b) is 1-sorted

the carrier of (b) is set

F

the Arrows of F

the carrier of F

[: the carrier of F

F

the Arrows of F

the carrier of F

[: the carrier of F

W is Element of the carrier of F

a is Element of the carrier of F

<^W,a^> is set

the Arrows of F

[W,a] is set

{W,a} is set

{W} is non empty trivial 1 -element set

{{W,a},{W}} is set

the Arrows of F

F

F

the Arrows of F

[F

{F

{F

{{F

the Arrows of F

b is Relation-like Function-like Element of <^W,a^>

F

(F

(F

the carrier of (F

(F

the carrier of (F

[: the carrier of (F

bool [: the carrier of (F

the carrier of F

the carrier of F

[: the carrier of F

bool [: the carrier of F

W is Element of the carrier of F

a is Element of the carrier of F

<^W,a^> is set

the Arrows of F

[W,a] is set

{W,a} is set

{W} is non empty trivial 1 -element set

{{W,a},{W}} is set

the Arrows of F

b is Element of the carrier of F

<^a,b^> is set

the Arrows of F

[a,b] is set

{a,b} is set

{a} is non empty trivial 1 -element set

{{a,b},{a}} is set

the Arrows of F

b1 is Element of the carrier of F

F

b9 is Element of the carrier of F

F

B is Element of the carrier of F

F

<^b1,b9^> is set

the Arrows of F

[b1,b9] is set

{b1,b9} is set

{b1} is non empty trivial 1 -element set

{{b1,b9},{b1}} is set

the Arrows of F

<^b9,B^> is set

the Arrows of F

[b9,B] is set

{b9,B} is set

{b9} is non empty trivial 1 -element set

{{b9,B},{b9}} is set

the Arrows of F

f1 is Relation-like Function-like Element of <^b1,b9^>

f is Relation-like Function-like Element of <^W,a^>

F

f2 is Relation-like Function-like Element of <^b9,B^>

a1 is Relation-like Function-like Element of <^a,b^>

F

the Arrows of F

[F

{F

{F

{{F

the Arrows of F

(F

(F

the carrier of (F

(F

the carrier of (F

[: the carrier of (F

bool [: the carrier of (F

(F

(F

the carrier of (F

(F

the carrier of (F

[: the carrier of (F

bool [: the carrier of (F

the Arrows of F

[F

{F

{F

{{F

the Arrows of F

(F

(F

the carrier of (F

[: the carrier of (F

bool [: the carrier of (F

(F

(F

the carrier of (F

[: the carrier of (F

bool [: the carrier of (F

(F

[: the carrier of (F

bool [: the carrier of (F

F

F

f2 * f1 is Relation-like Function-like Element of <^b1,B^>

<^b1,B^> is set

the Arrows of F

[b1,B] is set

{b1,B} is set

{{b1,B},{b1}} is set

the Arrows of F

a1 * f is Relation-like Function-like Element of <^W,b^>

<^W,b^> is set

the Arrows of F

[W,b] is set

{W,b} is set

{{W,b},{W}} is set

the Arrows of F

F

a is Element of the carrier of F

W is Element of the carrier of F

F

idm W is Relation-like Function-like retraction coretraction iso mono epi Element of <^W,W^>

<^W,W^> is non empty set

the Arrows of F

[W,W] is set

{W,W} is set

{W} is non empty trivial 1 -element set

{{W,W},{W}} is set

the Arrows of F

(F

id (F

the carrier of (F

[: the carrier of (F

bool [: the carrier of (F

id the carrier of (F

F

(F

id (F

the carrier of (F

[: the carrier of (F

bool [: the carrier of (F

id the carrier of (F

idm a is Relation-like Function-like retraction coretraction iso mono epi Element of <^a,a^>

<^a,a^> is non empty set

the Arrows of F

[a,a] is set

{a,a} is set

{a} is non empty trivial 1 -element set

{{a,a},{a}} is set

the Arrows of F

W is Element of the carrier of F

F

W is reflexive V149(F

a is Element of the carrier of F

W . a is Element of the carrier of F

(F

F

a is Element of the carrier of F

b is Element of the carrier of F

<^a,b^> is set

the Arrows of F

[a,b] is set

{a,b} is set

{a} is non empty trivial 1 -element set

{{a,b},{a}} is set

the Arrows of F

(F

(F

f is Relation-like Function-like Element of <^a,b^>

W . f is Relation-like Function-like Element of <^(W . a),(W . b)^>

W . a is Element of the carrier of F

W . b is Element of the carrier of F

<^(W . a),(W . b)^> is set

the Arrows of F

[(W . a),(W . b)] is set

{(W . a),(W . b)} is set

{(W . a)} is non empty trivial 1 -element set

{{(W . a),(W . b)},{(W . a)}} is set

the Arrows of F

(F

the carrier of (F

the carrier of (F

[: the carrier of (F

bool [: the carrier of (F

F

F

the Arrows of F

the carrier of F

[: the carrier of F

F

the Arrows of F

the carrier of F

[: the carrier of F

W is Element of the carrier of F

a is Element of the carrier of F

<^W,a^> is set

the Arrows of F

[W,a] is set

{W,a} is set

{W} is non empty trivial 1 -element set

{{W,a},{W}} is set

the Arrows of F

F

F

the Arrows of F

[F

{F

{F

{{F

the Arrows of F

b is Relation-like Function-like Element of <^W,a^>

F

(F

(F

the carrier of (F

(F

the carrier of (F

[: the carrier of (F

bool [: the carrier of (F

the carrier of F

the carrier of F

[: the carrier of F

bool [: the carrier of F

W is Element of the carrier of F

a is Element of the carrier of F

<^W,a^> is set

the Arrows of F

[W,a] is set

{W,a} is set

{W} is non empty trivial 1 -element set

{{W,a},{W}} is set

the Arrows of F

b is Element of the carrier of F

<^a,b^> is set

the Arrows of F

[a,b] is set

{a,b} is set

{a} is non empty trivial 1 -element set

{{a,b},{a}} is set

the Arrows of F

b1 is Element of the carrier of F

F

b9 is Element of the carrier of F

F

B is Element of the carrier of F

F

<^b9,b1^> is set

the Arrows of F

[b9,b1] is set

{b9,b1} is set

{b9} is non empty trivial 1 -element set

{{b9,b1},{b9}} is set

the Arrows of F

<^B,b9^> is set

the Arrows of F

[B,b9] is set

{B,b9} is set

{B} is non empty trivial 1 -element set

{{B,b9},{B}} is set

the Arrows of F

f1 is Relation-like Function-like Element of <^b9,b1^>

f is Relation-like Function-like Element of <^W,a^>

F

f2 is Relation-like Function-like Element of <^B,b9^>

a1 is Relation-like Function-like Element of <^a,b^>

F

the Arrows of F

[F

{F

{F

{{F

the Arrows of F

(F

(F

the carrier of (F

(F

the carrier of (F

[: the carrier of (F

bool [: the carrier of (F

(F

(F

the carrier of (F

(F

the carrier of (F

[: the carrier of (F

bool [: the carrier of (F

the Arrows of F

[F

{F

{F

{{F

the Arrows of F

(F

(F

the carrier of (F

[: the carrier of (F

bool [: the carrier of (F

(F

(F

the carrier of (F

[: the carrier of (F

bool [: the carrier of (F

(F

[: the carrier of (F

bool [: the carrier of (F

F

F

f1 * f2 is Relation-like Function-like Element of <^B,b1^>

<^B,b1^> is set

the Arrows of F

[B,b1] is set

{B,b1} is set

{{B,b1},{B}} is set

the Arrows of F

a1 * f is Relation-like Function-like Element of <^W,b^>

<^W,b^> is set

the Arrows of F

[W,b] is set

{W,b} is set

{{W,b},{W}} is set

the Arrows of F

F

a is Element of the carrier of F

W is Element of the carrier of F

F

idm W is Relation-like Function-like retraction coretraction iso mono epi Element of <^W,W^>

<^W,W^> is non empty set

the Arrows of F

[W,W] is set

{W,W} is set

{W} is non empty trivial 1 -element set

{{W,W},{W}} is set

the Arrows of F

(F

id (F

the carrier of (F

[: the carrier of (F

bool [: the carrier of (F

id the carrier of (F

F

(F

id (F

the carrier of (F

[: the carrier of (F

bool [: the carrier of (F

id the carrier of (F

idm a is Relation-like Function-like retraction coretraction iso mono epi Element of <^a,a^>

<^a,a^> is non empty set

the Arrows of F

[a,a] is set

{a,a} is set

{a} is non empty trivial 1 -element set

{{a,a},{a}} is set

the Arrows of F

W is Element of the carrier of F

F

W is reflexive V149(F

a is Element of the carrier of F

W . a is Element of the carrier of F

(F

F

a is Element of the carrier of F

b is Element of the carrier of F

<^a,b^> is set

the Arrows of F

[a,b] is set

{a,b} is set

{a} is non empty trivial 1 -element set

{{a,b},{a}} is set

the Arrows of F

(F

(F

f is Relation-like Function-like Element of <^a,b^>

W . f is Relation-like Function-like Element of <^(W . b),(W . a)^>

W . b is Element of the carrier of F

W . a is Element of the carrier of F

<^(W . b),(W . a)^> is set

the Arrows of F

[(W . b),(W . a)] is set

{(W . b),(W . a)} is set

{(W . b)} is non empty trivial 1 -element set

{{(W . b),(W . a)},{(W . b)}} is set

the Arrows of F

(F

the carrier of (F

the carrier of (F

[: the carrier of (F

bool [: the carrier of (F

F

F

the Arrows of F

the carrier of F

[: the carrier of F

F

the Arrows of F

the carrier of F

[: the carrier of F

W is Element of the carrier of F

F

a is Element of the carrier of F

F

(F

(F

W is Element of the carrier of F

a is Element of the carrier of F

<^W,a^> is set

the Arrows of F

[W,a] is set

{W,a} is set

{W} is non empty trivial 1 -element set

{{W,a},{W}