:: YELLOW21 semantic presentation

K139() is set
bool K139() is non empty set

bool omega is non empty V33() set
{} is 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

dom a is set
b is set
f is set

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

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

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

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

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

dom B is Element of bool b9
bool b9 is non empty set

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 set
a is set
(a) is 1-sorted
the carrier of (a) is set

(b) is 1-sorted

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

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

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

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

[:(),():] is set
bool [:(),():] is non empty set
dom (id ()) is Element of bool ()
bool () 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

MonFuncs (a1,b1) is set
b9 is set
B is set

dom a is set
b is set

the carrier of f is non empty set
a1 is set
b1 is set

the carrier of b9 is non empty set

dom b is set

[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,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

the carrier of f2 is non empty set

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

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

the carrier of b9 is non empty set

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

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

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

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

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

{} is non empty trivial 1 -element set

the carrier of a is non empty set

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

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

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

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

the carrier of W is non empty set
a is Element of the carrier of W

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

the carrier of W is non empty set

the carrier of W is non empty set
a is Element of the carrier of W
(a) is 1-sorted

the carrier of W is non empty set

the carrier of W is non empty set
a is Element of the carrier of W
(a) is 1-sorted

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

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

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

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

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

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

(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 * 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

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

the carrier of W is non empty set

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

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

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

the carrier of a is non empty set
b is Element of the carrier of a

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

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

the carrier of a is non empty set

the carrier of a is non empty set
(a) is 1-sorted

b is non empty 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
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

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

the carrier of f is non empty set

(a1) is 1-sorted
the carrier of a1 is non empty set
a1 is Element of the carrier of f

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

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

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

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

the carrier of W is non empty set

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

(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):]

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

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

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

the carrier of W is non empty set

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

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

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

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

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()

b9 is Element of the carrier of F2()

B is Element of the carrier of F2()

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

F4(W,a,f) is Relation-like Function-like set
f2 is Relation-like Function-like Element of <^b9,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()

<^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):]

<^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()

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

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

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

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

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

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()

b9 is Element of the carrier of F2()

B is Element of the carrier of F2()

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

F4(W,a,f) is Relation-like Function-like set
f2 is Relation-like Function-like Element of <^B,b9^>

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()

<^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):]

<^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()

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

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

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

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()

(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}