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}