:: 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
{} 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
{ b₁ where b₁ is Element of the carrier of L : b₁ 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
{ b₁ where b₁ is non empty directed Element of bool the carrier of L : g <= "\/" (b₁,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
c₁₈ is set
f9 . c₁₈ 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
c₁₈ is non empty directed Element of bool the carrier of L
"\/" (c₁₈,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:]
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
S is non empty set
g is non empty Relation-like non-empty non empty-yielding S -defined Function-like total 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 --> 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:]
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 non empty total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V211() up-complete /\-complete RelStr
the carrier of J is non empty set
L is non empty set
S is non empty set
[:L,S:] is non empty Relation-like set
g is non empty set
[:[:L,S:],g:] is non empty Relation-like set
bool [:[:L,S:],g:] is non empty set
S9 is non empty Relation-like [:L,S:] -defined g -valued Function-like total quasi_total Element of bool [:[:L,S:],g:]
curry S9 is non empty Relation-like L -defined Function-like total 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
L --> g is non empty Relation-like non-empty non empty-yielding 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 non empty Relation-like set
bool [:L,{g}:] is non empty set
dom S9 is non empty Relation-like L -defined S -valued Element of bool [:L,S:]
bool [:L,S:] is non empty set
J is non empty Relation-like [:L,S:] -defined Function-like total set
curry J is non empty Relation-like L -defined Function-like total set
K is set
(curry J) . K is set
(L --> S) . K is set
(L --> g) . K is set
[:((L --> S) . K),((L --> g) . K):] is Relation-like set
bool [:((L --> S) . K),((L --> g) . K):] is non empty set
proj2 J is non empty set
F is Relation-like Function-like set
proj1 F is set
proj2 F is set
curry S9 is non empty Relation-like L -defined Funcs (S,g) -valued Function-like total quasi_total Function-yielding V129() Element of bool [:L,(Funcs (S,g)):]
Funcs (S,g) is non empty functional FUNCTION_DOMAIN of S,g
[:L,(Funcs (S,g)):] is non empty Relation-like set
bool [:L,(Funcs (S,g)):] is non empty set
dom (curry S9) is non empty Element of bool L
bool L is non empty set
rng S9 is non empty Element of bool g
bool g is non empty set
[:S,g:] is non empty Relation-like set
bool [:S,g:] is non empty set
d is Relation-like Function-like set
dF is non empty Relation-like S -defined g -valued Function-like total quasi_total Element of bool [:S,g:]
L is non empty set
S is non empty set
[:L,S:] is non empty Relation-like 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
g is non empty set
[:[:L,S:],g:] is non empty Relation-like set
bool [:[:L,S:],g:] is non empty set
S9 is Element of L
(L --> S) . S9 is non empty set
J is Element of S
K is non empty Relation-like [:L,S:] -defined g -valued Function-like total quasi_total Element of bool [:[:L,S:],g:]
(L,S,g,K) is non empty Relation-like non-empty non empty-yielding L -defined Function-like total Function-yielding V129() ManySortedFunction of L --> S,L --> g
L --> g is non empty Relation-like non-empty non empty-yielding 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 non empty Relation-like set
bool [:L,{g}:] is non empty set
dom (L,S,g,K) is non empty Element of bool L
bool L is non empty set
(L,g,(L --> S),(L,S,g,K),S9) is non empty Relation-like (L --> S) . S9 -defined g -valued Function-like total quasi_total Element of bool [:((L --> S) . S9),g:]
[:((L --> S) . S9),g:] is non empty Relation-like set
bool [:((L --> S) . S9),g:] is non empty set
dom (L,g,(L --> S),(L,S,g,K),S9) is non empty Element of bool ((L --> S) . S9)
bool ((L --> S) . S9) is non empty set
K . (S9,J) is Element of g
[S9,J] is V31() set
{S9,J} is non empty finite countable set
{S9} is non empty trivial finite V54(1) countable set
{{S9,J},{S9}} is non empty finite V42() countable set
K . [S9,J] is set
(L,g,(L --> S),(L,S,g,K),S9) . J is set
dom K is non empty Relation-like L -defined S -valued Element of bool [:L,S:]
bool [:L,S:] is non empty set
proj1 (dom K) is non empty set
proj1 [:L,S:] is non empty set
rng K is non empty Element of bool g
bool g is non empty set
F is Relation-like Function-like set
proj1 F is set
proj2 F is set
[S9,J] is V31() Element of [:L,S:]
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
the Element of S is Element of S
g . the Element of S is non empty set
the Element of g . the Element of S is Element of g . the Element of S
Bottom L is Element of the carrier of L
proj1 (doms S9) is set
dom S9 is non empty Element of bool S
bool S is non empty set
dom g is non empty Element of bool S
proj2 g is non empty V22() set
union (proj2 g) is set
F is non empty set
d is Element of S
g . d is non empty set
S9 . d is non empty Relation-like Function-like set
dF is Element of F
(S9 . d) . dF is 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
gdF is Element of g . d
(S, the carrier of L,g,S9,d) . gdF is Element of the carrier of L
[:S,F:] is non empty Relation-like set
[:[:S,F:], the carrier of L:] is non empty Relation-like set
bool [:[:S,F:], the carrier of L:] is non empty set
d is non empty Relation-like [:S,F:] -defined the carrier of L -valued Function-like total quasi_total Element of bool [:[:S,F:], the carrier of L:]
d is non empty Relation-like [:S,F:] -defined the carrier of L -valued Function-like total quasi_total Element of bool [:[:S,F:], the carrier of L:]
dF is Element of S
g . dF is non empty set
gdF is set
S --> F is non empty Relation-like non-empty non empty-yielding S -defined {F} -valued Function-like constant total quasi_total Element of bool [:S,{F}:]
{F} is non empty trivial finite V54(1) countable set
[:S,{F}:] is non empty Relation-like set
bool [:S,{F}:] is non empty set
(S,F, the carrier of L,d) is non empty Relation-like non-empty non empty-yielding S -defined Function-like total Function-yielding V129() ManySortedFunction of S --> F,S --> the carrier of L
dF is Element of S
(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
rng (S, the carrier of L,g,S9,dF) is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
(S, the carrier of L,(S --> F),(S,F, the carrier of L,d),dF) is non empty Relation-like (S --> F) . dF -defined the carrier of L -valued Function-like total quasi_total Element of bool [:((S --> F) . dF), the carrier of L:]
(S --> F) . dF is non empty set
[:((S --> F) . dF), the carrier of L:] is non empty Relation-like set
bool [:((S --> F) . dF), the carrier of L:] is non empty set
rng (S, the carrier of L,(S --> F),(S,F, the carrier of L,d),dF) is non empty Element of bool the carrier of L
gdF is set
dom (S, the carrier of L,g,S9,dF) is non empty Element of bool (g . dF)
bool (g . dF) is non empty set
y is set
(S, the carrier of L,g,S9,dF) . y is set
x is Element of F
[dF,x] is V31() Element of [:S,F:]
{dF,x} is non empty finite countable set
{dF} is non empty trivial finite V54(1) countable set
{{dF,x},{dF}} is non empty finite V42() countable set
dom d is non empty Relation-like S -defined F -valued Element of bool [:S,F:]
bool [:S,F:] is non empty set
dom (S, the carrier of L,(S --> F),(S,F, the carrier of L,d),dF) is non empty Element of bool ((S --> F) . dF)
bool ((S --> F) . dF) is non empty set
(S --> F) . dF is non empty Element of {F}
d . (dF,x) is Element of the carrier of L
[dF,x] is V31() set
d . [dF,x] is set
(S, the carrier of L,(S --> F),(S,F, the carrier of L,d),dF) . x is set
dF is set
S9 . dF is Relation-like Function-like set
\\/ ((S9 . dF),L) is Element of the carrier of L
(S,F, the carrier of L,d) . dF is Relation-like Function-like set
\\/ (((S,F, the carrier of L,d) . dF),L) is Element of the carrier of L
gdF is Element of S
(S --> F) . gdF is non empty Element of {F}
[:((S --> F) . gdF), the carrier of L:] is non empty Relation-like set
bool [:((S --> F) . gdF), the carrier of L:] is non empty set
(S, the carrier of L,(S --> F),(S,F, the carrier of L,d),gdF) is non empty Relation-like (S --> F) . gdF -defined the carrier of L -valued Function-like total quasi_total Element of bool [:((S --> F) . gdF), the carrier of L:]
(S --> F) . gdF is non empty set
[:((S --> F) . gdF), the carrier of L:] is non empty Relation-like set
bool [:((S --> F) . gdF), the carrier of L:] is non empty set
[:F, the carrier of L:] is non empty Relation-like set
bool [:F, the carrier of L:] is non empty set
y is non empty Relation-like (S --> F) . gdF -defined the carrier of L -valued Function-like total quasi_total Element of bool [:((S --> F) . gdF), the carrier of L:]
x is non empty Relation-like F -defined the carrier of L -valued Function-like total quasi_total Element of bool [:F, the carrier of L:]
(S, the carrier of L,g,S9,gdF) is non empty Relation-like g . gdF -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(g . gdF), the carrier of L:]
g . gdF is non empty set
[:(g . gdF), the carrier of L:] is non empty Relation-like set
bool [:(g . gdF), the carrier of L:] is non empty set
\\/ ((S, the carrier of L,g,S9,gdF),L) is Element of the carrier of L
j is Element of F
x . j is Element of the carrier of L
dom (S, the carrier of L,g,S9,gdF) is non empty Element of bool (g . gdF)
bool (g . gdF) is non empty set
(S, the carrier of L,g,S9,gdF) . j is set
d . (gdF,j) is Element of the carrier of L
[gdF,j] is V31() set
{gdF,j} is non empty finite countable set
{gdF} is non empty trivial finite V54(1) countable set
{{gdF,j},{gdF}} is non empty finite V42() countable set
d . [gdF,j] is set
rng (S, the carrier of L,g,S9,gdF) 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,gdF)),L) is Element of the carrier of L
d . (gdF,j) is Element of the carrier of L
[gdF,j] is V31() set
{gdF,j} is non empty finite countable set
{gdF} is non empty trivial finite V54(1) countable set
{{gdF,j},{gdF}} is non empty finite V42() countable set
d . [gdF,j] is set
\\/ (x,L) is Element of the carrier of L
rng (S, the carrier of L,g,S9,gdF) 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,(S --> F),(S,F, the carrier of L,d),gdF) is non empty Element of bool the carrier of L
"\/" ((rng (S, the carrier of L,g,S9,gdF)),L) is Element of the carrier of L
"\/" ((rng (S, the carrier of L,(S --> F),(S,F, the carrier of L,d),gdF)),L) is Element of the carrier of L
rng x is non empty Element of bool the carrier of L
"\/" ((rng x),L) is Element of the carrier of L
doms (S,F, the carrier of L,d) is Relation-like non-empty Function-like set
proj1 (doms (S,F, the carrier of L,d)) is set
dom (S,F, the carrier of L,d) is non empty Element of bool S
product (doms (S,F, the carrier of L,d)) is non empty functional with_common_domain product-like set
dF is set
gdF is Relation-like Function-like set
proj1 gdF is set
y is set
gdF . y is set
(doms (S,F, the carrier of L,d)) . y is set
(doms S9) . y is set
x is Element of S
g . x is non empty set
(S, the carrier of L,g,S9,x) is non empty Relation-like g . x -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(g . x), the carrier of L:]
[:(g . x), the carrier of L:] is non empty Relation-like set
bool [:(g . x), the carrier of L:] is non empty set
dom (S, the carrier of L,g,S9,x) is non empty Element of bool (g . x)
bool (g . x) is non empty set
(S --> F) . x is non empty set
(S, the carrier of L,(S --> F),(S,F, the carrier of L,d),x) is non empty Relation-like (S --> F) . x -defined the carrier of L -valued Function-like total quasi_total Element of bool [:((S --> F) . x), the carrier of L:]
[:((S --> F) . x), the carrier of L:] is non empty Relation-like set
bool [:((S --> F) . x), the carrier of L:] is non empty set
dom (S, the carrier of L,(S --> F),(S,F, the carrier of L,d),x) is non empty Element of bool ((S --> F) . x)
bool ((S --> F) . x) 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
(S, the carrier of L,(S --> F),(S,F, the carrier of L,d)) is non empty Relation-like non-empty non empty-yielding product (doms (S,F, the carrier of L,d)) -defined Function-like total Function-yielding V129() ManySortedFunction of (product (doms (S,F, the carrier of L,d))) --> S,(product (doms (S,F, the carrier of L,d))) --> the carrier of L
(product (doms (S,F, the carrier of L,d))) --> S is non empty Relation-like non-empty non empty-yielding product (doms (S,F, the carrier of L,d)) -defined {S} -valued Function-like constant total quasi_total Element of bool [:(product (doms (S,F, the carrier of L,d))),{S}:]
[:(product (doms (S,F, the carrier of L,d))),{S}:] is non empty Relation-like set
bool [:(product (doms (S,F, the carrier of L,d))),{S}:] is non empty set
(product (doms (S,F, the carrier of L,d))) --> the carrier of L is non empty Relation-like non-empty non empty-yielding product (doms (S,F, the carrier of L,d)) -defined { the carrier of L} -valued Function-like constant total quasi_total Element of bool [:(product (doms (S,F, the carrier of L,d))),{ the carrier of L}:]
[:(product (doms (S,F, the carrier of L,d))),{ the carrier of L}:] is non empty Relation-like set
bool [:(product (doms (S,F, the carrier of L,d))),{ the carrier of L}:] is non empty set
dom (S, the carrier of L,(S --> F),(S,F, the carrier of L,d)) is non empty functional with_common_domain Element of bool (product (doms (S,F, the carrier of L,d)))
bool (product (doms (S,F, the carrier of L,d))) is non empty set
dF is set
(S, the carrier of L,g,S9) . dF is Relation-like Function-like set
//\ (((S, the carrier of L,g,S9) . dF),L) is Element of the carrier of L
(S, the carrier of L,(S --> F),(S,F, the carrier of L,d)) . dF is Relation-like Function-like set
//\ (((S, the carrier of L,(S --> F),(S,F, the carrier of L,d)) . dF),L) is Element of the carrier of L
gdF 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),gdF) 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
dom (S, the carrier of L,g,S9,(S, the carrier of L,g,S9),gdF) is non empty Element of bool S
(S, the carrier of L,(S --> F),(S,F, the carrier of L,d)) . gdF is Relation-like Function-like set
y is set
(S, the carrier of L,g,S9,(S, the carrier of L,g,S9),gdF) . y is set
((S, the carrier of L,(S --> F),(S,F, the carrier of L,d)) . gdF) . y is set
x is Element of S
gdF . x is set
g . x is non empty set
(S, the carrier of L,g,S9,(S, the carrier of L,g,S9),gdF) . x is Element of the carrier of L
(S, the carrier of L,g,S9,x) is non empty Relation-like g . x -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(g . x), the carrier of L:]
[:(g . x), the carrier of L:] is non empty Relation-like set
bool [:(g . x), the carrier of L:] is non empty set
j is Element of F
(S, the carrier of L,g,S9,x) . j is set
d . (x,j) is Element of the carrier of L
[x,j] is V31() set
{x,j} is non empty finite countable set
{x} is non empty trivial finite V54(1) countable set
{{x,j},{x}} is non empty finite V42() countable set
d . [x,j] is set
(S, the carrier of L,(S --> F),(S,F, the carrier of L,d),x) is non empty Relation-like (S --> F) . x -defined the carrier of L -valued Function-like total quasi_total Element of bool [:((S --> F) . x), the carrier of L:]
(S --> F) . x is non empty set
[:((S --> F) . x), the carrier of L:] is non empty Relation-like set
bool [:((S --> F) . x), the carrier of L:] is non empty set
(S, the carrier of L,(S --> F),(S,F, the carrier of L,d),x) . (gdF . x) is set
((S, the carrier of L,(S --> F),(S,F, the carrier of L,d)) . gdF) . x is set
proj1 ((S, the carrier of L,(S --> F),(S,F, the carrier of L,d)) . gdF) is set
dom d is non empty Relation-like S -defined F -valued Element of bool [:S,F:]
bool [:S,F:] is non empty set
proj1 (dom d) is non empty set
proj1 [:S,F:] is non empty set
(L,(S, the carrier of L,(S --> F),(S,F, the carrier of L,d))) is non empty Relation-like proj1 (S, the carrier of L,(S --> F),(S,F, the carrier of L,d)) -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(proj1 (S, the carrier of L,(S --> F),(S,F, the carrier of L,d))), the carrier of L:]
proj1 (S, the carrier of L,(S --> F),(S,F, the carrier of L,d)) is non empty set
[:(proj1 (S, the carrier of L,(S --> F),(S,F, the carrier of L,d))), the carrier of L:] is non empty Relation-like set
bool [:(proj1 (S, the carrier of L,(S --> F),(S,F, the carrier of L,d))), the carrier of L:] is non empty set
\\/ ((L,(S, the carrier of L,(S --> F),(S,F, the carrier of L,d))),L) is Element of the carrier of L
dF is set
(doms S9) . dF is set
(doms (S,F, the carrier of L,d)) . dF is set
gdF is Element of S
g . gdF is non empty set
(S, the carrier of L,g,S9,gdF) is non empty Relation-like g . gdF -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(g . gdF), the carrier of L:]
[:(g . gdF), the carrier of L:] is non empty Relation-like set
bool [:(g . gdF), the carrier of L:] is non empty set
dom (S, the carrier of L,g,S9,gdF) is non empty Element of bool (g . gdF)
bool (g . gdF) is non empty set
(S --> F) . gdF is non empty set
(S, the carrier of L,(S --> F),(S,F, the carrier of L,d),gdF) is non empty Relation-like (S --> F) . gdF -defined the carrier of L -valued Function-like total quasi_total Element of bool [:((S --> F) . gdF), the carrier of L:]
[:((S --> F) . gdF), the carrier of L:] is non empty Relation-like set
bool [:((S --> F) . gdF), the carrier of L:] is non empty set
dom (S, the carrier of L,(S --> F),(S,F, the carrier of L,d),gdF) is non empty Element of bool ((S --> F) . gdF)
bool ((S --> F) . gdF) is non empty set
dF is Element of S
g . dF is non empty set
dF is Element of S
g . dF is non empty set
gdF is set
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
{(Bottom L)} is non empty trivial finite V54(1) countable Element of bool the carrier of L
(rng (L,(S, the carrier of L,g,S9))) \/ {(Bottom L)} is non empty Element of bool the carrier of L
rng (L,(S, the carrier of L,(S --> F),(S,F, the carrier of L,d))) is non empty Element of bool the carrier of L
x is set
j is set
(S, the carrier of L,g,S9) . j is Relation-like Function-like set
//\ (((S, the carrier of L,g,S9) . j),L) is Element of the carrier of L
(S, the carrier of L,(S --> F),(S,F, the carrier of L,d)) . j is Relation-like Function-like set
//\ (((S, the carrier of L,(S --> F),(S,F, the carrier of L,d)) . j),L) is Element of the carrier of L
y is Element of F
S --> y is non empty Relation-like S -defined F -valued Function-like constant total quasi_total Element of bool [:S,F:]
bool [:S,F:] is non empty set
f9 is set
(S --> y) . f9 is set
(doms (S,F, the carrier of L,d)) . f9 is set
z is Element of S
(S --> y) . z is Element of F
(doms (S,F, the carrier of L,d)) . z is set
(S --> F) . z is non empty set
(S, the carrier of L,(S --> F),(S,F, the carrier of L,d),z) is non empty Relation-like (S --> F) . z -defined the carrier of L -valued Function-like total quasi_total Element of bool [:((S --> F) . z), the carrier of L:]
[:((S --> F) . z), the carrier of L:] is non empty Relation-like set
bool [:((S --> F) . z), the carrier of L:] is non empty set
dom (S, the carrier of L,(S --> F),(S,F, the carrier of L,d),z) is non empty Element of bool ((S --> F) . z)
bool ((S --> F) . z) is non empty set
dom (S --> y) is non empty Element of bool S
d . (dF,y) is Element of the carrier of L
[dF,y] is V31() set
{dF,y} is non empty finite countable set
{dF} is non empty trivial finite V54(1) countable set
{{dF,y},{dF}} is non empty finite V42() countable set
d . [dF,y] is set
(S, the carrier of L,(S --> F),(S,F, the carrier of L,d),dF) is non empty Relation-like (S --> F) . dF -defined the carrier of L -valued Function-like total quasi_total Element of bool [:((S --> F) . dF), the carrier of L:]
(S --> F) . dF is non empty set
[:((S --> F) . dF), the carrier of L:] is non empty Relation-like set
bool [:((S --> F) . dF), the carrier of L:] is non empty set
(S, the carrier of L,(S --> F),(S,F, the carrier of L,d),dF) . y is set
(S --> y) . dF is Element of F
(S, the carrier of L,(S --> F),(S,F, the carrier of L,d),dF) . ((S --> y) . dF) is set
(S, the carrier of L,(S --> F),(S,F, the carrier of L,d)) . (S --> y) is Relation-like Function-like set
proj2 ((S, the carrier of L,(S --> F),(S,F, the carrier of L,d)) . (S --> y)) is set
"/\" ((proj2 ((S, the carrier of L,(S --> F),(S,F, the carrier of L,d)) . (S --> y))),L) is Element of the carrier of L
j is Element of the carrier of L
//\ (((S, the carrier of L,(S --> F),(S,F, the carrier of L,d)) . (S --> y)),L) is Element of the carrier of L
x is set
j is set
(S, the carrier of L,(S --> F),(S,F, the carrier of L,d)) . j is Relation-like Function-like set
//\ (((S, the carrier of L,(S --> F),(S,F, the carrier of L,d)) . j),L) is Element of the carrier of L
X is Relation-like Function-like set
f9 is set
X . f9 is set
(doms S9) . f9 is set
z is Element of S
(doms S9) . z is set
g . z is non empty set
(S, the carrier of L,g,S9,z) is non empty Relation-like g . z -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(g . z), the carrier of L:]
[:(g . z), the carrier of L:] is non empty Relation-like set
bool [:(g . z), the carrier of L:] is non empty set
dom (S, the carrier of L,g,S9,z) is non empty Element of bool (g . z)
bool (g . z) is non empty set
proj1 X is set
(S, the carrier of L,g,S9) . X is Relation-like Function-like set
//\ (((S, the carrier of L,g,S9) . X),L) is Element of the carrier of L
X is Relation-like Function-like set
f9 is Element of S
X . f9 is set
g . f9 is non empty set
f9 is Element of S
X . f9 is set
g . f9 is non empty set
(S --> F) . f9 is non empty set
(S, the carrier of L,(S --> F),(S,F, the carrier of L,d),f9) is non empty Relation-like (S --> F) . f9 -defined the carrier of L -valued Function-like total quasi_total Element of bool [:((S --> F) . f9), the carrier of L:]
[:((S --> F) . f9), the carrier of L:] is non empty Relation-like set
bool [:((S --> F) . f9), the carrier of L:] is non empty set
dom (S, the carrier of L,(S --> F),(S,F, the carrier of L,d),f9) is non empty Element of bool ((S --> F) . f9)
bool ((S --> F) . f9) is non empty set
z is Element of F
d . (f9,z) is Element of the carrier of L
[f9,z] is V31() set
{f9,z} is non empty finite countable set
{f9} is non empty trivial finite V54(1) countable set
{{f9,z},{f9}} is non empty finite V42() countable set
d . [f9,z] is set
(S, the carrier of L,(S --> F),(S,F, the carrier of L,d),f9) . (X . f9) is set
(S, the carrier of L,(S --> F),(S,F, the carrier of L,d)) . X is Relation-like Function-like set
proj2 ((S, the carrier of L,(S --> F),(S,F, the carrier of L,d)) . X) is set
"/\" ((proj2 ((S, the carrier of L,(S --> F),(S,F, the carrier of L,d)) . X)),L) is Element of the carrier of L
//\ (((S, the carrier of L,(S --> F),(S,F, the carrier of L,d)) . X),L) is Element of the carrier of L
X is Relation-like Function-like set
f9 is Element of S
X . f9 is set
g . f9 is non empty set
"\/" ((rng (L,(S, the carrier of L,(S --> F),(S,F, the carrier of L,d)))),L) is Element of the carrier of L
"\/" (((rng (L,(S, the carrier of L,g,S9))) \/ {(Bottom L)}),L) is Element of the carrier of L
"\/" ((rng (L,(S, the carrier of L,g,S9))),L) is Element of the carrier of L
"\/" ({(Bottom L)},L) is Element of the carrier of L
("\/" ((rng (L,(S, the carrier of L,g,S9))),L)) "\/" ("\/" ({(Bottom L)},L)) is Element of the carrier of L
("\/" ((rng (L,(S, the carrier of L,g,S9))),L)) "\/" (Bottom L) is Element of the carrier of L
(\\/ ((L,(S, the carrier of L,g,S9)),L)) "\/" (Bottom L) is Element of the carrier of L
dF is Element of S
g . dF is non empty set
dF is Element of S
(S, the carrier of L,(S --> F),(S,F, the carrier of L,d),dF) is non empty Relation-like (S --> F) . dF -defined the carrier of L -valued Function-like total quasi_total Element of bool [:((S --> F) . dF), the carrier of L:]
(S --> F) . dF is non empty set
[:((S --> F) . dF), the carrier of L:] is non empty Relation-like set
bool [:((S --> F) . dF), the carrier of L:] is non empty set
rng (S, the carrier of L,(S --> F),(S,F, the carrier of L,d),dF) is non empty Element of bool the carrier of L
bool the carrier of L 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
rng (S, the carrier of L,g,S9,dF) is non empty Element of bool the carrier of L
y is Element of the carrier of L
x is Element of the carrier of L
dom (S, the carrier of L,(S --> F),(S,F, the carrier of L,d),dF) is non empty Element of bool ((S --> F) . dF)
bool ((S --> F) . dF) is non empty set
j is set
(S, the carrier of L,(S --> F),(S,F, the carrier of L,d),dF) . j is set
X is set
(S, the carrier of L,(S --> F),(S,F, the carrier of L,d),dF) . X is set
f9 is Element of F
d . (dF,f9) is Element of the carrier of L
[dF,f9] is V31() set
{dF,f9} is non empty finite countable set
{dF} is non empty trivial finite V54(1) countable set
{{dF,f9},{dF}} is non empty finite V42() countable set
d . [dF,f9] is set
z is Element of F
d . (dF,z) is Element of the carrier of L
[dF,z] is V31() set
{dF,z} is non empty finite countable set
{{dF,z},{dF}} is non empty finite V42() countable set
d . [dF,z] is set
dom (S, the carrier of L,g,S9,dF) is non empty Element of bool (g . dF)
bool (g . dF) is non empty set
(S, the carrier of L,g,S9,dF) . z is set
(S, the carrier of L,g,S9,dF) . f9 is set
j is Element of the carrier of L
(L,(S,F, the carrier of L,d)) is non empty Relation-like proj1 (S,F, the carrier of L,d) -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(proj1 (S,F, the carrier of L,d)), the carrier of L:]
proj1 (S,F, the carrier of L,d) is non empty set
[:(proj1 (S,F, the carrier of L,d)), the carrier of L:] is non empty Relation-like set
bool [:(proj1 (S,F, the carrier of L,d)), the carrier of L:] is non empty set
//\ ((L,(S,F, the carrier of L,d)),L) is Element of the carrier of L
S is non empty set
g is non empty set
[:S,g:] is non empty Relation-like 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,g:], the carrier of L:] is non empty Relation-like set
bool [:[:S,g:], the carrier of L:] is non empty set
S --> g is non empty Relation-like non-empty non empty-yielding S -defined {g} -valued Function-like constant total quasi_total Element of bool [:S,{g}:]
{g} is non empty trivial finite V54(1) countable set
[:S,{g}:] is non empty Relation-like set
bool [:S,{g}:] is non empty set
S9 is non empty Relation-like [:S,g:] -defined the carrier of L -valued Function-like total quasi_total Element of bool [:[:S,g:], the carrier of L:]
(S,g, the carrier of L,S9) is non empty Relation-like non-empty non empty-yielding S -defined Function-like total Function-yielding V129() ManySortedFunction of S --> g,S --> the carrier of L
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,(S,g, the carrier of L,S9)) is non empty Relation-like proj1 (S,g, the carrier of L,S9) -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(proj1 (S,g, the carrier of L,S9)), the carrier of L:]
proj1 (S,g, the carrier of L,S9) is non empty set
[:(proj1 (S,g, the carrier of L,S9)), the carrier of L:] is non empty Relation-like set
bool [:(proj1 (S,g, the carrier of L,S9)), the carrier of L:] is non empty set
//\ ((L,(S,g, the carrier of L,S9)),L) is Element of the carrier of L
(S, the carrier of L,(S --> g),(S,g, the carrier of L,S9)) is non empty Relation-like non-empty non empty-yielding product (doms (S,g, the carrier of L,S9)) -defined Function-like total Function-yielding V129() ManySortedFunction of (product (doms (S,g, the carrier of L,S9))) --> S,(product (doms (S,g, the carrier of L,S9))) --> the carrier of L
doms (S,g, the carrier of L,S9) is Relation-like non-empty Function-like set
product (doms (S,g, the carrier of L,S9)) is non empty functional with_common_domain product-like set
(product (doms (S,g, the carrier of L,S9))) --> S is non empty Relation-like non-empty non empty-yielding product (doms (S,g, the carrier of L,S9)) -defined {S} -valued Function-like constant total quasi_total Element of bool [:(product (doms (S,g, the carrier of L,S9))),{S}:]
{S} is non empty trivial finite V54(1) countable set
[:(product (doms (S,g, the carrier of L,S9))),{S}:] is non empty Relation-like set
bool [:(product (doms (S,g, the carrier of L,S9))),{S}:] is non empty set
(product (doms (S,g, the carrier of L,S9))) --> the carrier of L is non empty Relation-like non-empty non empty-yielding product (doms (S,g, the carrier of L,S9)) -defined { the carrier of L} -valued Function-like constant total quasi_total Element of bool [:(product (doms (S,g, the carrier of L,S9))),{ the carrier of L}:]
[:(product (doms (S,g, the carrier of L,S9))),{ the carrier of L}:] is non empty Relation-like set
bool [:(product (doms (S,g, the carrier of L,S9))),{ the carrier of L}:] is non empty set
(L,(S, the carrier of L,(S --> g),(S,g, the carrier of L,S9))) is non empty Relation-like proj1 (S, the carrier of L,(S --> g),(S,g, the carrier of L,S9)) -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(proj1 (S, the carrier of L,(S --> g),(S,g, the carrier of L,S9))), the carrier of L:]
proj1 (S, the carrier of L,(S --> g),(S,g, the carrier of L,S9)) is non empty set
[:(proj1 (S, the carrier of L,(S --> g),(S,g, the carrier of L,S9))), the carrier of L:] is non empty Relation-like set
bool [:(proj1 (S, the carrier of L,(S --> g),(S,g, the carrier of L,S9))), the carrier of L:] is non empty set
\\/ ((L,(S, the carrier of L,(S --> g),(S,g, the carrier of L,S9))),L) is Element of the carrier of L
J is non empty total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V211() up-complete /\-complete RelStr
the carrier of J is non empty set
L is non empty set
S is non empty set
Fin S is preBoolean set
Funcs (L,(Fin S)) is functional set
bool S is non empty set
g is Relation-like Function-like set
S9 is Element of L
g . S9 is set
proj2 g is set
J is Relation-like Function-like set
proj1 J is set
proj2 J is set
J is Relation-like Function-like set
proj1 J is set
proj2 J is set
S9 is Element of L
g . S9 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 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 set
[:S,g:] is non empty Relation-like set
Fin g is preBoolean set
Funcs (S,(Fin g)) is functional set
S --> g is non empty Relation-like non-empty non empty-yielding S -defined {g} -valued Function-like constant total quasi_total Element of bool [:S,{g}:]
{g} is non empty trivial finite V54(1) countable set
[:S,{g}:] is non empty Relation-like set
bool [:S,{g}:] is non empty set
S9 is non empty set
[:[:S,g:],S9:] is non empty Relation-like set
bool [:[:S,g:],S9:] is non empty set
J is Element of S
K is non empty Relation-like [:S,g:] -defined S9 -valued Function-like total quasi_total Element of bool [:[:S,g:],S9:]
(S,g,S9,K) is non empty Relation-like non-empty non empty-yielding S -defined Function-like total Function-yielding V129() ManySortedFunction of S --> g,S --> S9
S --> S9 is non empty Relation-like non-empty non empty-yielding S -defined {S9} -valued Function-like constant total quasi_total Element of bool [:S,{S9}:]
{S9} is non empty trivial finite V54(1) countable set
[:S,{S9}:] is non empty Relation-like set
bool [:S,{S9}:] is non empty set
(S,S9,(S --> g),(S,g,S9,K),J) is non empty Relation-like (S --> g) . J -defined S9 -valued Function-like total quasi_total Element of bool [:((S --> g) . J),S9:]
(S --> g) . J is non empty set
[:((S --> g) . J),S9:] is non empty Relation-like set
bool [:((S --> g) . J),S9:] is non empty set
rng (S,S9,(S --> g),(S,g,S9,K),J) is non empty Element of bool S9
bool S9 is non empty set
bool (rng (S,S9,(S --> g),(S,g,S9,K),J)) is non empty set
F is non empty Relation-like non-empty non empty-yielding S -defined Function-like total set
F . J is non empty set
bool g is non empty set
d is non empty Relation-like non-empty non empty-yielding S -defined Function-like total Function-yielding V129() ManySortedFunction of F,S --> the carrier of L
(S, the carrier of L,F,d,J) is non empty Relation-like F . J -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(F . J), the carrier of L:]
[:(F . J), the carrier of L:] is non empty Relation-like set
bool [:(F . J), the carrier of L:] is non empty set
rng (S, the carrier of L,F,d,J) is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
dF is set
dom (S, the carrier of L,F,d,J) is non empty Element of bool (F . J)
bool (F . J) is non empty set
gdF is set
(S, the carrier of L,F,d,J) . gdF is set
y is Element of g
dom (S,S9,(S --> g),(S,g,S9,K),J) is non empty Element of bool ((S --> g) . J)
bool ((S --> g) . J) is non empty set
K . (J,y) is Element of S9
[J,y] is V31() set
{J,y} is non empty finite countable set
{J} is non empty trivial finite V54(1) countable set
{{J,y},{J}} is non empty finite V42() countable set
K . [J,y] is set
(S,S9,(S --> g),(S,g,S9,K),J) . y 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
bool 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 set
[:S,g:] is non empty Relation-like set
[:[:S,g:], the carrier of L:] is non empty Relation-like set
bool [:[:S,g:], the carrier of L:] is non empty set
Fin g is preBoolean set
Funcs (S,(Fin g)) is functional set
S9 is non empty Relation-like [:S,g:] -defined the carrier of L -valued Function-like total quasi_total Element of bool [:[:S,g:], the carrier of L:]
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being non empty Relation-like non-empty non empty-yielding S -defined Function-like total set st
( b₂ in Funcs (S,(Fin g)) & ex b₃ being non empty Relation-like non-empty non empty-yielding S -defined Function-like total Function-yielding V129() ManySortedFunction of b₂,S --> the carrier of L st
( ( for b₄ being Element of S
for b₅ being set holds
( not b₅ in b₂ . b₄ or (S, the carrier of L,b₂,b₃,b₄) . b₅ = S9 . (b₄,b₅) ) ) & b₁ = //\ ((L,b₃),L) ) ) } is set
(S,g, the carrier of L,S9) is non empty Relation-like non-empty non empty-yielding S -defined Function-like total Function-yielding V129() ManySortedFunction of S --> g,S --> the carrier of L
S --> g is non empty Relation-like non-empty non empty-yielding S -defined {g} -valued Function-like constant total quasi_total Element of bool [:S,{g}:]
{g} is non empty trivial finite V54(1) countable set
[:S,{g}:] is non empty Relation-like set
bool [:S,{g}:] is non empty set
(L,(S,g, the carrier of L,S9)) is non empty Relation-like proj1 (S,g, the carrier of L,S9) -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(proj1 (S,g, the carrier of L,S9)), the carrier of L:]
proj1 (S,g, the carrier of L,S9) is non empty set
[:(proj1 (S,g, the carrier of L,S9)), the carrier of L:] is non empty Relation-like set
bool [:(proj1 (S,g, the carrier of L,S9)), the carrier of L:] is non empty set
//\ ((L,(S,g, the carrier of L,S9)),L) is Element of the carrier of L
J is Element of bool the carrier of L
"\/" (J,L) is Element of the carrier of L
K is non empty Relation-like non-empty non empty-yielding S -defined Function-like total set
F is non empty Relation-like non-empty non empty-yielding S -defined Function-like total Function-yielding V129() ManySortedFunction of K,S --> the carrier of L
d is Element of S
(S, the carrier of L,K,F,d) is non empty Relation-like K . d -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(K . d), the carrier of L:]
K . d is non empty set
[:(K . d), the carrier of L:] is non empty Relation-like set
bool [:(K . d), the carrier of L:] is non empty set
\\/ ((S, the carrier of L,K,F,d),L) is Element of the carrier of L
(S, the carrier of L,(S --> g),(S,g, the carrier of L,S9),d) is non empty Relation-like (S --> g) . d -defined the carrier of L -valued Function-like total quasi_total Element of bool [:((S --> g) . d), the carrier of L:]
(S --> g) . d is non empty set
[:((S --> g) . d), the carrier of L:] is non empty Relation-like set
bool [:((S --> g) . d), the carrier of L:] is non empty set
\\/ ((S, the carrier of L,(S --> g),(S,g, the carrier of L,S9),d),L) is Element of the carrier of L
rng (S, the carrier of L,(S --> g),(S,g, the carrier of L,S9),d) is non empty Element of bool the carrier of L
rng (S, the carrier of L,K,F,d) is non empty Element of bool the carrier of L
bool (rng (S, the carrier of L,(S --> g),(S,g, the carrier of L,S9),d)) is non empty set
"\/" ((rng (S, the carrier of L,K,F,d)),L) is Element of the carrier of L
"\/" ((rng (S, the carrier of L,(S --> g),(S,g, the carrier of L,S9),d)),L) is Element of the carrier of L
K is non empty Relation-like non-empty non empty-yielding S -defined Function-like total set
F is non empty Relation-like non-empty non empty-yielding S -defined Function-like total Function-yielding V129() ManySortedFunction of K,S --> the carrier of L
(L,F) is non empty Relation-like proj1 F -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(proj1 F), the carrier of L:]
proj1 F is non empty set
[:(proj1 F), the carrier of L:] is non empty Relation-like set
bool [:(proj1 F), the carrier of L:] is non empty set
//\ ((L,F),L) is Element of the carrier of L
rng (L,(S,g, the carrier of L,S9)) is non empty Element of bool the carrier of L
d is Element of the carrier of L
dF is Element of S
(S, the carrier of L,(S --> g),(S,g, the carrier of L,S9),dF) is non empty Relation-like (S --> g) . dF -defined the carrier of L -valued Function-like total quasi_total Element of bool [:((S --> g) . dF), the carrier of L:]
(S --> g) . dF is non empty set
[:((S --> g) . dF), the carrier of L:] is non empty Relation-like set
bool [:((S --> g) . dF), the carrier of L:] is non empty set
\\/ ((S, the carrier of L,(S --> g),(S,g, the carrier of L,S9),dF),L) is Element of the carrier of L
(S, the carrier of L,K,F,dF) is non empty Relation-like K . dF -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(K . dF), the carrier of L:]
K . dF is non empty set
[:(K . dF), the carrier of L:] is non empty Relation-like set
bool [:(K . dF), the carrier of L:] is non empty set
\\/ ((S, the carrier of L,K,F,dF),L) is Element of the carrier of L
rng (L,F) is non empty Element of bool the carrier of L
"/\" ((rng (L,F)),L) is Element of the carrier of L
"/\" ((rng (L,(S,g, the carrier of L,S9))),L) is Element of the carrier of L
K is Element of the carrier of L
d is non empty Relation-like non-empty non empty-yielding S -defined Function-like total set
F is Element of the carrier of L
dF is non empty Relation-like non-empty non empty-yielding S -defined Function-like total Function-yielding V129() ManySortedFunction of d,S --> the carrier of L
(L,dF) is non empty Relation-like proj1 dF -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(proj1 dF), the carrier of L:]
proj1 dF is non empty set
[:(proj1 dF), the carrier of L:] is non empty Relation-like set
bool [:(proj1 dF), the carrier of L:] is non empty set
//\ ((L,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
bool the carrier of L is non empty set
g is non empty set
bool g is non empty set
{ b₁ where b₁ is Element of bool g : ( b₁ is finite & not b₁ = {} ) } is set
the Element of g is Element of g
{ the Element of g} is non empty trivial finite V54(1) countable Element of bool g
S is non empty set
[:S,g:] is non empty Relation-like set
[:[:S,g:], the carrier of L:] is non empty Relation-like set
bool [:[:S,g:], the carrier of L:] is non empty set
K is non empty set
Funcs (S,K) is non empty functional FUNCTION_DOMAIN of S,K
S --> g is non empty Relation-like non-empty non empty-yielding S -defined {g} -valued Function-like constant total quasi_total Element of bool [:S,{g}:]
{g} is non empty trivial finite V54(1) countable set
[:S,{g}:] is non empty Relation-like set
bool [:S,{g}:] is non empty set
F is non empty Relation-like [:S,g:] -defined the carrier of L -valued Function-like total quasi_total Element of bool [:[:S,g:], the carrier of L:]
(S,g, the carrier of L,F) is non empty Relation-like non-empty non empty-yielding S -defined Function-like total Function-yielding V129() ManySortedFunction of S --> g,S --> the carrier of L
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,(Funcs (S,K)):] is non empty Relation-like set
[:[:S,(Funcs (S,K)):], the carrier of L:] is non empty Relation-like set
bool [:[:S,(Funcs (S,K)):], the carrier of L:] is non empty set
gdF is non empty Relation-like [:S,(Funcs (S,K)):] -defined the carrier of L -valued Function-like total quasi_total Element of bool [:[:S,(Funcs (S,K)):], the carrier of L:]
gdF is non empty Relation-like [:S,(Funcs (S,K)):] -defined the carrier of L -valued Function-like total quasi_total Element of bool [:[:S,(Funcs (S,K)):], the carrier of L:]
(S,(Funcs (S,K)), the carrier of L,gdF) is non empty Relation-like non-empty non empty-yielding S -defined Function-like total Function-yielding V129() ManySortedFunction of S --> (Funcs (S,K)),S --> the carrier of L
S --> (Funcs (S,K)) is non empty Relation-like non-empty non empty-yielding S -defined {(Funcs (S,K))} -valued Function-like constant total quasi_total Element of bool [:S,{(Funcs (S,K))}:]
{(Funcs (S,K))} is non empty trivial finite V54(1) countable set
[:S,{(Funcs (S,K))}:] is non empty Relation-like set
bool [:S,{(Funcs (S,K))}:] is non empty set
j is Element of S
(S, the carrier of L,(S --> g),(S,g, the carrier of L,F),j) is non empty Relation-like (S --> g) . j -defined the carrier of L -valued Function-like total quasi_total Element of bool [:((S --> g) . j), the carrier of L:]
(S --> g) . j is non empty set
[:((S --> g) . j), the carrier of L:] is non empty Relation-like set
bool [:((S --> g) . j), the carrier of L:] is non empty set
rng (S, the carrier of L,(S --> g),(S,g, the carrier of L,F),j) is non empty Element of bool the carrier of L
bool (rng (S, the carrier of L,(S --> g),(S,g, the carrier of L,F),j)) is non empty set
(S, the carrier of L,(S --> (Funcs (S,K))),(S,(Funcs (S,K)), the carrier of L,gdF),j) is non empty Relation-like (S --> (Funcs (S,K))) . j -defined the carrier of L -valued Function-like total quasi_total Element of bool [:((S --> (Funcs (S,K))) . j), the carrier of L:]
(S --> (Funcs (S,K))) . j is non empty set
[:((S --> (Funcs (S,K))) . j), the carrier of L:] is non empty Relation-like set
bool [:((S --> (Funcs (S,K))) . j), the carrier of L:] is non empty set
rng (S, the carrier of L,(S --> (Funcs (S,K))),(S,(Funcs (S,K)), the carrier of L,gdF),j) is non empty Element of bool the carrier of L
c₁₈ is finite countable Element of bool (rng (S, the carrier of L,(S --> g),(S,g, the carrier of L,F),j))
c₁₈ is Element of the carrier of L
dom (S, the carrier of L,(S --> (Funcs (S,K))),(S,(Funcs (S,K)), the carrier of L,gdF),j) is non empty Element of bool ((S --> (Funcs (S,K))) . j)
bool ((S --> (Funcs (S,K))) . j) is non empty set
j is set
(S, the carrier of L,(S --> (Funcs (S,K))),(S,(Funcs (S,K)), the carrier of L,gdF),j) . j is set
hj is non empty Relation-like S -defined K -valued Function-like total quasi_total Element of Funcs (S,K)
hj . j is Element of K
(S, the carrier of L,(S --> g),(S,g, the carrier of L,F),j) .: (hj . j) is Element of bool the carrier of L
k is Element of bool g
x is finite countable Element of bool (rng (S, the carrier of L,(S --> g),(S,g, the carrier of L,F),j))
"\/" (x,L) is Element of the carrier of L
gdF . (j,hj) is Element of the carrier of L
[j,hj] is V31() set
{j,hj} is non empty finite countable set
{j} is non empty trivial finite V54(1) countable set
{{j,hj},{j}} is non empty finite V42() countable set
gdF . [j,hj] is set
"\/" (((S, the carrier of L,(S --> g),(S,g, the carrier of L,F),j) .: (hj . j)),L) is Element of the carrier of L
c₁₈ is finite countable Element of bool (rng (S, the carrier of L,(S --> g),(S,g, the carrier of L,F),j))
"\/" (c₁₈,L) is Element of the carrier of L
dom (S, the carrier of L,(S --> g),(S,g, the carrier of L,F),j) is non empty Element of bool ((S --> g) . j)
bool ((S --> g) . j) is non empty set
j is set
(S, the carrier of L,(S --> g),(S,g, the carrier of L,F),j) .: j is Element of bool the carrier of L
{j} is non empty trivial finite V54(1) countable set
S --> j is non empty Relation-like S -defined {j} -valued Function-like constant total quasi_total Element of bool [:S,{j}:]
[:S,{j}:] is non empty Relation-like set
bool [:S,{j}:] is non empty set
dom (S --> j) is non empty Element of bool S
bool S is non empty set
rng (S --> j) is non empty trivial finite V54(1) countable Element of bool {j}
bool {j} is non empty finite V42() countable set
hj is non empty Relation-like S -defined K -valued Function-like total quasi_total Element of Funcs (S,K)
hj . j is Element of K
dom (S, the carrier of L,(S --> (Funcs (S,K))),(S,(Funcs (S,K)), the carrier of L,gdF),j) is non empty Element of bool ((S --> (Funcs (S,K))) . j)
bool ((S --> (Funcs (S,K))) . j) is non empty set
(S, the carrier of L,(S --> (Funcs (S,K))),(S,(Funcs (S,K)), the carrier of L,gdF),j) . hj is set
gdF . (j,hj) is Element of the carrier of L
[j,hj] is V31() set
{j,hj} is non empty finite countable set
{j} is non empty trivial finite V54(1) countable set
{{j,hj},{j}} is non empty finite V42() countable set
gdF . [j,hj] is set
j is Element of S
(S, the carrier of L,(S --> (Funcs (S,K))),(S,(Funcs (S,K)), the carrier of L,gdF),j) is non empty Relation-like (S --> (Funcs (S,K))) . j -defined the carrier of L -valued Function-like total quasi_total Element of bool [:((S --> (Funcs (S,K))) . j), the carrier of L:]
(S --> (Funcs (S,K))) . j is non empty set
[:((S --> (Funcs (S,K))) . j), the carrier of L:] is non empty Relation-like set
bool [:((S --> (Funcs (S,K))) . j), the carrier of L:] is non empty set
rng (S, the carrier of L,(S --> (Funcs (S,K))),(S,(Funcs (S,K)), the carrier of L,gdF),j) is non empty Element of bool the carrier of L
(S, the carrier of L,(S --> g),(S,g, the carrier of L,F),j) is non empty Relation-like (S --> g) . j -defined the carrier of L -valued Function-like total quasi_total Element of bool [:((S --> g) . j), the carrier of L:]
(S --> g) . j is non empty set
[:((S --> g) . j), the carrier of L:] is non empty Relation-like set
bool [:((S --> g) . j), the carrier of L:] is non empty set
rng (S, the carrier of L,(S --> g),(S,g, the carrier of L,F),j) is non empty Element of bool the carrier of L
bool (rng (S, the carrier of L,(S --> g),(S,g, the carrier of L,F),j)) is non empty set
X is finite countable Element of bool (rng (S, the carrier of L,(S --> g),(S,g, the carrier of L,F),j))
"\/" (X,L) is Element of the carrier of L
X is finite countable Element of bool (rng (S, the carrier of L,(S --> g),(S,g, the carrier of L,F),j))
f9 is Element of the carrier of L
(L,(S,(Funcs (S,K)), the carrier of L,gdF)) is non empty Relation-like proj1 (S,(Funcs (S,K)), the carrier of L,gdF) -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(proj1 (S,(Funcs (S,K)), the carrier of L,gdF)), the carrier of L:]
proj1 (S,(Funcs (S,K)), the carrier of L,gdF) is non empty set
[:(proj1 (S,(Funcs (S,K)), the carrier of L,gdF)), the carrier of L:] is non empty Relation-like set
bool [:(proj1 (S,(Funcs (S,K)), the carrier of L,gdF)), the carrier of L:] is non empty set
//\ ((L,(S,(Funcs (S,K)), the carrier of L,gdF)),L) is Element of the carrier of L
(S, the carrier of L,(S --> (Funcs (S,K))),(S,(Funcs (S,K)), the carrier of L,gdF)) is non empty Relation-like non-empty non empty-yielding product (doms (S,(Funcs (S,K)), the carrier of L,gdF)) -defined Function-like total Function-yielding V129() ManySortedFunction of (product (doms (S,(Funcs (S,K)), the carrier of L,gdF))) --> S,(product (doms (S,(Funcs (S,K)), the carrier of L,gdF))) --> the carrier of L
doms (S,(Funcs (S,K)), the carrier of L,gdF) is Relation-like non-empty Function-like set
product (doms (S,(Funcs (S,K)), the carrier of L,gdF)) is non empty functional with_common_domain product-like set
(product (doms (S,(Funcs (S,K)), the carrier of L,gdF))) --> S is non empty Relation-like non-empty non empty-yielding product (doms (S,(Funcs (S,K)), the carrier of L,gdF)) -defined {S} -valued Function-like constant total quasi_total Element of bool [:(product (doms (S,(Funcs (S,K)), the carrier of L,gdF))),{S}:]
{S} is non empty trivial finite V54(1) countable set
[:(product (doms (S,(Funcs (S,K)), the carrier of L,gdF))),{S}:] is non empty Relation-like set
bool [:(product (doms (S,(Funcs (S,K)), the carrier of L,gdF))),{S}:] is non empty set
(product (doms (S,(Funcs (S,K)), the carrier of L,gdF))) --> the carrier of L is non empty Relation-like non-empty non empty-yielding product (doms (S,(Funcs (S,K)), the carrier of L,gdF)) -defined { the carrier of L} -valued Function-like constant total quasi_total Element of bool [:(product (doms (S,(Funcs (S,K)), the carrier of L,gdF))),{ the carrier of L}:]
[:(product (doms (S,(Funcs (S,K)), the carrier of L,gdF))),{ the carrier of L}:] is non empty Relation-like set
bool [:(product (doms (S,(Funcs (S,K)), the carrier of L,gdF))),{ the carrier of L}:] is non empty set
(L,(S, the carrier of L,(S --> (Funcs (S,K))),(S,(Funcs (S,K)), the carrier of L,gdF))) is non empty Relation-like proj1 (S, the carrier of L,(S --> (Funcs (S,K))),(S,(Funcs (S,K)), the carrier of L,gdF)) -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(proj1 (S, the carrier of L,(S --> (Funcs (S,K))),(S,(Funcs (S,K)), the carrier of L,gdF))), the carrier of L:]
proj1 (S, the carrier of L,(S --> (Funcs (S,K))),(S,(Funcs (S,K)), the carrier of L,gdF)) is non empty set
[:(proj1 (S, the carrier of L,(S --> (Funcs (S,K))),(S,(Funcs (S,K)), the carrier of L,gdF))), the carrier of L:] is non empty Relation-like set
bool [:(proj1 (S, the carrier of L,(S --> (Funcs (S,K))),(S,(Funcs (S,K)), the carrier of L,gdF))), the carrier of L:] is non empty set
\\/ ((L,(S, the carrier of L,(S --> (Funcs (S,K))),(S,(Funcs (S,K)), the carrier of L,gdF))),L) is Element of the carrier of L
dom (S,g, the carrier of L,F) is non empty Element of bool S
bool S is non empty set
j is set
(S,g, the carrier of L,F) . j is Relation-like Function-like set
\\/ (((S,g, the carrier of L,F) . j),L) is Element of the carrier of L
(S,(Funcs (S,K)), the carrier of L,gdF) . j is Relation-like Function-like set
\\/ (((S,(Funcs (S,K)), the carrier of L,gdF) . j),L) is Element of the carrier of L
X is Element of S
(S, the carrier of L,(S --> (Funcs (S,K))),(S,(Funcs (S,K)), the carrier of L,gdF),X) is non empty Relation-like (S --> (Funcs (S,K))) . X -defined the carrier of L -valued Function-like total quasi_total Element of bool [:((S --> (Funcs (S,K))) . X), the carrier of L:]
(S --> (Funcs (S,K))) . X is non empty set
[:((S --> (Funcs (S,K))) . X), the carrier of L:] is non empty Relation-like set
bool [:((S --> (Funcs (S,K))) . X), the carrier of L:] is non empty set
rng (S, the carrier of L,(S --> (Funcs (S,K))),(S,(Funcs (S,K)), the carrier of L,gdF),X) is non empty Element of bool the carrier of L
(S, the carrier of L,(S --> g),(S,g, the carrier of L,F),X) is non empty Relation-like (S --> g) . X -defined the carrier of L -valued Function-like total quasi_total Element of bool [:((S --> g) . X), the carrier of L:]
(S --> g) . X is non empty set
[:((S --> g) . X), the carrier of L:] is non empty Relation-like set
bool [:((S --> g) . X), the carrier of L:] is non empty set
rng (S, the carrier of L,(S --> g),(S,g, the carrier of L,F),X) is non empty Element of bool the carrier of L
bool (rng (S, the carrier of L,(S --> g),(S,g, the carrier of L,F),X)) is non empty set
f9 is Element of the carrier of L
z is finite countable Element of bool (rng (S, the carrier of L,(S --> g),(S,g, the carrier of L,F),X))
"\/" (z,L) is Element of the carrier of L
f9 is finite countable Element of bool (rng (S, the carrier of L,(S --> g),(S,g, the carrier of L,F),X))
"\/" ((rng (S, the carrier of L,(S --> g),(S,g, the carrier of L,F),X)),L) is Element of the carrier of L
"\/" ((rng (S, the carrier of L,(S --> (Funcs (S,K))),(S,(Funcs (S,K)), the carrier of L,gdF),X)),L) is Element of the carrier of L
\\/ ((S, the carrier of L,(S --> g),(S,g, the carrier of L,F),X),L) is Element of the carrier of L
d is Element of bool the carrier of L
Fin g is preBoolean set
Funcs (S,(Fin g)) is functional set
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being non empty Relation-like non-empty non empty-yielding S -defined Function-like total set st
( b₂ in Funcs (S,(Fin g)) & ex b₃ being non empty Relation-like non-empty non empty-yielding S -defined Function-like total Function-yielding V129() ManySortedFunction of b₂,S --> the carrier of L st
( ( for b₄ being Element of S
for b₅ being set holds
( not b₅ in b₂ . b₄ or (S, the carrier of L,b₂,b₃,b₄) . b₅ = F . (b₄,b₅) ) ) & b₁ = //\ ((L,b₃),L) ) ) } is set
"\/" (d,L) is Element of the carrier of L
(L,(S,g, the carrier of L,F)) is non empty Relation-like proj1 (S,g, the carrier of L,F) -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(proj1 (S,g, the carrier of L,F)), the carrier of L:]
proj1 (S,g, the carrier of L,F) is non empty set
[:(proj1 (S,g, the carrier of L,F)), the carrier of L:] is non empty Relation-like set
bool [:(proj1 (S,g, the carrier of L,F)), the carrier of L:] is non empty set
//\ ((L,(S,g, the carrier of L,F)),L) is Element of the carrier of L
j is set
X is Element of bool g
id S is non empty Relation-like S -defined S -valued Function-like one-to-one total quasi_total Element of bool [:S,S:]
[:S,S:] is non empty Relation-like set
bool [:S,S:] is non empty set
j is Relation-like Function-like Function-yielding V129() set
Frege j is Relation-like product (doms j) -defined Function-like total Function-yielding V129() set
doms j is Relation-like Function-like set
product (doms j) is functional with_common_domain product-like set
(Frege j) . (id S) is Relation-like Function-like set
dom (S, the carrier of L,(S --> (Funcs (S,K))),(S,(Funcs (S,K)), the carrier of L,gdF)) is non empty functional with_common_domain Element of bool (product (doms (S,(Funcs (S,K)), the carrier of L,gdF)))
bool (product (doms (S,(Funcs (S,K)), the carrier of L,gdF))) is non empty set
proj1 j is set
dom (S,(Funcs (S,K)), the carrier of L,gdF) is non empty Element of bool S
proj1 (doms j) is set
f9 is set
(id S) . f9 is set
(doms j) . f9 is set
z is Element of S
j . z is Relation-like Function-like set
(S --> (Funcs (S,K))) . z is non empty Element of {(Funcs (S,K))}
(id S) . z is Element of S
(doms j) . z is set
j is Relation-like Function-like set
proj1 j is set
proj2 j is set
dom (id S) is non empty Element of bool S
dom (Frege j) is functional with_common_domain Element of bool (product (doms j))
bool (product (doms j)) is non empty set
proj1 ((Frege j) . (id S)) is set
z is Element of S
((Frege j) . (id S)) . z is set
j . z is Relation-like Function-like set
(j . z) . z is set
(id S) . z is Element of S
(j . z) . ((id S) . z) is set
(S --> (Funcs (S,K))) . z is non empty Element of {(Funcs (S,K))}
j is Relation-like Function-like set
proj1 j is set
proj2 j is set
c₁₈ is Element of bool g
f9 is non empty Relation-like S -defined Function-like total set
z is set
f9 . z is set
proj2 ((Frege j) . (id S)) is set
z is set
j is set
((Frege j) . (id S)) . j is set
j is Relation-like Function-like doms (S,(Funcs (S,K)), the carrier of L,gdF) -compatible Element of product (doms (S,(Funcs (S,K)), the carrier of L,gdF))
(S, the carrier of L,(S --> (Funcs (S,K))),(S,(Funcs (S,K)), the carrier of L,gdF),(S, the carrier of L,(S --> (Funcs (S,K))),(S,(Funcs (S,K)), the carrier of L,gdF)),j) 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,(S --> (Funcs (S,K))),(S,(Funcs (S,K)), the carrier of L,gdF),(S, the carrier of L,(S --> (Funcs (S,K))),(S,(Funcs (S,K)), the carrier of L,gdF)),j),L) is Element of the carrier of L
dom (S, the carrier of L,(S --> (Funcs (S,K))),(S,(Funcs (S,K)), the carrier of L,gdF)) is non empty functional with_common_domain Element of bool (product (doms (S,(Funcs (S,K)), the carrier of L,gdF)))
bool (product (doms (S,(Funcs (S,K)), the carrier of L,gdF))) is non empty set
proj1 j is set
X is set
j . X is set
dom (S,(Funcs (S,K)), the carrier of L,gdF) is non empty Element of bool S
f9 is Element of S
j . f9 is set
(S --> (Funcs (S,K))) . f9 is non empty Element of {(Funcs (S,K))}
X is Relation-like Function-like Function-yielding V129() set
Frege X is Relation-like product (doms X) -defined Function-like total Function-yielding V129() set
doms X is Relation-like Function-like set
product (doms X) is functional with_common_domain product-like set
(Frege X) . (id S) is Relation-like Function-like set
f9 is non empty Relation-like non-empty non empty-yielding S -defined Function-like total set
z is set
f9 . z is set
(S --> the carrier of L) . z is set
c₁₈ is set
F . (z,c₁₈) is set
[z,c₁₈] is V31() set
{z,c₁₈} is non empty finite countable set
{z} is non empty trivial finite V54(1) countable set
{{z,c₁₈},{z}} is non empty finite V42() countable set
F . [z,c₁₈] is set
j is Element of S
f9 . j is non empty set
j is Element of g
[j,j] is V31() Element of [:S,g:]
{j,j} is non empty finite countable set
{j} is non empty trivial finite V54(1) countable set
{{j,j},{j}} is non empty finite V42() countable set
F . [j,j] is Element of the carrier of L
hj is Element of the carrier of L
z is non empty Relation-like non-empty non empty-yielding S -defined Function-like total Function-yielding V129() ManySortedFunction of f9,S --> the carrier of L
z is non empty Relation-like non-empty non empty-yielding S -defined Function-like total Function-yielding V129() ManySortedFunction of f9,S --> the carrier of L
j is non empty Relation-like non-empty non empty-yielding S -defined Function-like total Function-yielding V129() ManySortedFunction of f9,S --> the carrier of L
c₁₈ is Element of S
f9 . c₁₈ is non empty set
(S, the carrier of L,f9,j,c₁₈) is non empty Relation-like f9 . c₁₈ -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(f9 . c₁₈), the carrier of L:]
[:(f9 . c₁₈), the carrier of L:] is non empty Relation-like set
bool [:(f9 . c₁₈), the carrier of L:] is non empty set
j is set
(S, the carrier of L,f9,j,c₁₈) . j is set
F . (c₁₈,j) is set
[c₁₈,j] is V31() set
{c₁₈,j} is non empty finite countable set
{c₁₈} is non empty trivial finite V54(1) countable set
{{c₁₈,j},{c₁₈}} is non empty finite V42() countable set
F . [c₁₈,j] is set
(S --> the carrier of L) . c₁₈ is non empty Element of { the carrier of L}
[:(f9 . c₁₈),((S --> the carrier of L) . c₁₈):] is non empty Relation-like set
bool [:(f9 . c₁₈),((S --> the carrier of L) . c₁₈):] is non empty set
hj is non empty Relation-like f9 . c₁₈ -defined (S --> the carrier of L) . c₁₈ -valued Function-like total quasi_total Element of bool [:(f9 . c₁₈),((S --> the carrier of L) . c₁₈):]
(L,j) is non empty Relation-like proj1 j -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(proj1 j), the carrier of L:]
proj1 j is non empty set
[:(proj1 j), the carrier of L:] is non empty Relation-like set
bool [:(proj1 j), the carrier of L:] is non empty set
rng (L,j) is non empty Element of bool the carrier of L
c₁₈ is Element of the carrier of L
j is Element of S
(S, the carrier of L,f9,j,j) is non empty Relation-like f9 . j -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(f9 . j), the carrier of L:]
f9 . j is non empty set
[:(f9 . j), the carrier of L:] is non empty Relation-like set
bool [:(f9 . j), the carrier of L:] is non empty set
\\/ ((S, the carrier of L,f9,j,j),L) is Element of the carrier of L
dom (S,(Funcs (S,K)), the carrier of L,gdF) is non empty Element of bool S
(S --> g) . j is non empty set
(S, the carrier of L,(S --> g),(S,g, the carrier of L,F),j) is non empty Relation-like (S --> g) . j -defined the carrier of L -valued Function-like total quasi_total Element of bool [:((S --> g) . j), the carrier of L:]
[:((S --> g) . j), the carrier of L:] is non empty Relation-like set
bool [:((S --> g) . j), the carrier of L:] is non empty set
(S, the carrier of L,(S --> g),(S,g, the carrier of L,F),j) .: (f9 . j) is Element of bool the carrier of L
rng (S, the carrier of L,f9,j,j) is non empty Element of bool the carrier of L
hj is set
dom (S, the carrier of L,(S --> g),(S,g, the carrier of L,F),j) is non empty Element of bool ((S --> g) . j)
bool ((S --> g) . j) is non empty set
x is set
(S, the carrier of L,(S --> g),(S,g, the carrier of L,F),j) . x is set
k is Element of g
dom (S, the carrier of L,f9,j,j) is non empty Element of bool (f9 . j)
bool (f9 . j) is non empty set
F . (j,k) is Element of the carrier of L
[j,k] is V31() set
{j,k} is non empty finite countable set
{j} is non empty trivial finite V54(1) countable set
{{j,k},{j}} is non empty finite V42() countable set
F . [j,k] is set
(S, the carrier of L,f9,j,j) . k is set
"\/" (((S, the carrier of L,(S --> g),(S,g, the carrier of L,F),j) .: (f9 . j)),L) is Element of the carrier of L
"\/" ((rng (S, the carrier of L,f9,j,j)),L) is Element of the carrier of L
j . j is set
(S --> (Funcs (S,K))) . j is non empty Element of {(Funcs (S,K))}
(S, the carrier of L,(S --> (Funcs (S,K))),(S,(Funcs (S,K)), the carrier of L,gdF),(S, the carrier of L,(S --> (Funcs (S,K))),(S,(Funcs (S,K)), the carrier of L,gdF)),j) . j is Element of the carrier of L
hj is non empty Relation-like S -defined K -valued Function-like total quasi_total Element of Funcs (S,K)
hj . j is Element of K
(S, the carrier of L,(S --> g),(S,g, the carrier of L,F),j) .: (hj . j) is Element of bool the carrier of L
"\/" (((S, the carrier of L,(S --> g),(S,g, the carrier of L,F),j) .: (hj . j)),L) is Element of the carrier of L
gdF . (j,hj) is Element of the carrier of L
[j,hj] is V31() set
{j,hj} is non empty finite countable set
{j} is non empty trivial finite V54(1) countable set
{{j,hj},{j}} is non empty finite V42() countable set
gdF . [j,hj] is set
(S, the carrier of L,(S --> (Funcs (S,K))),(S,(Funcs (S,K)), the carrier of L,gdF),j) is non empty Relation-like (S --> (Funcs (S,K))) . j -defined the carrier of L -valued Function-like total quasi_total Element of bool [:((S --> (Funcs (S,K))) . j), the carrier of L:]
(S --> (Funcs (S,K))) . j is non empty set
[:((S --> (Funcs (S,K))) . j), the carrier of L:] is non empty Relation-like set
bool [:((S --> (Funcs (S,K))) . j), the carrier of L:] is non empty set
(S, the carrier of L,(S --> (Funcs (S,K))),(S,(Funcs (S,K)), the carrier of L,gdF),j) . (j . j) is set
"/\" ((rng (L,j)),L) is Element of the carrier of L
//\ ((L,j),L) is Element of the carrier of L
rng (L,(S, the carrier of L,(S --> (Funcs (S,K))),(S,(Funcs (S,K)), the carrier of L,gdF))) is non empty Element of bool the carrier of L
j is Element of the carrier of L
dom (S, the carrier of L,(S --> (Funcs (S,K))),(S,(Funcs (S,K)), the carrier of L,gdF)) is non empty functional with_common_domain Element of bool (product (doms (S,(Funcs (S,K)), the carrier of L,gdF)))
bool (product (doms (S,(Funcs (S,K)), the carrier of L,gdF))) is non empty set
X is set
(S, the carrier of L,(S --> (Funcs (S,K))),(S,(Funcs (S,K)), the carrier of L,gdF)) . X is Relation-like Function-like set
//\ (((S, the carrier of L,(S --> (Funcs (S,K))),(S,(Funcs (S,K)), the carrier of L,gdF)) . X),L) is Element of the carrier of L
f9 is Relation-like Function-like doms (S,(Funcs (S,K)), the carrier of L,gdF) -compatible Element of product (doms (S,(Funcs (S,K)), the carrier of L,gdF))
(S, the carrier of L,(S --> (Funcs (S,K))),(S,(Funcs (S,K)), the carrier of L,gdF),(S, the carrier of L,(S --> (Funcs (S,K))),(S,(Funcs (S,K)), the carrier of L,gdF)),f9) 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,(S --> (Funcs (S,K))),(S,(Funcs (S,K)), the carrier of L,gdF),(S, the carrier of L,(S --> (Funcs (S,K))),(S,(Funcs (S,K)), the carrier of L,gdF)),f9),L) is Element of the carrier of L
"\/" ((rng (L,(S, the carrier of L,(S --> (Funcs (S,K))),(S,(Funcs (S,K)), the carrier of L,gdF)))),L) is Element of the carrier of L
dom (S,(Funcs (S,K)), the carrier of L,gdF) is non empty Element of bool S
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
bool the carrier of L is non empty set
S is non empty set
g is non empty set
[:S,g:] is non empty Relation-like set
[:[:S,g:], the carrier of L:] is non empty Relation-like set
bool [:[:S,g:], the carrier of L:] is non empty set
S --> g is non empty Relation-like non-empty non empty-yielding S -defined {g} -valued Function-like constant total quasi_total Element of bool [:S,{g}:]
{g} is non empty trivial finite V54(1) countable set
[:S,{g}:] is non empty Relation-like set
bool [:S,{g}:] is non empty set
S9 is non empty Relation-like [:S,g:] -defined the carrier of L -valued Function-like total quasi_total Element of bool [:[:S,g:], the carrier of L:]
(S,g, the carrier of L,S9) is non empty Relation-like non-empty non empty-yielding S -defined Function-like total Function-yielding V129() ManySortedFunction of S --> g,S --> the carrier of L
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,(S,g, the carrier of L,S9)) is non empty Relation-like proj1 (S,g, the carrier of L,S9) -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(proj1 (S,g, the carrier of L,S9)), the carrier of L:]
proj1 (S,g, the carrier of L,S9) is non empty set
[:(proj1 (S,g, the carrier of L,S9)), the carrier of L:] is non empty Relation-like set
bool [:(proj1 (S,g, the carrier of L,S9)), the carrier of L:] is non empty set
//\ ((L,(S,g, the carrier of L,S9)),L) is Element of the carrier of L
(S, the carrier of L,(S --> g),(S,g, the carrier of L,S9)) is non empty Relation-like non-empty non empty-yielding product (doms (S,g, the carrier of L,S9)) -defined Function-like total Function-yielding V129() ManySortedFunction of (product (doms (S,g, the carrier of L,S9))) --> S,(product (doms (S,g, the carrier of L,S9))) --> the carrier of L
doms (S,g, the carrier of L,S9) is Relation-like non-empty Function-like set
product (doms (S,g, the carrier of L,S9)) is non empty functional with_common_domain product-like set
(product (doms (S,g, the carrier of L,S9))) --> S is non empty Relation-like non-empty non empty-yielding product (doms (S,g, the carrier of L,S9)) -defined {S} -valued Function-like constant total quasi_total Element of bool [:(product (doms (S,g, the carrier of L,S9))),{S}:]
{S} is non empty trivial finite V54(1) countable set
[:(product (doms (S,g, the carrier of L,S9))),{S}:] is non empty Relation-like set
bool [:(product (doms (S,g, the carrier of L,S9))),{S}:] is non empty set
(product (doms (S,g, the carrier of L,S9))) --> the carrier of L is non empty Relation-like non-empty non empty-yielding product (doms (S,g, the carrier of L,S9)) -defined { the carrier of L} -valued Function-like constant total quasi_total Element of bool [:(product (doms (S,g, the carrier of L,S9))),{ the carrier of L}:]
[:(product (doms (S,g, the carrier of L,S9))),{ the carrier of L}:] is non empty Relation-like set
bool [:(product (doms (S,g, the carrier of L,S9))),{ the carrier of L}:] is non empty set
(L,(S, the carrier of L,(S --> g),(S,g, the carrier of L,S9))) is non empty Relation-like proj1 (S, the carrier of L,(S --> g),(S,g, the carrier of L,S9)) -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(proj1 (S, the carrier of L,(S --> g),(S,g, the carrier of L,S9))), the carrier of L:]
proj1 (S, the carrier of L,(S --> g),(S,g, the carrier of L,S9)) is non empty set
[:(proj1 (S, the carrier of L,(S --> g),(S,g, the carrier of L,S9))), the carrier of L:] is non empty Relation-like set
bool [:(proj1 (S, the carrier of L,(S --> g),(S,g, the carrier of L,S9))), the carrier of L:] is non empty set
\\/ ((L,(S, the carrier of L,(S --> g),(S,g, the carrier of L,S9))),L) is Element of the carrier of L
Fin g is preBoolean set
Funcs (S,(Fin g)) is functional set
{ b₁ where b₁ is Element of the carrier of L : S₁[b₁] } is set
J is Element of bool the carrier of L
K is Element of the carrier of L
F is Element of the carrier of L
d is non empty Relation-like non-empty non empty-yielding S -defined Function-like total set
dF is non empty Relation-like non-empty non empty-yielding S -defined Function-like total Function-yielding V129() ManySortedFunction of d,S --> the carrier of L
(L,dF) is non empty Relation-like proj1 dF -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(proj1 dF), the carrier of L:]
proj1 dF is non empty set
[:(proj1 dF), the carrier of L:] is non empty Relation-like set
bool [:(proj1 dF), the carrier of L:] is non empty set
//\ ((L,dF),L) is Element of the carrier of L
d is non empty Relation-like non-empty non empty-yielding S -defined Function-like total set
dF is non empty Relation-like non-empty non empty-yielding S -defined Function-like total Function-yielding V129() ManySortedFunction of d,S --> the carrier of L
(L,dF) is non empty Relation-like proj1 dF -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(proj1 dF), the carrier of L:]
proj1 dF is non empty set
[:(proj1 dF), the carrier of L:] is non empty Relation-like set
bool [:(proj1 dF), the carrier of L:] is non empty set
//\ ((L,dF),L) is Element of the carrier of L
dF is non empty Relation-like non-empty non empty-yielding S -defined Function-like total Function-yielding V129() ManySortedFunction of d,S --> the carrier of L
(L,dF) is non empty Relation-like proj1 dF -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(proj1 dF), the carrier of L:]
proj1 dF is non empty set
[:(proj1 dF), the carrier of L:] is non empty Relation-like set
bool [:(proj1 dF), the carrier of L:] is non empty set
//\ ((L,dF),L) is Element of the carrier of L
gdF is set
(S,g, the carrier of L,S9) . gdF is Relation-like Function-like set
y is Element of S
(S, the carrier of L,d,dF,y) is non empty Relation-like d . y -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(d . y), the carrier of L:]
d . y is non empty set
[:(d . y), the carrier of L:] is non empty Relation-like set
bool [:(d . y), the carrier of L:] is non empty set
\\/ ((S, the carrier of L,d,dF,y),L) is Element of the carrier of L
rng (L,dF) is non empty Element of bool the carrier of L
"/\" ((rng (L,dF)),L) is Element of the carrier of L
(S, the carrier of L,(S --> g),(S,g, the carrier of L,S9),y) is non empty Relation-like (S --> g) . y -defined the carrier of L -valued Function-like total quasi_total Element of bool [:((S --> g) . y), the carrier of L:]
(S --> g) . y is non empty set
[:((S --> g) . y), the carrier of L:] is non empty Relation-like set
bool [:((S --> g) . y), the carrier of L:] is non empty set
rng (S, the carrier of L,(S --> g),(S,g, the carrier of L,S9),y) is non empty Element of bool the carrier of L
rng (S, the carrier of L,d,dF,y) is non empty Element of bool the carrier of L
bool (rng (S, the carrier of L,(S --> g),(S,g, the carrier of L,S9),y)) is non empty set
x is Element of the carrier of L
dom (S, the carrier of L,(S --> g),(S,g, the carrier of L,S9),y) is non empty Element of bool ((S --> g) . y)
bool ((S --> g) . y) is non empty set
j is set
(S, the carrier of L,(S --> g),(S,g, the carrier of L,S9),y) . j is set
X is Element of g
((S,g, the carrier of L,S9) . gdF) . X is set
"\/" ((rng (S, the carrier of L,d,dF,y)),L) is Element of the carrier of L
gdF is Relation-like Function-like set
proj1 gdF is set
proj2 gdF is set
proj1 (doms (S,g, the carrier of L,S9)) is set
dom (S,g, the carrier of L,S9) is non empty Element of bool S
bool S is non empty set
y is set
gdF . y is set
(doms (S,g, the carrier of L,S9)) . y is set
x is Element of S
(doms (S,g, the carrier of L,S9)) . x is set
(S --> g) . x is non empty set
(S, the carrier of L,(S --> g),(S,g, the carrier of L,S9),x) is non empty Relation-like (S --> g) . x -defined the carrier of L -valued Function-like total quasi_total Element of bool [:((S --> g) . x), the carrier of L:]
[:((S --> g) . x), the carrier of L:] is non empty Relation-like set
bool [:((S --> g) . x), the carrier of L:] is non empty set
dom (S, the carrier of L,(S --> g),(S,g, the carrier of L,S9),x) is non empty Element of bool ((S --> g) . x)
bool ((S --> g) . x) is non empty set
y is Relation-like Function-like doms (S,g, the carrier of L,S9) -compatible Element of product (doms (S,g, the carrier of L,S9))
(S, the carrier of L,(S --> g),(S,g, the carrier of L,S9),(S, the carrier of L,(S --> g),(S,g, the carrier of L,S9)),y) 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
x is Element of S
(S, the carrier of L,(S --> g),(S,g, the carrier of L,S9),(S, the carrier of L,(S --> g),(S,g, the carrier of L,S9)),y) . x is Element of the carrier of L
(S, the carrier of L,(S --> g),(S,g, the carrier of L,S9),x) is non empty Relation-like (S --> g) . x -defined the carrier of L -valued Function-like total quasi_total Element of bool [:((S --> g) . x), the carrier of L:]
(S --> g) . x is non empty set
[:((S --> g) . x), the carrier of L:] is non empty Relation-like set
bool [:((S --> g) . x), the carrier of L:] is non empty set
y . x is set
(S, the carrier of L,(S --> g),(S,g, the carrier of L,S9),x) . (y . x) is set
dom (S, the carrier of L,(S --> g),(S,g, the carrier of L,S9)) is non empty functional with_common_domain Element of bool (product (doms (S,g, the carrier of L,S9)))
bool (product (doms (S,g, the carrier of L,S9))) is non empty set
j is Element of the carrier of L
//\ ((S, the carrier of L,(S --> g),(S,g, the carrier of L,S9),(S, the carrier of L,(S --> g),(S,g, the carrier of L,S9)),y),L) is Element of the carrier of L
rng (L,(S, the carrier of L,(S --> g),(S,g, the carrier of L,S9))) is non empty Element of bool the carrier of L
"\/" ((rng (L,(S, the carrier of L,(S --> g),(S,g, the carrier of L,S9)))),L) is Element of the carrier of L
"\/" (J,L) is Element of the carrier of L
S is non empty set
g is non empty set
[:S,g:] is non empty Relation-like 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,g:], the carrier of L:] is non empty Relation-like set
bool [:[:S,g:], the carrier of L:] is non empty set
bool the carrier of L is non empty set
J is Element of bool the carrier of L
Fin g is preBoolean set
Funcs (S,(Fin g)) is functional 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 [:S,g:] -defined the carrier of L -valued Function-like total quasi_total Element of bool [:[:S,g:], the carrier of L:]
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being non empty Relation-like non-empty non empty-yielding S -defined Function-like total set st
( b₂ in Funcs (S,(Fin g)) & ex b₃ being non empty Relation-like non-empty non empty-yielding S -defined Function-like total Function-yielding V129() ManySortedFunction of b₂,S --> the carrier of L st
( ( for b₄ being Element of S
for b₅ being set holds
( not b₅ in b₂ . b₄ or (S, the carrier of L,b₂,b₃,b₄) . b₅ = S9 . (b₄,b₅) ) ) & b₁ = //\ ((L,b₃),L) ) ) } is set
(S,g, the carrier of L,S9) is non empty Relation-like non-empty non empty-yielding S -defined Function-like total Function-yielding V129() ManySortedFunction of S --> g,S --> the carrier of L
S --> g is non empty Relation-like non-empty non empty-yielding S -defined {g} -valued Function-like constant total quasi_total Element of bool [:S,{g}:]
{g} is non empty trivial finite V54(1) countable set
[:S,{g}:] is non empty Relation-like set
bool [:S,{g}:] is non empty set
(L,(S,g, the carrier of L,S9)) is non empty Relation-like proj1 (S,g, the carrier of L,S9) -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(proj1 (S,g, the carrier of L,S9)), the carrier of L:]
proj1 (S,g, the carrier of L,S9) is non empty set
[:(proj1 (S,g, the carrier of L,S9)), the carrier of L:] is non empty Relation-like set
bool [:(proj1 (S,g, the carrier of L,S9)), the carrier of L:] is non empty set
//\ ((L,(S,g, the carrier of L,S9)),L) is Element of the carrier of L
"\/" (J,L) is Element of the carrier of L
K is non empty total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V211() up-complete /\-complete RelStr
the carrier of K is non empty set
bool the carrier of K is non empty set
L is non empty trivial finite 1 -element total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V211() connected up-complete /\-complete satisfying_axiom_of_approximation continuous RelStr
the carrier of L is non empty trivial finite V54(1) countable set
S is non empty total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V211() up-complete /\-complete RelStr
g is non empty total reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous RelStr
the carrier of g is non empty set
S9 is non empty set
S9 --> the carrier of g is non empty Relation-like non-empty non empty-yielding S9 -defined { the carrier of g} -valued Function-like constant total quasi_total Element of bool [:S9,{ the carrier of g}:]
{ the carrier of g} is non empty trivial finite V54(1) countable set
[:S9,{ the carrier of g}:] is non empty Relation-like set
bool [:S9,{ the carrier of g}:] is non empty set
J is non empty Relation-like non-empty non empty-yielding S9 -defined Function-like total set
K is non empty Relation-like non-empty non empty-yielding S9 -defined Function-like total Function-yielding V129() ManySortedFunction of J,S9 --> the carrier of g
(g,K) is non empty Relation-like proj1 K -defined the carrier of g -valued Function-like total quasi_total Element of bool [:(proj1 K), the carrier of g:]
proj1 K is non empty set
[:(proj1 K), the carrier of g:] is non empty Relation-like set
bool [:(proj1 K), the carrier of g:] is non empty set
//\ ((g,K),g) is Element of the carrier of g
(S9, the carrier of g,J,K) is non empty Relation-like non-empty non empty-yielding product (doms K) -defined Function-like total Function-yielding V129() ManySortedFunction of (product (doms K)) --> S9,(product (doms K)) --> the carrier of g
doms K is Relation-like non-empty Function-like set
product (doms K) is non empty functional with_common_domain product-like set
(product (doms K)) --> S9 is non empty Relation-like non-empty non empty-yielding product (doms K) -defined {S9} -valued Function-like constant total quasi_total Element of bool [:(product (doms K)),{S9}:]
{S9} is non empty trivial finite V54(1) countable set
[:(product (doms K)),{S9}:] is non empty Relation-like set
bool [:(product (doms K)),{S9}:] is non empty set
(product (doms K)) --> the carrier of g is non empty Relation-like non-empty non empty-yielding product (doms K) -defined { the carrier of g} -valued Function-like constant total quasi_total Element of bool [:(product (doms K)),{ the carrier of g}:]
[:(product (doms K)),{ the carrier of g}:] is non empty Relation-like set
bool [:(product (doms K)),{ the carrier of g}:] is non empty set
(g,(S9, the carrier of g,J,K)) is non empty Relation-like proj1 (S9, the carrier of g,J,K) -defined the carrier of g -valued Function-like total quasi_total Element of bool [:(proj1 (S9, the carrier of g,J,K)), the carrier of g:]
proj1 (S9, the carrier of g,J,K) is non empty set
[:(proj1 (S9, the carrier of g,J,K)), the carrier of g:] is non empty Relation-like set
bool [:(proj1 (S9, the carrier of g,J,K)), the carrier of g:] is non empty set
\\/ ((g,(S9, the carrier of g,J,K)),g) is Element of the carrier of g
F is Element of S9
(S9, the carrier of g,J,K,F) is non empty Relation-like J . F -defined the carrier of g -valued Function-like total quasi_total Element of bool [:(J . F), the carrier of g:]
J . F is non empty set
[:(J . F), the carrier of g:] is non empty Relation-like set
bool [:(J . F), the carrier of g:] is non empty set
rng (S9, the carrier of g,J,K,F) is non empty Element of bool the carrier of g
bool the carrier of g is non empty set
S9 is non empty set
J is non empty Relation-like non-empty non empty-yielding S9 -defined Function-like total set
S9 --> the carrier of L is non empty Relation-like non-empty non empty-yielding S9 -defined { the carrier of L} -valued Function-like constant total quasi_total Element of bool [:S9,{ the carrier of L}:]
{ the carrier of L} is non empty trivial finite V42() V54(1) countable set
[:S9,{ the carrier of L}:] is non empty Relation-like set
bool [:S9,{ the carrier of L}:] is non empty set
K is non empty Relation-like non-empty non empty-yielding S9 -defined Function-like total Function-yielding V129() ManySortedFunction of J,S9 --> the carrier of L
(L,K) is non empty Relation-like proj1 K -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(proj1 K), the carrier of L:]
proj1 K is non empty set
[:(proj1 K), the carrier of L:] is non empty Relation-like set
bool [:(proj1 K), the carrier of L:] is non empty set
//\ ((L,K),L) is Element of the carrier of L
(S9, the carrier of L,J,K) is non empty Relation-like non-empty non empty-yielding product (doms K) -defined Function-like total Function-yielding V129() ManySortedFunction of (product (doms K)) --> S9,(product (doms K)) --> the carrier of L
doms K is Relation-like non-empty Function-like set
product (doms K) is non empty functional with_common_domain product-like set
(product (doms K)) --> S9 is non empty Relation-like non-empty non empty-yielding product (doms K) -defined {S9} -valued Function-like constant total quasi_total Element of bool [:(product (doms K)),{S9}:]
{S9} is non empty trivial finite V54(1) countable set
[:(product (doms K)),{S9}:] is non empty Relation-like set
bool [:(product (doms K)),{S9}:] is non empty set
(product (doms K)) --> the carrier of L is non empty Relation-like non-empty non empty-yielding product (doms K) -defined { the carrier of L} -valued Function-like constant total quasi_total Element of bool [:(product (doms K)),{ the carrier of L}:]
[:(product (doms K)),{ the carrier of L}:] is non empty Relation-like set
bool [:(product (doms K)),{ the carrier of L}:] is non empty set
(L,(S9, the carrier of L,J,K)) is non empty Relation-like proj1 (S9, the carrier of L,J,K) -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(proj1 (S9, the carrier of L,J,K)), the carrier of L:]
proj1 (S9, the carrier of L,J,K) is non empty set
[:(proj1 (S9, the carrier of L,J,K)), the carrier of L:] is non empty Relation-like set
bool [:(proj1 (S9, the carrier of L,J,K)), the carrier of L:] is non empty set
\\/ ((L,(S9, the carrier of L,J,K)),L) is Element of the carrier of L
the set is set
{ the set } is non empty trivial finite V54(1) countable set
[:{ the set },{ the set }:] is non empty Relation-like finite countable set
bool [:{ the set },{ the set }:] is non empty finite V42() countable set
the Relation-like { the set } -defined { the set } -valued total quasi_total finite V43() V46() V50() countable Element of bool [:{ the set },{ the set }:] is Relation-like { the set } -defined { the set } -valued total quasi_total finite V43() V46() V50() countable Element of bool [:{ the set },{ the set }:]
RelStr(# { the set }, the Relation-like { the set } -defined { the set } -valued total quasi_total finite V43() V46() V50() countable Element of bool [:{ the set },{ the set }:] #) is non empty trivial finite 1 -element strict total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V211() connected up-complete /\-complete satisfying_axiom_of_approximation continuous () RelStr
L is non empty total reflexive transitive antisymmetric with_suprema with_infima () RelStr
the carrier of L is non empty 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:]
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
L is non empty total reflexive transitive antisymmetric with_suprema with_infima RelStr
L is non empty transitive antisymmetric with_infima 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 Element of bool the carrier of L
S9 is Element of bool the carrier of L
{ (S "/\" b₁) where b₁ is Element of the carrier of L : b₁ in g } is set
"\/" (S9,L) is Element of the carrier of L
"\/" (g,L) is Element of the carrier of L
S "/\" ("\/" (g,L)) is Element of the carrier of L
J is Element of the carrier of L
K is Element of the carrier of L
S "/\" K 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 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 non empty Element of bool the carrier of L
"\/" (S,L) is Element of the carrier of L
g is Element of the carrier of L
g "/\" ("\/" (S,L)) is Element of the carrier of L
{ (g "/\" b₁) where b₁ is Element of the carrier of L : b₁ in S } is set
"\/" ( { (g "/\" b₁) where b₁ is Element of the carrier of L : b₁ in S } ,L) is Element of the carrier of L
2 is non empty V13() V14() V15() V19() finite V52() countable Element of K286()
{1,2} is non empty finite V42() countable Element of bool K286()
{1} is non empty trivial finite V42() V54(1) countable Element of bool K286()
(1,2) --> ({1},S) is Relation-like K286() -defined Function-like finite countable set
{1} --> g is non empty Relation-like {1} -defined the carrier of L -valued Function-like constant total quasi_total finite countable Element of bool [:{1}, the carrier of L:]
[:{1}, the carrier of L:] is non empty Relation-like set
bool [:{1}, the carrier of L:] is non empty set
id S is non empty Relation-like S -defined S -valued Function-like one-to-one total quasi_total Element of bool [:S,S:]
[:S,S:] is non empty Relation-like set
bool [:S,S:] is non empty set
(1,2) --> (({1} --> g),(id S)) is Relation-like K286() -defined Function-like finite countable set
((1,2) --> (({1} --> g),(id S))) . 1 is set
dom ((1,2) --> ({1},S)) is finite countable Element of bool K286()
((1,2) --> ({1},S)) . 2 is set
dom ((1,2) --> (({1} --> g),(id S))) is finite countable Element of bool K286()
((1,2) --> (({1} --> g),(id S))) . 2 is set
((1,2) --> ({1},S)) . 1 is set
y is non empty Relation-like {1,2} -defined Function-like total set
x is set
y . x is set
gdF is non empty Relation-like {1,2} -defined Function-like total set
x is non empty Relation-like non-empty non empty-yielding {1,2} -defined Function-like total set
{1,2} --> the carrier of L is non empty Relation-like non-empty non empty-yielding {1,2} -defined { the carrier of L} -valued Function-like constant total quasi_total finite countable Element of bool [:{1,2},{ the carrier of L}:]
{ the carrier of L} is non empty trivial finite V54(1) countable set
[:{1,2},{ the carrier of L}:] is non empty Relation-like finite countable set
bool [:{1,2},{ the carrier of L}:] is non empty finite V42() countable set
j is set
gdF . j is set
x . j is set
({1,2} --> the carrier of L) . j is set
[:(x . j),(({1,2} --> the carrier of L) . j):] is Relation-like set
bool [:(x . j),(({1,2} --> the carrier of L) . j):] is non empty set
j is non empty Relation-like non-empty non empty-yielding {1,2} -defined Function-like total Function-yielding V129() ManySortedFunction of x,{1,2} --> the carrier of L
({1,2}, the carrier of L,x,j) is non empty Relation-like non-empty non empty-yielding product (doms j) -defined Function-like total Function-yielding V129() ManySortedFunction of (product (doms j)) --> {1,2},(product (doms j)) --> the carrier of L
doms j is Relation-like non-empty Function-like set
product (doms j) is non empty functional with_common_domain product-like set
(product (doms j)) --> {1,2} is non empty Relation-like non-empty non empty-yielding product (doms j) -defined bool K286() -valued {{1,2}} -valued Function-like constant total quasi_total Element of bool [:(product (doms j)),{{1,2}}:]
{{1,2}} is non empty trivial finite V42() V54(1) countable set
[:(product (doms j)),{{1,2}}:] is non empty Relation-like set
bool [:(product (doms j)),{{1,2}}:] is non empty set
(product (doms j)) --> the carrier of L is non empty Relation-like non-empty non empty-yielding product (doms j) -defined { the carrier of L} -valued Function-like constant total quasi_total Element of bool [:(product (doms j)),{ the carrier of L}:]
[:(product (doms j)),{ the carrier of L}:] is non empty Relation-like set
bool [:(product (doms j)),{ the carrier of L}:] is non empty set
(L,({1,2}, the carrier of L,x,j)) is non empty Relation-like proj1 ({1,2}, the carrier of L,x,j) -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(proj1 ({1,2}, the carrier of L,x,j)), the carrier of L:]
proj1 ({1,2}, the carrier of L,x,j) is non empty set
[:(proj1 ({1,2}, the carrier of L,x,j)), the carrier of L:] is non empty Relation-like set
bool [:(proj1 ({1,2}, the carrier of L,x,j)), the carrier of L:] is non empty set
rng (L,({1,2}, the carrier of L,x,j)) is non empty Element of bool the carrier of L
X is Element of the carrier of L
dom ({1,2}, the carrier of L,x,j) is non empty functional with_common_domain Element of bool (product (doms j))
bool (product (doms j)) is non empty set
f9 is set
({1,2}, the carrier of L,x,j) . f9 is Relation-like Function-like set
//\ ((({1,2}, the carrier of L,x,j) . f9),L) is Element of the carrier of L
z is Relation-like Function-like set
dF is finite countable Element of {1,2}
z . dF is set
x . dF is non empty set
z . 2 is set
d is finite countable Element of {1,2}
z . d is set
x . d is non empty set
j is Element of S
{g,j} is non empty finite countable Element of bool the carrier of L
({1,2}, the carrier of L,x,j) . z is Relation-like Function-like set
proj2 (({1,2}, the carrier of L,x,j) . z) is set
c₁₈ is set
({1,2}, the carrier of L,x,j,d) is non empty Relation-like x . d -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(x . d), the carrier of L:]
[:(x . d), the carrier of L:] is non empty Relation-like set
bool [:(x . d), the carrier of L:] is non empty set
({1,2}, the carrier of L,x,j,d) . (z . d) is set
({1,2}, the carrier of L,x,j,dF) is non empty Relation-like x . dF -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(x . dF), the carrier of L:]
[:(x . dF), the carrier of L:] is non empty Relation-like set
bool [:(x . dF), the carrier of L:] is non empty set
({1,2}, the carrier of L,x,j,dF) . (z . dF) is set
g "/\" j is Element of the carrier of L
{g,(z . 2)} is non empty finite countable set
"/\" ((proj2 (({1,2}, the carrier of L,x,j) . z)),L) is Element of the carrier of L
"/\" ({g,j},L) is Element of the carrier of L
"\/" ((rng (L,({1,2}, the carrier of L,x,j))),L) is Element of the carrier of L
\\/ ((L,({1,2}, the carrier of L,x,j)),L) is Element of the carrier of L
g "/\" is non empty Relation-like the carrier of L -defined the carrier of L -valued Function-like total quasi_total Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
(g "/\") .: S is Element of bool the carrier of L
X is Element of bool the carrier of L
"\/" (X,L) is Element of the carrier of L
(L,j) is non empty Relation-like proj1 j -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(proj1 j), the carrier of L:]
proj1 j is non empty set
[:(proj1 j), the carrier of L:] is non empty Relation-like set
bool [:(proj1 j), the carrier of L:] is non empty set
rng (L,j) is non empty Element of bool the carrier of L
f9 is Element of the carrier of L
z is finite countable Element of {1,2}
({1,2}, the carrier of L,x,j,z) is non empty Relation-like x . z -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(x . z), the carrier of L:]
x . z is non empty set
[:(x . z), the carrier of L:] is non empty Relation-like set
bool [:(x . z), the carrier of L:] is non empty set
\\/ (({1,2}, the carrier of L,x,j,z),L) is Element of the carrier of L
rng ({1,2}, the carrier of L,x,j,z) is non empty Element of bool 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
rng ({1,2}, the carrier of L,x,j,z) is non empty Element of bool the carrier of L
"/\" ((rng (L,j)),L) is Element of the carrier of L
//\ ((L,j),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 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 bool the carrier of L
"\/" (S,L) is Element of the carrier of L
g is Element of the carrier of L
g "/\" ("\/" (S,L)) is Element of the carrier of L
{ (g "/\" b₁) where b₁ is Element of the carrier of L : b₁ in S } is set
"\/" ( { (g "/\" b₁) where b₁ is Element of the carrier of L : b₁ in S } ,L) is Element of the carrier of L
the Element of { (g "/\" b₁) where b₁ is Element of the carrier of L : b₁ in S } is Element of { (g "/\" b₁) where b₁ is Element of the carrier of L : b₁ in S }
K is Element of the carrier of L
g "/\" K is Element of the carrier of L
Bottom L is Element of the carrier of L
L is non empty total reflexive transitive antisymmetric with_suprema with_infima RelStr
S 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
the carrier of S is non empty set
bool the carrier of S is non empty set
S9 is Element of the carrier of S
g is Element of bool the carrier of S
"\/" (g,S) is Element of the carrier of S
S9 "/\" ("\/" (g,S)) is Element of the carrier of S
{ (S9 "/\" b₁) where b₁ is Element of the carrier of S : b₁ in g } is set
"\/" ( { (S9 "/\" b₁) where b₁ is Element of the carrier of S : b₁ in g } ,S) is Element of the carrier of S
g is Element of the carrier of S
g "/\" is non empty Relation-like the carrier of S -defined the carrier of S -valued Function-like total quasi_total Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty Relation-like set
bool [: the carrier of S, the carrier of S:] 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 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
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
K is Element of the carrier of L
F 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 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
[:S, the carrier of L:] is non empty Relation-like set
bool [:S, the carrier of L:] is non empty set
dF is Relation-like Function-like set
(S, the carrier of L,g,S9) . dF is Relation-like Function-like set
y is set
(S, the carrier of L,g,S9) . y is Relation-like Function-like set
//\ (((S, the carrier of L,g,S9) . y),L) is Element of the carrier of L
x is Relation-like Function-like set
(S, the carrier of L,g,S9) . x is Relation-like Function-like set
proj2 ((S, the carrier of L,g,S9) . x) is set
j 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:]
gdF 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:]
X is Element of S
g . X is non empty set
j . X is Element of the carrier of L
(S, the carrier of L,g,S9,X) is non empty Relation-like g . X -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(g . X), the carrier of L:]
[:(g . X), the carrier of L:] is non empty Relation-like set
bool [:(g . X), the carrier of L:] is non empty set
gdF . X is Element of the carrier of L
dom S9 is non empty Element of bool S
bool S is non empty set
x . X is set
dom (S, the carrier of L,g,S9,X) is non empty Element of bool (g . X)
bool (g . X) is non empty set
(S, the carrier of L,g,S9,X) . (x . X) is set
rng (S, the carrier of L,g,S9,X) is non empty Element of bool the carrier of L
dF . X is set
(S, the carrier of L,g,S9,X) . (dF . X) is set
f9 is Element of the carrier of L
z is set
(S, the carrier of L,g,S9,X) . z is set
j is Element of g . X
(S, the carrier of L,g,S9,X) . j is Element of the carrier of L
proj2 g is non empty V22() set
union (proj2 g) is set
X is set
g . X is set
S9 . X is Relation-like Function-like set
j . X is set
gdF . X is set
f9 is Element of S
g . f9 is non empty set
j . f9 is Element of the carrier of L
(S, the carrier of L,g,S9,f9) is non empty Relation-like g . f9 -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(g . f9), the carrier of L:]
[:(g . f9), the carrier of L:] is non empty Relation-like set
bool [:(g . f9), the carrier of L:] is non empty set
gdF . f9 is Element of the carrier of L
z is Element of g . f9
(S, the carrier of L,g,S9,f9) . z is Element of the carrier of L
(S9 . X) . z is set
dom g is non empty Element of bool S
bool S is non empty set
j is Element of the carrier of L
c₁₈ is Element of the carrier of L
j is Element of the carrier of L
X is Relation-like Function-like set
proj1 X is set
proj2 X is set
f9 is set
proj1 (doms S9) is set
dom S9 is non empty Element of bool S
bool S is non empty set
(doms S9) . f9 is set
z is Element of S
g . z is non empty set
(S, the carrier of L,g,S9,z) is non empty Relation-like g . z -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(g . z), the carrier of L:]
[:(g . z), the carrier of L:] is non empty Relation-like set
bool [:(g . z), the carrier of L:] is non empty set
dom (S, the carrier of L,g,S9,z) is non empty Element of bool (g . z)
bool (g . z) is non empty set
X . f9 is set
(S, the carrier of L,g,S9) . X is Relation-like Function-like set
f9 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:]
//\ (f9,L) is Element of the carrier of L
z is Element of the carrier of L
"/\" ((proj2 ((S, the carrier of L,g,S9) . x)),L) is Element of the carrier of L
j is Element of S
dom j is non empty Element of bool S
j . j is Element of the carrier of L
rng j is non empty Element of bool the carrier of L
(S, the carrier of L,g,S9,j) is non empty Relation-like g . j -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(g . j), the carrier of L:]
g . j is non empty set
[:(g . j), the carrier of L:] is non empty Relation-like set
bool [:(g . j), the carrier of L:] is non empty set
X . j is set
(S, the carrier of L,g,S9,j) . (X . j) is set
((S, the carrier of L,g,S9) . X) . j is set
f9 . j is Element of the carrier of L
proj2 ((S, the carrier of L,g,S9) . dF) is set
"/\" ((proj2 ((S, the carrier of L,g,S9) . dF)),L) is Element of the carrier of L
j is Element of S
dom gdF is non empty Element of bool S
gdF . j is Element of the carrier of L
rng gdF is non empty Element of bool the carrier of L
(S, the carrier of L,g,S9,j) is non empty Relation-like g . j -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(g . j), the carrier of L:]
g . j is non empty set
[:(g . j), the carrier of L:] is non empty Relation-like set
bool [:(g . j), the carrier of L:] is non empty set
X . j is set
(S, the carrier of L,g,S9,j) . (X . j) is set
((S, the carrier of L,g,S9) . X) . j is set
f9 . j 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
S is non empty total reflexive transitive antisymmetric with_infima full meet-inheriting infs-inheriting filtered-infs-inheriting directed-sups-inheriting SubRelStr of L
the carrier of S is non empty set
S9 is non empty set
S9 --> the carrier of S is non empty Relation-like non-empty non empty-yielding S9 -defined { the carrier of S} -valued Function-like constant total quasi_total Element of bool [:S9,{ the carrier of S}:]
{ the carrier of S} is non empty trivial finite V54(1) countable set
[:S9,{ the carrier of S}:] is non empty Relation-like set
bool [:S9,{ the carrier of S}:] is non empty set
J is non empty Relation-like non-empty non empty-yielding S9 -defined Function-like total set
K is non empty Relation-like non-empty non empty-yielding S9 -defined Function-like total Function-yielding V129() ManySortedFunction of J,S9 --> the carrier of S
(S,K) is non empty Relation-like proj1 K -defined the carrier of S -valued Function-like total quasi_total Element of bool [:(proj1 K), the carrier of S:]
proj1 K is non empty set
[:(proj1 K), the carrier of S:] is non empty Relation-like set
bool [:(proj1 K), the carrier of S:] is non empty set
//\ ((S,K),S) is Element of the carrier of S
(S9, the carrier of S,J,K) is non empty Relation-like non-empty non empty-yielding product (doms K) -defined Function-like total Function-yielding V129() ManySortedFunction of (product (doms K)) --> S9,(product (doms K)) --> the carrier of S
doms K is Relation-like non-empty Function-like set
product (doms K) is non empty functional with_common_domain product-like set
(product (doms K)) --> S9 is non empty Relation-like non-empty non empty-yielding product (doms K) -defined {S9} -valued Function-like constant total quasi_total Element of bool [:(product (doms K)),{S9}:]
{S9} is non empty trivial finite V54(1) countable set
[:(product (doms K)),{S9}:] is non empty Relation-like set
bool [:(product (doms K)),{S9}:] is non empty set
(product (doms K)) --> the carrier of S is non empty Relation-like non-empty non empty-yielding product (doms K) -defined { the carrier of S} -valued Function-like constant total quasi_total Element of bool [:(product (doms K)),{ the carrier of S}:]
[:(product (doms K)),{ the carrier of S}:] is non empty Relation-like set
bool [:(product (doms K)),{ the carrier of S}:] is non empty set
(S,(S9, the carrier of S,J,K)) is non empty Relation-like proj1 (S9, the carrier of S,J,K) -defined the carrier of S -valued Function-like total quasi_total Element of bool [:(proj1 (S9, the carrier of S,J,K)), the carrier of S:]
proj1 (S9, the carrier of S,J,K) is non empty set
[:(proj1 (S9, the carrier of S,J,K)), the carrier of S:] is non empty Relation-like set
bool [:(proj1 (S9, the carrier of S,J,K)), the carrier of S:] is non empty set
\\/ ((S,(S9, the carrier of S,J,K)),S) is Element of the carrier of S
F is set
d is Element of S9
(S9, the carrier of S,J,K,d) is non empty Relation-like J . d -defined the carrier of S -valued Function-like total quasi_total Element of bool [:(J . d), the carrier of S:]
J . d is non empty set
[:(J . d), the carrier of S:] is non empty Relation-like set
bool [:(J . d), the carrier of S:] is non empty set
the carrier of L is non empty set
S9 --> the carrier of L is non empty Relation-like non-empty non empty-yielding S9 -defined { the carrier of L} -valued Function-like constant total quasi_total Element of bool [:S9,{ the carrier of L}:]
{ the carrier of L} is non empty trivial finite V54(1) countable set
[:S9,{ the carrier of L}:] is non empty Relation-like set
bool [:S9,{ the carrier of L}:] is non empty set
(S9 --> the carrier of L) . F is set
K . F is Relation-like Function-like set
J . F is set
[:(J . F),((S9 --> the carrier of L) . F):] is Relation-like set
bool [:(J . F),((S9 --> the carrier of L) . F):] is non empty set
rng (S,K) is non empty Element of bool the carrier of S
bool the carrier of S is non empty set
"/\" ((rng (S,K)),L) is Element of the carrier of L
d is set
F is non empty Relation-like non-empty non empty-yielding S9 -defined Function-like total Function-yielding V129() ManySortedFunction of J,S9 --> the carrier of L
(L,F) is non empty Relation-like proj1 F -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(proj1 F), the carrier of L:]
proj1 F is non empty set
[:(proj1 F), the carrier of L:] is non empty Relation-like set
bool [:(proj1 F), the carrier of L:] is non empty set
rng (L,F) is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
dF is Element of S9
(S9, the carrier of L,J,F,dF) is non empty Relation-like J . dF -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(J . dF), the carrier of L:]
J . dF is non empty set
[:(J . dF), the carrier of L:] is non empty Relation-like set
bool [:(J . dF), the carrier of L:] is non empty set
\\/ ((S9, the carrier of L,J,F,dF),L) is Element of the carrier of L
g is non empty total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V211() up-complete /\-complete RelStr
(S9, the carrier of S,J,K,dF) is non empty Relation-like J . dF -defined the carrier of S -valued Function-like total quasi_total Element of bool [:(J . dF), the carrier of S:]
[:(J . dF), the carrier of S:] is non empty Relation-like set
bool [:(J . dF), the carrier of S:] is non empty set
rng (S9, the carrier of S,J,K,dF) is non empty Element of bool the carrier of S
rng (S9, the carrier of L,J,F,dF) is non empty Element of bool the carrier of L
"\/" ((rng (S9, the carrier of L,J,F,dF)),L) is Element of the carrier of L
"\/" ((rng (S9, the carrier of S,J,K,dF)),S) is Element of the carrier of S
\\/ ((S9, the carrier of S,J,K,dF),S) is Element of the carrier of S
d is set
dF is Element of S9
(S9, the carrier of S,J,K,dF) is non empty Relation-like J . dF -defined the carrier of S -valued Function-like total quasi_total Element of bool [:(J . dF), the carrier of S:]
J . dF is non empty set
[:(J . dF), the carrier of S:] is non empty Relation-like set
bool [:(J . dF), the carrier of S:] is non empty set
\\/ ((S9, the carrier of S,J,K,dF),S) is Element of the carrier of S
rng (S9, the carrier of S,J,K,dF) is non empty Element of bool the carrier of S
"\/" ((rng (S9, the carrier of S,J,K,dF)),S) is Element of the carrier of S
(S9, the carrier of L,J,F,dF) is non empty Relation-like J . dF -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(J . dF), the carrier of L:]
[:(J . dF), the carrier of L:] is non empty Relation-like set
bool [:(J . dF), the carrier of L:] is non empty set
rng (S9, the carrier of L,J,F,dF) is non empty Element of bool the carrier of L
"\/" ((rng (S9, the carrier of L,J,F,dF)),L) is Element of the carrier of L
\\/ ((S9, the carrier of L,J,F,dF),L) is Element of the carrier of L
"/\" ((rng (L,F)),L) is Element of the carrier of L
"/\" ((rng (S,K)),S) is Element of the carrier of S
//\ ((L,F),L) is Element of the carrier of L
d is set
rng (S,(S9, the carrier of S,J,K)) is non empty Element of bool the carrier of S
dom (S9, the carrier of S,J,K) is non empty functional with_common_domain Element of bool (product (doms K))
bool (product (doms K)) is non empty set
dF is set
(S9, the carrier of S,J,K) . dF is Relation-like Function-like set
//\ (((S9, the carrier of S,J,K) . dF),S) is Element of the carrier of S
gdF is Relation-like Function-like set
(S9, the carrier of S,J,K) . gdF is Relation-like Function-like set
[:S9, the carrier of S:] is non empty Relation-like set
bool [:S9, the carrier of S:] is non empty set
proj2 ((S9, the carrier of S,J,K) . gdF) is set
"/\" ((proj2 ((S9, the carrier of S,J,K) . gdF)),L) is Element of the carrier of L
"/\" ((proj2 ((S9, the carrier of S,J,K) . gdF)),S) is Element of the carrier of S
(S9, the carrier of L,J,F) is non empty Relation-like non-empty non empty-yielding product (doms F) -defined Function-like total Function-yielding V129() ManySortedFunction of (product (doms F)) --> S9,(product (doms F)) --> the carrier of L
doms F is Relation-like non-empty Function-like set
product (doms F) is non empty functional with_common_domain product-like set
(product (doms F)) --> S9 is non empty Relation-like non-empty non empty-yielding product (doms F) -defined {S9} -valued Function-like constant total quasi_total Element of bool [:(product (doms F)),{S9}:]
[:(product (doms F)),{S9}:] is non empty Relation-like set
bool [:(product (doms F)),{S9}:] is non empty set
(product (doms F)) --> the carrier of L is non empty Relation-like non-empty non empty-yielding product (doms F) -defined { the carrier of L} -valued Function-like constant total quasi_total Element of bool [:(product (doms F)),{ the carrier of L}:]
[:(product (doms F)),{ the carrier of L}:] is non empty Relation-like set
bool [:(product (doms F)),{ the carrier of L}:] is non empty set
(S9, the carrier of L,J,F) . gdF is Relation-like Function-like set
proj2 ((S9, the carrier of L,J,F) . gdF) is set
"/\" ((proj2 ((S9, the carrier of L,J,F) . gdF)),L) is Element of the carrier of L
//\ (((S9, the carrier of L,J,F) . gdF),L) is Element of the carrier of L
(L,(S9, the carrier of L,J,F)) is non empty Relation-like proj1 (S9, the carrier of L,J,F) -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(proj1 (S9, the carrier of L,J,F)), the carrier of L:]
proj1 (S9, the carrier of L,J,F) is non empty set
[:(proj1 (S9, the carrier of L,J,F)), the carrier of L:] is non empty Relation-like set
bool [:(proj1 (S9, the carrier of L,J,F)), the carrier of L:] is non empty set
rng (L,(S9, the carrier of L,J,F)) is non empty Element of bool the carrier of L
d is set
dom (S9, the carrier of L,J,F) is non empty functional with_common_domain Element of bool (product (doms F))
bool (product (doms F)) is non empty set
dF is set
(S9, the carrier of L,J,F) . dF is Relation-like Function-like set
//\ (((S9, the carrier of L,J,F) . dF),L) is Element of the carrier of L
gdF is Relation-like Function-like doms F -compatible Element of product (doms F)
(S9, the carrier of S,J,K) . gdF is Relation-like Function-like set
proj2 ((S9, the carrier of S,J,K) . gdF) is set
"/\" ((proj2 ((S9, the carrier of S,J,K) . gdF)),L) is Element of the carrier of L
(S9, the carrier of L,J,F,(S9, the carrier of L,J,F),gdF) is non empty Relation-like S9 -defined the carrier of L -valued Function-like total quasi_total Element of bool [:S9, the carrier of L:]
[:S9, the carrier of L:] is non empty Relation-like set
bool [:S9, the carrier of L:] is non empty set
rng (S9, the carrier of L,J,F,(S9, the carrier of L,J,F),gdF) is non empty Element of bool the carrier of L
"/\" ((rng (S9, the carrier of L,J,F,(S9, the carrier of L,J,F),gdF)),L) is Element of the carrier of L
"/\" ((proj2 ((S9, the carrier of S,J,K) . gdF)),S) is Element of the carrier of S
//\ (((S9, the carrier of S,J,K) . gdF),S) is Element of the carrier of S
d is Element of S9
(S9, the carrier of L,J,F,d) is non empty Relation-like J . d -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(J . d), the carrier of L:]
J . d is non empty set
[:(J . d), the carrier of L:] is non empty Relation-like set
bool [:(J . d), the carrier of L:] is non empty set
rng (S9, the carrier of L,J,F,d) is non empty Element of bool the carrier of L
(S9, the carrier of S,J,K,d) is non empty Relation-like J . d -defined the carrier of S -valued Function-like total quasi_total Element of bool [:(J . d), the carrier of S:]
[:(J . d), the carrier of S:] is non empty Relation-like set
bool [:(J . d), the carrier of S:] is non empty set
rng (S9, the carrier of S,J,K,d) is non empty Element of bool the carrier of S
\\/ ((L,(S9, the carrier of L,J,F)),L) is Element of the carrier of L
"\/" ((rng (L,(S9, the carrier of L,J,F))),L) is Element of the carrier of L
"\/" ((rng (S,(S9, the carrier of S,J,K))),S) is Element of the carrier of S
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 total reflexive transitive antisymmetric RelStr
the carrier of S is non empty set
[: the carrier of L, the carrier of S:] is non empty Relation-like set
bool [: the carrier of L, the carrier of S:] is non empty set
g is non empty Relation-like the carrier of L -defined the carrier of S -valued Function-like total quasi_total Element of bool [: the carrier of L, the carrier of S:]
bool the carrier of S is non empty set
S9 is Element of bool the carrier of S
g " S9 is Element of bool the carrier of L
bool the carrier of L is non empty set
rng g is non empty Element of bool the carrier of S
g .: (g " S9) is Element of bool the carrier of S
L is set
S is set
L --> S is Relation-like L -defined Function-like constant total set
g is Relation-like L -defined Function-like set
L is set
S is set
[:L,S:] is Relation-like set
bool [:L,S:] is non empty set
g is set
S9 is Relation-like L -defined S -valued Function-like quasi_total Element of bool [:L,S:]
g --> S9 is Relation-like g -defined bool [:L,S:] -valued Function-like constant total Function-yielding V129() set
g --> L is Relation-like g -defined {L} -valued Function-like constant total quasi_total Element of bool [:g,{L}:]
{L} is non empty trivial finite V54(1) countable set
[:g,{L}:] is Relation-like set
bool [:g,{L}:] is non empty set
g --> S is Relation-like g -defined {S} -valued Function-like constant total quasi_total Element of bool [:g,{S}:]
{S} is non empty trivial finite V54(1) countable set
[:g,{S}:] is Relation-like set
bool [:g,{S}:] is non empty set
F is set
(g --> S9) . F is Relation-like Function-like set
(g --> L) . F is set
(g --> S) . F is set
[:((g --> L) . F),((g --> S) . F):] is Relation-like set
bool [:((g --> L) . F),((g --> S) . F):] is non empty set
L is non empty set
S is set
g is set
[:S,g:] is Relation-like set
bool [:S,g:] is non empty set
[:g,S:] is Relation-like set
bool [:g,S:] is non empty set
id S is Relation-like S -defined S -valued Function-like one-to-one total quasi_total Element of bool [:S,S:]
[:S,S:] is Relation-like set
bool [:S,S:] is non empty set
L --> S is non empty 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 non empty Relation-like set
bool [:L,{S}:] is non empty set
id (L --> S) is non empty Relation-like L -defined Function-like total Function-yielding V129() ManySortedFunction of L --> S,L --> S
S9 is Relation-like S -defined g -valued Function-like quasi_total Element of bool [:S,g:]
(S,g,L,S9) is non empty Relation-like L -defined bool [:S,g:] -valued Function-like constant total Function-yielding V129() ManySortedFunction of L --> S,L --> g
L --> g is non empty Relation-like 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 non empty Relation-like set
bool [:L,{g}:] is non empty set
J is Relation-like g -defined S -valued Function-like quasi_total Element of bool [:g,S:]
J * S9 is Relation-like S -defined S -valued Function-like Element of bool [:S,S:]
(g,S,L,J) is non empty Relation-like L -defined bool [:g,S:] -valued Function-like constant total Function-yielding V129() ManySortedFunction of L --> g,L --> S
(g,S,L,J) ** (S,g,L,S9) is Relation-like Function-like Function-yielding V129() set
proj1 ((g,S,L,J) ** (S,g,L,S9)) is set
F is non empty Relation-like L -defined Function-like total set
d is set
F . d is set
(L --> S) . d is set
id ((L --> S) . d) is Relation-like (L --> S) . d -defined (L --> S) . d -valued Function-like one-to-one total quasi_total Element of bool [:((L --> S) . d),((L --> S) . d):]
[:((L --> S) . d),((L --> S) . d):] is Relation-like set
bool [:((L --> S) . d),((L --> S) . d):] is non empty set
(g,S,L,J) . d is Relation-like Function-like set
(S,g,L,S9) . d is Relation-like Function-like set
d is set
F . d is set
(L --> S) . d is set
id ((L --> S) . d) is Relation-like (L --> S) . d -defined (L --> S) . d -valued Function-like one-to-one total quasi_total Element of bool [:((L --> S) . d),((L --> S) . d):]
[:((L --> S) . d),((L --> S) . d):] is Relation-like set
bool [:((L --> S) . d),((L --> S) . d):] is non empty set
d is non empty Relation-like L -defined Function-like total Function-yielding V129() ManySortedFunction of L --> S,L --> S
dF is set
d . dF is Relation-like Function-like set
(L --> S) . dF is set
id ((L --> S) . dF) is Relation-like (L --> S) . dF -defined (L --> S) . dF -valued Function-like one-to-one total quasi_total Element of bool [:((L --> S) . dF),((L --> S) . dF):]
[:((L --> S) . dF),((L --> S) . dF):] is Relation-like set
bool [:((L --> S) . dF),((L --> S) . dF):] is non empty set
L is non empty 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
g is set
[:S,g:] is Relation-like set
bool [:S,g:] is non empty set
L --> g is non empty Relation-like 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 non empty Relation-like set
bool [:L,{g}:] is non empty set
S9 is non empty Relation-like L -defined Function-like total set
J is non empty Relation-like L -defined Function-like total Function-yielding V129() ManySortedFunction of S9,L --> S
K is Relation-like S -defined g -valued Function-like quasi_total Element of bool [:S,g:]
(S,g,L,K) is non empty Relation-like L -defined bool [:S,g:] -valued Function-like constant total Function-yielding V129() ManySortedFunction of L --> S,L --> g
(S,g,L,K) ** J is Relation-like Function-like Function-yielding V129() set
proj1 ((S,g,L,K) ** J) is set
d is non empty Relation-like L -defined Function-like total set
dF is set
d . dF is set
S9 . dF is set
(L --> g) . dF is set
[:(S9 . dF),((L --> g) . dF):] is Relation-like set
bool [:(S9 . dF),((L --> g) . dF):] is non empty set
[:(S9 . dF),S:] is Relation-like set
bool [:(S9 . dF),S:] is non empty set
gdF is Element of L
(L,S,S9,J,gdF) is Relation-like S9 . gdF -defined S -valued Function-like total quasi_total Element of bool [:(S9 . gdF),S:]
S9 . gdF is set
[:(S9 . gdF),S:] is Relation-like set
bool [:(S9 . gdF),S:] is non empty set
J . dF is Relation-like Function-like set
(S,g,L,K) . dF is Relation-like Function-like set
(J . dF) * ((S,g,L,K) . dF) is Relation-like Function-like set
y is Relation-like S9 . dF -defined S -valued Function-like total quasi_total Element of bool [:(S9 . dF),S:]
K * y is Relation-like S9 . dF -defined g -valued Function-like quasi_total Element of bool [:(S9 . dF),g:]
[:(S9 . dF),g:] is Relation-like set
bool [:(S9 . dF),g:] is non empty set
L --> K is non empty Relation-like L -defined bool [:S,g:] -valued Function-like constant total quasi_total Function-yielding V129() Element of bool [:L,(bool [:S,g:]):]
[:L,(bool [:S,g:]):] is non empty Relation-like set
bool [:L,(bool [:S,g:]):] is non empty set
(L --> K) ** J is Relation-like Function-like Function-yielding V129() set
L is non empty 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
g is non empty set
[:S,g:] is non empty Relation-like set
bool [:S,g:] is non empty set
L --> g is non empty Relation-like non-empty non empty-yielding 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 non empty Relation-like set
bool [:L,{g}:] is non empty set
S9 is non empty Relation-like L -defined Function-like total set
J is non empty Relation-like L -defined Function-like total Function-yielding V129() ManySortedFunction of S9,L --> S
doms J is Relation-like Function-like set
K is non empty Relation-like S -defined g -valued Function-like total quasi_total Element of bool [:S,g:]
(S,g,L,K) is non empty Relation-like non-empty non empty-yielding L -defined bool [:S,g:] -valued Function-like constant total Function-yielding V129() ManySortedFunction of L --> S,L --> g
(S,g,L,K) ** J is non empty Relation-like L -defined Function-like total Function-yielding V129() ManySortedFunction of S9,L --> g
doms ((S,g,L,K) ** J) is Relation-like Function-like set
proj1 (doms ((S,g,L,K) ** J)) is set
dom ((S,g,L,K) ** J) is non empty Element of bool L
bool L is non empty set
F is set
d is Element of L
dom J is non empty Element of bool L
(L,S,S9,J,d) is Relation-like S9 . d -defined S -valued Function-like total quasi_total Element of bool [:(S9 . d),S:]
S9 . d is set
[:(S9 . d),S:] is Relation-like set
bool [:(S9 . d),S:] is non empty set
rng (L,S,S9,J,d) is Element of bool S
bool S is non empty set
dom K is non empty Element of bool S
(doms ((S,g,L,K) ** J)) . d is set
(L,g,S9,((S,g,L,K) ** J),d) is Relation-like S9 . d -defined g -valued Function-like total quasi_total Element of bool [:(S9 . d),g:]
[:(S9 . d),g:] is Relation-like set
bool [:(S9 . d),g:] is non empty set
dom (L,g,S9,((S,g,L,K) ** J),d) is Element of bool (S9 . d)
bool (S9 . d) is non empty set
(L --> S) . d is non empty set
(L,g,(L --> S),(S,g,L,K),d) is non empty Relation-like (L --> S) . d -defined g -valued Function-like total quasi_total Element of bool [:((L --> S) . d),g:]
[:((L --> S) . d),g:] is non empty Relation-like set
bool [:((L --> S) . d),g:] is non empty set
(L,g,(L --> S),(S,g,L,K),d) * (L,S,S9,J,d) is Relation-like S9 . d -defined g -valued Function-like Element of bool [:(S9 . d),g:]
dom ((L,g,(L --> S),(S,g,L,K),d) * (L,S,S9,J,d)) is Element of bool (S9 . d)
K * (L,S,S9,J,d) is Relation-like S9 . d -defined g -valued Function-like total quasi_total Element of bool [:(S9 . d),g:]
dom (K * (L,S,S9,J,d)) is Element of bool (S9 . d)
dom (L,S,S9,J,d) is Element of bool (S9 . d)
(doms J) . d is set
(doms ((S,g,L,K) ** J)) . F is set
(doms J) . F is set
proj1 (doms 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 non empty total reflexive transitive antisymmetric RelStr
the carrier of S is non empty set
[: the carrier of L, the carrier of S:] is non empty Relation-like set
bool [: the carrier of L, the carrier of S:] is non empty set
g is non empty Relation-like the carrier of L -defined the carrier of S -valued Function-like total quasi_total Element of bool [: the carrier of L, the carrier of S:]
S9 is non empty total reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V211() up-complete /\-complete RelStr
the carrier of S9 is non empty set
J is non empty set
J --> the carrier of S9 is non empty Relation-like non-empty non empty-yielding J -defined { the carrier of S9} -valued Function-like constant total quasi_total Element of bool [:J,{ the carrier of S9}:]
{ the carrier of S9} is non empty trivial finite V54(1) countable set
[:J,{ the carrier of S9}:] is non empty Relation-like set
bool [:J,{ the carrier of S9}:] is non empty set
K is non empty Relation-like non-empty non empty-yielding J -defined Function-like total set
F is non empty Relation-like non-empty non empty-yielding J -defined Function-like total Function-yielding V129() ManySortedFunction of K,J --> the carrier of S9
(S9,F) is non empty Relation-like proj1 F -defined the carrier of S9 -valued Function-like total quasi_total Element of bool [:(proj1 F), the carrier of S9:]
proj1 F is non empty set
[:(proj1 F), the carrier of S9:] is non empty Relation-like set
bool [:(proj1 F), the carrier of S9:] is non empty set
//\ ((S9,F),S9) is Element of the carrier of S9
(J, the carrier of S9,K,F) is non empty Relation-like non-empty non empty-yielding product (doms F) -defined Function-like total Function-yielding V129() ManySortedFunction of (product (doms F)) --> J,(product (doms F)) --> the carrier of S9
doms F is Relation-like non-empty Function-like set
product (doms F) is non empty functional with_common_domain product-like set
(product (doms F)) --> J is non empty Relation-like non-empty non empty-yielding product (doms F) -defined {J} -valued Function-like constant total quasi_total Element of bool [:(product (doms F)),{J}:]
{J} is non empty trivial finite V54(1) countable set
[:(product (doms F)),{J}:] is non empty Relation-like set
bool [:(product (doms F)),{J}:] is non empty set
(product (doms F)) --> the carrier of S9 is non empty Relation-like non-empty non empty-yielding product (doms F) -defined { the carrier of S9} -valued Function-like constant total quasi_total Element of bool [:(product (doms F)),{ the carrier of S9}:]
[:(product (doms F)),{ the carrier of S9}:] is non empty Relation-like set
bool [:(product (doms F)),{ the carrier of S9}:] is non empty set
(S9,(J, the carrier of S9,K,F)) is non empty Relation-like proj1 (J, the carrier of S9,K,F) -defined the carrier of S9 -valued Function-like total quasi_total Element of bool [:(proj1 (J, the carrier of S9,K,F)), the carrier of S9:]
proj1 (J, the carrier of S9,K,F) is non empty set
[:(proj1 (J, the carrier of S9,K,F)), the carrier of S9:] is non empty Relation-like set
bool [:(proj1 (J, the carrier of S9,K,F)), the carrier of S9:] is non empty set
\\/ ((S9,(J, the carrier of S9,K,F)),S9) is Element of the carrier of S9
[: the carrier of S, the carrier of L:] is non empty Relation-like set
bool [: the carrier of S, the carrier of L:] is non empty set
d is non empty Relation-like the carrier of S -defined the carrier of L -valued Function-like total quasi_total Element of bool [: the carrier of S, the carrier of L:]
[g,d] is V31() Connection of L,S
{g,d} is non empty functional finite countable set
{g} is non empty trivial functional finite V54(1) with_common_domain countable set
{{g,d},{g}} is non empty finite V42() countable set
J --> the carrier of L is non empty Relation-like non-empty non empty-yielding J -defined { the carrier of L} -valued Function-like constant total quasi_total Element of bool [:J,{ the carrier of L}:]
{ the carrier of L} is non empty trivial finite V54(1) countable set
[:J,{ the carrier of L}:] is non empty Relation-like set
bool [:J,{ the carrier of L}:] is non empty set
( the carrier of S, the carrier of L,J,d) is non empty Relation-like non-empty non empty-yielding J -defined bool [: the carrier of S, the carrier of L:] -valued Function-like constant total Function-yielding V129() ManySortedFunction of J --> the carrier of S,J --> the carrier of L
J --> the carrier of S is non empty Relation-like non-empty non empty-yielding J -defined { the carrier of S} -valued Function-like constant total quasi_total Element of bool [:J,{ the carrier of S}:]
{ the carrier of S} is non empty trivial finite V54(1) countable set
[:J,{ the carrier of S}:] is non empty Relation-like set
bool [:J,{ the carrier of S}:] is non empty set
( the carrier of S, the carrier of L,J,d) ** F is Relation-like Function-like Function-yielding V129() set
dF is non empty Relation-like non-empty non empty-yielding J -defined Function-like total Function-yielding V129() ManySortedFunction of K,J --> the carrier of L
(L,dF) is non empty Relation-like proj1 dF -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(proj1 dF), the carrier of L:]
proj1 dF is non empty set
[:(proj1 dF), the carrier of L:] is non empty Relation-like set
bool [:(proj1 dF), the carrier of L:] is non empty set
rng (L,dF) is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
gdF is Element of the carrier of S
d . gdF is Element of the carrier of L
{gdF} is non empty trivial finite V54(1) countable Element of bool the carrier of S
bool the carrier of S is non empty set
g " {gdF} is Element of bool the carrier of L
g * d is non empty Relation-like the carrier of S -defined the carrier of S -valued Function-like total quasi_total Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty Relation-like set
bool [: the carrier of S, the carrier of S:] is non empty set
id S is non empty Relation-like the carrier of S -defined the carrier of S -valued Function-like total quasi_total Element of bool [: the carrier of S, the carrier of S:]
id the carrier of S is non empty Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one total quasi_total Element of bool [: the carrier of S, the carrier of S:]
doms dF is Relation-like non-empty Function-like set
product (doms dF) is non empty functional with_common_domain product-like set
(J, the carrier of L,K,dF) is non empty Relation-like non-empty non empty-yielding product (doms dF) -defined Function-like total Function-yielding V129() ManySortedFunction of (product (doms dF)) --> J,(product (doms dF)) --> the carrier of L
(product (doms dF)) --> J is non empty Relation-like non-empty non empty-yielding product (doms dF) -defined {J} -valued Function-like constant total quasi_total Element of bool [:(product (doms dF)),{J}:]
[:(product (doms dF)),{J}:] is non empty Relation-like set
bool [:(product (doms dF)),{J}:] is non empty set
(product (doms dF)) --> the carrier of L is non empty Relation-like non-empty non empty-yielding product (doms dF) -defined { the carrier of L} -valued Function-like constant total quasi_total Element of bool [:(product (doms dF)),{ the carrier of L}:]
[:(product (doms dF)),{ the carrier of L}:] is non empty Relation-like set
bool [:(product (doms dF)),{ the carrier of L}:] is non empty set
dom (J, the carrier of L,K,dF) is non empty functional with_common_domain Element of bool (product (doms dF))
bool (product (doms dF)) is non empty set
gdF is set
(J, the carrier of S9,K,F) . gdF is Relation-like Function-like set
proj2 ((J, the carrier of S9,K,F) . gdF) is set
(J, the carrier of L,K,dF) . gdF is Relation-like Function-like set
proj2 ((J, the carrier of L,K,dF) . gdF) is set
g .: (proj2 ((J, the carrier of L,K,dF) . gdF)) is Element of bool the carrier of S
bool the carrier of S is non empty set
dom (J, the carrier of S9,K,F) is non empty functional with_common_domain Element of bool (product (doms F))
bool (product (doms F)) is non empty set
y is Relation-like Function-like doms dF -compatible Element of product (doms dF)
(J, the carrier of L,K,dF,(J, the carrier of L,K,dF),y) is non empty Relation-like J -defined the carrier of L -valued Function-like total quasi_total Element of bool [:J, the carrier of L:]
[:J, the carrier of L:] is non empty Relation-like set
bool [:J, the carrier of L:] is non empty set
dom (J, the carrier of L,K,dF,(J, the carrier of L,K,dF),y) is non empty Element of bool J
bool J is non empty set
dom dF is non empty Element of bool J
x is set
j is Element of J
dom F is non empty Element of bool J
y . j is set
K . j is non empty set
(J, the carrier of L,K,dF,j) is non empty Relation-like K . j -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(K . j), the carrier of L:]
[:(K . j), the carrier of L:] is non empty Relation-like set
bool [:(K . j), the carrier of L:] is non empty set
dom (J, the carrier of L,K,dF,j) is non empty Element of bool (K . j)
bool (K . j) is non empty set
(J --> the carrier of S) . j is non empty set
(J, the carrier of S9,K,F,j) is non empty Relation-like K . j -defined the carrier of S9 -valued Function-like total quasi_total Element of bool [:(K . j), the carrier of S9:]
[:(K . j), the carrier of S9:] is non empty Relation-like set
bool [:(K . j), the carrier of S9:] is non empty set
(J, the carrier of L,(J --> the carrier of S),( the carrier of S, the carrier of L,J,d),j) is non empty Relation-like (J --> the carrier of S) . j -defined the carrier of L -valued Function-like total quasi_total Element of bool [:((J --> the carrier of S) . j), the carrier of L:]
[:((J --> the carrier of S) . j), the carrier of L:] is non empty Relation-like set
bool [:((J --> the carrier of S) . j), the carrier of L:] is non empty set
(J, the carrier of L,(J --> the carrier of S),( the carrier of S, the carrier of L,J,d),j) * (J, the carrier of S9,K,F,j) is Relation-like K . j -defined the carrier of L -valued Function-like Element of bool [:(K . j), the carrier of L:]
dom ((J, the carrier of L,(J --> the carrier of S),( the carrier of S, the carrier of L,J,d),j) * (J, the carrier of S9,K,F,j)) is Element of bool (K . j)
d * (J, the carrier of S9,K,F,j) is Relation-like K . j -defined the carrier of L -valued Function-like Element of bool [:(K . j), the carrier of L:]
dom (d * (J, the carrier of S9,K,F,j)) is Element of bool (K . j)
g * (J, the carrier of L,K,dF,(J, the carrier of L,K,dF),y) is non empty Relation-like J -defined the carrier of S -valued Function-like total quasi_total Element of bool [:J, the carrier of S:]
[:J, the carrier of S:] is non empty Relation-like set
bool [:J, the carrier of S:] is non empty set
(g * (J, the carrier of L,K,dF,(J, the carrier of L,K,dF),y)) . j is Element of the carrier of S
(J, the carrier of L,K,dF,(J, the carrier of L,K,dF),y) . j is Element of the carrier of L
g . ((J, the carrier of L,K,dF,(J, the carrier of L,K,dF),y) . j) is Element of the carrier of S
(J, the carrier of L,K,dF,j) . (y . j) is set
g . ((J, the carrier of L,K,dF,j) . (y . j)) is set
((J, the carrier of L,(J --> the carrier of S),( the carrier of S, the carrier of L,J,d),j) * (J, the carrier of S9,K,F,j)) . (y . j) is set
g . (((J, the carrier of L,(J --> the carrier of S),( the carrier of S, the carrier of L,J,d),j) * (J, the carrier of S9,K,F,j)) . (y . j)) is set
(d * (J, the carrier of S9,K,F,j)) . (y . j) is set
g . ((d * (J, the carrier of S9,K,F,j)) . (y . j)) is set
g * (d * (J, the carrier of S9,K,F,j)) is Relation-like K . j -defined the carrier of S -valued Function-like Element of bool [:(K . j), the carrier of S:]
[:(K . j), the carrier of S:] is non empty Relation-like set
bool [:(K . j), the carrier of S:] is non empty set
(g * (d * (J, the carrier of S9,K,F,j))) . (y . j) is set
(id the carrier of S) * (J, the carrier of S9,K,F,j) is Relation-like K . j -defined the carrier of S -valued Function-like Element of bool [:(K . j), the carrier of S:]
((id the carrier of S) * (J, the carrier of S9,K,F,j)) . (y . j) is set
(J, the carrier of S9,K,F,j) . (y . j) is set
(J, the carrier of S9,K,F) . y is Relation-like Function-like set
((J, the carrier of S9,K,F) . y) . j is set
(g * (J, the carrier of L,K,dF,(J, the carrier of L,K,dF),y)) . x is set
((J, the carrier of S9,K,F) . y) . x is set
dom g is non empty Element of bool the carrier of L
rng (J, the carrier of L,K,dF,(J, the carrier of L,K,dF),y) is non empty Element of bool the carrier of L
dom (g * (J, the carrier of L,K,dF,(J, the carrier of L,K,dF),y)) is non empty Element of bool J
proj1 ((J, the carrier of S9,K,F) . y) is set
proj2 ((J, the carrier of S9,K,F) . y) is set
rng (g * (J, the carrier of L,K,dF,(J, the carrier of L,K,dF),y)) is non empty Element of bool the carrier of S
g .: (rng (J, the carrier of L,K,dF,(J, the carrier of L,K,dF),y)) is Element of bool the carrier of S
rng (S9,(J, the carrier of S9,K,F)) is non empty Element of bool the carrier of S9
bool the carrier of S9 is non empty set
(L,(J, the carrier of L,K,dF)) is non empty Relation-like proj1 (J, the carrier of L,K,dF) -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(proj1 (J, the carrier of L,K,dF)), the carrier of L:]
proj1 (J, the carrier of L,K,dF) is non empty set
[:(proj1 (J, the carrier of L,K,dF)), the carrier of L:] is non empty Relation-like set
bool [:(proj1 (J, the carrier of L,K,dF)), the carrier of L:] is non empty set
rng (L,(J, the carrier of L,K,dF)) is non empty Element of bool the carrier of L
g .: (rng (L,(J, the carrier of L,K,dF))) is Element of bool the carrier of S
bool the carrier of S is non empty set
gdF is set
dom (J, the carrier of S9,K,F) is non empty functional with_common_domain Element of bool (product (doms F))
bool (product (doms F)) is non empty set
y is set
(J, the carrier of S9,K,F) . y is Relation-like Function-like set
//\ (((J, the carrier of S9,K,F) . y),S) is Element of the carrier of S
x is Relation-like Function-like doms F -compatible Element of product (doms F)
j is Relation-like Function-like doms dF -compatible Element of product (doms dF)
(J, the carrier of L,K,dF,(J, the carrier of L,K,dF),j) is non empty Relation-like J -defined the carrier of L -valued Function-like total quasi_total Element of bool [:J, the carrier of L:]
[:J, the carrier of L:] is non empty Relation-like set
bool [:J, the carrier of L:] is non empty set
rng (J, the carrier of L,K,dF,(J, the carrier of L,K,dF),j) is non empty Element of bool the carrier of L
(J, the carrier of S9,K,F,(J, the carrier of S9,K,F),x) is non empty Relation-like J -defined the carrier of S9 -valued Function-like total quasi_total Element of bool [:J, the carrier of S9:]
[:J, the carrier of S9:] is non empty Relation-like set
bool [:J, the carrier of S9:] is non empty set
rng (J, the carrier of S9,K,F,(J, the carrier of S9,K,F),x) is non empty Element of bool the carrier of S9
(J, the carrier of L,K,dF) . x is Relation-like Function-like set
proj2 ((J, the carrier of L,K,dF) . x) is set
g .: (proj2 ((J, the carrier of L,K,dF) . x)) is Element of bool the carrier of S
"/\" ((g .: (proj2 ((J, the carrier of L,K,dF) . x))),S) is Element of the carrier of S
"/\" ((rng (J, the carrier of L,K,dF,(J, the carrier of L,K,dF),j)),L) is Element of the carrier of L
g . ("/\" ((rng (J, the carrier of L,K,dF,(J, the carrier of L,K,dF),j)),L)) is Element of the carrier of S
//\ ((J, the carrier of L,K,dF,(J, the carrier of L,K,dF),j),L) is Element of the carrier of L
g . (//\ ((J, the carrier of L,K,dF,(J, the carrier of L,K,dF),j),L)) is Element of the carrier of S
gdF is set
y is set
g . y is set
x is set
(J, the carrier of L,K,dF) . x is Relation-like Function-like set
//\ (((J, the carrier of L,K,dF) . x),L) is Element of the carrier of L
j is Relation-like Function-like doms dF -compatible Element of product (doms dF)
(J, the carrier of L,K,dF,(J, the carrier of L,K,dF),j) is non empty Relation-like J -defined the carrier of L -valued Function-like total quasi_total Element of bool [:J, the carrier of L:]
[:J, the carrier of L:] is non empty Relation-like set
bool [:J, the carrier of L:] is non empty set
rng (J, the carrier of L,K,dF,(J, the carrier of L,K,dF),j) is non empty Element of bool the carrier of L
g .: (rng (J, the carrier of L,K,dF,(J, the carrier of L,K,dF),j)) is Element of bool the carrier of S
"/\" ((g .: (rng (J, the carrier of L,K,dF,(J, the carrier of L,K,dF),j))),S) is Element of the carrier of S
"/\" ((rng (J, the carrier of L,K,dF,(J, the carrier of L,K,dF),j)),L) is Element of the carrier of L
g . ("/\" ((rng (J, the carrier of L,K,dF,(J, the carrier of L,K,dF),j)),L)) is Element of the carrier of S
dom (J, the carrier of S9,K,F) is non empty functional with_common_domain Element of bool (product (doms F))
bool (product (doms F)) is non empty set
(J, the carrier of S9,K,F) . j is Relation-like Function-like set
proj2 ((J, the carrier of S9,K,F) . j) is set
f9 is Relation-like Function-like doms F -compatible Element of product (doms F)
(J, the carrier of S9,K,F,(J, the carrier of S9,K,F),f9) is non empty Relation-like J -defined the carrier of S9 -valued Function-like total quasi_total Element of bool [:J, the carrier of S9:]
[:J, the carrier of S9:] is non empty Relation-like set
bool [:J, the carrier of S9:] is non empty set
//\ ((J, the carrier of S9,K,F,(J, the carrier of S9,K,F),f9),S9) is Element of the carrier of S9
gdF is Element of J
(J, the carrier of L,K,dF,gdF) is non empty Relation-like K . gdF -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(K . gdF), the carrier of L:]
K . gdF is non empty set
[:(K . gdF), the carrier of L:] is non empty Relation-like set
bool [:(K . gdF), the carrier of L:] is non empty set
rng (J, the carrier of L,K,dF,gdF) is non empty Element of bool the carrier of L
(J --> the carrier of S) . gdF is non empty set
(J, the carrier of L,(J --> the carrier of S),( the carrier of S, the carrier of L,J,d),gdF) is non empty Relation-like (J --> the carrier of S) . gdF -defined the carrier of L -valued Function-like total quasi_total Element of bool [:((J --> the carrier of S) . gdF), the carrier of L:]
[:((J --> the carrier of S) . gdF), the carrier of L:] is non empty Relation-like set
bool [:((J --> the carrier of S) . gdF), the carrier of L:] is non empty set
(J, the carrier of S9,K,F,gdF) is non empty Relation-like K . gdF -defined the carrier of S9 -valued Function-like total quasi_total Element of bool [:(K . gdF), the carrier of S9:]
[:(K . gdF), the carrier of S9:] is non empty Relation-like set
bool [:(K . gdF), the carrier of S9:] is non empty set
d * (J, the carrier of S9,K,F,gdF) is Relation-like K . gdF -defined the carrier of L -valued Function-like Element of bool [:(K . gdF), the carrier of L:]
rng (d * (J, the carrier of S9,K,F,gdF)) is Element of bool the carrier of L
rng (J, the carrier of S9,K,F,gdF) is non empty Element of bool the carrier of S9
d .: (rng (J, the carrier of S9,K,F,gdF)) is Element of bool the carrier of L
( the carrier of L, the carrier of S,J,g) is non empty Relation-like non-empty non empty-yielding J -defined bool [: the carrier of L, the carrier of S:] -valued Function-like constant total Function-yielding V129() ManySortedFunction of J --> the carrier of L,J --> the carrier of S
( the carrier of L, the carrier of S,J,g) ** dF is non empty Relation-like non-empty non empty-yielding J -defined Function-like total Function-yielding V129() ManySortedFunction of K,J --> the carrier of S
gdF is non empty Relation-like non-empty non empty-yielding J -defined Function-like total Function-yielding V129() ManySortedFunction of K,J --> the carrier of S
(S,gdF) is non empty Relation-like proj1 gdF -defined the carrier of S -valued Function-like total quasi_total Element of bool [:(proj1 gdF), the carrier of S:]
proj1 gdF is non empty set
[:(proj1 gdF), the carrier of S:] is non empty Relation-like set
bool [:(proj1 gdF), the carrier of S:] is non empty set
rng (S,gdF) is non empty Element of bool the carrier of S
g .: (rng (L,dF)) is Element of bool the carrier of S
y is set
x is Element of J
(J, the carrier of S,K,gdF,x) is non empty Relation-like K . x -defined the carrier of S -valued Function-like total quasi_total Element of bool [:(K . x), the carrier of S:]
K . x is non empty set
[:(K . x), the carrier of S:] is non empty Relation-like set
bool [:(K . x), the carrier of S:] is non empty set
\\/ ((J, the carrier of S,K,gdF,x),S) is Element of the carrier of S
(J --> the carrier of L) . x is non empty set
(J, the carrier of L,K,dF,x) is non empty Relation-like K . x -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(K . x), the carrier of L:]
[:(K . x), the carrier of L:] is non empty Relation-like set
bool [:(K . x), the carrier of L:] is non empty set
(J, the carrier of S,(J --> the carrier of L),( the carrier of L, the carrier of S,J,g),x) is non empty Relation-like (J --> the carrier of L) . x -defined the carrier of S -valued Function-like total quasi_total Element of bool [:((J --> the carrier of L) . x), the carrier of S:]
[:((J --> the carrier of L) . x), the carrier of S:] is non empty Relation-like set
bool [:((J --> the carrier of L) . x), the carrier of S:] is non empty set
(J, the carrier of S,(J --> the carrier of L),( the carrier of L, the carrier of S,J,g),x) * (J, the carrier of L,K,dF,x) is Relation-like K . x -defined the carrier of S -valued Function-like Element of bool [:(K . x), the carrier of S:]
g * (J, the carrier of L,K,dF,x) is non empty Relation-like K . x -defined the carrier of S -valued Function-like total quasi_total Element of bool [:(K . x), the carrier of S:]
rng (J, the carrier of S,K,gdF,x) is non empty Element of bool the carrier of S
rng (J, the carrier of L,K,dF,x) is non empty Element of bool the carrier of L
g .: (rng (J, the carrier of L,K,dF,x)) is Element of bool the carrier of S
"\/" ((g .: (rng (J, the carrier of L,K,dF,x))),S) is Element of the carrier of S
"\/" ((rng (J, the carrier of L,K,dF,x)),L) is Element of the carrier of L
g . ("\/" ((rng (J, the carrier of L,K,dF,x)),L)) is Element of the carrier of S
\\/ ((J, the carrier of L,K,dF,x),L) is Element of the carrier of L
g . (\\/ ((J, the carrier of L,K,dF,x),L)) is Element of the carrier of S
y is set
x is set
g . x is set
j is Element of J
(J, the carrier of L,K,dF,j) is non empty Relation-like K . j -defined the carrier of L -valued Function-like total quasi_total Element of bool [:(K . j), the carrier of L:]
K . j is non empty set
[:(K . j), the carrier of L:] is non empty Relation-like set
bool [:(K . j), the carrier of L:] is non empty set
\\/ ((J, the carrier of L,K,dF,j),L) is Element of the carrier of L
rng (J, the carrier of L,K,dF,j) is non empty Element of bool the carrier of L
g .: (rng (J, the carrier of L,K,dF,j)) is Element of bool the carrier of S
"\/" ((g .: (rng (J, the carrier of L,K,dF,j))),S) is Element of the carrier of S
"\/" ((rng (J, the carrier of L,K,dF,j)),L) is Element of the carrier of L
g . ("\/" ((rng (J, the carrier of L,K,dF,j)),L)) is Element of the carrier of S
(J, the carrier of S,K,gdF,j) is non empty Relation-like K . j -defined the carrier of S -valued Function-like total quasi_total Element of bool [:(K . j), the carrier of S:]
[:(K . j), the carrier of S:] is non empty Relation-like set
bool [:(K . j), the carrier of S:] is non empty set
(J --> the carrier of L) . j is non empty set
(J, the carrier of S,(J --> the carrier of L),( the carrier of L, the carrier of S,J,g),j) is non empty Relation-like (J --> the carrier of L) . j -defined the carrier of S -valued Function-like total quasi_total Element of bool [:((J --> the carrier of L) . j), the carrier of S:]
[:((J --> the carrier of L) . j), the carrier of S:] is non empty Relation-like set
bool [:((J --> the carrier of L) . j), the carrier of S:] is non empty set
(J, the carrier of S,(J --> the carrier of L),( the carrier of L, the carrier of S,J,g),j) * (J, the carrier of L,K,dF,j) is Relation-like K . j -defined the carrier of S -valued Function-like Element of bool [:(K . j), the carrier of S:]
g * (J, the carrier of L,K,dF,j) is non empty Relation-like K . j -defined the carrier of S -valued Function-like total quasi_total Element of bool [:(K . j), the carrier of S:]
rng (J, the carrier of S,K,gdF,j) is non empty Element of bool the carrier of S
\\/ ((J, the carrier of S,K,gdF,j),S) is Element of the carrier of S
id (J --> the carrier of S) is non empty Relation-like non-empty non empty-yielding J -defined Function-like total Function-yielding V129() ManySortedFunction of J --> the carrier of S,J --> the carrier of S
(id (J --> the carrier of S)) ** F is Relation-like Function-like Function-yielding V129() set
J --> d is non empty Relation-like non-empty non empty-yielding J -defined bool [: the carrier of S, the carrier of L:] -valued Function-like constant total quasi_total Function-yielding V129() Element of bool [:J,(bool [: the carrier of S, the carrier of L:]):]
[:J,(bool [: the carrier of S, the carrier of L:]):] is non empty Relation-like set
bool [:J,(bool [: the carrier of S, the carrier of L:]):] is non empty set
J --> g is non empty Relation-like non-empty non empty-yielding J -defined bool [: the carrier of L, the carrier of S:] -valued Function-like constant total quasi_total Function-yielding V129() Element of bool [:J,(bool [: the carrier of L, the carrier of S:]):]
[:J,(bool [: the carrier of L, the carrier of S:]):] is non empty Relation-like set
bool [:J,(bool [: the carrier of L, the carrier of S:]):] is non empty set
(J --> g) ** (J --> d) is Relation-like Function-like Function-yielding V129() set
((J --> g) ** (J --> d)) ** F is Relation-like Function-like Function-yielding V129() set
"/\" ((rng (S,gdF)),S) is Element of the carrier of S
"/\" ((g .: (rng (L,dF))),S) is Element of the carrier of S
"/\" ((rng (L,dF)),L) is Element of the carrier of L
g . ("/\" ((rng (L,dF)),L)) is Element of the carrier of S
//\ ((L,dF),L) is Element of the carrier of L
g . (//\ ((L,dF),L)) is Element of the carrier of S
\\/ ((L,(J, the carrier of L,K,dF)),L) is Element of the carrier of L
g . (\\/ ((L,(J, the carrier of L,K,dF)),L)) is Element of the carrier of S
"\/" ((rng (L,(J, the carrier of L,K,dF))),L) is Element of the carrier of L
g . ("\/" ((rng (L,(J, the carrier of L,K,dF))),L)) is Element of the carrier of S
"\/" ((g .: (rng (L,(J, the carrier of L,K,dF)))),S) is Element of the carrier of S
"\/" ((rng (S9,(J, the carrier of S9,K,F))),S9) is Element of the carrier of S9