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
{} is empty Relation-like non-empty empty-yielding V13() V14() V15() V17() V18() V19() Function-like one-to-one constant functional finite finite-yielding V42() V52() V54( {} ) Cardinal-yielding countable Function-yielding V129() set
{{}} is non empty trivial functional finite V42() V54(1) with_common_domain countable set
1 is non empty V13() V14() V15() V19() finite V52() countable Element of K286()
K309({{}}) is M19({{}})
[:K309({{}}),{{}}:] is Relation-like set
bool [:K309({{}}),{{}}:] 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
L is non empty total reflexive transitive antisymmetric with_infima up-complete satisfying_axiom_of_approximation continuous RelStr
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
"\/" ((waybelow S),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
L is non empty total reflexive transitive antisymmetric with_infima up-complete RelStr
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
"\/" ((waybelow S),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
L is non empty total reflexive transitive antisymmetric with_infima up-complete RelStr
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
"\/" ((waybelow g),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
K is non empty total reflexive transitive antisymmetric with_infima up-complete RelStr
the carrier of K is non empty set
bool the carrier of K is non empty set
L is non empty total reflexive transitive antisymmetric with_infima up-complete RelStr
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
L is non empty total reflexive transitive antisymmetric with_infima up-complete RelStr
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
"\/" ((waybelow S),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
L is non empty total reflexive transitive antisymmetric with_infima up-complete RelStr
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 total reflexive transitive antisymmetric with_infima up-complete RelStr
the carrier of g is non empty set
bool the carrier of g is non empty set
L is non empty total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V211() up-complete /\-complete satisfying_axiom_of_approximation continuous RelStr
Ids L is non empty set
InclPoset (Ids L) is non empty strict total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V211() up-complete /\-complete RelStr
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
(SupMap L) " (uparrow J) is Element of bool the carrier of (InclPoset (Ids L))
bool the carrier of (InclPoset (Ids L)) is non empty set
"/\" (((SupMap L) " (uparrow J)),(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
(SupMap L) " (uparrow {J}) is Element of bool the carrier of (InclPoset (Ids L))
"/\" (((SupMap L) " (uparrow {J})),(InclPoset (Ids L))) is Element of the carrier of (InclPoset (Ids L))
dom (SupMap L) 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))
(SupMap L) . dF is Element of the carrier of L
(SupMap L) . d is set
gdF is Element of the carrier of (InclPoset (Ids L))
(SupMap 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
(SupMap L) . ("/\" (((SupMap L) " (uparrow J)),(InclPoset (Ids L)))) is Element of the carrier of L
[(SupMap L),S9] is V31() Connection of InclPoset (Ids L),L
{(SupMap L),S9} is non empty functional finite countable set
{(SupMap L)} is non empty trivial functional finite V54(1) with_common_domain countable set
{{(SupMap L),S9},{(SupMap L)}} is non empty finite V42() countable set
L is non empty total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V211() up-complete /\-complete RelStr
Ids L is non empty set
InclPoset (Ids L) is non empty strict total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V211() up-complete /\-complete RelStr
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
(SupMap L) " (uparrow S9) is Element of bool the carrier of (InclPoset (Ids L))
bool the carrier of (InclPoset (Ids L)) is non empty set
"/\" (((SupMap L) " (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))
(SupMap L) . d is Element of the carrier of L
dom (SupMap L) 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)):]
[(SupMap L),F] is V31() Connection of InclPoset (Ids L),L
{(SupMap L),F} is non empty functional finite countable set
{(SupMap L)} is non empty trivial functional finite V54(1) with_common_domain countable set
{{(SupMap L),F},{(SupMap L)}} is non empty finite V42() countable set
F . S9 is Element of the carrier of (InclPoset (Ids L))
(SupMap L) . K is set
(SupMap L) . ("/\" (((SupMap L) " (uparrow S9)),(InclPoset (Ids L)))) is Element of the carrier of L
"\/" (K,L) is Element of the carrier of L
L is non empty total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V211() up-complete /\-complete RelStr
Ids L is non empty set
InclPoset (Ids L) is non empty strict total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V211() up-complete /\-complete RelStr
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)):]
[(SupMap L),g] is V31() Connection of InclPoset (Ids L),L
{(SupMap L),g} is non empty functional finite countable set
{(SupMap L)} is non empty trivial functional finite V54(1) with_common_domain countable set
{{(SupMap L),g},{(SupMap L)}} is non empty finite V42() countable set
L is set
L is set
L is set
S is set
L --> S is Relation-like L -defined {S} -valued Function-like constant total quasi_total Element of bool [:L,{S}:]
{S} is non empty trivial finite V54(1) countable set
[:L,{S}:] is Relation-like set
bool [:L,{S}:] is non empty set
g is Relation-like L -defined Function-like total set
S9 is Relation-like L -defined Function-like total Function-yielding V129() ManySortedFunction of g,L --> S
J is set
S9 . J is Relation-like Function-like 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
g is non empty Relation-like L -defined Function-like total set
S is non empty set
L --> S is non empty Relation-like non-empty non empty-yielding L -defined {S} -valued Function-like constant total quasi_total Element of bool [:L,{S}:]
{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
S9 is non empty Relation-like L -defined Function-like total Function-yielding V129() ManySortedFunction of g,L --> S
J is Element of L
S9 . J is Relation-like Function-like set
g . J is set
[:(g . J),S:] is Relation-like set
bool [:(g . J),S:] is non empty set
L is non empty set
g is non empty Relation-like non-empty non empty-yielding L -defined Function-like total set
S is non empty set
L --> S is non empty Relation-like non-empty non empty-yielding L -defined {S} -valued Function-like constant total quasi_total Element of bool [:L,{S}:]
{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
S9 is non empty Relation-like L -defined Function-like total Function-yielding V129() ManySortedFunction of g,L --> S
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
g is Relation-like non-empty L -defined Function-like total set
S is non empty set
L --> S is Relation-like non-empty L -defined {S} -valued Function-like constant total quasi_total Element of bool [:L,{S}:]
{S} is non empty trivial finite V54(1) countable set
[:L,{S}:] is Relation-like set
bool [:L,{S}:] is non empty set
S9 is Relation-like L -defined Function-like total Function-yielding V129() ManySortedFunction of g,L --> S
dom S9 is Element of bool L
bool L is non empty set
J is set
S9 . J is Relation-like Function-like 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
L is Relation-like Function-like Function-yielding V129() set
doms L is Relation-like Function-like set
product (doms L) is functional with_common_domain product-like set
Frege L is Relation-like product (doms L) -defined Function-like total Function-yielding V129() set
dom (Frege L) is functional with_common_domain Element of bool (product (doms L))
bool (product (doms L)) is non empty set
L is Relation-like Function-like Function-yielding V129() set
doms L is Relation-like Function-like set
product (doms L) is functional with_common_domain product-like set
Frege L is Relation-like product (doms L) -defined Function-like total Function-yielding V129() set
dom (Frege L) is functional with_common_domain Element of bool (product (doms L))
bool (product (doms L)) is non empty set
proj1 L is set
S is Relation-like Function-like set
proj1 S is set
(Frege L) . S is Relation-like Function-like set
proj1 ((Frege L) . S) is set
proj1 (doms L) is set
g is Relation-like Function-like set
proj1 g is set
L .. S is Relation-like Function-like set
proj1 (L .. S) is set
L is Relation-like Function-like Function-yielding V129() set
doms L is Relation-like Function-like set
product (doms L) is functional with_common_domain product-like set
Frege L is Relation-like product (doms L) -defined Function-like total Function-yielding V129() set
dom (Frege L) is functional with_common_domain Element of bool (product (doms L))
bool (product (doms L)) is non empty set
proj1 L is set
S is Relation-like Function-like set
(Frege L) . S is Relation-like Function-like set
proj2 ((Frege L) . S) is set
S9 is set
S . S9 is set
L . S9 is Relation-like Function-like set
proj1 (L . S9) is set
((Frege L) . S) . S9 is set
(L . S9) . (S . S9) is set
proj1 (doms L) is set
(doms L) . S9 is set
L .. S is Relation-like Function-like set
proj1 ((Frege L) . S) is set
L is set
S is set
L --> S is Relation-like L -defined {S} -valued Function-like constant total quasi_total Element of bool [:L,{S}:]
{S} is non empty trivial finite V54(1) countable set
[:L,{S}:] is Relation-like set
bool [:L,{S}:] is non empty set
[:L,S:] is Relation-like set
bool [:L,S:] is non empty set
g is Relation-like L -defined Function-like total set
S9 is Relation-like L -defined Function-like total Function-yielding V129() ManySortedFunction of g,L --> S
doms S9 is Relation-like Function-like set
product (doms S9) is functional with_common_domain product-like set
Frege S9 is Relation-like product (doms S9) -defined Function-like total Function-yielding V129() set
dom (Frege S9) is functional with_common_domain Element of bool (product (doms S9))
bool (product (doms S9)) is non empty set
J is Relation-like Function-like set
(Frege S9) . J is Relation-like Function-like 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
S9 . d is Relation-like Function-like 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
L --> S is Relation-like L -defined {S} -valued Function-like constant total quasi_total Element of bool [:L,{S}:]
{S} is non empty trivial finite V54(1) countable set
[:L,{S}:] is Relation-like set
bool [:L,{S}:] is non empty set
g is Relation-like L -defined Function-like total set
S9 is Relation-like L -defined Function-like total Function-yielding V129() ManySortedFunction of g,L --> S
doms S9 is Relation-like Function-like set
product (doms S9) is functional with_common_domain product-like set
Frege S9 is Relation-like product (doms S9) -defined Function-like total Function-yielding V129() set
dom (Frege S9) is functional with_common_domain Element of bool (product (doms S9))
bool (product (doms S9)) is non empty set
J is Relation-like Function-like set
(Frege S9) . J is Relation-like Function-like set
proj2 ((Frege S9) . J) is set
K is set
((Frege S9) . J) . K is set
S9 . K is Relation-like Function-like 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
S is Relation-like L -defined Function-like total set
g is non empty set
L --> g is Relation-like non-empty L -defined {g} -valued Function-like constant total quasi_total Element of bool [:L,{g}:]
{g} is non empty trivial finite V54(1) countable set
[:L,{g}:] is Relation-like set
bool [:L,{g}:] is non empty set
S9 is Relation-like L -defined Function-like total Function-yielding V129() ManySortedFunction of S,L --> g
doms S9 is Relation-like Function-like set
product (doms S9) is functional with_common_domain product-like set
Frege S9 is Relation-like product (doms S9) -defined Function-like total Function-yielding V129() set
dom (Frege S9) is functional with_common_domain Element of bool (product (doms S9))
bool (product (doms S9)) is non empty set
J is Relation-like Function-like set
K is set
J . K is set
S . K is set
S9 . K is Relation-like Function-like 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
L is Relation-like non-empty Function-like set
doms L is Relation-like Function-like set
proj1 (doms L) is set
S is set
(doms L) . S is set
proj2 L is V22() set
SubFuncs (proj2 L) is set
L " (SubFuncs (proj2 L)) is set
L . S is set
proj1 L is set
g is Relation-like Function-like set
proj1 g is set
L is set
g is Relation-like L -defined Function-like total set
S is set
L --> S is Relation-like L -defined {S} -valued Function-like constant total quasi_total Element of bool [:L,{S}:]
{S} is non empty trivial finite V54(1) countable set
[:L,{S}:] is Relation-like set
bool [:L,{S}:] is non empty set
S9 is Relation-like L -defined Function-like total Function-yielding V129() ManySortedFunction of g,L --> S
Frege S9 is Relation-like Function-like set
doms S9 is Relation-like Function-like set
product (doms S9) is functional with_common_domain product-like set
(product (doms S9)) --> L is Relation-like 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 Relation-like set
bool [:(product (doms S9)),{L}:] is non empty set
(product (doms S9)) --> S is Relation-like product (doms S9) -defined {S} -valued Function-like constant total quasi_total Element of bool [:(product (doms S9)),{S}:]
[:(product (doms S9)),{S}:] is Relation-like set
bool [:(product (doms S9)),{S}:] is non empty set
Frege S9 is Relation-like product (doms S9) -defined Function-like total Function-yielding V129() 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
gdF is Relation-like Function-like set
(Frege S9) . gdF is Relation-like Function-like set
L is non empty set
g is non empty Relation-like non-empty non empty-yielding L -defined Function-like total set
S is non empty set
L --> S is non empty Relation-like non-empty non empty-yielding L -defined {S} -valued Function-like constant total quasi_total Element of bool [:L,{S}:]
{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
S9 is non empty Relation-like non-empty non empty-yielding L -defined Function-like total Function-yielding V129() ManySortedFunction of g,L --> S
doms S9 is Relation-like non-empty Function-like set
product (doms S9) is non empty functional with_common_domain product-like 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
K is Relation-like Function-like doms S9 -compatible Element of product (doms S9)
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
S is Relation-like Function-like Function-yielding V129() set
proj1 S is set
L is non empty RelStr
the carrier of L is non empty set
[:(proj1 S), the carrier of L:] is Relation-like set
bool [:(proj1 S), the carrier of L:] is non empty set
g is Relation-like Function-like set
proj1 g is set
g is Relation-like Function-like set
proj1 g is set
proj2 g is set
S9 is set
J is set
g . J is set
S . J is Relation-like Function-like 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 [:(proj1 S), the carrier of L:]
J is set
S9 . J is set
S . J is Relation-like Function-like 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 [:(proj1 S), the carrier of L:]
S9 is Relation-like proj1 S -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(proj1 S), the carrier of L:]
J is set
g . J is set
S . J is Relation-like Function-like set
\\/ ((S . J),L) is Element of the carrier of L
S9 . J is set
dom g is Element of bool (proj1 S)
bool (proj1 S) is non empty set
dom S9 is Element of bool (proj1 S)
g is Relation-like Function-like set
proj1 g is set
g is Relation-like Function-like set
proj1 g is set
proj2 g is set
S9 is set
J is set
g . J is set
S . J is Relation-like Function-like 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 [:(proj1 S), the carrier of L:]
J is set
S9 . J is set
S . J is Relation-like Function-like 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 [:(proj1 S), the carrier of L:]
S9 is Relation-like proj1 S -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(proj1 S), the carrier of L:]
J is set
g . J is set
S . J is Relation-like Function-like set
//\ ((S . J),L) is Element of the carrier of L
S9 . J is set
dom g is Element of bool (proj1 S)
bool (proj1 S) is non empty set
dom S9 is Element of bool (proj1 S)
L is set
S is Relation-like L -defined Function-like total 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
L --> S is Relation-like L -defined {S} -valued Function-like constant total quasi_total Element of bool [:L,{S}:]
{S} is non empty trivial finite V54(1) countable set
[:L,{S}:] is Relation-like 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
S is Relation-like Function-like Function-yielding V129() set
proj1 S is set
g is Relation-like Function-like Function-yielding V129() 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 [:(proj1 S), the carrier of L:]
[:(proj1 S), the carrier of L:] is Relation-like set
bool [:(proj1 S), 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 [:(proj1 g), the carrier of L:]
[:(proj1 g), the carrier of L:] is Relation-like set
bool [:(proj1 g), the carrier of L:] is non empty set
S9 is set
(L,S) . S9 is set
(L,g) . S9 is set
S . S9 is Relation-like Function-like set
\\/ ((S . S9),L) is Element of the carrier of L
g . S9 is Relation-like Function-like set
\\/ ((g . S9),L) is Element of the carrier of L
dom (L,S) is Element of bool (proj1 S)
bool (proj1 S) is non empty set
dom (L,g) is Element of bool (proj1 g)
bool (proj1 g) is non empty set
L is non empty RelStr
the carrier of L is non empty set
S is Relation-like Function-like Function-yielding V129() set
proj1 S is set
g is Relation-like Function-like Function-yielding V129() 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 [:(proj1 S), the carrier of L:]
[:(proj1 S), the carrier of L:] is Relation-like set
bool [:(proj1 S), 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 [:(proj1 g), the carrier of L:]
[:(proj1 g), the carrier of L:] is Relation-like set
bool [:(proj1 g), the carrier of L:] is non empty set
S9 is set
(L,S) . S9 is set
(L,g) . S9 is set
S . S9 is Relation-like Function-like set
//\ ((S . S9),L) is Element of the carrier of L
g . S9 is Relation-like Function-like set
//\ ((g . S9),L) is Element of the carrier of L
dom (L,S) is Element of bool (proj1 S)
bool (proj1 S) is non empty set
dom (L,g) is Element of bool (proj1 g)
bool (proj1 g) is non empty set
L is set
S is non empty RelStr
the carrier of S is non empty set
g is Relation-like Function-like Function-yielding V129() set
(S,g) is Relation-like proj1 g -defined the carrier of S -valued Function-like total quasi_total Element of bool [:(proj1 g), the carrier of S:]
proj1 g is set
[:(proj1 g), the carrier of S:] is Relation-like set
bool [:(proj1 g), 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 [:(proj1 g), the carrier of S:]
rng (S,g) is Element of bool the carrier of S
dom (S,g) is Element of bool (proj1 g)
bool (proj1 g) is non empty set
S9 is set
(S,g) . S9 is set
J is set
g . J is Relation-like Function-like set
\\/ ((g . J),S) is Element of the carrier of S
S9 is set
g . S9 is Relation-like Function-like set
\\/ ((g . S9),S) is Element of the carrier of S
(S,g) . S9 is set
dom (S,g) is Element of bool (proj1 g)
bool (proj1 g) is non empty set
S9 is set
(S,g) . S9 is set
J is set
g . J is Relation-like Function-like set
//\ ((g . J),S) is Element of the carrier of S
S9 is set
g . S9 is Relation-like Function-like 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
S9 is non empty Relation-like g -defined Function-like total 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 [:(proj1 J), the carrier of S:]
proj1 J is non empty set
[:(proj1 J), the carrier of S:] is non empty Relation-like set
bool [:(proj1 J), 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 [:(proj1 J), 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 is Relation-like Function-like 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 is Relation-like Function-like 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
S is non empty Relation-like L -defined Function-like total 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
L is non empty total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V211() up-complete /\-complete RelStr
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
g is non empty Relation-like non-empty non empty-yielding S -defined Function-like total set
S9 is non empty Relation-like non-empty non empty-yielding S -defined Function-like total Function-yielding V129() ManySortedFunction of g,S --> the carrier of L
doms S9 is Relation-like non-empty Function-like set
product (doms S9) is non empty functional with_common_domain product-like 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
L is non empty total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V211() up-complete /\-complete RelStr
the carrier of L is non empty set
S is Element of the carrier of L
g is Relation-like Function-like Function-yielding V129() set
doms g is Relation-like Function-like set
product (doms g) is functional with_common_domain product-like set
Frege g is Relation-like product (doms g) -defined Function-like total Function-yielding V129() set
dom (Frege g) is functional with_common_domain Element of bool (product (doms g))
bool (product (doms g)) is non empty set
(L,(Frege g)) is Relation-like proj1 (Frege g) -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(proj1 (Frege g)), the carrier of L:]
proj1 (Frege g) is set
[:(proj1 (Frege g)), the carrier of L:] is Relation-like set
bool [:(proj1 (Frege g)), the carrier of L:] is non empty set
\\/ ((L,(Frege g)),L) is Element of the carrier of L
rng (L,(Frege g)) 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
(Frege g) . J is Relation-like Function-like set
//\ (((Frege g) . J),L) is Element of the carrier of L
K is Relation-like Function-like set
"\/" ((rng (L,(Frege g))),L) is Element of the carrier of L
L is non empty total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V211() up-complete /\-complete RelStr
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
g is non empty Relation-like non-empty non empty-yielding S -defined Function-like total set
S9 is non empty Relation-like non-empty non empty-yielding S -defined Function-like total Function-yielding V129() ManySortedFunction of g,S --> 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
doms S9 is Relation-like non-empty Function-like set
product (doms S9) is non empty functional with_common_domain product-like 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}:]
{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
F is Relation-like Function-like doms S9 -compatible Element of product (doms S9)
(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
d is Relation-like Function-like 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
L is non empty total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V211() up-complete /\-complete RelStr
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
"\/" ((waybelow S),L) is Element of the carrier of L
L is non empty total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V211() up-complete /\-complete RelStr
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
g is non empty Relation-like non-empty non empty-yielding S -defined Function-like total set
S9 is non empty Relation-like non-empty non empty-yielding S -defined Function-like total Function-yielding V129() ManySortedFunction of g,S --> 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
(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
doms S9 is Relation-like non-empty Function-like set
product (doms S9) is non empty functional with_common_domain product-like 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}:]
{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 (proj2 g) is set
K is set
g . K is set
S9 . K is Relation-like Function-like 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
K is Relation-like Function-like 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
K is Relation-like Function-like set
K is Relation-like Function-like set
[:S, the carrier of L:] is non empty Relation-like set
bool [:S, the carrier of L:] is non empty set
F is Relation-like Function-like doms S9 -compatible Element of product (doms S9)
(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
L is non empty total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V211() up-complete /\-complete RelStr
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
Tarski-Class (the_transitive-closure_of the carrier of L) is V13() subset-closed Tarski universal 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
J is V13() subset-closed Tarski universal set
waybelow g is non empty directed lower Element of bool the carrier of L
"\/" ((waybelow g),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
id K is non empty Relation-like K -defined K -valued Function-like one-to-one total quasi_total Element of bool [:K,K:]
[:K,K:] is non empty Relation-like set
bool [:K,K:] is non empty set
d is non empty Relation-like K -defined Function-like total 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
gdF is non empty Relation-like non-empty non empty-yielding K -defined Function-like total set
y is Relation-like Function-like set
proj1 y is set
y is Relation-like Function-like set
proj1 y is set
x is non empty Relation-like K -defined Function-like total 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
j is non empty Relation-like K -defined Function-like total Function-yielding V129() 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
j . X is Relation-like Function-like 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
j . f9 is Relation-like Function-like 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
X is non empty Relation-like non-empty non empty-yielding K -defined Function-like total Function-yielding V129() ManySortedFunction of gdF,K --> the carrier of L
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
doms X is Relation-like non-empty Function-like set
product (doms X) is non empty functional with_common_domain product-like set
(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
(product (doms X)) --> K is non empty Relation-like non-empty non empty-yielding product (doms X) -defined {K} -valued Function-like constant total quasi_total Element of bool [:(product (doms X)),{K}:]
{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
f9 is Relation-like Function-like 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 [:(proj1 X), the carrier of L:]
proj1 X is non empty set
[:(proj1 X), the carrier of L:] is non empty Relation-like set
bool [:(proj1 X), 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
L is non empty total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V211() up-complete /\-complete RelStr
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
g is non empty Relation-like non-empty non empty-yielding S -defined Function-like total 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
S9 is non empty Relation-like non-empty non empty-yielding S -defined Function-like total Function-yielding V129() ManySortedFunction of g,S --> 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