:: WAYBEL_5 semantic presentation

K282() is set
K286() is non empty non trivial V13() V14() V15() non finite V52() V53() countable denumerable Element of bool K282()
bool K282() is non empty set
K42() is non empty non trivial V13() V14() V15() non finite V52() V53() countable denumerable set
bool K42() is non empty non trivial non finite set
K204() is L6()
the carrier of K204() is set
bool K286() is non empty non trivial non finite set
K331() is set

1 is non empty V13() V14() V15() V19() finite V52() countable Element of K286()
K309() is M19()

bool is non empty set
PFuncs (K309(),) is set
{{},1} is non empty finite V42() countable set
[:1,1:] is non empty Relation-like finite countable set
bool [:1,1:] is non empty finite V42() countable set
[:[:1,1:],1:] is non empty Relation-like finite countable set
bool [:[:1,1:],1:] is non empty finite V42() countable set

the carrier of L is non empty set
bool the carrier of L is non empty set
S is Element of the carrier of L
waybelow S is non empty directed lower Element of bool the carrier of L
"\/" ((),L) is Element of the carrier of L
g is non empty directed lower Element of bool the carrier of L
"\/" (g,L) is Element of the carrier of L
S9 is set
{ b1 where b1 is Element of the carrier of L : b1 is_way_below S } is set
J is Element of the carrier of L

the carrier of L is non empty set
bool the carrier of L is non empty set
S is Element of the carrier of L
waybelow S is lower Element of bool the carrier of L
"\/" ((),L) is Element of the carrier of L
S is Element of the carrier of L
waybelow S is lower Element of bool the carrier of L
g is Element of the carrier of L
waybelow g is lower Element of bool the carrier of L

the carrier of L is non empty set
bool the carrier of L is non empty set
S is Element of the carrier of L
waybelow S is lower Element of bool the carrier of L
g is Element of the carrier of L
waybelow g is lower Element of bool the carrier of L
"\/" ((),L) is Element of the carrier of L
S9 is Element of the carrier of L
J is non empty directed lower Element of bool the carrier of L
"\/" (J,L) is Element of the carrier of L
waybelow S9 is lower Element of bool the carrier of L

the carrier of K is non empty set
bool the carrier of K is non empty set

the carrier of L is non empty set
bool the carrier of L is non empty set
S is Element of the carrier of L
waybelow S is lower Element of bool the carrier of L
g is non empty directed lower Element of bool the carrier of L
"\/" (g,L) is Element of the carrier of L
S9 is non empty directed lower Element of bool the carrier of L
"\/" (S9,L) is Element of the carrier of L

the carrier of L is non empty set
bool the carrier of L is non empty set
S is Element of the carrier of L
g is non empty directed lower Element of bool the carrier of L
"\/" (g,L) is Element of the carrier of L
S9 is set
K is non empty directed lower Element of bool the carrier of L
"\/" (K,L) is Element of the carrier of L
J is Element of the carrier of L
waybelow S is lower Element of bool the carrier of L
S9 is set
J is Element of the carrier of L
"\/" ((),L) is Element of the carrier of L
S9 is non empty directed lower Element of bool the carrier of L
"\/" (S9,L) is Element of the carrier of L

the carrier of L is non empty set
bool the carrier of L is non empty set
S is Element of the carrier of L

the carrier of g is non empty set
bool the carrier of g is non empty set

Ids L is non empty set

SupMap L is non empty Relation-like the carrier of (InclPoset (Ids L)) -defined the carrier of L -valued Function-like total quasi_total monotone Element of bool [: the carrier of (InclPoset (Ids L)), the carrier of L:]
the carrier of (InclPoset (Ids L)) is non empty set
the carrier of L is non empty set
[: the carrier of (InclPoset (Ids L)), the carrier of L:] is non empty Relation-like set
bool [: the carrier of (InclPoset (Ids L)), the carrier of L:] is non empty set
[: the carrier of L, the carrier of (InclPoset (Ids L)):] is non empty Relation-like set
bool [: the carrier of L, the carrier of (InclPoset (Ids L)):] is non empty set
S9 is non empty Relation-like the carrier of L -defined the carrier of (InclPoset (Ids L)) -valued Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
S9 is non empty Relation-like the carrier of L -defined the carrier of (InclPoset (Ids L)) -valued Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
J is Element of the carrier of L
S9 . J is Element of the carrier of (InclPoset (Ids L))
uparrow J is non empty filtered upper Element of bool the carrier of L
bool the carrier of L is non empty set
() " () is Element of bool the carrier of (InclPoset (Ids L))
bool the carrier of (InclPoset (Ids L)) is non empty set
"/\" ((() " ()),(InclPoset (Ids L))) is Element of the carrier of (InclPoset (Ids L))
{J} is non empty trivial finite V54(1) countable Element of bool the carrier of L
uparrow {J} is non empty upper Element of bool the carrier of L
() " () is Element of bool the carrier of (InclPoset (Ids L))
"/\" ((() " ()),(InclPoset (Ids L))) is Element of the carrier of (InclPoset (Ids L))
dom () is non empty Element of bool the carrier of (InclPoset (Ids L))
d is non empty directed lower Element of bool the carrier of L
"\/" (d,L) is Element of the carrier of L
dF is Element of the carrier of (InclPoset (Ids L))
gdF is Element of the carrier of (InclPoset (Ids L))
() . dF is Element of the carrier of L
() . d is set
gdF is Element of the carrier of (InclPoset (Ids L))
() . gdF is Element of the carrier of L
y is non empty directed lower Element of bool the carrier of L
"\/" (y,L) is Element of the carrier of L
F is non empty directed lower Element of bool the carrier of L
"\/" (F,L) is Element of the carrier of L
() . ("/\" ((() " ()),(InclPoset (Ids L)))) is Element of the carrier of L
[(),S9] is V31() Connection of InclPoset (Ids L),L
{(),S9} is non empty functional finite countable set

{{(),S9},{()}} is non empty finite V42() countable set

Ids L is non empty set

SupMap L is non empty Relation-like the carrier of (InclPoset (Ids L)) -defined the carrier of L -valued Function-like total quasi_total monotone Element of bool [: the carrier of (InclPoset (Ids L)), the carrier of L:]
the carrier of (InclPoset (Ids L)) is non empty set
the carrier of L is non empty set
[: the carrier of (InclPoset (Ids L)), the carrier of L:] is non empty Relation-like set
bool [: the carrier of (InclPoset (Ids L)), the carrier of L:] is non empty set
bool the carrier of L is non empty set
S9 is Element of the carrier of L
uparrow S9 is non empty filtered upper Element of bool the carrier of L
() " (uparrow S9) is Element of bool the carrier of (InclPoset (Ids L))
bool the carrier of (InclPoset (Ids L)) is non empty set
"/\" ((() " (uparrow S9)),(InclPoset (Ids L))) is Element of the carrier of (InclPoset (Ids L))
K is non empty directed lower Element of bool the carrier of L
F is non empty directed lower Element of bool the carrier of L
"\/" (F,L) is Element of the carrier of L
d is Element of the carrier of (InclPoset (Ids L))
() . d is Element of the carrier of L
dom () is non empty Element of bool the carrier of (InclPoset (Ids L))
[: the carrier of L, the carrier of (InclPoset (Ids L)):] is non empty Relation-like set
bool [: the carrier of L, the carrier of (InclPoset (Ids L)):] is non empty set
F is non empty Relation-like the carrier of L -defined the carrier of (InclPoset (Ids L)) -valued Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
[(),F] is V31() Connection of InclPoset (Ids L),L
{(),F} is non empty functional finite countable set

{{(),F},{()}} is non empty finite V42() countable set
F . S9 is Element of the carrier of (InclPoset (Ids L))
() . K is set
() . ("/\" ((() " (uparrow S9)),(InclPoset (Ids L)))) is Element of the carrier of L
"\/" (K,L) is Element of the carrier of L

Ids L is non empty set

SupMap L is non empty Relation-like the carrier of (InclPoset (Ids L)) -defined the carrier of L -valued Function-like total quasi_total monotone Element of bool [: the carrier of (InclPoset (Ids L)), the carrier of L:]
the carrier of (InclPoset (Ids L)) is non empty set
the carrier of L is non empty set
[: the carrier of (InclPoset (Ids L)), the carrier of L:] is non empty Relation-like set
bool [: the carrier of (InclPoset (Ids L)), the carrier of L:] is non empty set
[: the carrier of L, the carrier of (InclPoset (Ids L)):] is non empty Relation-like set
bool [: the carrier of L, the carrier of (InclPoset (Ids L)):] is non empty set
g is non empty Relation-like the carrier of L -defined the carrier of (InclPoset (Ids L)) -valued Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
[(),g] is V31() Connection of InclPoset (Ids L),L
{(),g} is non empty functional finite countable set

{{(),g},{()}} is non empty finite V42() countable set
L is set
L is set
L is set
S is set

{S} is non empty trivial finite V54(1) countable set

bool [:L,{S}:] is non empty set

J is set

g . J is set
[:(g . J),S:] is Relation-like set
bool [:(g . J),S:] is non empty set
(L --> S) . J is set
L is non empty set

S is non empty set

{S} is non empty trivial finite V54(1) countable set
[:L,{S}:] is non empty Relation-like set
bool [:L,{S}:] is non empty set

J is Element of L

g . J is set
[:(g . J),S:] is Relation-like set
bool [:(g . J),S:] is non empty set
L is non empty set

S is non empty set

{S} is non empty trivial finite V54(1) countable set
[:L,{S}:] is non empty Relation-like set
bool [:L,{S}:] is non empty set

J is Element of L
(L,S,g,S9,J) is non empty Relation-like g . J -defined S -valued Function-like total quasi_total Element of bool [:(g . J),S:]
g . J is non empty set
[:(g . J),S:] is non empty Relation-like set
bool [:(g . J),S:] is non empty set
rng (L,S,g,S9,J) is non empty Element of bool S
bool S is non empty set
L is set

S is non empty set

{S} is non empty trivial finite V54(1) countable set

bool [:L,{S}:] is non empty set

dom S9 is Element of bool L
bool L is non empty set
J is set

g . J is set
the Element of g . J is Element of g . J
[:(g . J),S:] is Relation-like set
bool [:(g . J),S:] is non empty set
proj1 (S9 . J) is set
(S9 . J) . the Element of g . J is set
[ the Element of g . J,((S9 . J) . the Element of g . J)] is V31() set
{ the Element of g . J,((S9 . J) . the Element of g . J)} is non empty finite countable set
{ the Element of g . J} is non empty trivial finite V54(1) countable set
{{ the Element of g . J,((S9 . J) . the Element of g . J)},{ the Element of g . J}} is non empty finite V42() countable set
S is set

dom () is functional with_common_domain Element of bool (product (doms L))
bool (product (doms L)) is non empty set

dom () is functional with_common_domain Element of bool (product (doms L))
bool (product (doms L)) is non empty set
proj1 L is set

proj1 S is set

proj1 (() . S) is set
proj1 (doms L) is set

proj1 g is set

proj1 (L .. S) is set

dom () is functional with_common_domain Element of bool (product (doms L))
bool (product (doms L)) is non empty set
proj1 L is set

proj2 (() . S) is set
S9 is set
S . S9 is set

proj1 (L . S9) is set
(() . S) . S9 is set
(L . S9) . (S . S9) is set
proj1 (doms L) is set
(doms L) . S9 is set

proj1 (() . S) is set
L is set
S is set

{S} is non empty trivial finite V54(1) countable set

bool [:L,{S}:] is non empty set
[:L,S:] is Relation-like set
bool [:L,S:] is non empty set

dom (Frege S9) is functional with_common_domain Element of bool (product (doms S9))
bool (product (doms S9)) is non empty set

proj1 ((Frege S9) . J) is set
dom S9 is Element of bool L
bool L is non empty set
proj2 ((Frege S9) . J) is set
F is set
d is set
((Frege S9) . J) . d is set

g . d is set
[:(g . d),S:] is Relation-like set
bool [:(g . d),S:] is non empty set
proj2 (S9 . d) is set
J . d is set
(S9 . d) . (J . d) is set
proj1 (S9 . d) is set
L is set
S is set

{S} is non empty trivial finite V54(1) countable set

bool [:L,{S}:] is non empty set

dom (Frege S9) is functional with_common_domain Element of bool (product (doms S9))
bool (product (doms S9)) is non empty set

proj2 ((Frege S9) . J) is set
K is set
((Frege S9) . J) . K is set

J . K is set
(S9 . K) . (J . K) is set
dom S9 is Element of bool L
bool L is non empty set
L is set

g is non empty set

{g} is non empty trivial finite V54(1) countable set

bool [:L,{g}:] is non empty set

dom (Frege S9) is functional with_common_domain Element of bool (product (doms S9))
bool (product (doms S9)) is non empty set

K is set
J . K is set
S . K is set

[:(S . K),g:] is Relation-like set
bool [:(S . K),g:] is non empty set
dom S9 is Element of bool L
bool L is non empty set
proj1 (S9 . K) is set

proj1 (doms L) is set
S is set
(doms L) . S is set
proj2 L is V22() set
SubFuncs () is set
L " (SubFuncs ()) is set
L . S is set
proj1 L is set

proj1 g is set
L is set

S is set

{S} is non empty trivial finite V54(1) countable set

bool [:L,{S}:] is non empty set

{L} is non empty trivial finite V54(1) countable set
[:(product (doms S9)),{L}:] is Relation-like set
bool [:(product (doms S9)),{L}:] is non empty set

[:(product (doms S9)),{S}:] is Relation-like set
bool [:(product (doms S9)),{S}:] is non empty set

dF is set
(Frege S9) . dF is Relation-like Function-like set
((product (doms S9)) --> L) . dF is set
((product (doms S9)) --> S) . dF is set
[:(((product (doms S9)) --> L) . dF),(((product (doms S9)) --> S) . dF):] is Relation-like set
bool [:(((product (doms S9)) --> L) . dF),(((product (doms S9)) --> S) . dF):] is non empty set
dom (Frege S9) is functional with_common_domain Element of bool (product (doms S9))
bool (product (doms S9)) is non empty set

(Frege S9) . gdF is Relation-like Function-like set
L is non empty set

S is non empty set

{S} is non empty trivial finite V54(1) countable set
[:L,{S}:] is non empty Relation-like set
bool [:L,{S}:] is non empty set

(product (doms S9)) --> L is non empty Relation-like non-empty non empty-yielding product (doms S9) -defined {L} -valued Function-like constant total quasi_total Element of bool [:(product (doms S9)),{L}:]
{L} is non empty trivial finite V54(1) countable set
[:(product (doms S9)),{L}:] is non empty Relation-like set
bool [:(product (doms S9)),{L}:] is non empty set
(product (doms S9)) --> S is non empty Relation-like non-empty non empty-yielding product (doms S9) -defined {S} -valued Function-like constant total quasi_total Element of bool [:(product (doms S9)),{S}:]
[:(product (doms S9)),{S}:] is non empty Relation-like set
bool [:(product (doms S9)),{S}:] is non empty set
J is non empty Relation-like non-empty non empty-yielding product (doms S9) -defined Function-like total Function-yielding V129() ManySortedFunction of (product (doms S9)) --> L,(product (doms S9)) --> S

J . K is non empty Relation-like Function-like set
[:L,S:] is non empty Relation-like set
bool [:L,S:] is non empty set
((product (doms S9)) --> L) . K is non empty Element of {L}
((product (doms S9)),S,((product (doms S9)) --> L),J,K) is non empty Relation-like ((product (doms S9)) --> L) . K -defined S -valued Function-like total quasi_total Element of bool [:(((product (doms S9)) --> L) . K),S:]
((product (doms S9)) --> L) . K is non empty set
[:(((product (doms S9)) --> L) . K),S:] is non empty Relation-like set
bool [:(((product (doms S9)) --> L) . K),S:] is non empty set

proj1 S is set
L is non empty RelStr
the carrier of L is non empty set
[:(), the carrier of L:] is Relation-like set
bool [:(), the carrier of L:] is non empty set

proj1 g is set

proj1 g is set
proj2 g is set
S9 is set
J is set
g . J is set

\\/ ((S . J),L) is Element of the carrier of L
S9 is Relation-like proj1 S -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(), the carrier of L:]
J is set
S9 . J is set

\\/ ((S . J),L) is Element of the carrier of L
g is Relation-like proj1 S -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(), the carrier of L:]
S9 is Relation-like proj1 S -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(), the carrier of L:]
J is set
g . J is set

\\/ ((S . J),L) is Element of the carrier of L
S9 . J is set
dom g is Element of bool ()
bool () is non empty set
dom S9 is Element of bool ()

proj1 g is set

proj1 g is set
proj2 g is set
S9 is set
J is set
g . J is set

//\ ((S . J),L) is Element of the carrier of L
S9 is Relation-like proj1 S -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(), the carrier of L:]
J is set
S9 . J is set

//\ ((S . J),L) is Element of the carrier of L
g is Relation-like proj1 S -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(), the carrier of L:]
S9 is Relation-like proj1 S -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(), the carrier of L:]
J is set
g . J is set

//\ ((S . J),L) is Element of the carrier of L
S9 . J is set
dom g is Element of bool ()
bool () is non empty set
dom S9 is Element of bool ()
L is set

g is non empty RelStr
the carrier of g is non empty set
L --> the carrier of g is Relation-like non-empty L -defined { the carrier of g} -valued Function-like constant total quasi_total Element of bool [:L,{ the carrier of g}:]
{ the carrier of g} is non empty trivial finite V54(1) countable set
[:L,{ the carrier of g}:] is Relation-like set
bool [:L,{ the carrier of g}:] is non empty set
L is set
S is set

{S} is non empty trivial finite V54(1) countable set

bool [:L,{S}:] is non empty set
g is non empty RelStr
the carrier of g is non empty set
L --> the carrier of g is Relation-like non-empty L -defined { the carrier of g} -valued Function-like constant total quasi_total Element of bool [:L,{ the carrier of g}:]
{ the carrier of g} is non empty trivial finite V54(1) countable set
[:L,{ the carrier of g}:] is Relation-like set
bool [:L,{ the carrier of g}:] is non empty set
L is non empty RelStr
the carrier of L is non empty set

proj1 S is set

proj1 g is set
(L,S) is Relation-like proj1 S -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(), the carrier of L:]
[:(), the carrier of L:] is Relation-like set
bool [:(), the carrier of L:] is non empty set
(L,g) is Relation-like proj1 g -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(), the carrier of L:]
[:(), the carrier of L:] is Relation-like set
bool [:(), the carrier of L:] is non empty set
S9 is set
(L,S) . S9 is set
(L,g) . S9 is set

\\/ ((S . S9),L) is Element of the carrier of L

\\/ ((g . S9),L) is Element of the carrier of L
dom (L,S) is Element of bool ()
bool () is non empty set
dom (L,g) is Element of bool ()
bool () is non empty set
L is non empty RelStr
the carrier of L is non empty set

proj1 S is set

proj1 g is set
(L,S) is Relation-like proj1 S -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(), the carrier of L:]
[:(), the carrier of L:] is Relation-like set
bool [:(), the carrier of L:] is non empty set
(L,g) is Relation-like proj1 g -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(), the carrier of L:]
[:(), the carrier of L:] is Relation-like set
bool [:(), the carrier of L:] is non empty set
S9 is set
(L,S) . S9 is set
(L,g) . S9 is set

//\ ((S . S9),L) is Element of the carrier of L

//\ ((g . S9),L) is Element of the carrier of L
dom (L,S) is Element of bool ()
bool () is non empty set
dom (L,g) is Element of bool ()
bool () is non empty set
L is set
S is non empty RelStr
the carrier of S is non empty set

(S,g) is Relation-like proj1 g -defined the carrier of S -valued Function-like total quasi_total Element of bool [:(), the carrier of S:]
proj1 g is set
[:(), the carrier of S:] is Relation-like set
bool [:(), the carrier of S:] is non empty set
rng (S,g) is Element of bool the carrier of S
bool the carrier of S is non empty set
(S,g) is Relation-like proj1 g -defined the carrier of S -valued Function-like total quasi_total Element of bool [:(), the carrier of S:]
rng (S,g) is Element of bool the carrier of S
dom (S,g) is Element of bool ()
bool () is non empty set
S9 is set
(S,g) . S9 is set
J is set

\\/ ((g . J),S) is Element of the carrier of S
S9 is set

\\/ ((g . S9),S) is Element of the carrier of S
(S,g) . S9 is set
dom (S,g) is Element of bool ()
bool () is non empty set
S9 is set
(S,g) . S9 is set
J is set

//\ ((g . J),S) is Element of the carrier of S
S9 is set

//\ ((g . S9),S) is Element of the carrier of S
(S,g) . S9 is set
L is set
S is non empty RelStr
the carrier of S is non empty set
g is non empty set
g --> the carrier of S is non empty Relation-like non-empty non empty-yielding g -defined { the carrier of S} -valued Function-like constant total quasi_total Element of bool [:g,{ the carrier of S}:]
{ the carrier of S} is non empty trivial finite V54(1) countable set
[:g,{ the carrier of S}:] is non empty Relation-like set
bool [:g,{ the carrier of S}:] is non empty set

J is non empty Relation-like g -defined Function-like total Function-yielding V129() ManySortedFunction of S9,g --> the carrier of S
(S,J) is non empty Relation-like proj1 J -defined the carrier of S -valued Function-like total quasi_total Element of bool [:(), the carrier of S:]
proj1 J is non empty set
[:(), the carrier of S:] is non empty Relation-like set
bool [:(), the carrier of S:] is non empty set
rng (S,J) is non empty Element of bool the carrier of S
bool the carrier of S is non empty set
(S,J) is non empty Relation-like proj1 J -defined the carrier of S -valued Function-like total quasi_total Element of bool [:(), the carrier of S:]
rng (S,J) is non empty Element of bool the carrier of S
dom J is non empty Element of bool g
bool g is non empty set
K is set

\\/ ((J . K),S) is Element of the carrier of S
F is Element of g
d is Element of g
(g, the carrier of S,S9,J,d) is Relation-like S9 . d -defined the carrier of S -valued Function-like total quasi_total Element of bool [:(S9 . d), the carrier of S:]
S9 . d is set
[:(S9 . d), the carrier of S:] is Relation-like set
bool [:(S9 . d), the carrier of S:] is non empty set
\\/ ((g, the carrier of S,S9,J,d),S) is Element of the carrier of S
K is Element of g
(g, the carrier of S,S9,J,K) is Relation-like S9 . K -defined the carrier of S -valued Function-like total quasi_total Element of bool [:(S9 . K), the carrier of S:]
S9 . K is set
[:(S9 . K), the carrier of S:] is Relation-like set
bool [:(S9 . K), the carrier of S:] is non empty set
\\/ ((g, the carrier of S,S9,J,K),S) is Element of the carrier of S
K is set

//\ ((J . K),S) is Element of the carrier of S
F is Element of g
d is Element of g
(g, the carrier of S,S9,J,d) is Relation-like S9 . d -defined the carrier of S -valued Function-like total quasi_total Element of bool [:(S9 . d), the carrier of S:]
S9 . d is set
[:(S9 . d), the carrier of S:] is Relation-like set
bool [:(S9 . d), the carrier of S:] is non empty set
//\ ((g, the carrier of S,S9,J,d),S) is Element of the carrier of S
K is Element of g
(g, the carrier of S,S9,J,K) is Relation-like S9 . K -defined the carrier of S -valued Function-like total quasi_total Element of bool [:(S9 . K), the carrier of S:]
S9 . K is set
[:(S9 . K), the carrier of S:] is Relation-like set
bool [:(S9 . K), the carrier of S:] is non empty set
//\ ((g, the carrier of S,S9,J,K),S) is Element of the carrier of S
L is non empty set

g is non empty RelStr
the carrier of g is non empty set
L --> the carrier of g is non empty Relation-like non-empty non empty-yielding L -defined { the carrier of g} -valued Function-like constant total quasi_total Element of bool [:L,{ the carrier of g}:]
{ the carrier of g} is non empty trivial finite V54(1) countable set
[:L,{ the carrier of g}:] is non empty Relation-like set
bool [:L,{ the carrier of g}:] is non empty set
S9 is non empty Relation-like L -defined Function-like total Function-yielding V129() ManySortedFunction of S,L --> the carrier of g
(g,S9) is non empty Relation-like proj1 S9 -defined the carrier of g -valued Function-like total quasi_total Element of bool [:(proj1 S9), the carrier of g:]
proj1 S9 is non empty set
[:(proj1 S9), the carrier of g:] is non empty Relation-like set
bool [:(proj1 S9), the carrier of g:] is non empty set
rng (g,S9) is non empty Element of bool the carrier of g
bool the carrier of g is non empty set
(g,S9) is non empty Relation-like proj1 S9 -defined the carrier of g -valued Function-like total quasi_total Element of bool [:(proj1 S9), the carrier of g:]
rng (g,S9) is non empty Element of bool the carrier of g

the carrier of L is non empty set
S is non empty set
S --> the carrier of L is non empty Relation-like non-empty non empty-yielding S -defined { the carrier of L} -valued Function-like constant total quasi_total Element of bool [:S,{ the carrier of L}:]
{ the carrier of L} is non empty trivial finite V54(1) countable set
[:S,{ the carrier of L}:] is non empty Relation-like set
bool [:S,{ the carrier of L}:] is non empty set

(S, the carrier of L,g,S9) is non empty Relation-like non-empty non empty-yielding product (doms S9) -defined Function-like total Function-yielding V129() ManySortedFunction of (product (doms S9)) --> S,(product (doms S9)) --> the carrier of L
(product (doms S9)) --> S is non empty Relation-like non-empty non empty-yielding product (doms S9) -defined {S} -valued Function-like constant total quasi_total Element of bool [:(product (doms S9)),{S}:]
{S} is non empty trivial finite V54(1) countable set
[:(product (doms S9)),{S}:] is non empty Relation-like set
bool [:(product (doms S9)),{S}:] is non empty set
(product (doms S9)) --> the carrier of L is non empty Relation-like non-empty non empty-yielding product (doms S9) -defined { the carrier of L} -valued Function-like constant total quasi_total Element of bool [:(product (doms S9)),{ the carrier of L}:]
[:(product (doms S9)),{ the carrier of L}:] is non empty Relation-like set
bool [:(product (doms S9)),{ the carrier of L}:] is non empty set
dom (S, the carrier of L,g,S9) is non empty functional with_common_domain Element of bool (product (doms S9))
bool (product (doms S9)) is non empty set
J is set

the carrier of L is non empty set
S is Element of the carrier of L

dom () is functional with_common_domain Element of bool (product (doms g))
bool (product (doms g)) is non empty set
(L,()) is Relation-like proj1 () -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(proj1 ()), the carrier of L:]
proj1 () is set
[:(proj1 ()), the carrier of L:] is Relation-like set
bool [:(proj1 ()), the carrier of L:] is non empty set
\\/ ((L,()),L) is Element of the carrier of L
rng (L,()) is Element of bool the carrier of L
bool the carrier of L is non empty set
S9 is Element of the carrier of L
J is set

//\ ((() . J),L) is Element of the carrier of L

"\/" ((rng (L,())),L) is Element of the carrier of L

the carrier of L is non empty set
S is non empty set
S --> the carrier of L is non empty Relation-like non-empty non empty-yielding S -defined { the carrier of L} -valued Function-like constant total quasi_total Element of bool [:S,{ the carrier of L}:]
{ the carrier of L} is non empty trivial finite V54(1) countable set
[:S,{ the carrier of L}:] is non empty Relation-like set
bool [:S,{ the carrier of L}:] is non empty set

(S, the carrier of L,g,S9) is non empty Relation-like non-empty non empty-yielding product (doms S9) -defined Function-like total Function-yielding V129() ManySortedFunction of (product (doms S9)) --> S,(product (doms S9)) --> the carrier of L

(product (doms S9)) --> S is non empty Relation-like non-empty non empty-yielding product (doms S9) -defined {S} -valued Function-like constant total quasi_total Element of bool [:(product (doms S9)),{S}:]
{S} is non empty trivial finite V54(1) countable set
[:(product (doms S9)),{S}:] is non empty Relation-like set
bool [:(product (doms S9)),{S}:] is non empty set
(product (doms S9)) --> the carrier of L is non empty Relation-like non-empty non empty-yielding product (doms S9) -defined { the carrier of L} -valued Function-like constant total quasi_total Element of bool [:(product (doms S9)),{ the carrier of L}:]
[:(product (doms S9)),{ the carrier of L}:] is non empty Relation-like set
bool [:(product (doms S9)),{ the carrier of L}:] is non empty set
(L,(S, the carrier of L,g,S9)) is non empty Relation-like proj1 (S, the carrier of L,g,S9) -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(proj1 (S, the carrier of L,g,S9)), the carrier of L:]
proj1 (S, the carrier of L,g,S9) is non empty set
[:(proj1 (S, the carrier of L,g,S9)), the carrier of L:] is non empty Relation-like set
bool [:(proj1 (S, the carrier of L,g,S9)), the carrier of L:] is non empty set
\\/ ((L,(S, the carrier of L,g,S9)),L) is Element of the carrier of L
(L,S9) is non empty Relation-like proj1 S9 -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(proj1 S9), the carrier of L:]
proj1 S9 is non empty set
[:(proj1 S9), the carrier of L:] is non empty Relation-like set
bool [:(proj1 S9), the carrier of L:] is non empty set
//\ ((L,S9),L) is Element of the carrier of L
K is Element of S
(S, the carrier of L,g,S9,K) is non empty Relation-like g . K -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(g . K), the carrier of L:]
g . K is non empty set
[:(g . K), the carrier of L:] is non empty Relation-like set
bool [:(g . K), the carrier of L:] is non empty set
\\/ ((S, the carrier of L,g,S9,K),L) is Element of the carrier of L

(S, the carrier of L,g,S9,(S, the carrier of L,g,S9),F) is non empty Relation-like S -defined the carrier of L -valued Function-like total quasi_total Element of bool [:S, the carrier of L:]
[:S, the carrier of L:] is non empty Relation-like set
bool [:S, the carrier of L:] is non empty set
//\ ((S, the carrier of L,g,S9,(S, the carrier of L,g,S9),F),L) is Element of the carrier of L
dom (S, the carrier of L,g,S9) is non empty functional with_common_domain Element of bool (product (doms S9))
bool (product (doms S9)) is non empty set
F . K is set
d is Element of g . K
(S, the carrier of L,g,S9,K) . d is Element of the carrier of L
(S, the carrier of L,g,S9,(S, the carrier of L,g,S9),F) . K is Element of the carrier of L
rng (L,S9) is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
K is Element of the carrier of L
F is Element of S
(S, the carrier of L,g,S9,F) is non empty Relation-like g . F -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(g . F), the carrier of L:]
g . F is non empty set
[:(g . F), the carrier of L:] is non empty Relation-like set
bool [:(g . F), the carrier of L:] is non empty set
\\/ ((S, the carrier of L,g,S9,F),L) is Element of the carrier of L
dom (S, the carrier of L,g,S9) is non empty functional with_common_domain Element of bool (product (doms S9))
bool (product (doms S9)) is non empty set

(S, the carrier of L,g,S9) . d is Relation-like Function-like set
//\ (((S, the carrier of L,g,S9) . d),L) is Element of the carrier of L
"/\" ((rng (L,S9)),L) is Element of the carrier of L

the carrier of L is non empty set
S is Element of the carrier of L
g is Element of the carrier of L
S9 is Element of the carrier of L
waybelow S is non empty directed lower Element of bool the carrier of L
bool the carrier of L is non empty set
"\/" ((),L) is Element of the carrier of L

the carrier of L is non empty set
S is non empty set
S --> the carrier of L is non empty Relation-like non-empty non empty-yielding S -defined { the carrier of L} -valued Function-like constant total quasi_total Element of bool [:S,{ the carrier of L}:]
{ the carrier of L} is non empty trivial finite V54(1) countable set
[:S,{ the carrier of L}:] is non empty Relation-like set
bool [:S,{ the carrier of L}:] is non empty set

(L,S9) is non empty Relation-like proj1 S9 -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(proj1 S9), the carrier of L:]
proj1 S9 is non empty set
[:(proj1 S9), the carrier of L:] is non empty Relation-like set
bool [:(proj1 S9), the carrier of L:] is non empty set
//\ ((L,S9),L) is Element of the carrier of L
(S, the carrier of L,g,S9) is non empty Relation-like non-empty non empty-yielding product (doms S9) -defined Function-like total Function-yielding V129() ManySortedFunction of (product (doms S9)) --> S,(product (doms S9)) --> the carrier of L

(product (doms S9)) --> S is non empty Relation-like non-empty non empty-yielding product (doms S9) -defined {S} -valued Function-like constant total quasi_total Element of bool [:(product (doms S9)),{S}:]
{S} is non empty trivial finite V54(1) countable set
[:(product (doms S9)),{S}:] is non empty Relation-like set
bool [:(product (doms S9)),{S}:] is non empty set
(product (doms S9)) --> the carrier of L is non empty Relation-like non-empty non empty-yielding product (doms S9) -defined { the carrier of L} -valued Function-like constant total quasi_total Element of bool [:(product (doms S9)),{ the carrier of L}:]
[:(product (doms S9)),{ the carrier of L}:] is non empty Relation-like set
bool [:(product (doms S9)),{ the carrier of L}:] is non empty set
(L,(S, the carrier of L,g,S9)) is non empty Relation-like proj1 (S, the carrier of L,g,S9) -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(proj1 (S, the carrier of L,g,S9)), the carrier of L:]
proj1 (S, the carrier of L,g,S9) is non empty set
[:(proj1 (S, the carrier of L,g,S9)), the carrier of L:] is non empty Relation-like set
bool [:(proj1 (S, the carrier of L,g,S9)), the carrier of L:] is non empty set
\\/ ((L,(S, the carrier of L,g,S9)),L) is Element of the carrier of L
J is Element of the carrier of L
K is Element of S
(S, the carrier of L,g,S9,K) is non empty Relation-like g . K -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(g . K), the carrier of L:]
g . K is non empty set
[:(g . K), the carrier of L:] is non empty Relation-like set
bool [:(g . K), the carrier of L:] is non empty set
\\/ ((S, the carrier of L,g,S9,K),L) is Element of the carrier of L
rng (L,S9) is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
"/\" ((rng (L,S9)),L) is Element of the carrier of L
dom (S, the carrier of L,g,S9) is non empty functional with_common_domain Element of bool (product (doms S9))
bool (product (doms S9)) is non empty set
K is Element of S
g . K is non empty set
(S, the carrier of L,g,S9,K) is non empty Relation-like g . K -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(g . K), the carrier of L:]
[:(g . K), the carrier of L:] is non empty Relation-like set
bool [:(g . K), the carrier of L:] is non empty set
\\/ ((S, the carrier of L,g,S9,K),L) is Element of the carrier of L
rng (S, the carrier of L,g,S9,K) is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
"\/" ((rng (S, the carrier of L,g,S9,K)),L) is Element of the carrier of L
F is Element of the carrier of L
dom (S, the carrier of L,g,S9,K) is non empty Element of bool (g . K)
bool (g . K) is non empty set
d is set
(S, the carrier of L,g,S9,K) . d is set
dF is Element of g . K
(S, the carrier of L,g,S9,K) . dF is Element of the carrier of L
proj2 g is non empty V22() set
union () is set
K is set
g . K is set

F is Element of S
g . F is non empty set
(S, the carrier of L,g,S9,F) is non empty Relation-like g . F -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(g . F), the carrier of L:]
[:(g . F), the carrier of L:] is non empty Relation-like set
bool [:(g . F), the carrier of L:] is non empty set
d is Element of g . F
(S, the carrier of L,g,S9,F) . d is Element of the carrier of L
(S9 . K) . d is set
dom g is non empty Element of bool S
bool S is non empty set

proj1 K is set
proj2 K is set
F is set
proj1 (doms S9) is set
dom S9 is non empty Element of bool S
bool S is non empty set
(doms S9) . F is set
d is Element of S
g . d is non empty set
(S, the carrier of L,g,S9,d) is non empty Relation-like g . d -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(g . d), the carrier of L:]
[:(g . d), the carrier of L:] is non empty Relation-like set
bool [:(g . d), the carrier of L:] is non empty set
dom (S, the carrier of L,g,S9,d) is non empty Element of bool (g . d)
bool (g . d) is non empty set
K . F is set
F is Element of S
K . F is set
g . F is non empty set
d is Element of S
(S, the carrier of L,g,S9,d) is non empty Relation-like g . d -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(g . d), the carrier of L:]
g . d is non empty set
[:(g . d), the carrier of L:] is non empty Relation-like set
bool [:(g . d), the carrier of L:] is non empty set
K . d is set
(S, the carrier of L,g,S9,d) . (K . d) is set

[:S, the carrier of L:] is non empty Relation-like set
bool [:S, the carrier of L:] is non empty set

(S, the carrier of L,g,S9,(S, the carrier of L,g,S9),F) is non empty Relation-like S -defined the carrier of L -valued Function-like total quasi_total Element of bool [:S, the carrier of L:]
dF is Element of S
dom S9 is non empty Element of bool S
bool S is non empty set
(S, the carrier of L,g,S9,dF) is non empty Relation-like g . dF -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(g . dF), the carrier of L:]
g . dF is non empty set
[:(g . dF), the carrier of L:] is non empty Relation-like set
bool [:(g . dF), the carrier of L:] is non empty set
F . dF is set
(S, the carrier of L,g,S9,dF) . (F . dF) is set
d is non empty Relation-like S -defined the carrier of L -valued Function-like total quasi_total Element of bool [:S, the carrier of L:]
d . dF is Element of the carrier of L
gdF is Element of the carrier of L
//\ ((S, the carrier of L,g,S9,(S, the carrier of L,g,S9),F),L) is Element of the carrier of L
rng (L,(S, the carrier of L,g,S9)) is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
"\/" ((rng (L,(S, the carrier of L,g,S9))),L) is Element of the carrier of L

the carrier of L is non empty set
the_universe_of the carrier of L is non empty V13() subset-closed Tarski universal set
bool the carrier of L is non empty set
g is Element of the carrier of L
{ b1 where b1 is non empty directed Element of bool the carrier of L : g <= "\/" (b1,L) } is set
the_transitive-closure_of the carrier of L is V13() set

K is set
F is non empty directed Element of bool the carrier of L
"\/" (F,L) is Element of the carrier of L

waybelow g is non empty directed lower Element of bool the carrier of L
"\/" ((),L) is Element of the carrier of L
{g} is non empty trivial finite V54(1) countable Element of bool the carrier of L
"\/" ({g},L) is Element of the carrier of L
K is non empty set

[:K,K:] is non empty Relation-like set
bool [:K,K:] is non empty set

dF is Element of K
d . dF is set
gdF is Element of K
y is non empty directed Element of bool the carrier of L
"\/" (y,L) is Element of the carrier of L
gdF is set
d . gdF is set
y is Element of K

proj1 y is set

proj1 y is set

dom x is non empty Element of bool K
bool K is non empty set
j is set
x . j is set
gdF . j is set
id (gdF . j) is Relation-like gdF . j -defined gdF . j -valued Function-like one-to-one total quasi_total Element of bool [:(gdF . j),(gdF . j):]
[:(gdF . j),(gdF . j):] is Relation-like set
bool [:(gdF . j),(gdF . j):] is non empty set

K --> the carrier of L is non empty Relation-like non-empty non empty-yielding K -defined { the carrier of L} -valued Function-like constant total quasi_total Element of bool [:K,{ the carrier of L}:]
{ the carrier of L} is non empty trivial finite V54(1) countable set
[:K,{ the carrier of L}:] is non empty Relation-like set
bool [:K,{ the carrier of L}:] is non empty set
X is set

gdF . X is set
(K --> the carrier of L) . X is set
[:(gdF . X),((K --> the carrier of L) . X):] is Relation-like set
bool [:(gdF . X),((K --> the carrier of L) . X):] is non empty set
f9 is Element of K
gdF . f9 is non empty set

id (gdF . f9) is non empty Relation-like gdF . f9 -defined gdF . f9 -valued Function-like one-to-one total quasi_total Element of bool [:(gdF . f9),(gdF . f9):]
[:(gdF . f9),(gdF . f9):] is non empty Relation-like set
bool [:(gdF . f9),(gdF . f9):] is non empty set
proj2 (j . f9) is set
(K --> the carrier of L) . f9 is non empty Element of { the carrier of L}
proj1 (j . f9) is set

f9 is Element of K
gdF . f9 is non empty set
(K, the carrier of L,gdF,X,f9) is non empty Relation-like gdF . f9 -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(gdF . f9), the carrier of L:]
[:(gdF . f9), the carrier of L:] is non empty Relation-like set
bool [:(gdF . f9), the carrier of L:] is non empty set
z is Element of gdF . f9
(K, the carrier of L,gdF,X,f9) . z is Element of the carrier of L
id (gdF . f9) is non empty Relation-like gdF . f9 -defined gdF . f9 -valued Function-like one-to-one total quasi_total Element of bool [:(gdF . f9),(gdF . f9):]
[:(gdF . f9),(gdF . f9):] is non empty Relation-like set
bool [:(gdF . f9),(gdF . f9):] is non empty set
f9 is Element of K
(K, the carrier of L,gdF,X,f9) is non empty Relation-like gdF . f9 -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(gdF . f9), the carrier of L:]
gdF . f9 is non empty set
[:(gdF . f9), the carrier of L:] is non empty Relation-like set
bool [:(gdF . f9), the carrier of L:] is non empty set
rng (K, the carrier of L,gdF,X,f9) is non empty Element of bool the carrier of L
z is set
dom (K, the carrier of L,gdF,X,f9) is non empty Element of bool (gdF . f9)
bool (gdF . f9) is non empty set
j is set
(K, the carrier of L,gdF,X,f9) . j is set
z is set
(K, the carrier of L,gdF,X,f9) . z is set
f9 is Element of K
(K, the carrier of L,gdF,X,f9) is non empty Relation-like gdF . f9 -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(gdF . f9), the carrier of L:]
gdF . f9 is non empty set
[:(gdF . f9), the carrier of L:] is non empty Relation-like set
bool [:(gdF . f9), the carrier of L:] is non empty set
rng (K, the carrier of L,gdF,X,f9) is non empty Element of bool the carrier of L

(K, the carrier of L,gdF,X) is non empty Relation-like non-empty non empty-yielding product (doms X) -defined Function-like total Function-yielding V129() ManySortedFunction of (product (doms X)) --> K,(product (doms X)) --> the carrier of L

{K} is non empty trivial finite V54(1) countable set
[:(product (doms X)),{K}:] is non empty Relation-like set
bool [:(product (doms X)),{K}:] is non empty set
(product (doms X)) --> the carrier of L is non empty Relation-like non-empty non empty-yielding product (doms X) -defined { the carrier of L} -valued Function-like constant total quasi_total Element of bool [:(product (doms X)),{ the carrier of L}:]
[:(product (doms X)),{ the carrier of L}:] is non empty Relation-like set
bool [:(product (doms X)),{ the carrier of L}:] is non empty set
dom (K, the carrier of L,gdF,X) is non empty functional with_common_domain Element of bool (product (doms X))
bool (product (doms X)) is non empty set

(K, the carrier of L,gdF,X) . f9 is Relation-like Function-like set
//\ (((K, the carrier of L,gdF,X) . f9),L) is Element of the carrier of L
j is Element of K
f9 . j is set
gdF . j is non empty set
dom X is non empty Element of bool K
(K, the carrier of L,gdF,X,j) is non empty Relation-like gdF . j -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(gdF . j), the carrier of L:]
[:(gdF . j), the carrier of L:] is non empty Relation-like set
bool [:(gdF . j), the carrier of L:] is non empty set
dom (K, the carrier of L,gdF,X,j) is non empty Element of bool (gdF . j)
bool (gdF . j) is non empty set
proj1 f9 is set
dom X is non empty Element of bool K
j is set
proj2 f9 is set
c18 is set
f9 . c18 is set
j is Element of K
gdF . j is non empty set
[:K, the carrier of L:] is non empty Relation-like set
bool [:K, the carrier of L:] is non empty set
c18 is non empty directed Element of bool the carrier of L
"\/" (c18,L) is Element of the carrier of L
j is non empty Relation-like K -defined the carrier of L -valued Function-like total quasi_total Element of bool [:K, the carrier of L:]
//\ (j,L) is Element of the carrier of L
j is Element of K
j . j is Element of the carrier of L
gdF . j is non empty set
hj is set
dom j is non empty Element of bool K
x is Element of K
j . x is Element of the carrier of L
gdF . x is non empty set
(K, the carrier of L,gdF,X) . j is Relation-like Function-like set
((K, the carrier of L,gdF,X) . j) . hj is set
(K, the carrier of L,gdF,X,x) is non empty Relation-like gdF . x -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(gdF . x), the carrier of L:]
[:(gdF . x), the carrier of L:] is non empty Relation-like set
bool [:(gdF . x), the carrier of L:] is non empty set
(K, the carrier of L,gdF,X,x) . (j . x) is set
j . hj is set
proj1 ((K, the carrier of L,gdF,X) . j) is set
(L,(K, the carrier of L,gdF,X)) is non empty Relation-like proj1 (K, the carrier of L,gdF,X) -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(proj1 (K, the carrier of L,gdF,X)), the carrier of L:]
proj1 (K, the carrier of L,gdF,X) is non empty set
[:(proj1 (K, the carrier of L,gdF,X)), the carrier of L:] is non empty Relation-like set
bool [:(proj1 (K, the carrier of L,gdF,X)), the carrier of L:] is non empty set
\\/ ((L,(K, the carrier of L,gdF,X)),L) is Element of the carrier of L
(L,X) is non empty Relation-like proj1 X -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(), the carrier of L:]
proj1 X is non empty set
[:(), the carrier of L:] is non empty Relation-like set
bool [:(), the carrier of L:] is non empty set
rng (L,X) is non empty Element of bool the carrier of L
f9 is Element of the carrier of L
z is Element of K
(K, the carrier of L,gdF,X,z) is non empty Relation-like gdF . z -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(gdF . z), the carrier of L:]
gdF . z is non empty set
[:(gdF . z), the carrier of L:] is non empty Relation-like set
bool [:(gdF . z), the carrier of L:] is non empty set
\\/ ((K, the carrier of L,gdF,X,z),L) is Element of the carrier of L
j is non empty directed Element of bool the carrier of L
"\/" (j,L) is Element of the carrier of L
rng (K, the carrier of L,gdF,X,z) is non empty Element of bool the carrier of L
"\/" ((rng (K, the carrier of L,gdF,X,z)),L) is Element of the carrier of L
"/\" ((rng (L,X)),L) is Element of the carrier of L
//\ ((L,X),L) is Element of the carrier of L
dF is Element of K
(K, the carrier of L,gdF,X,dF) is non empty Relation-like gdF . dF -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(gdF . dF), the carrier of L:]
gdF . dF is non empty set
[:(gdF . dF), the carrier of L:] is non empty Relation-like set
bool [:(gdF . dF), the carrier of L:] is non empty set
\\/ ((K, the carrier of L,gdF,X,dF),L) is Element of the carrier of L
rng (K, the carrier of L,gdF,X,dF) is non empty Element of bool the carrier of L
"\/" ((rng (K, the carrier of L,gdF,X,dF)),L) is Element of the carrier of L

the carrier of L is non empty set
the_universe_of the carrier of L is non empty V13() subset-closed Tarski universal set
S is non empty set

S --> the carrier of L is non empty Relation-like non-empty non empty-yielding S -defined { the carrier of L} -valued Function-like constant total quasi_total Element of bool [:S,{ the carrier of L}:]
{ the carrier of L} is non empty trivial finite V54(1) countable set
[:S,{ the carrier of L}:] is non empty Relation-like set
bool [:S,{ the carrier of L}:] is non empty set

(L,S9) is non empty Relation-like proj1 S9 -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(proj1 S9), the carrier of L