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

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

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

f9 . c

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

"\/" (c

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