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
F1() is non empty set
a is set
[:F1(),F1():] is non empty set
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 F1()
a1 is Element of F1()
[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 F1()
[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 F1()
a1 is Element of F1()
[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 (H2(f),H2(a1)) is functional 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 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 F1()
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 H2(f) is Relation-like H2(f) -defined H2(f) -valued Function-like one-to-one V16(H2(f)) quasi_total Element of bool [:H2(f),H2(f):]
[:H2(f),H2(f):] is set
bool [:H2(f),H2(f):] is non empty set
[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
F1() is non empty set
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):]
F1() is non empty set
(F1()) is non empty set
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
F1() 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 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
F1() 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 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
F1() is non empty transitive semi-functional V110() with_units reflexive para-functional set-id-inheriting concrete () () AltCatStr
the Arrows of F1() is Relation-like [: the carrier of F1(), the carrier of F1():] -defined Function-like V16([: the carrier of F1(), the carrier of F1():]) set
the carrier of F1() is non empty set
[: the carrier of F1(), the carrier of F1():] is non empty set
F2() is non empty transitive semi-functional V110() with_units reflexive para-functional set-id-inheriting concrete () () AltCatStr
the Arrows of F2() is Relation-like [: the carrier of F2(), the carrier of F2():] -defined Function-like V16([: the carrier of F2(), the carrier of F2():]) set
the carrier of F2() is non empty set
[: the carrier of F2(), the carrier of F2():] is non empty set
W is Element of the carrier of F1()
a is Element of the carrier of F1()
<^W,a^> is set
the Arrows of F1() . (W,a) is set
[W,a] is set
{W,a} is set
{W} is non empty trivial 1 -element set
{{W,a},{W}} is set
the Arrows of F1() . [W,a] is set
F3(W) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
F3(a) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the Arrows of F2() . (F3(W),F3(a)) is set
[F3(W),F3(a)] is set
{F3(W),F3(a)} is set
{F3(W)} is non empty trivial 1 -element set
{{F3(W),F3(a)},{F3(W)}} is set
the Arrows of F2() . [F3(W),F3(a)] is set
b is Relation-like Function-like Element of <^W,a^>
F4(W,a,b) is Relation-like Function-like set
(F1(),W,a,b) is Relation-like the carrier of (F1(),W) -defined the carrier of (F1(),a) -valued Function-like non empty V16( the carrier of (F1(),W)) quasi_total monotone Element of bool [: the carrier of (F1(),W), the carrier of (F1(),a):]
(F1(),W) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (F1(),W) is non empty set
(F1(),a) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (F1(),a) is non empty set
[: the carrier of (F1(),W), the carrier of (F1(),a):] is non empty set
bool [: the carrier of (F1(),W), the carrier of (F1(),a):] is non empty set
the carrier of F3(W) is non empty set
the carrier of F3(a) is non empty set
[: the carrier of F3(W), the carrier of F3(a):] is non empty set
bool [: the carrier of F3(W), the carrier of F3(a):] is non empty set
W is Element of the carrier of F1()
a is Element of the carrier of F1()
<^W,a^> is set
the Arrows of F1() . (W,a) is set
[W,a] is set
{W,a} is set
{W} is non empty trivial 1 -element set
{{W,a},{W}} is set
the Arrows of F1() . [W,a] is set
b is Element of the carrier of F1()
<^a,b^> is set
the Arrows of F1() . (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 F1() . [a,b] is set
b1 is Element of the carrier of F2()
F3(W) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
b9 is Element of the carrier of F2()
F3(a) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
B is Element of the carrier of F2()
F3(b) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
<^b1,b9^> is set
the Arrows of F2() . (b1,b9) is set
[b1,b9] is set
{b1,b9} is set
{b1} is non empty trivial 1 -element set
{{b1,b9},{b1}} is set
the Arrows of F2() . [b1,b9] is set
<^b9,B^> is set
the Arrows of F2() . (b9,B) is set
[b9,B] is set
{b9,B} is set
{b9} is non empty trivial 1 -element set
{{b9,B},{b9}} is set
the Arrows of F2() . [b9,B] is set
f1 is Relation-like Function-like Element of <^b1,b9^>
f is Relation-like Function-like Element of <^W,a^>
F4(W,a,f) is Relation-like Function-like set
f2 is Relation-like Function-like Element of <^b9,B^>
a1 is Relation-like Function-like Element of <^a,b^>
F4(a,b,a1) is Relation-like Function-like set
the Arrows of F2() . (F3(W),F3(a)) is set
[F3(W),F3(a)] is set
{F3(W),F3(a)} is set
{F3(W)} is non empty trivial 1 -element set
{{F3(W),F3(a)},{F3(W)}} is set
the Arrows of F2() . [F3(W),F3(a)] is set
(F2(),b1,b9,f1) is Relation-like the carrier of (F2(),b1) -defined the carrier of (F2(),b9) -valued Function-like non empty V16( the carrier of (F2(),b1)) quasi_total monotone Element of bool [: the carrier of (F2(),b1), the carrier of (F2(),b9):]
(F2(),b1) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (F2(),b1) is non empty set
(F2(),b9) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (F2(),b9) is non empty set
[: the carrier of (F2(),b1), the carrier of (F2(),b9):] is non empty set
bool [: the carrier of (F2(),b1), the carrier of (F2(),b9):] is non empty set
(F1(),a,b,a1) is Relation-like the carrier of (F1(),a) -defined the carrier of (F1(),b) -valued Function-like non empty V16( the carrier of (F1(),a)) quasi_total monotone Element of bool [: the carrier of (F1(),a), the carrier of (F1(),b):]
(F1(),a) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (F1(),a) is non empty set
(F1(),b) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (F1(),b) is non empty set
[: the carrier of (F1(),a), the carrier of (F1(),b):] is non empty set
bool [: the carrier of (F1(),a), the carrier of (F1(),b):] is non empty set
the Arrows of F2() . (F3(a),F3(b)) is set
[F3(a),F3(b)] is set
{F3(a),F3(b)} is set
{F3(a)} is non empty trivial 1 -element set
{{F3(a),F3(b)},{F3(a)}} is set
the Arrows of F2() . [F3(a),F3(b)] is set
(F2(),b9,B,f2) is Relation-like the carrier of (F2(),b9) -defined the carrier of (F2(),B) -valued Function-like non empty V16( the carrier of (F2(),b9)) quasi_total monotone Element of bool [: the carrier of (F2(),b9), the carrier of (F2(),B):]
(F2(),B) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (F2(),B) is non empty set
[: the carrier of (F2(),b9), the carrier of (F2(),B):] is non empty set
bool [: the carrier of (F2(),b9), the carrier of (F2(),B):] is non empty set
(F1(),W,a,f) is Relation-like the carrier of (F1(),W) -defined the carrier of (F1(),a) -valued Function-like non empty V16( the carrier of (F1(),W)) quasi_total monotone Element of bool [: the carrier of (F1(),W), the carrier of (F1(),a):]
(F1(),W) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (F1(),W) is non empty set
[: the carrier of (F1(),W), the carrier of (F1(),a):] is non empty set
bool [: the carrier of (F1(),W), the carrier of (F1(),a):] is non empty set
(F1(),a,b,a1) * (F1(),W,a,f) is Relation-like the carrier of (F1(),W) -defined the carrier of (F1(),b) -valued Function-like non empty V16( the carrier of (F1(),W)) quasi_total Element of bool [: the carrier of (F1(),W), the carrier of (F1(),b):]
[: the carrier of (F1(),W), the carrier of (F1(),b):] is non empty set
bool [: the carrier of (F1(),W), the carrier of (F1(),b):] is non empty set
F4(W,b,((F1(),a,b,a1) * (F1(),W,a,f))) is Relation-like Function-like set
F4(W,a,f) * F4(a,b,a1) is Relation-like Function-like set
f2 * f1 is Relation-like Function-like Element of <^b1,B^>
<^b1,B^> is set
the Arrows of F2() . (b1,B) is set
[b1,B] is set
{b1,B} is set
{{b1,B},{b1}} is set
the Arrows of F2() . [b1,B] is set
a1 * f is Relation-like Function-like Element of <^W,b^>
<^W,b^> is set
the Arrows of F1() . (W,b) is set
[W,b] is set
{W,b} is set
{{W,b},{W}} is set
the Arrows of F1() . [W,b] is set
F4(W,b,(a1 * f)) is Relation-like Function-like set
a is Element of the carrier of F2()
W is Element of the carrier of F1()
F3(W) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
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 F1() . (W,W) is set
[W,W] is set
{W,W} is set
{W} is non empty trivial 1 -element set
{{W,W},{W}} is set
the Arrows of F1() . [W,W] is set
(F1(),W) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
id (F1(),W) is Relation-like the carrier of (F1(),W) -defined the carrier of (F1(),W) -valued Function-like non empty V16( the carrier of (F1(),W)) quasi_total monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving Element of bool [: the carrier of (F1(),W), the carrier of (F1(),W):]
the carrier of (F1(),W) is non empty set
[: the carrier of (F1(),W), the carrier of (F1(),W):] is non empty set
bool [: the carrier of (F1(),W), the carrier of (F1(),W):] is non empty set
id the carrier of (F1(),W) is Relation-like the carrier of (F1(),W) -defined the carrier of (F1(),W) -valued Function-like one-to-one non empty V16( the carrier of (F1(),W)) quasi_total Element of bool [: the carrier of (F1(),W), the carrier of (F1(),W):]
F4(W,W,(idm W)) is Relation-like Function-like set
(F2(),a) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
id (F2(),a) is Relation-like the carrier of (F2(),a) -defined the carrier of (F2(),a) -valued Function-like non empty V16( the carrier of (F2(),a)) quasi_total monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving Element of bool [: the carrier of (F2(),a), the carrier of (F2(),a):]
the carrier of (F2(),a) is non empty set
[: the carrier of (F2(),a), the carrier of (F2(),a):] is non empty set
bool [: the carrier of (F2(),a), the carrier of (F2(),a):] is non empty set
id the carrier of (F2(),a) is Relation-like the carrier of (F2(),a) -defined the carrier of (F2(),a) -valued Function-like one-to-one non empty V16( the carrier of (F2(),a)) quasi_total Element of bool [: the carrier of (F2(),a), the carrier of (F2(),a):]
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 F2() . (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 F2() . [a,a] is set
W is Element of the carrier of F1()
F3(W) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
W is reflexive V149(F1(),F2()) strict Covariant id-preserving comp-preserving covariant Functor of F1(),F2()
a is Element of the carrier of F1()
W . a is Element of the carrier of F2()
(F1(),a) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
F3((F1(),a)) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
a is Element of the carrier of F1()
b is Element of the carrier of F1()
<^a,b^> is set
the Arrows of F1() . (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 F1() . [a,b] is set
(F1(),a) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
(F1(),b) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
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 F2()
W . b is Element of the carrier of F2()
<^(W . a),(W . b)^> is set
the Arrows of F2() . ((W . a),(W . b)) is set
[(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 F2() . [(W . a),(W . b)] is set
(F1(),a,b,f) is Relation-like the carrier of (F1(),a) -defined the carrier of (F1(),b) -valued Function-like non empty V16( the carrier of (F1(),a)) quasi_total monotone Element of bool [: the carrier of (F1(),a), the carrier of (F1(),b):]
the carrier of (F1(),a) is non empty set
the carrier of (F1(),b) is non empty set
[: the carrier of (F1(),a), the carrier of (F1(),b):] is non empty set
bool [: the carrier of (F1(),a), the carrier of (F1(),b):] is non empty set
F4((F1(),a),(F1(),b),(F1(),a,b,f)) is Relation-like Function-like set
F1() is non empty transitive semi-functional V110() with_units reflexive para-functional set-id-inheriting concrete () () AltCatStr
the Arrows of F1() is Relation-like [: the carrier of F1(), the carrier of F1():] -defined Function-like V16([: the carrier of F1(), the carrier of F1():]) set
the carrier of F1() is non empty set
[: the carrier of F1(), the carrier of F1():] is non empty set
F2() is non empty transitive semi-functional V110() with_units reflexive para-functional set-id-inheriting concrete () () AltCatStr
the Arrows of F2() is Relation-like [: the carrier of F2(), the carrier of F2():] -defined Function-like V16([: the carrier of F2(), the carrier of F2():]) set
the carrier of F2() is non empty set
[: the carrier of F2(), the carrier of F2():] is non empty set
W is Element of the carrier of F1()
a is Element of the carrier of F1()
<^W,a^> is set
the Arrows of F1() . (W,a) is set
[W,a] is set
{W,a} is set
{W} is non empty trivial 1 -element set
{{W,a},{W}} is set
the Arrows of F1() . [W,a] is set
F3(a) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
F3(W) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the Arrows of F2() . (F3(a),F3(W)) is set
[F3(a),F3(W)] is set
{F3(a),F3(W)} is set
{F3(a)} is non empty trivial 1 -element set
{{F3(a),F3(W)},{F3(a)}} is set
the Arrows of F2() . [F3(a),F3(W)] is set
b is Relation-like Function-like Element of <^W,a^>
F4(W,a,b) is Relation-like Function-like set
(F1(),W,a,b) is Relation-like the carrier of (F1(),W) -defined the carrier of (F1(),a) -valued Function-like non empty V16( the carrier of (F1(),W)) quasi_total monotone Element of bool [: the carrier of (F1(),W), the carrier of (F1(),a):]
(F1(),W) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (F1(),W) is non empty set
(F1(),a) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (F1(),a) is non empty set
[: the carrier of (F1(),W), the carrier of (F1(),a):] is non empty set
bool [: the carrier of (F1(),W), the carrier of (F1(),a):] is non empty set
the carrier of F3(a) is non empty set
the carrier of F3(W) is non empty set
[: the carrier of F3(a), the carrier of F3(W):] is non empty set
bool [: the carrier of F3(a), the carrier of F3(W):] is non empty set
W is Element of the carrier of F1()
a is Element of the carrier of F1()
<^W,a^> is set
the Arrows of F1() . (W,a) is set
[W,a] is set
{W,a} is set
{W} is non empty trivial 1 -element set
{{W,a},{W}} is set
the Arrows of F1() . [W,a] is set
b is Element of the carrier of F1()
<^a,b^> is set
the Arrows of F1() . (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 F1() . [a,b] is set
b1 is Element of the carrier of F2()
F3(W) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
b9 is Element of the carrier of F2()
F3(a) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
B is Element of the carrier of F2()
F3(b) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
<^b9,b1^> is set
the Arrows of F2() . (b9,b1) is set
[b9,b1] is set
{b9,b1} is set
{b9} is non empty trivial 1 -element set
{{b9,b1},{b9}} is set
the Arrows of F2() . [b9,b1] is set
<^B,b9^> is set
the Arrows of F2() . (B,b9) is set
[B,b9] is set
{B,b9} is set
{B} is non empty trivial 1 -element set
{{B,b9},{B}} is set
the Arrows of F2() . [B,b9] is set
f1 is Relation-like Function-like Element of <^b9,b1^>
f is Relation-like Function-like Element of <^W,a^>
F4(W,a,f) is Relation-like Function-like set
f2 is Relation-like Function-like Element of <^B,b9^>
a1 is Relation-like Function-like Element of <^a,b^>
F4(a,b,a1) is Relation-like Function-like set
the Arrows of F2() . (F3(a),F3(W)) is set
[F3(a),F3(W)] is set
{F3(a),F3(W)} is set
{F3(a)} is non empty trivial 1 -element set
{{F3(a),F3(W)},{F3(a)}} is set
the Arrows of F2() . [F3(a),F3(W)] is set
(F2(),b9,b1,f1) is Relation-like the carrier of (F2(),b9) -defined the carrier of (F2(),b1) -valued Function-like non empty V16( the carrier of (F2(),b9)) quasi_total monotone Element of bool [: the carrier of (F2(),b9), the carrier of (F2(),b1):]
(F2(),b9) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (F2(),b9) is non empty set
(F2(),b1) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (F2(),b1) is non empty set
[: the carrier of (F2(),b9), the carrier of (F2(),b1):] is non empty set
bool [: the carrier of (F2(),b9), the carrier of (F2(),b1):] is non empty set
(F1(),a,b,a1) is Relation-like the carrier of (F1(),a) -defined the carrier of (F1(),b) -valued Function-like non empty V16( the carrier of (F1(),a)) quasi_total monotone Element of bool [: the carrier of (F1(),a), the carrier of (F1(),b):]
(F1(),a) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (F1(),a) is non empty set
(F1(),b) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (F1(),b) is non empty set
[: the carrier of (F1(),a), the carrier of (F1(),b):] is non empty set
bool [: the carrier of (F1(),a), the carrier of (F1(),b):] is non empty set
the Arrows of F2() . (F3(b),F3(a)) is set
[F3(b),F3(a)] is set
{F3(b),F3(a)} is set
{F3(b)} is non empty trivial 1 -element set
{{F3(b),F3(a)},{F3(b)}} is set
the Arrows of F2() . [F3(b),F3(a)] is set
(F2(),B,b9,f2) is Relation-like the carrier of (F2(),B) -defined the carrier of (F2(),b9) -valued Function-like non empty V16( the carrier of (F2(),B)) quasi_total monotone Element of bool [: the carrier of (F2(),B), the carrier of (F2(),b9):]
(F2(),B) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (F2(),B) is non empty set
[: the carrier of (F2(),B), the carrier of (F2(),b9):] is non empty set
bool [: the carrier of (F2(),B), the carrier of (F2(),b9):] is non empty set
(F1(),W,a,f) is Relation-like the carrier of (F1(),W) -defined the carrier of (F1(),a) -valued Function-like non empty V16( the carrier of (F1(),W)) quasi_total monotone Element of bool [: the carrier of (F1(),W), the carrier of (F1(),a):]
(F1(),W) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (F1(),W) is non empty set
[: the carrier of (F1(),W), the carrier of (F1(),a):] is non empty set
bool [: the carrier of (F1(),W), the carrier of (F1(),a):] is non empty set
(F1(),a,b,a1) * (F1(),W,a,f) is Relation-like the carrier of (F1(),W) -defined the carrier of (F1(),b) -valued Function-like non empty V16( the carrier of (F1(),W)) quasi_total Element of bool [: the carrier of (F1(),W), the carrier of (F1(),b):]
[: the carrier of (F1(),W), the carrier of (F1(),b):] is non empty set
bool [: the carrier of (F1(),W), the carrier of (F1(),b):] is non empty set
F4(W,b,((F1(),a,b,a1) * (F1(),W,a,f))) is Relation-like Function-like set
F4(a,b,a1) * F4(W,a,f) is Relation-like Function-like set
f1 * f2 is Relation-like Function-like Element of <^B,b1^>
<^B,b1^> is set
the Arrows of F2() . (B,b1) is set
[B,b1] is set
{B,b1} is set
{{B,b1},{B}} is set
the Arrows of F2() . [B,b1] is set
a1 * f is Relation-like Function-like Element of <^W,b^>
<^W,b^> is set
the Arrows of F1() . (W,b) is set
[W,b] is set
{W,b} is set
{{W,b},{W}} is set
the Arrows of F1() . [W,b] is set
F4(W,b,(a1 * f)) is Relation-like Function-like set
a is Element of the carrier of F2()
W is Element of the carrier of F1()
F3(W) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
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 F1() . (W,W) is set
[W,W] is set
{W,W} is set
{W} is non empty trivial 1 -element set
{{W,W},{W}} is set
the Arrows of F1() . [W,W] is set
(F1(),W) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
id (F1(),W) is Relation-like the carrier of (F1(),W) -defined the carrier of (F1(),W) -valued Function-like non empty V16( the carrier of (F1(),W)) quasi_total monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving Element of bool [: the carrier of (F1(),W), the carrier of (F1(),W):]
the carrier of (F1(),W) is non empty set
[: the carrier of (F1(),W), the carrier of (F1(),W):] is non empty set
bool [: the carrier of (F1(),W), the carrier of (F1(),W):] is non empty set
id the carrier of (F1(),W) is Relation-like the carrier of (F1(),W) -defined the carrier of (F1(),W) -valued Function-like one-to-one non empty V16( the carrier of (F1(),W)) quasi_total Element of bool [: the carrier of (F1(),W), the carrier of (F1(),W):]
F4(W,W,(idm W)) is Relation-like Function-like set
(F2(),a) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
id (F2(),a) is Relation-like the carrier of (F2(),a) -defined the carrier of (F2(),a) -valued Function-like non empty V16( the carrier of (F2(),a)) quasi_total monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving Element of bool [: the carrier of (F2(),a), the carrier of (F2(),a):]
the carrier of (F2(),a) is non empty set
[: the carrier of (F2(),a), the carrier of (F2(),a):] is non empty set
bool [: the carrier of (F2(),a), the carrier of (F2(),a):] is non empty set
id the carrier of (F2(),a) is Relation-like the carrier of (F2(),a) -defined the carrier of (F2(),a) -valued Function-like one-to-one non empty V16( the carrier of (F2(),a)) quasi_total Element of bool [: the carrier of (F2(),a), the carrier of (F2(),a):]
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 F2() . (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 F2() . [a,a] is set
W is Element of the carrier of F1()
F3(W) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
W is reflexive V149(F1(),F2()) strict Contravariant id-preserving comp-reversing contravariant Functor of F1(),F2()
a is Element of the carrier of F1()
W . a is Element of the carrier of F2()
(F1(),a) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
F3((F1(),a)) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
a is Element of the carrier of F1()
b is Element of the carrier of F1()
<^a,b^> is set
the Arrows of F1() . (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 F1() . [a,b] is set
(F1(),a) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
(F1(),b) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
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 F2()
W . a is Element of the carrier of F2()
<^(W . b),(W . a)^> is set
the Arrows of F2() . ((W . b),(W . a)) is set
[(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 F2() . [(W . b),(W . a)] is set
(F1(),a,b,f) is Relation-like the carrier of (F1(),a) -defined the carrier of (F1(),b) -valued Function-like non empty V16( the carrier of (F1(),a)) quasi_total monotone Element of bool [: the carrier of (F1(),a), the carrier of (F1(),b):]
the carrier of (F1(),a) is non empty set
the carrier of (F1(),b) is non empty set
[: the carrier of (F1(),a), the carrier of (F1(),b):] is non empty set
bool [: the carrier of (F1(),a), the carrier of (F1(),b):] is non empty set
F4((F1(),a),(F1(),b),(F1(),a,b,f)) is Relation-like Function-like set
F1() is non empty transitive semi-functional V110() with_units reflexive para-functional set-id-inheriting concrete () () AltCatStr
the Arrows of F1() is Relation-like [: the carrier of F1(), the carrier of F1():] -defined Function-like V16([: the carrier of F1(), the carrier of F1():]) set
the carrier of F1() is non empty set
[: the carrier of F1(), the carrier of F1():] is non empty set
F2() is non empty transitive semi-functional V110() with_units reflexive para-functional set-id-inheriting concrete () () AltCatStr
the Arrows of F2() is Relation-like [: the carrier of F2(), the carrier of F2():] -defined Function-like V16([: the carrier of F2(), the carrier of F2():]) set
the carrier of F2() is non empty set
[: the carrier of F2(), the carrier of F2():] is non empty set
W is Element of the carrier of F1()
F3(W) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
a is Element of the carrier of F1()
F3(a) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
(F1(),W) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
(F1(),a) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
W is Element of the carrier of F2()
a is Element of the carrier of F2()
<^W,a^> is set
the Arrows of F2() . (W,a) is set
[W,a] is set
{W,a} is set
{W} is non empty trivial 1 -element set
{{W,a},{W}} is set
the Arrows of F2() . [W,a] is set
b is Relation-like Function-like Element of <^W,a^>
(F2(),W,a,b) is Relation-like the carrier of (F2(),W) -defined the carrier of (F2(),a) -valued Function-like non empty V16( the carrier of (F2(),W)) quasi_total monotone Element of bool [: the carrier of (F2(),W), the carrier of (F2(),a):]
(F2(),W) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (F2(),W) is non empty set
(F2(),a) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (F2(),a) is non empty set
[: the carrier of (F2(),W), the carrier of (F2(),a):] is non empty set
bool [: the carrier of (F2(),W), the carrier of (F2(),a):] 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
a1 is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
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
b1 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:]
F3(f) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
F3(a1) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
F4(f,a1,b1) is Relation-like Function-like set
b9 is Element of the carrier of F1()
B is Element of the carrier of F1()
<^b9,B^> is set
the Arrows of F1() . (b9,B) is set
[b9,B] is set
{b9,B} is set
{b9} is non empty trivial 1 -element set
{{b9,B},{b9}} is set
the Arrows of F1() . [b9,B] is set
W is Element of the carrier of F1()
a is Element of the carrier of F1()
<^W,a^> is set
the Arrows of F1() . (W,a) is set
[W,a] is set
{W,a} is set
{W} is non empty trivial 1 -element set
{{W,a},{W}} is set
the Arrows of F1() . [W,a] is set
b is Relation-like Function-like Element of <^W,a^>
F4(W,a,b) is Relation-like Function-like set
f is Relation-like Function-like Element of <^W,a^>
F4(W,a,f) is Relation-like Function-like set
(F1(),W,a,f) is Relation-like the carrier of (F1(),W) -defined the carrier of (F1(),a) -valued Function-like non empty V16( the carrier of (F1(),W)) quasi_total monotone Element of bool [: the carrier of (F1(),W), the carrier of (F1(),a):]
(F1(),W) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (F1(),W) is non empty set
(F1(),a) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (F1(),a) is non empty set
[: the carrier of (F1(),W), the carrier of (F1(),a):] is non empty set
bool [: the carrier of (F1(),W), the carrier of (F1(),a):] is non empty set
(F1(),W,a,b) is Relation-like the carrier of (F1(),W) -defined the carrier of (F1(),a) -valued Function-like non empty V16( the carrier of (F1(),W)) quasi_total monotone Element of bool [: the carrier of (F1(),W), the carrier of (F1(),a):]
W is reflexive V149(F1(),F2()) Covariant id-preserving comp-preserving covariant Functor of F1(),F2()
F1() is non empty transitive semi-functional V110() with_units reflexive para-functional set-id-inheriting concrete () () AltCatStr
the Arrows of F1() is Relation-like [: the carrier of F1(), the carrier of F1():] -defined Function-like V16([: the carrier of F1(), the carrier of F1():]) set
the carrier of F1() is non empty set
[: the carrier of F1(), the carrier of F1():] is non empty set
F2() is non empty transitive semi-functional V110() with_units reflexive para-functional set-id-inheriting concrete () () AltCatStr
the Arrows of F2() is Relation-like [: the carrier of F2(), the carrier of F2():] -defined Function-like V16([: the carrier of F2(), the carrier of F2():]) set
the carrier of F2() is non empty set
[: the carrier of F2(), the carrier of F2():] is non empty set
W is Element of the carrier of F1()
F3(W) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
a is Element of the carrier of F1()
F3(a) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
(F1(),W) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
(F1(),a) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
W is Element of the carrier of F2()
a is Element of the carrier of F2()
<^W,a^> is set
the Arrows of F2() . (W,a) is set
[W,a] is set
{W,a} is set
{W} is non empty trivial 1 -element set
{{W,a},{W}} is set
the Arrows of F2() . [W,a] is set
b is Relation-like Function-like Element of <^W,a^>
(F2(),W,a,b) is Relation-like the carrier of (F2(),W) -defined the carrier of (F2(),a) -valued Function-like non empty V16( the carrier of (F2(),W)) quasi_total monotone Element of bool [: the carrier of (F2(),W), the carrier of (F2(),a):]
(F2(),W) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (F2(),W) is non empty set
(F2(),a) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (F2(),a) is non empty set
[: the carrier of (F2(),W), the carrier of (F2(),a):] is non empty set
bool [: the carrier of (F2(),W), the carrier of (F2(),a):] 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
a1 is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
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
b1 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:]
F3(f) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
F3(a1) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
F4(f,a1,b1) is Relation-like Function-like set
b9 is Element of the carrier of F1()
B is Element of the carrier of F1()
<^b9,B^> is set
the Arrows of F1() . (b9,B) is set
[b9,B] is set
{b9,B} is set
{b9} is non empty trivial 1 -element set
{{b9,B},{b9}} is set
the Arrows of F1() . [b9,B] is set
W is Element of the carrier of F1()
a is Element of the carrier of F1()
<^W,a^> is set
the Arrows of F1() . (W,a) is set
[W,a] is set
{W,a} is set
{W} is non empty trivial 1 -element set
{{W,a},{W}} is set
the Arrows of F1() . [W,a] is set
b is Relation-like Function-like Element of <^W,a^>
F4(W,a,b) is Relation-like Function-like set
f is Relation-like Function-like Element of <^W,a^>
F4(W,a,f) is Relation-like Function-like set
(F1(),W,a,b) is Relation-like the carrier of (F1(),W) -defined the carrier of (F1(),a) -valued Function-like non empty V16( the carrier of (F1(),W)) quasi_total monotone Element of bool [: the carrier of (F1(),W), the carrier of (F1(),a):]
(F1(),W) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (F1(),W) is non empty set
(F1(),a) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (F1(),a) is non empty set
[: the carrier of (F1(),W), the carrier of (F1(),a):] is non empty set
bool [: the carrier of (F1(),W), the carrier of (F1(),a):] is non empty set
(F1(),W,a,f) is Relation-like the carrier of (F1(),W) -defined the carrier of (F1(),a) -valued Function-like non empty V16( the carrier of (F1(),W)) quasi_total monotone Element of bool [: the carrier of (F1(),W), the carrier of (F1(),a):]
W is reflexive V149(F1(),F2()) Contravariant id-preserving comp-reversing contravariant Functor of F1(),F2()
the non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
{ the non empty V57() reflexive transitive antisymmetric with_suprema with_infima 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 with_suprema with_infima 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 non empty transitive strict semi-functional V110() with_units reflexive para-functional set-id-inheriting concrete () () AltCatStr
the carrier of b is non empty set
f is Element of the carrier of b
(b,f) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (b,f) is non empty set
a1 is Element of the carrier of b
(b,a1) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (b,a1) is non empty set
[: the carrier of (b,f), the carrier of (b,a1):] is non empty set
bool [: the carrier of (b,f), the carrier of (b,a1):] is non empty set
<^f,a1^> is set
the Arrows of b is Relation-like [: the carrier of b, the carrier of b:] -defined Function-like V16([: the carrier of b, the carrier of b:]) set
[: the carrier of b, the carrier of b:] is non empty set
the Arrows of b . (f,a1) is set
[f,a1] is set
{f,a1} is set
{f} is non empty trivial 1 -element set
{{f,a1},{f}} is set
the Arrows of b . [f,a1] is set
b1 is Relation-like the carrier of (b,f) -defined the carrier of (b,a1) -valued Function-like non empty V16( the carrier of (b,f)) quasi_total Element of bool [: the carrier of (b,f), the carrier of (b,a1):]
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
(W,a) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
(W,b) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
f is Relation-like Function-like Element of <^a,b^>
(W,a,b,f) 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) is non empty set
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
[: the carrier of (W,b), the carrier of (W,a):] is non empty set
bool [: the carrier of (W,b), the carrier of (W,a):] is non empty set
id (W,b) is Relation-like the carrier of (W,b) -defined the carrier of (W,b) -valued Function-like non empty V16( the carrier of (W,b)) quasi_total monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving Element of bool [: the carrier of (W,b), the carrier of (W,b):]
[: the carrier of (W,b), the carrier of (W,b):] is non empty set
bool [: the carrier of (W,b), the carrier of (W,b):] is non empty set
id the carrier of (W,b) is Relation-like the carrier of (W,b) -defined the carrier of (W,b) -valued Function-like one-to-one non empty V16( the carrier of (W,b)) quasi_total Element of bool [: the carrier of (W,b), the carrier of (W,b):]
id (W,a) is Relation-like the carrier of (W,a) -defined the carrier of (W,a) -valued Function-like non empty V16( the carrier of (W,a)) quasi_total monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving Element of bool [: the carrier of (W,a), the carrier of (W,a):]
[: the carrier of (W,a), the carrier of (W,a):] is non empty set
bool [: the carrier of (W,a), the carrier of (W,a):] is non empty set
id the carrier of (W,a) is Relation-like the carrier of (W,a) -defined the carrier of (W,a) -valued Function-like one-to-one non empty V16( the carrier of (W,a)) quasi_total Element of bool [: the carrier of (W,a), the carrier of (W,a):]
a1 is Relation-like the carrier of (W,b) -defined the carrier of (W,a) -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,a):]
(W,a,b,f) * a1 is Relation-like the carrier of (W,b) -defined the carrier of (W,b) -valued Function-like non empty V16( the carrier of (W,b)) quasi_total Element of bool [: the carrier of (W,b), the carrier of (W,b):]
a1 * (W,a,b,f) is Relation-like the carrier of (W,a) -defined the carrier of (W,a) -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,a):]
<^b,a^> is set
the Arrows of W . (b,a) is set
[b,a] is set
{b,a} is set
{b} is non empty trivial 1 -element set
{{b,a},{b}} is set
the Arrows of W . [b,a] is set
b1 is Relation-like Function-like Element of <^b,a^>
(W,b,a,b1) is Relation-like the carrier of (W,b) -defined the carrier of (W,a) -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,a):]
idm b is Relation-like Function-like retraction coretraction iso mono epi Element of <^b,b^>
<^b,b^> is non empty set
the Arrows of W . (b,b) is set
[b,b] is set
{b,b} is set
{{b,b},{b}} is set
the Arrows of W . [b,b] is set
f * b1 is Relation-like Function-like Element of <^b,b^>
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 W . (a,a) is set
[a,a] is set
{a,a} is set
{{a,a},{a}} is set
the Arrows of W . [a,a] is set
b1 * f is Relation-like Function-like Element of <^a,a^>
f " is Relation-like Function-like Element of <^b,a^>
f * (f ") is Relation-like Function-like Element of <^b,b^>
(f ") * f is Relation-like Function-like Element of <^a,a^>
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
<^b,a^> is set
the Arrows of W . (b,a) is set
[b,a] is set
{b,a} is set
{b} is non empty trivial 1 -element set
{{b,a},{b}} is set
the Arrows of W . [b,a] is set
(W,a) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
(W,b) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
f is Relation-like Function-like Element of <^a,b^>
(W,a,b,f) 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) is non empty set
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
f " is Relation-like Function-like Element of <^b,a^>
f * (f ") is Relation-like Function-like Element of <^b,b^>
<^b,b^> is non empty set
the Arrows of W . (b,b) is set
[b,b] is set
{b,b} is set
{{b,b},{b}} is set
the Arrows of W . [b,b] is set
idm b is Relation-like Function-like retraction coretraction iso mono epi Element of <^b,b^>
(f ") * f is Relation-like Function-like Element of <^a,a^>
<^a,a^> is non empty set
the Arrows of W . (a,a) is set
[a,a] is set
{a,a} is set
{{a,a},{a}} is set
the Arrows of W . [a,a] is set
idm a is Relation-like Function-like retraction coretraction iso mono epi Element of <^a,a^>
id (W,a) is Relation-like the carrier of (W,a) -defined the carrier of (W,a) -valued Function-like non empty V16( the carrier of (W,a)) quasi_total monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving Element of bool [: the carrier of (W,a), the carrier of (W,a):]
[: the carrier of (W,a), the carrier of (W,a):] is non empty set
bool [: the carrier of (W,a), the carrier of (W,a):] is non empty set
id the carrier of (W,a) is Relation-like the carrier of (W,a) -defined the carrier of (W,a) -valued Function-like one-to-one non empty V16( the carrier of (W,a)) quasi_total Element of bool [: the carrier of (W,a), the carrier of (W,a):]
id (W,b) is Relation-like the carrier of (W,b) -defined the carrier of (W,b) -valued Function-like non empty V16( the carrier of (W,b)) quasi_total monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving Element of bool [: the carrier of (W,b), the carrier of (W,b):]
[: the carrier of (W,b), the carrier of (W,b):] is non empty set
bool [: the carrier of (W,b), the carrier of (W,b):] is non empty set
id the carrier of (W,b) is Relation-like the carrier of (W,b) -defined the carrier of (W,b) -valued Function-like one-to-one non empty V16( the carrier of (W,b)) quasi_total Element of bool [: the carrier of (W,b), the carrier of (W,b):]
(W,b,a,(f ")) is Relation-like the carrier of (W,b) -defined the carrier of (W,a) -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,a):]
[: the carrier of (W,b), the carrier of (W,a):] is non empty set
bool [: the carrier of (W,b), the carrier of (W,a):] is non empty set
(W,a,b,f) * (W,b,a,(f ")) is Relation-like the carrier of (W,b) -defined the carrier of (W,b) -valued Function-like non empty V16( the carrier of (W,b)) quasi_total Element of bool [: the carrier of (W,b), the carrier of (W,b):]
(W,b,a,(f ")) * (W,a,b,f) is Relation-like the carrier of (W,a) -defined the carrier of (W,a) -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,a):]
F1() is non empty transitive semi-functional V110() with_units reflexive para-functional set-id-inheriting concrete () () AltCatStr
the carrier of F1() is non empty set
F2() is non empty transitive semi-functional V110() with_units reflexive para-functional set-id-inheriting concrete () () AltCatStr
the carrier of F2() is non empty set
W is reflexive V149(F2(),F1()) Covariant id-preserving comp-preserving covariant Functor of F2(),F1()
W is Element of the carrier of F2()
a is Element of the carrier of F2()
<^W,a^> is set
the Arrows of F2() is Relation-like [: the carrier of F2(), the carrier of F2():] -defined Function-like V16([: the carrier of F2(), the carrier of F2():]) set
[: the carrier of F2(), the carrier of F2():] is non empty set
the Arrows of F2() . (W,a) is set
[W,a] is set
{W,a} is set
{W} is non empty trivial 1 -element set
{{W,a},{W}} is set
the Arrows of F2() . [W,a] is set
F8(W) is Relation-like Function-like set
F4(W) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
F4(a) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
F8(a) is Relation-like Function-like set
b is Relation-like Function-like Element of <^W,a^>
F6(W,a,b) is Relation-like Function-like set
F5(F4(W),F4(a),F6(W,a,b)) is Relation-like Function-like set
F8(W) * F5(F4(W),F4(a),F6(W,a,b)) is Relation-like Function-like set
b * F8(a) is Relation-like Function-like set
(F2(),W,a,b) is Relation-like the carrier of (F2(),W) -defined the carrier of (F2(),a) -valued Function-like non empty V16( the carrier of (F2(),W)) quasi_total monotone Element of bool [: the carrier of (F2(),W), the carrier of (F2(),a):]
(F2(),W) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (F2(),W) is non empty set
(F2(),a) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (F2(),a) is non empty set
[: the carrier of (F2(),W), the carrier of (F2(),a):] is non empty set
bool [: the carrier of (F2(),W), the carrier of (F2(),a):] is non empty set
W is Element of the carrier of F1()
a is Element of the carrier of F1()
<^W,a^> is set
the Arrows of F1() is Relation-like [: the carrier of F1(), the carrier of F1():] -defined Function-like V16([: the carrier of F1(), the carrier of F1():]) set
[: the carrier of F1(), the carrier of F1():] is non empty set
the Arrows of F1() . (W,a) is set
[W,a] is set
{W,a} is set
{W} is non empty trivial 1 -element set
{{W,a},{W}} is set
the Arrows of F1() . [W,a] is set
F3(W) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
F3(a) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
F7(a) is Relation-like Function-like set
F7(W) is Relation-like Function-like set
b is Relation-like Function-like Element of <^W,a^>
F5(W,a,b) is Relation-like Function-like set
F6(F3(W),F3(a),F5(W,a,b)) is Relation-like Function-like set
F6(F3(W),F3(a),F5(W,a,b)) * F7(a) is Relation-like Function-like set
F7(W) * b is Relation-like Function-like set
(F1(),W,a,b) is Relation-like the carrier of (F1(),W) -defined the carrier of (F1(),a) -valued Function-like non empty V16( the carrier of (F1(),W)) quasi_total monotone Element of bool [: the carrier of (F1(),W), the carrier of (F1(),a):]
(F1(),W) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (F1(),W) is non empty set
(F1(),a) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (F1(),a) is non empty set
[: the carrier of (F1(),W), the carrier of (F1(),a):] is non empty set
bool [: the carrier of (F1(),W), the carrier of (F1(),a):] is non empty set
a is Element of the carrier of F2()
W is Element of the carrier of F2()
F4(W) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
F3(F4(W)) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
F8(W) is Relation-like Function-like set
<^W,a^> is set
the Arrows of F2() is Relation-like [: the carrier of F2(), the carrier of F2():] -defined Function-like V16([: the carrier of F2(), the carrier of F2():]) set
[: the carrier of F2(), the carrier of F2():] is non empty set
the Arrows of F2() . (W,a) is set
[W,a] is set
{W,a} is set
{W} is non empty trivial 1 -element set
{{W,a},{W}} is set
the Arrows of F2() . [W,a] is set
F8(W) " is Relation-like Function-like set
<^a,W^> is set
the Arrows of F2() . (a,W) is set
[a,W] is set
{a,W} is set
{a} is non empty trivial 1 -element set
{{a,W},{a}} is set
the Arrows of F2() . [a,W] is set
(F2(),W) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (F2(),W) is non empty set
the carrier of F3(F4(W)) is non empty set
[: the carrier of (F2(),W), the carrier of F3(F4(W)):] is non empty set
bool [: the carrier of (F2(),W), the carrier of F3(F4(W)):] is non empty set
b is Relation-like the carrier of (F2(),W) -defined the carrier of F3(F4(W)) -valued Function-like non empty V16( the carrier of (F2(),W)) quasi_total monotone Element of bool [: the carrier of (F2(),W), the carrier of F3(F4(W)):]
b " is Relation-like Function-like set
(F2(),a) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
[: the carrier of F3(F4(W)), the carrier of (F2(),W):] is non empty set
bool [: the carrier of F3(F4(W)), the carrier of (F2(),W):] is non empty set
f is Relation-like the carrier of F3(F4(W)) -defined the carrier of (F2(),W) -valued Function-like non empty V16( the carrier of F3(F4(W))) quasi_total Element of bool [: the carrier of F3(F4(W)), the carrier of (F2(),W):]
W is Element of the carrier of F1()
a is Element of the carrier of F1()
F3(a) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
F4(F3(a)) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
F7(a) is Relation-like Function-like set
<^W,a^> is set
the Arrows of F1() is Relation-like [: the carrier of F1(), the carrier of F1():] -defined Function-like V16([: the carrier of F1(), the carrier of F1():]) set
[: the carrier of F1(), the carrier of F1():] is non empty set
the Arrows of F1() . (W,a) is set
[W,a] is set
{W,a} is set
{W} is non empty trivial 1 -element set
{{W,a},{W}} is set
the Arrows of F1() . [W,a] is set
F7(a) " is Relation-like Function-like set
<^a,W^> is set
the Arrows of F1() . (a,W) is set
[a,W] is set
{a,W} is set
{a} is non empty trivial 1 -element set
{{a,W},{a}} is set
the Arrows of F1() . [a,W] is set
the carrier of F4(F3(a)) is non empty set
(F1(),a) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (F1(),a) is non empty set
[: the carrier of F4(F3(a)), the carrier of (F1(),a):] is non empty set
bool [: the carrier of F4(F3(a)), the carrier of (F1(),a):] is non empty set
b is Relation-like the carrier of F4(F3(a)) -defined the carrier of (F1(),a) -valued Function-like non empty V16( the carrier of F4(F3(a))) quasi_total monotone Element of bool [: the carrier of F4(F3(a)), the carrier of (F1(),a):]
b " is Relation-like Function-like set
(F1(),W) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
[: the carrier of (F1(),a), the carrier of F4(F3(a)):] is non empty set
bool [: the carrier of (F1(),a), the carrier of F4(F3(a)):] is non empty set
f is Relation-like the carrier of (F1(),a) -defined the carrier of F4(F3(a)) -valued Function-like non empty V16( the carrier of (F1(),a)) quasi_total Element of bool [: the carrier of (F1(),a), the carrier of F4(F3(a)):]
W is reflexive V149(F1(),F2()) Covariant id-preserving comp-preserving covariant Functor of F1(),F2()
W is set
{W} is non empty trivial 1 -element set
a is set
a \ {W} is Element of bool a
bool a is non empty set
(a \ {W}) \/ {W} is set
W is Relation-like set
5 is non empty set
W is Relation-like set
W |_2 5 is Relation-like set
[:5,5:] is non empty set
W /\ [:5,5:] is set
W is set
a is set
[W,a] is set
{W,a} is set
{W} is non empty trivial 1 -element set
{{W,a},{W}} is set
b is Relation-like Function-like one-to-one set
b " is Relation-like Function-like one-to-one set
dom b is set
b . W is set
b . a is set
[(b . W),(b . a)] is set
{(b . W),(b . a)} is set
{(b . W)} is non empty trivial 1 -element set
{{(b . W),(b . a)},{(b . W)}} is set
f is Relation-like set
b * f is Relation-like set
(b * f) * (b ") is Relation-like set
rng b is set
dom (b ") is set
rng (b ") is set
a1 is set
[W,a1] is set
{W,a1} is set
{{W,a1},{W}} is set
[a1,a] is set
{a1,a} is set
{a1} is non empty trivial 1 -element set
{{a1,a},{a1}} is set
(b ") . a1 is set
b1 is set
[W,b1] is set
{W,b1} is set
{{W,b1},{W}} is set
[b1,a1] is set
{b1,a1} is set
{b1} is non empty trivial 1 -element set
{{b1,a1},{b1}} is set
(b ") . (b . a) is set
[(b . a),a] is set
{(b . a),a} is set
{(b . a)} is non empty trivial 1 -element set
{{(b . a),a},{(b . a)}} is set
[W,(b . W)] is set
{W,(b . W)} is set
{{W,(b . W)},{W}} is set
[W,(b . a)] is set
{W,(b . a)} is set
{{W,(b . a)},{W}} is set
W is Relation-like Function-like one-to-one set
a is Relation-like reflexive set
W * a is Relation-like set
W " is Relation-like Function-like one-to-one set
(W * a) * (W ") is Relation-like set
b is set
field ((W * a) * (W ")) is set
[b,b] is set
{b,b} is set
{b} is non empty trivial 1 -element set
{{b,b},{b}} is set
field a is set
dom ((W * a) * (W ")) is set
rng ((W * a) * (W ")) is set
(dom ((W * a) * (W "))) \/ (rng ((W * a) * (W "))) is set
f is set
[b,f] is set
{b,f} is set
{{b,f},{b}} is set
W . b is set
W . f is set
[(W . b),(W . f)] is set
{(W . b),(W . f)} is set
{(W . b)} is non empty trivial 1 -element set
{{(W . b),(W . f)},{(W . b)}} is set
[(W . b),(W . b)] is set
{(W . b),(W . b)} is set
{{(W . b),(W . b)},{(W . b)}} is set
dom W is set
f is set
[f,b] is set
{f,b} is set
{f} is non empty trivial 1 -element set
{{f,b},{f}} is set
W . f is set
W . b is set
[(W . f),(W . b)] is set
{(W . f),(W . b)} is set
{(W . f)} is non empty trivial 1 -element set
{{(W . f),(W . b)},{(W . f)}} is set
[(W . b),(W . b)] is set
{(W . b),(W . b)} is set
{(W . b)} is non empty trivial 1 -element set
{{(W . b),(W . b)},{(W . b)}} is set
dom W is set
W is Relation-like Function-like one-to-one set
a is Relation-like antisymmetric set
W * a is Relation-like set
W " is Relation-like Function-like one-to-one set
(W * a) * (W ") is Relation-like set
b is set
field ((W * a) * (W ")) 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
[f,b] is set
{f,b} is set
{f} is non empty trivial 1 -element set
{{f,b},{f}} is set
dom W is set
field a is set
W . f is set
W . b is set
[(W . f),(W . b)] is set
{(W . f),(W . b)} is set
{(W . f)} is non empty trivial 1 -element set
{{(W . f),(W . b)},{(W . f)}} is set
[(W . b),(W . f)] is set
{(W . b),(W . f)} is set
{(W . b)} is non empty trivial 1 -element set
{{(W . b),(W . f)},{(W . b)}} is set
W is Relation-like Function-like one-to-one set
a is Relation-like transitive set
W * a is Relation-like set
W " is Relation-like Function-like one-to-one set
(W * a) * (W ") is Relation-like set
b is set
field ((W * a) * (W ")) is set
f is set
a1 is set
[b,f] is set
{b,f} is set
{b} is non empty trivial 1 -element set
{{b,f},{b}} is set
[f,a1] is set
{f,a1} is set
{f} is non empty trivial 1 -element set
{{f,a1},{f}} is set
[b,a1] is set
{b,a1} is set
{{b,a1},{b}} is set
dom W is set
W . f is set
W . a1 is set
[(W . f),(W . a1)] is set
{(W . f),(W . a1)} is set
{(W . f)} is non empty trivial 1 -element set
{{(W . f),(W . a1)},{(W . f)}} is set
field a is set
W . b is set
[(W . b),(W . f)] is set
{(W . b),(W . f)} is set
{(W . b)} is non empty trivial 1 -element set
{{(W . b),(W . f)},{(W . b)}} is set
[(W . b),(W . a1)] is set
{(W . b),(W . a1)} is set
{{(W . b),(W . a1)},{(W . b)}} is set
W is set
[:W,W:] is set
bool [:W,W:] is non empty set
a is epsilon-transitive epsilon-connected ordinal set
b is Relation-like Function-like set
dom b is set
rng b is set
[:W,a:] is set
bool [:W,a:] is non empty set
[:a,W:] is set
bool [:a,W:] is non empty set
f is Relation-like W -defined a -valued Function-like quasi_total Element of bool [:W,a:]
f " is Relation-like Function-like set
a1 is Relation-like a -defined W -valued Function-like quasi_total Element of bool [:a,W:]
dom a1 is Element of bool a
bool a is non empty set
RelIncl a is Relation-like a -defined a -valued well_founded well-ordering V16(a) quasi_total reflexive antisymmetric connected transitive Element of bool [:a,a:]
[:a,a:] is set
bool [:a,a:] is non empty set
dom (RelIncl a) is Element of bool a
rng (RelIncl a) is Element of bool a
f * (RelIncl a) is Relation-like W -defined a -valued Element of bool [:W,a:]
rng (f * (RelIncl a)) is Element of bool a
(f * (RelIncl a)) * a1 is Relation-like W -defined W -valued Element of bool [:W,W:]
dom (f * (RelIncl a)) is Element of bool W
bool W is non empty set
dom ((f * (RelIncl a)) * a1) is Element of bool W
rng a1 is Element of bool W
rng ((f * (RelIncl a)) * a1) is Element of bool W
field ((f * (RelIncl a)) * a1) is set
W \/ W is set
b1 is Relation-like Function-like one-to-one set
b1 * (RelIncl a) is Relation-like set
b1 " is Relation-like Function-like one-to-one set
(b1 * (RelIncl a)) * (b1 ") is Relation-like reflexive antisymmetric transitive set
B is Relation-like W -defined W -valued Element of bool [:W,W:]
f1 is Relation-like W -defined W -valued V16(W) quasi_total reflexive antisymmetric transitive Element of bool [:W,W:]
dom f is Element of bool W
field f1 is set
rng f is Element of bool a
field (RelIncl a) is set
f2 is set
g2 is set
[f2,g2] is set
{f2,g2} is set
{f2} is non empty trivial 1 -element set
{{f2,g2},{f2}} is set
f . f2 is set
f . g2 is set
[(f . f2),(f . g2)] is set
{(f . f2),(f . g2)} is set
{(f . f2)} is non empty trivial 1 -element set
{{(f . f2),(f . g2)},{(f . f2)}} is set
g1 is set
[f2,g1] is set
{f2,g1} is set
{{f2,g1},{f2}} is set
[g1,g2] is set
{g1,g2} is set
{g1} is non empty trivial 1 -element set
{{g1,g2},{g1}} is set
a1 . g1 is set
f9 is set
[f2,f9] is set
{f2,f9} is set
{{f2,f9},{f2}} is set
[f9,g1] is set
{f9,g1} is set
{f9} is non empty trivial 1 -element set
{{f9,g1},{f9}} is set
[f2,(f . f2)] is set
{f2,(f . f2)} is set
{{f2,(f . f2)},{f2}} is set
[f2,(f . g2)] is set
{f2,(f . g2)} is set
{{f2,(f . g2)},{f2}} is set
(f ") . (f . g2) is set
[(f . g2),g2] is set
{(f . g2),g2} is set
{(f . g2)} is non empty trivial 1 -element set
{{(f . g2),g2},{(f . g2)}} is set
order_type_of f1 is epsilon-transitive epsilon-connected ordinal set
W is non empty set
[:W,W:] is non empty set
bool [:W,W:] is non empty set
the Element of W is Element of W
{ the Element of W} is non empty trivial 1 -element set
W \ { the Element of W} is Element of bool W
bool W is non empty set
card (W \ { the Element of W}) is epsilon-transitive epsilon-connected ordinal cardinal set
{(card (W \ { the Element of W}))} is non empty trivial 1 -element set
succ (card (W \ { the Element of W})) is non empty epsilon-transitive epsilon-connected ordinal set
(card (W \ { the Element of W})) \/ {(card (W \ { the Element of W}))} is set
(W \ { the Element of W}) \/ { the Element of W} is set
b is Relation-like W -defined W -valued V16(W) quasi_total reflexive antisymmetric transitive Element of bool [:W,W:]
order_type_of b is epsilon-transitive epsilon-connected ordinal set
field b is set
RelIncl (order_type_of b) is Relation-like order_type_of b -defined order_type_of b -valued well_founded well-ordering V16( order_type_of b) quasi_total reflexive antisymmetric connected transitive Element of bool [:(order_type_of b),(order_type_of b):]
[:(order_type_of b),(order_type_of b):] is set
bool [:(order_type_of b),(order_type_of b):] is non empty set
f is Relation-like Function-like set
rng f is set
field (RelIncl (order_type_of b)) is set
dom f is set
f . (card (W \ { the Element of W})) is set
a1 is set
b1 is set
[b1,a1] is set
{b1,a1} is set
{b1} is non empty trivial 1 -element set
{{b1,a1},{b1}} is set
f " is Relation-like Function-like set
(f ") . b1 is set
b9 is epsilon-transitive epsilon-connected ordinal set
[b9,(card (W \ { the Element of W}))] is set
{b9,(card (W \ { the Element of W}))} is set
{b9} is non empty trivial 1 -element set
{{b9,(card (W \ { the Element of W}))},{b9}} is set
f . b9 is set
[(f . b9),a1] is set
{(f . b9),a1} is set
{(f . b9)} is non empty trivial 1 -element set
{{(f . b9),a1},{(f . b9)}} is set
W is non empty V57() reflexive RelStr
the InternalRel of W is Relation-like the carrier of W -defined the carrier of W -valued V16( the carrier of W) quasi_total reflexive 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
the carrier of W \/ the carrier of W is set
field the InternalRel of W is set
a is Element of the carrier of W
b is set
[b,a] is set
{b,a} is set
{b} is non empty trivial 1 -element set
{{b,a},{b}} is set
f is Element of the carrier of W
the Element of the carrier of W is Element of the carrier of W
b is set
[ the Element of the carrier of W, the Element of the carrier of W] is set
{ the Element of the carrier of W, the Element of the carrier of W} is set
{ the Element of the carrier of W} is non empty trivial 1 -element set
{{ the Element of the carrier of W, the Element of the carrier of W},{ the Element of the carrier of W}} is set
[ the Element of the carrier of W,b] is set
{ the Element of the carrier of W,b} is set
{{ the Element of the carrier of W,b},{ the Element of the carrier of W}} is set
f is Element of the carrier of W
a1 is Element of the carrier of W
[a1,a1] is set
{a1,a1} is set
{a1} is non empty trivial 1 -element set
{{a1,a1},{a1}} is set
[a1,f] is set
{a1,f} is set
{{a1,f},{a1}} is set
W is non empty V57() reflexive transitive antisymmetric upper-bounded RelStr
the InternalRel of W is Relation-like the carrier of W -defined the carrier of W -valued V16( the carrier of W) quasi_total reflexive antisymmetric transitive 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
field the InternalRel of W is set
a is Element of the carrier of W
b is Element of the carrier of W
[a,b] is set
{a,b} is set
{a} is non empty trivial 1 -element set
{{a,b},{a}} is set
[b,a] is set
{b,a} is set
{b} is non empty trivial 1 -element set
{{b,a},{b}} is set
the Element of the carrier of W is Element of the carrier of W
b is set
f is set
a1 is set
a1 is set
[ the Element of the carrier of W,a1] is set
{ the Element of the carrier of W,a1} is set
{ the Element of the carrier of W} is non empty trivial 1 -element set
{{ the Element of the carrier of W,a1},{ the Element of the carrier of W}} is set
b1 is Element of the carrier of W
b9 is Element of the carrier of W
[b9,b1] is set
{b9,b1} is set
{b9} is non empty trivial 1 -element set
{{b9,b1},{b9}} is set
b9 is set
B is Element of the carrier of W
f1 is Element of the carrier of W
[f1,B] is set
{f1,B} is set
{f1} is non empty trivial 1 -element set
{{f1,B},{f1}} is set
f1 is Element of the carrier of W
f2 is Element of the carrier of W
[f2,f1] is set
{f2,f1} is set
{f2} is non empty trivial 1 -element set
{{f2,f1},{f2}} is set
[B,f1] is set
{B,f1} is set
{B} is non empty trivial 1 -element set
{{B,f1},{B}} is set
W is non empty V57() reflexive transitive antisymmetric upper-bounded RelStr
the InternalRel of W is Relation-like the carrier of W -defined the carrier of W -valued V16( the carrier of W) quasi_total reflexive antisymmetric transitive 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
order_type_of the InternalRel of W is epsilon-transitive epsilon-connected ordinal set
RelIncl (order_type_of the InternalRel of W) is Relation-like order_type_of the InternalRel of W -defined order_type_of the InternalRel of W -valued well_founded well-ordering V16( order_type_of the InternalRel of W) quasi_total reflexive antisymmetric connected transitive Element of bool [:(order_type_of the InternalRel of W),(order_type_of the InternalRel of W):]
[:(order_type_of the InternalRel of W),(order_type_of the InternalRel of W):] is set
bool [:(order_type_of the InternalRel of W),(order_type_of the InternalRel of W):] is non empty set
field (RelIncl (order_type_of the InternalRel of W)) is set
b1 is Element of the carrier of W
a1 is Element of the carrier of W
b9 is Relation-like Function-like set
[b1,a1] is set
{b1,a1} is set
{b1} is non empty trivial 1 -element set
{{b1,a1},{b1}} is set
b9 . b1 is set
b9 . a1 is set
[(b9 . b1),(b9 . a1)] is set
{(b9 . b1),(b9 . a1)} is set
{(b9 . b1)} is non empty trivial 1 -element set
{{(b9 . b1),(b9 . a1)},{(b9 . b1)}} is set
f1 is epsilon-transitive epsilon-connected ordinal set
B is epsilon-transitive epsilon-connected ordinal set
succ f1 is non empty epsilon-transitive epsilon-connected ordinal set
[(succ f1),(b9 . a1)] is set
{(succ f1),(b9 . a1)} is set
{(succ f1)} is non empty trivial 1 -element with_non-empty_elements non empty-membered set
{{(succ f1),(b9 . a1)},{(succ f1)}} is set
rng b9 is set
dom b9 is set
f2 is set
b9 . f2 is set
field the InternalRel of W is set
g2 is Element of the carrier of W
bool the carrier of W is non empty set
g1 is non empty directed Element of bool the carrier of W
sup g1 is Element of the carrier of W
f is non empty V57() reflexive transitive antisymmetric lower-bounded upper-bounded V121() with_suprema with_infima complete connected up-complete /\-complete satisfying_axiom_of_approximation continuous RelStr
f9 is Element of the carrier of W
[f9,g2] is set
{f9,g2} is set
{f9} is non empty trivial 1 -element set
{{f9,g2},{f9}} is set
b9 . f9 is set
[(b9 . f9),(succ f1)] is set
{(b9 . f9),(succ f1)} is set
{(b9 . f9)} is non empty trivial 1 -element set
{{(b9 . f9),(succ f1)},{(b9 . f9)}} is set
g9 is epsilon-transitive epsilon-connected ordinal set
[g9,f1] is set
{g9,f1} is set
{g9} is non empty trivial 1 -element set
{{g9,f1},{g9}} is set
[f9,b1] is set
{f9,b1} is set
{{f9,b1},{f9}} is set
[g2,b1] is set
{g2,b1} is set
{g2} is non empty trivial 1 -element set
{{g2,b1},{g2}} is set
[(succ f1),f1] is set
{(succ f1),f1} is set
{{(succ f1),f1},{(succ f1)}} is set
[(b9 . b1),(succ f1)] is set
{(b9 . b1),(succ f1)} is set
{{(b9 . b1),(succ f1)},{(b9 . b1)}} is set
[b1,g2] is set
{b1,g2} is set
{{b1,g2},{b1}} is set
[g2,a1] is set
{g2,a1} is set
{g2} is non empty trivial 1 -element set
{{g2,a1},{g2}} is set
W is non empty V57() reflexive transitive antisymmetric upper-bounded RelStr
the InternalRel of W is Relation-like the carrier of W -defined the carrier of W -valued V16( the carrier of W) quasi_total reflexive antisymmetric transitive 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
a is non empty V57() reflexive transitive antisymmetric lower-bounded upper-bounded V121() with_suprema with_infima complete connected up-complete /\-complete satisfying_axiom_of_approximation continuous RelStr
the carrier of a is non empty set
b is Element of the carrier of a
f is Element of the carrier of a
a1 is Element of the carrier of a
b1 is Element of the carrier of a
CompactSublatt a is non empty strict V57() reflexive transitive antisymmetric full V124(a) with_suprema M24(a)
the carrier of (CompactSublatt a) is non empty set
W is non empty set
[:W,W:] is non empty set
bool [:W,W:] is non empty set
a is Relation-like W -defined W -valued well_founded well-ordering V16(W) quasi_total reflexive antisymmetric connected transitive () Element of bool [:W,W:]
RelStr(# W,a #) is non empty strict V57() reflexive transitive antisymmetric RelStr
W is non empty set
a is Element of W
b is non empty set
[:b,b:] is non empty set
bool [:b,b:] is non empty set
the Relation-like b -defined b -valued well_founded well-ordering V16(b) quasi_total reflexive antisymmetric connected transitive () Element of bool [:b,b:] is Relation-like b -defined b -valued well_founded well-ordering V16(b) quasi_total reflexive antisymmetric connected transitive () Element of bool [:b,b:]
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:]
RelStr(# b, the Relation-like b -defined b -valued well_founded well-ordering V16(b) quasi_total reflexive antisymmetric connected transitive () Element of bool [:b,b:] #) is non empty strict V57() reflexive transitive antisymmetric lower-bounded upper-bounded V121() satisfying_axiom_K algebraic with_suprema with_infima complete connected up-complete /\-complete satisfying_axiom_of_approximation continuous RelStr
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
b9 is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of b9 is non empty set
[: the carrier of b1, the carrier of b9:] is non empty set
bool [: the carrier of b1, the carrier of b9:] is non empty set
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:]
f1 is Relation-like the carrier of b1 -defined the carrier of b9 -valued Function-like non empty V16( the carrier of b1) quasi_total Element of bool [: the carrier of b1, the carrier of b9:]
f1 * B is Relation-like the carrier of a1 -defined the carrier of b9 -valued Function-like non empty V16( the carrier of a1) quasi_total Element of bool [: the carrier of a1, the carrier of b9:]
[: the carrier of a1, the carrier of b9:] is non empty set
bool [: the carrier of a1, the carrier of b9:] is non empty 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
a1 is non empty transitive strict semi-functional V110() with_units reflexive para-functional set-id-inheriting concrete () () AltCatStr
the carrier of 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
b9 is Element of the carrier of f
(f,b9) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (f,b9) is non empty set
[: the carrier of (f,b1), the carrier of (f,b9):] is non empty set
bool [: the carrier of (f,b1), the carrier of (f,b9):] is non empty set
B is Relation-like the carrier of (f,b1) -defined the carrier of (f,b9) -valued Function-like non empty V16( the carrier of (f,b1)) quasi_total monotone Element of bool [: the carrier of (f,b1), the carrier of (f,b9):]
<^b1,b9^> 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 . (b1,b9) is set
[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 . [b1,b9] is set
f1 is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of f1 is non empty set
f2 is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of f2 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
g2 is Relation-like the carrier of f1 -defined the carrier of f2 -valued Function-like non empty V16( the carrier of f1) quasi_total Element of bool [: the carrier of f1, the carrier of f2:]
b1 is Element of the carrier of a1
(a1,b1) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (a1,b1) is non empty set
b9 is Element of the carrier of a1
(a1,b9) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (a1,b9) is non empty set
[: the carrier of (a1,b1), the carrier of (a1,b9):] is non empty set
bool [: the carrier of (a1,b1), the carrier of (a1,b9):] is non empty set
B is Relation-like the carrier of (a1,b1) -defined the carrier of (a1,b9) -valued Function-like non empty V16( the carrier of (a1,b1)) quasi_total monotone Element of bool [: the carrier of (a1,b1), the carrier of (a1,b9):]
<^b1,b9^> is set
the Arrows of a1 is Relation-like [: the carrier of a1, the carrier of a1:] -defined Function-like V16([: the carrier of a1, the carrier of a1:]) set
[: the carrier of a1, the carrier of a1:] is non empty set
the Arrows of a1 . (b1,b9) is set
[b1,b9] is set
{b1,b9} is set
{b1} is non empty trivial 1 -element set
{{b1,b9},{b1}} is set
the Arrows of a1 . [b1,b9] is set
f1 is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of f1 is non empty set
f2 is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of f2 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
g2 is Relation-like the carrier of f1 -defined the carrier of f2 -valued Function-like non empty V16( the carrier of f1) quasi_total Element of bool [: the carrier of f1, the carrier of f2:]
W is non empty non empty-membered set
(W) is non empty transitive strict semi-functional V110() with_units reflexive para-functional set-id-inheriting concrete () () AltCatStr
the carrier of (W) is non empty set
b is Element of the carrier of (W)
((W),b) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
f is non empty set
b is Element of the carrier of (W)
((W),b) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of ((W),b) is non empty set
f is Element of the carrier of (W)
((W),f) is non empty V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of ((W),f) is non empty set
[: 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
<^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
a1 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 Element of bool [: the carrier of ((W),b), the carrier of ((W),f):]
B is non empty set
b1 is non empty V57() reflexive transitive antisymmetric lower-bounded upper-bounded V121() with_suprema with_infima complete up-complete /\-complete RelStr
the carrier of b1 is non empty set
b9 is non empty V57() reflexive transitive antisymmetric lower-bounded upper-bounded V121() with_suprema with_infima complete up-complete /\-complete RelStr
the carrier of b9 is non empty set
[: the carrier of b1, the carrier of b9:] is non empty set
bool [: the carrier of b1, the carrier of b9:] is non empty set
B is non empty set
W is non empty non empty-membered set
(W) is non empty transitive strict 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 set
a is set
b is Element of the carrier of (W)
((W),b) is non empty V57() reflexive transitive antisymmetric lower-bounded upper-bounded V121() with_suprema with_infima complete up-complete /\-complete RelStr
the carrier of ((W),b) is non empty set
f is non empty set
f is non empty set
W is non empty non empty-membered set
(W) is non empty transitive strict 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 set
a is set
b is Element of the carrier of (W)
((W),b) is non empty V57() reflexive transitive antisymmetric lower-bounded upper-bounded V121() with_suprema with_infima complete up-complete /\-complete RelStr
b is non empty V57() reflexive transitive antisymmetric lower-bounded upper-bounded V121() with_suprema with_infima complete up-complete /\-complete RelStr
(b) is 1-sorted
the carrier of (b) is set
W is non empty non empty-membered set
(W) is non empty transitive strict 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 V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of a is non empty set
(a) is 1-sorted
(W) is non empty set
W is non empty non empty-membered set
(W) is non empty transitive strict 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
((W),a) is non empty V57() reflexive transitive antisymmetric lower-bounded upper-bounded V121() with_suprema with_infima complete up-complete /\-complete RelStr
the carrier of ((W),a) is non empty set
((W),b) is non empty V57() reflexive transitive antisymmetric lower-bounded upper-bounded V121() with_suprema with_infima complete up-complete /\-complete 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
f is 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):]
((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
b1 is non empty set
a1 is non empty set
W is non empty non empty-membered set
(W) is non empty transitive strict 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
((W),a) is non empty V57() reflexive transitive antisymmetric lower-bounded upper-bounded V121() with_suprema with_infima complete up-complete /\-complete RelStr
the carrier of ((W),a) is non empty set
((W),b) is non empty V57() reflexive transitive antisymmetric lower-bounded upper-bounded V121() with_suprema with_infima complete up-complete /\-complete 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
the 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 directed-sups-preserving Element of bool [: the carrier of ((W),a), the carrier of ((W),b):] 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 directed-sups-preserving Element of bool [: the carrier of ((W),a), the carrier of ((W),b):]
W is non empty transitive V110() with_units reflexive set-id-inheriting AltCatStr
a is non empty transitive V110() with_units reflexive id-inheriting SubCatStr of W
the carrier of a is non empty set
b is Element of the carrier of a
idm b is retraction coretraction iso mono epi Element of <^b,b^>
<^b,b^> 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
the Arrows of a . (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 a . [b,b] is set
a -carrier_of b is set
dom (idm b) is set
id (a -carrier_of b) is Relation-like a -carrier_of b -defined a -carrier_of b -valued Function-like one-to-one V16(a -carrier_of b) quasi_total Element of bool [:(a -carrier_of b),(a -carrier_of b):]
[:(a -carrier_of b),(a -carrier_of b):] is set
bool [:(a -carrier_of b),(a -carrier_of b):] is non empty set
the carrier of W is non empty set
f is Element of the carrier of W
idm f is retraction coretraction iso mono epi Element of <^f,f^>
<^f,f^> 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 . (f,f) is set
[f,f] is set
{f,f} is set
{f} is non empty trivial 1 -element set
{{f,f},{f}} is set
the Arrows of W . [f,f] is set
W -carrier_of f is set
dom (idm f) is set
id (W -carrier_of f) is Relation-like W -carrier_of f -defined W -carrier_of f -valued Function-like one-to-one V16(W -carrier_of f) quasi_total Element of bool [:(W -carrier_of f),(W -carrier_of f):]
[:(W -carrier_of f),(W -carrier_of f):] is set
bool [:(W -carrier_of f),(W -carrier_of f):] is non empty set
W is non empty transitive V110() with_units reflexive para-functional AltCatStr
a is non empty transitive V110() with_units reflexive id-inheriting SubCatStr of W
the carrier of W is non empty set
b is Relation-like the carrier of W -defined Function-like V16( the carrier of W) set
the carrier of a is non empty set
b | the carrier of a is Relation-like Function-like set
dom b is Element of bool the carrier of W
bool the carrier of W is non empty set
dom (b | the carrier of a) is set
a1 is Relation-like the carrier of a -defined Function-like V16( the carrier of a) set
b1 is Element of the carrier of a
b9 is Element of the carrier of a
<^b1,b9^> 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 . (b1,b9) is set
[b1,b9] is set
{b1,b9} is set
{b1} is non empty trivial 1 -element set
{{b1,b9},{b1}} is set
the Arrows of a . [b1,b9] is set
a1 . b1 is set
a1 . b9 is set
Funcs ((a1 . b1),(a1 . b9)) is functional set
b . b1 is set
b . b9 is set
B is Element of the carrier of W
f1 is Element of the carrier of W
<^B,f1^> 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,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 W . [B,f1] is set
W is non empty transitive semi-functional V110() with_units reflexive AltCatStr
a is non empty transitive V110() SubCatStr of W
the carrier of a is non empty set
b is Element of the carrier of a
f is Element of the carrier of a
<^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 Element of the carrier of a
<^f,a1^> is set
the Arrows of a . (f,a1) is set
[f,a1] is set
{f,a1} is set
{f} is non empty trivial 1 -element set
{{f,a1},{f}} is set
the Arrows of a . [f,a1] is set
<^b,a1^> is set
the Arrows of a . (b,a1) is set
[b,a1] is set
{b,a1} is set
{{b,a1},{b}} is set
the Arrows of a . [b,a1] is set
the carrier of W is non empty set
b1 is Element of the carrier of W
b9 is Element of the carrier of W
<^b1,b9^> 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 . (b1,b9) is set
[b1,b9] is set
{b1,b9} is set
{b1} is non empty trivial 1 -element set
{{b1,b9},{b1}} is set
the Arrows of W . [b1,b9] is set
B is Element of the carrier of W
<^b9,B^> is set
the Arrows of W . (b9,B) is set
[b9,B] is set
{b9,B} is set
{b9} is non empty trivial 1 -element set
{{b9,B},{b9}} is set
the Arrows of W . [b9,B] is set
f1 is Element of <^b,f^>
f2 is Element of <^f,a1^>
f2 * f1 is Element of <^b,a1^>
<^b1,B^> is set
the Arrows of W . (b1,B) is set
[b1,B] is set
{b1,B} is set
{{b1,B},{b1}} is set
the Arrows of W . [b1,B] is set
f9 is Relation-like Function-like set
g9 is Relation-like Function-like set
f9 * g9 is Relation-like Function-like set
g1 is Element of <^b1,b9^>
g2 is Element of <^b9,B^>
g2 * g1 is Element of <^b1,B^>
W is non empty transitive V110() with_units reflexive () AltCatStr
a is non empty transitive V110() with_units reflexive id-inheriting SubCatStr of W
the carrier of a is non empty set
b is Element of the carrier of a
a -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 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,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 a . [b,b] is set
dom (idm b) is set
the carrier of W is non empty set
f is Element of the carrier of W
W -carrier_of f is set
idm f is retraction coretraction iso mono epi Element of <^f,f^>
<^f,f^> 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 . (f,f) is set
[f,f] is set
{f,f} is set
{f} is non empty trivial 1 -element set
{{f,f},{f}} is set
the Arrows of W . [f,f] is set
dom (idm f) is set
a1 is 1-sorted
the carrier of a1 is set
W is non empty transitive semi-functional V110() with_units reflexive para-functional set-id-inheriting concrete () () AltCatStr
a is non empty transitive semi-functional V110() with_units reflexive id-inheriting para-functional set-id-inheriting concrete () SubCatStr of W
the carrier of a is non empty set
the carrier of W is non empty set
b is Element of the carrier of a
f is Element of the carrier of W
b is Element of the carrier of a
f is Element of the carrier of a
<^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
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
a1 is Element of the carrier of W
b1 is Element of the carrier of W
<^a1,b1^> 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 . (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
W is non empty transitive semi-functional V110() with_units reflexive para-functional set-id-inheriting concrete () () () AltCatStr
a is non empty transitive semi-functional V110() with_units reflexive id-inheriting para-functional set-id-inheriting concrete () () SubCatStr of W
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 Element of bool [: the carrier of (a,b), the carrier of (a,f):]
the carrier of W is non empty set
b1 is Element of the carrier of W
b9 is Element of the carrier of W
<^b1,b9^> 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 . (b1,b9) is set
[b1,b9] is set
{b1,b9} is set
{b1} is non empty trivial 1 -element set
{{b1,b9},{b1}} is set
the Arrows of W . [b1,b9] is set
W is non empty transitive semi-functional V110() with_units reflexive para-functional set-id-inheriting concrete () () () AltCatStr
a is non empty transitive semi-functional V110() with_units reflexive id-inheriting para-functional set-id-inheriting concrete () () SubCatStr of W
the carrier of a is non empty set
b is Element of the carrier of a
the carrier of W is non empty set
f is Element of the carrier of W
W is non empty non empty-membered set
(W) is non empty transitive strict 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 set
[:a,a:] is non empty set
bool [:a,a:] is non empty set
the Relation-like a -defined a -valued well_founded well-ordering V16(a) quasi_total reflexive antisymmetric connected transitive () Element of bool [:a,a:] is Relation-like a -defined a -valued well_founded well-ordering V16(a) quasi_total reflexive antisymmetric connected transitive () Element of bool [:a,a:]
RelStr(# a, the Relation-like a -defined a -valued well_founded well-ordering V16(a) quasi_total reflexive antisymmetric connected transitive () Element of bool [:a,a:] #) is non empty strict V57() reflexive transitive antisymmetric lower-bounded upper-bounded V121() satisfying_axiom_K algebraic with_suprema with_infima complete connected up-complete /\-complete satisfying_axiom_of_approximation continuous RelStr
a1 is Element of the carrier of (W)
((W),a1) is non empty V57() reflexive transitive antisymmetric lower-bounded upper-bounded V121() with_suprema with_infima complete up-complete /\-complete RelStr
a1 is non empty transitive strict semi-functional V110() with_units reflexive full id-inheriting para-functional set-id-inheriting concrete () () () () SubCatStr of (W)
the carrier of a1 is non empty set
b1 is non empty transitive strict semi-functional V110() with_units reflexive full id-inheriting para-functional set-id-inheriting concrete () () () () SubCatStr of (W)
the carrier of b1 is non empty set
the Arrows of a1 is Relation-like [: the carrier of a1, the carrier of a1:] -defined Function-like V16([: the carrier of a1, the carrier of a1:]) set
[: the carrier of a1, the carrier of a1:] is non empty set
the Comp of a1 is Relation-like [: the carrier of a1, the carrier of a1, the carrier of a1:] -defined Function-like V16([: the carrier of a1, the carrier of a1, the carrier of a1:]) M21([: the carrier of a1, the carrier of a1, the carrier of a1:],{| the Arrows of a1, the Arrows of a1|},{| the Arrows of a1|})
[: the carrier of a1, the carrier of a1, the carrier of a1:] is non empty set
{| the Arrows of a1, the Arrows of a1|} is Relation-like [: the carrier of a1, the carrier of a1, the carrier of a1:] -defined Function-like V16([: the carrier of a1, the carrier of a1, the carrier of a1:]) set
{| the Arrows of a1|} is Relation-like [: the carrier of a1, the carrier of a1, the carrier of a1:] -defined Function-like V16([: the carrier of a1, the carrier of a1, the carrier of a1:]) set
AltCatStr(# the carrier of a1, the Arrows of a1, the Comp of a1 #) is strict AltCatStr
the Arrows of b1 is Relation-like [: the carrier of b1, the carrier of b1:] -defined Function-like V16([: the carrier of b1, the carrier of b1:]) set
[: the carrier of b1, the carrier of b1:] is non empty set
the Comp of b1 is Relation-like [: the carrier of b1, the carrier of b1, the carrier of b1:] -defined Function-like V16([: the carrier of b1, the carrier of b1, the carrier of b1:]) M21([: the carrier of b1, the carrier of b1, the carrier of b1:],{| the Arrows of b1, the Arrows of b1|},{| the Arrows of b1|})
[: the carrier of b1, the carrier of b1, the carrier of b1:] is non empty set
{| the Arrows of b1, the Arrows of b1|} is Relation-like [: the carrier of b1, the carrier of b1, the carrier of b1:] -defined Function-like V16([: the carrier of b1, the carrier of b1, the carrier of b1:]) set
{| the Arrows of b1|} is Relation-like [: the carrier of b1, the carrier of b1, the carrier of b1:] -defined Function-like V16([: the carrier of b1, the carrier of b1, the carrier of b1:]) set
AltCatStr(# the carrier of b1, the Arrows of b1, the Comp of b1 #) is strict AltCatStr
W is non empty non empty-membered set
(W) is non empty transitive strict semi-functional V110() with_units reflexive full id-inheriting para-functional set-id-inheriting concrete () () () () SubCatStr of (W)
(W) is non empty transitive strict 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 set
[:a,a:] is non empty set
bool [:a,a:] is non empty set
the Relation-like a -defined a -valued well_founded well-ordering V16(a) quasi_total reflexive antisymmetric connected transitive () Element of bool [:a,a:] is Relation-like a -defined a -valued well_founded well-ordering V16(a) quasi_total reflexive antisymmetric connected transitive () Element of bool [:a,a:]
RelStr(# a, the Relation-like a -defined a -valued well_founded well-ordering V16(a) quasi_total reflexive antisymmetric connected transitive () Element of bool [:a,a:] #) is non empty strict V57() reflexive transitive antisymmetric lower-bounded upper-bounded V121() satisfying_axiom_K algebraic with_suprema with_infima complete connected up-complete /\-complete satisfying_axiom_of_approximation continuous RelStr
the carrier of (W) is non empty set
a1 is Element of the carrier of (W)
((W),a1) is non empty V57() reflexive transitive antisymmetric lower-bounded upper-bounded V121() with_suprema with_infima complete up-complete /\-complete RelStr
b1 is Element of the carrier of (W)
((W),b1) is non empty V57() reflexive transitive antisymmetric lower-bounded upper-bounded V121() with_suprema with_infima complete up-complete /\-complete RelStr
a1 is non empty transitive strict semi-functional V110() with_units reflexive full id-inheriting para-functional set-id-inheriting concrete () () () () SubCatStr of (W)
the carrier of a1 is non empty set
b1 is non empty transitive strict semi-functional V110() with_units reflexive full id-inheriting para-functional set-id-inheriting concrete () () () () SubCatStr of (W)
the carrier of b1 is non empty set
the Arrows of a1 is Relation-like [: the carrier of a1, the carrier of a1:] -defined Function-like V16([: the carrier of a1, the carrier of a1:]) set
[: the carrier of a1, the carrier of a1:] is non empty set
the Comp of a1 is Relation-like [: the carrier of a1, the carrier of a1, the carrier of a1:] -defined Function-like V16([: the carrier of a1, the carrier of a1, the carrier of a1:]) M21([: the carrier of a1, the carrier of a1, the carrier of a1:],{| the Arrows of a1, the Arrows of a1|},{| the Arrows of a1|})
[: the carrier of a1, the carrier of a1, the carrier of a1:] is non empty set
{| the Arrows of a1, the Arrows of a1|} is Relation-like [: the carrier of a1, the carrier of a1, the carrier of a1:] -defined Function-like V16([: the carrier of a1, the carrier of a1, the carrier of a1:]) set
{| the Arrows of a1|} is Relation-like [: the carrier of a1, the carrier of a1, the carrier of a1:] -defined Function-like V16([: the carrier of a1, the carrier of a1, the carrier of a1:]) set
AltCatStr(# the carrier of a1, the Arrows of a1, the Comp of a1 #) is strict AltCatStr
the Arrows of b1 is Relation-like [: the carrier of b1, the carrier of b1:] -defined Function-like V16([: the carrier of b1, the carrier of b1:]) set
[: the carrier of b1, the carrier of b1:] is non empty set
the Comp of b1 is Relation-like [: the carrier of b1, the carrier of b1, the carrier of b1:] -defined Function-like V16([: the carrier of b1, the carrier of b1, the carrier of b1:]) M21([: the carrier of b1, the carrier of b1, the carrier of b1:],{| the Arrows of b1, the Arrows of b1|},{| the Arrows of b1|})
[: the carrier of b1, the carrier of b1, the carrier of b1:] is non empty set
{| the Arrows of b1, the Arrows of b1|} is Relation-like [: the carrier of b1, the carrier of b1, the carrier of b1:] -defined Function-like V16([: the carrier of b1, the carrier of b1, the carrier of b1:]) set
{| the Arrows of b1|} is Relation-like [: the carrier of b1, the carrier of b1, the carrier of b1:] -defined Function-like V16([: the carrier of b1, the carrier of b1, the carrier of b1:]) set
AltCatStr(# the carrier of b1, the Arrows of b1, the Comp of b1 #) is strict AltCatStr
W is non empty non empty-membered set
(W) is non empty transitive strict semi-functional V110() with_units reflexive full id-inheriting para-functional set-id-inheriting concrete () () () () SubCatStr of (W)
(W) is non empty transitive strict 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 V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of a is non empty set
b is Element of the carrier of (W)
((W),b) is non empty V57() reflexive transitive antisymmetric lower-bounded upper-bounded V121() with_suprema with_infima complete up-complete /\-complete RelStr
the carrier of (W) is non empty set
b is Element of the carrier of (W)
((W),b) is non empty V57() reflexive transitive antisymmetric lower-bounded upper-bounded V121() with_suprema with_infima complete up-complete /\-complete RelStr
W is non empty non empty-membered set
(W) is non empty transitive strict semi-functional V110() with_units reflexive full id-inheriting para-functional set-id-inheriting concrete () () () () SubCatStr of (W)
(W) is non empty transitive strict semi-functional V110() with_units reflexive full id-inheriting para-functional set-id-inheriting concrete () () () () SubCatStr of (W)
(W) is non empty transitive strict 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 V57() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of a is non empty set
b is Element of the carrier of (W)
((W),b) is non empty V57() reflexive transitive antisymmetric lower-bounded upper-bounded V121() with_suprema with_infima complete up-complete /\-complete RelStr
the carrier of (W) is non empty set
b is Element of the carrier of (W)
((W),b) is non empty V57() reflexive transitive antisymmetric lower-bounded upper-bounded V121() with_suprema with_infima complete up-complete /\-complete RelStr
W is non empty non empty-membered set
(W) is non empty transitive strict semi-functional V110() with_units reflexive full id-inheriting para-functional set-id-inheriting concrete () () () () SubCatStr of (W)
(W) is non empty transitive strict 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
((W),a) is non empty V57() reflexive transitive antisymmetric lower-bounded upper-bounded V121() with_suprema with_infima complete up-complete /\-complete RelStr
the carrier of ((W),a) is non empty set
((W),b) is non empty V57() reflexive transitive antisymmetric lower-bounded upper-bounded V121() with_suprema with_infima complete up-complete /\-complete 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
f is set
the carrier of (W) is non empty set
a1 is Element of the carrier of (W)
b1 is Element of the carrier of (W)
<^a1,b1^> 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) . (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
W is non empty non empty-membered set
(W) is non empty transitive strict semi-functional V110() with_units reflexive full id-inheriting para-functional set-id-inheriting concrete () () () () SubCatStr of (W)
(W) is non empty transitive strict semi-functional V110() with_units reflexive full id-inheriting para-functional set-id-inheriting concrete () () () () SubCatStr of (W)
(W) is non empty transitive strict 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
((W),a) is non empty V57() reflexive transitive antisymmetric lower-bounded upper-bounded V121() with_suprema with_infima complete up-complete /\-complete RelStr
the carrier of ((W),a) is non empty set
((W),b) is non empty V57() reflexive transitive antisymmetric lower-bounded upper-bounded V121() with_suprema with_infima complete up-complete /\-complete 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
f is set
the carrier of (W) is non empty set
a1 is Element of the carrier of (W)
b1 is Element of the carrier of (W)
<^a1,b1^> 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) . (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
W is non empty non empty-membered set
(W) is non empty transitive strict semi-functional V110() with_units reflexive full id-inheriting para-functional set-id-inheriting concrete () () () () SubCatStr of (W)
(W) is non empty transitive strict 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
((W),a) is non empty V57() reflexive transitive antisymmetric lower-bounded upper-bounded V121() with_suprema with_infima complete up-complete /\-complete RelStr
the carrier of ((W),a) is non empty set
((W),b) is non empty V57() reflexive transitive antisymmetric lower-bounded upper-bounded V121() with_suprema with_infima complete up-complete /\-complete 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
the 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 directed-sups-preserving Element of bool [: the carrier of ((W),a), the carrier of ((W),b):] 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 directed-sups-preserving Element of bool [: the carrier of ((W),a), the carrier of ((W),b):]
W is non empty non empty-membered set
(W) is non empty transitive strict semi-functional V110() with_units reflexive full id-inheriting para-functional set-id-inheriting concrete () () () () SubCatStr of (W)
(W) is non empty transitive strict semi-functional V110() with_units reflexive full id-inheriting para-functional set-id-inheriting concrete () () () () SubCatStr of (W)
(W) is non empty transitive strict 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
((W),a) is non empty V57() reflexive transitive antisymmetric lower-bounded upper-bounded V121() with_suprema with_infima complete up-complete /\-complete RelStr
the carrier of ((W),a) is non empty set
((W),b) is non empty V57() reflexive transitive antisymmetric lower-bounded upper-bounded V121() with_suprema with_infima complete up-complete /\-complete 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
the 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 directed-sups-preserving Element of bool [: the carrier of ((W),a), the carrier of ((W),b):] 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 directed-sups-preserving Element of bool [: the carrier of ((W),a), the carrier of ((W),b):]