:: UNIALG_2 semantic presentation

NAT is non empty V29() V30() V31() V36() V41() V42() Element of bool REAL

REAL is set

bool REAL is non empty set

NAT is non empty V29() V30() V31() V36() V41() V42() set

bool NAT is non empty V36() set

bool NAT is non empty V36() set

K229() is non empty set

0 is empty functional V29() V30() V31() V33() V34() V35() V36() V41() V43( {} ) FinSequence-membered V89() Element of NAT

{} is empty functional V29() V30() V31() V33() V34() V35() V36() V41() V43( {} ) FinSequence-membered V89() set

the empty functional V29() V30() V31() V33() V34() V35() V36() V41() V43( {} ) FinSequence-membered V89() set is empty functional V29() V30() V31() V33() V34() V35() V36() V41() V43( {} ) FinSequence-membered V89() set

1 is non empty set

{0,1} is non empty set

2 is non empty set

3 is non empty set

Seg 1 is Element of bool NAT

{1} is non empty trivial V43(1) set

Seg 2 is Element of bool NAT

{1,2} is non empty set

dom {} is set

rng {} is set

a is non empty V84() quasi_total non-empty UAStr

signature a is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT

b is non empty V84() quasi_total non-empty UAStr

signature b is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT

a is non empty V84() quasi_total non-empty UAStr

signature a is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT

U0 is non empty V84() quasi_total non-empty UAStr

the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)

the carrier of U0 is non empty set

the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0

PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set

len the charact of U0 is non empty V29() V30() V31() V35() V36() V41() Element of NAT

L is non empty V84() quasi_total non-empty UAStr

the charact of L is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of L *), the carrier of L) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of L *), the carrier of L)

the carrier of L is non empty set

the carrier of L * is non empty functional FinSequence-membered FinSequenceSet of the carrier of L

PFuncs (( the carrier of L *), the carrier of L) is non empty functional set

len the charact of L is non empty V29() V30() V31() V35() V36() V41() Element of NAT

signature U0 is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT

len (signature U0) is V29() V30() V31() V35() V36() V41() Element of NAT

signature L is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT

len (signature L) is V29() V30() V31() V35() V36() V41() Element of NAT

U0 is non empty V84() quasi_total non-empty UAStr

L is non empty V84() quasi_total non-empty UAStr

a is non empty V84() quasi_total non-empty UAStr

signature U0 is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT

signature L is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT

signature a is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT

U0 is non empty V84() quasi_total non-empty UAStr

the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)

the carrier of U0 is non empty set

the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0

PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set

rng the charact of U0 is set

bool (PFuncs (( the carrier of U0 *), the carrier of U0)) is non empty set

U0 is non empty V84() quasi_total non-empty UAStr

the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)

the carrier of U0 is non empty set

the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0

PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set

rng the charact of U0 is set

L is non empty set

dom the charact of U0 is Element of bool NAT

a is Element of L

b is V29() V30() V31() V35() V36() V41() set

the charact of U0 . b is homogeneous set

[:( the carrier of U0 *), the carrier of U0:] is non empty set

bool [:( the carrier of U0 *), the carrier of U0:] is non empty set

x is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like Element of bool [:( the carrier of U0 *), the carrier of U0:]

U0 is non empty V84() quasi_total non-empty UAStr

the carrier of U0 is non empty set

bool the carrier of U0 is non empty set

the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0

(U0) is non empty PFuncsDomHQN of the carrier of U0

the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)

PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set

rng the charact of U0 is set

U0 is non empty V84() quasi_total non-empty UAStr

the carrier of U0 is non empty set

bool the carrier of U0 is non empty set

U0 is non empty V84() quasi_total non-empty UAStr

the carrier of U0 is non empty set

bool the carrier of U0 is non empty set

the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0

(U0) is non empty PFuncsDomHQN of the carrier of U0

the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)

PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set

rng the charact of U0 is set

L is non empty Element of bool the carrier of U0

a is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)

arity a is V29() V30() V31() V35() V36() V41() Element of NAT

(arity a) -tuples_on L is non empty functional FinSequence-membered FinSequenceSet of L

a | ((arity a) -tuples_on L) is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like Element of bool [:( the carrier of U0 *), the carrier of U0:]

[:( the carrier of U0 *), the carrier of U0:] is non empty set

bool [:( the carrier of U0 *), the carrier of U0:] is non empty set

L * is non empty functional FinSequence-membered FinSequenceSet of L

[:(L *),L:] is non empty set

bool [:(L *),L:] is non empty set

(arity a) -tuples_on the carrier of U0 is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0

b is set

{ b

x is Relation-like NAT -defined L -valued Function-like V36() FinSequence-like FinSubsequence-like Element of L *

len x is V29() V30() V31() V35() V36() V41() Element of NAT

rng x is set

y is Relation-like NAT -defined the carrier of U0 -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of the carrier of U0

y is Relation-like NAT -defined the carrier of U0 -valued Function-like V36() FinSequence-like FinSubsequence-like Element of the carrier of U0 *

{ b

dom (a | ((arity a) -tuples_on L)) is functional FinSequence-membered set

dom a is functional FinSequence-membered V89() set

(dom a) /\ ((arity a) -tuples_on L) is set

((arity a) -tuples_on the carrier of U0) /\ ((arity a) -tuples_on L) is set

rng (a | ((arity a) -tuples_on L)) is set

b is set

x is set

(a | ((arity a) -tuples_on L)) . x is set

{ b

y is Relation-like NAT -defined L -valued Function-like V36() FinSequence-like FinSubsequence-like Element of L *

len y is V29() V30() V31() V35() V36() V41() Element of NAT

(a | ((arity a) -tuples_on L)) . y is set

a . y is set

{ (b

union { (b

b is Relation-like L * -defined L -valued Function-like Element of bool [:(L *),L:]

x is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set

dom b is functional FinSequence-membered set

y is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set

len x is V29() V30() V31() V35() V36() V41() Element of NAT

len y is V29() V30() V31() V35() V36() V41() Element of NAT

{ b

y is Relation-like NAT -defined L -valued Function-like V36() FinSequence-like FinSubsequence-like Element of L *

len y is V29() V30() V31() V35() V36() V41() Element of NAT

z is Relation-like NAT -defined L -valued Function-like V36() FinSequence-like FinSubsequence-like Element of L *

len z is V29() V30() V31() V35() V36() V41() Element of NAT

x is Relation-like NAT -defined L -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of L

len x is V29() V30() V31() V35() V36() V41() Element of NAT

dom b is functional FinSequence-membered set

y is Relation-like NAT -defined L -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of L

len y is V29() V30() V31() V35() V36() V41() Element of NAT

{ b

y is Relation-like NAT -defined L -valued Function-like V36() FinSequence-like FinSubsequence-like Element of L *

len y is V29() V30() V31() V35() V36() V41() Element of NAT

U0 is non empty V84() quasi_total non-empty UAStr

the carrier of U0 is non empty set

bool the carrier of U0 is non empty set

L is non empty Element of bool the carrier of U0

L * is non empty functional FinSequence-membered FinSequenceSet of L

PFuncs ((L *),L) is non empty functional set

the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)

the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0

PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set

dom the charact of U0 is Element of bool NAT

(U0) is non empty PFuncsDomHQN of the carrier of U0

rng the charact of U0 is set

len the charact of U0 is non empty V29() V30() V31() V35() V36() V41() Element of NAT

Seg (len the charact of U0) is non empty V36() V43( len the charact of U0) Element of bool NAT

a is V29() V30() V31() V35() V36() V41() set

the charact of U0 . a is homogeneous set

b is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)

(U0,L,b) is non empty Relation-like L * -defined L -valued Function-like homogeneous quasi_total Element of bool [:(L *),L:]

[:(L *),L:] is non empty set

bool [:(L *),L:] is non empty set

x is Element of PFuncs ((L *),L)

y is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)

(U0,L,y) is non empty Relation-like L * -defined L -valued Function-like homogeneous quasi_total Element of bool [:(L *),L:]

a is Relation-like NAT -defined PFuncs ((L *),L) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((L *),L)

dom a is Element of bool NAT

b is Relation-like NAT -defined PFuncs ((L *),L) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((L *),L)

dom b is Element of bool NAT

x is set

the charact of U0 . x is homogeneous set

b . x is set

y is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)

(U0,L,y) is non empty Relation-like L * -defined L -valued Function-like homogeneous quasi_total Element of bool [:(L *),L:]

[:(L *),L:] is non empty set

bool [:(L *),L:] is non empty set

a is Relation-like NAT -defined PFuncs ((L *),L) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((L *),L)

dom a is Element of bool NAT

b is Relation-like NAT -defined PFuncs ((L *),L) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((L *),L)

dom b is Element of bool NAT

x is V29() V30() V31() V35() V36() V41() set

a . x is set

b . x is set

the charact of U0 . x is homogeneous set

y is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)

(U0,L,y) is non empty Relation-like L * -defined L -valued Function-like homogeneous quasi_total Element of bool [:(L *),L:]

[:(L *),L:] is non empty set

bool [:(L *),L:] is non empty set

U0 is non empty V84() quasi_total non-empty UAStr

the carrier of U0 is non empty set

bool the carrier of U0 is non empty set

the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0

(U0) is non empty PFuncsDomHQN of the carrier of U0

the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)

PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set

rng the charact of U0 is set

L is non empty Element of bool the carrier of U0

a is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)

b is Relation-like NAT -defined L -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of L

len b is V29() V30() V31() V35() V36() V41() Element of NAT

arity a is V29() V30() V31() V35() V36() V41() Element of NAT

a . b is set

dom a is functional FinSequence-membered V89() set

(arity a) -tuples_on L is non empty functional FinSequence-membered FinSequenceSet of L

(len b) -tuples_on L is non empty functional FinSequence-membered FinSequenceSet of L

rng a is set

a is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)

(U0,L,a) is non empty Relation-like L * -defined L -valued Function-like homogeneous quasi_total Element of bool [:(L *),L:]

L * is non empty functional FinSequence-membered FinSequenceSet of L

[:(L *),L:] is non empty set

bool [:(L *),L:] is non empty set

dom a is functional FinSequence-membered V89() set

arity a is V29() V30() V31() V35() V36() V41() Element of NAT

(arity a) -tuples_on L is non empty functional FinSequence-membered FinSequenceSet of L

a | ((arity a) -tuples_on L) is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like Element of bool [:( the carrier of U0 *), the carrier of U0:]

[:( the carrier of U0 *), the carrier of U0:] is non empty set

bool [:( the carrier of U0 *), the carrier of U0:] is non empty set

a is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)

(U0,L,a) is non empty Relation-like L * -defined L -valued Function-like homogeneous quasi_total Element of bool [:(L *),L:]

L * is non empty functional FinSequence-membered FinSequenceSet of L

[:(L *),L:] is non empty set

bool [:(L *),L:] is non empty set

U0 is non empty V84() quasi_total non-empty UAStr

the carrier of U0 is non empty set

bool the carrier of U0 is non empty set

the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0

(U0) is non empty PFuncsDomHQN of the carrier of U0

the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)

PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set

rng the charact of U0 is set

L is non empty Element of bool the carrier of U0

a is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)

(U0,L,a) is non empty Relation-like L * -defined L -valued Function-like homogeneous quasi_total Element of bool [:(L *),L:]

L * is non empty functional FinSequence-membered FinSequenceSet of L

[:(L *),L:] is non empty set

bool [:(L *),L:] is non empty set

arity (U0,L,a) is V29() V30() V31() V35() V36() V41() Element of NAT

arity a is V29() V30() V31() V35() V36() V41() Element of NAT

(arity a) -tuples_on L is non empty functional FinSequence-membered FinSequenceSet of L

a | ((arity a) -tuples_on L) is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like Element of bool [:( the carrier of U0 *), the carrier of U0:]

[:( the carrier of U0 *), the carrier of U0:] is non empty set

bool [:( the carrier of U0 *), the carrier of U0:] is non empty set

dom (U0,L,a) is functional FinSequence-membered V89() set

dom a is functional FinSequence-membered V89() set

(dom a) /\ ((arity a) -tuples_on L) is set

(arity a) -tuples_on the carrier of U0 is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0

((arity a) -tuples_on the carrier of U0) /\ ((arity a) -tuples_on L) is set

(arity (U0,L,a)) -tuples_on L is non empty functional FinSequence-membered FinSequenceSet of L

U0 is non empty V84() quasi_total non-empty UAStr

the carrier of U0 is non empty set

bool the carrier of U0 is non empty set

L is non empty V84() quasi_total non-empty UAStr

the carrier of L is non empty set

the charact of L is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of L *), the carrier of L) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of L *), the carrier of L)

the carrier of L * is non empty functional FinSequence-membered FinSequenceSet of the carrier of L

PFuncs (( the carrier of L *), the carrier of L) is non empty functional set

the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)

the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0

PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set

a is non empty Element of bool the carrier of U0

(U0,a) is Relation-like NAT -defined PFuncs ((a *),a) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((a *),a)

a * is non empty functional FinSequence-membered FinSequenceSet of a

PFuncs ((a *),a) is non empty functional set

dom the charact of U0 is Element of bool NAT

dom (U0,a) is Element of bool NAT

b is V29() V30() V31() V35() V36() V41() set

the charact of U0 . b is homogeneous set

(U0,a) . b is set

(U0) is non empty PFuncsDomHQN of the carrier of U0

rng the charact of U0 is set

x is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)

(U0,a,x) is non empty Relation-like a * -defined a -valued Function-like homogeneous quasi_total Element of bool [:(a *),a:]

[:(a *),a:] is non empty set

bool [:(a *),a:] is non empty set

a is non empty Element of bool the carrier of U0

(U0,a) is Relation-like NAT -defined PFuncs ((a *),a) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((a *),a)

a * is non empty functional FinSequence-membered FinSequenceSet of a

PFuncs ((a *),a) is non empty functional set

U0 is non empty V84() quasi_total non-empty UAStr

the carrier of U0 is non empty set

the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)

the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0

PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set

UAStr(# the carrier of U0, the charact of U0 #) is non empty strict UAStr

L is non empty strict V84() quasi_total non-empty UAStr

the carrier of L is non empty set

bool the carrier of U0 is non empty set

the charact of L is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of L *), the carrier of L) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of L *), the carrier of L)

the carrier of L * is non empty functional FinSequence-membered FinSequenceSet of the carrier of L

PFuncs (( the carrier of L *), the carrier of L) is non empty functional set

a is non empty Element of bool the carrier of U0

(U0,a) is Relation-like NAT -defined PFuncs ((a *),a) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((a *),a)

a * is non empty functional FinSequence-membered FinSequenceSet of a

PFuncs ((a *),a) is non empty functional set

b is V29() V30() V31() V35() V36() V41() set

dom the charact of U0 is Element of bool NAT

(U0) is non empty PFuncsDomHQN of the carrier of U0

rng the charact of U0 is set

the charact of U0 . b is homogeneous set

dom (U0,a) is Element of bool NAT

(U0,a) . b is set

x is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)

(U0,a,x) is non empty Relation-like a * -defined a -valued Function-like homogeneous quasi_total Element of bool [:(a *),a:]

[:(a *),a:] is non empty set

bool [:(a *),a:] is non empty set

a is non empty V84() quasi_total non-empty (U0)

U0 is non empty V84() quasi_total non-empty UAStr

the carrier of U0 is non empty set

the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0

(U0) is non empty PFuncsDomHQN of the carrier of U0

the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)

PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set

rng the charact of U0 is set

L is non empty V84() quasi_total non-empty UAStr

the carrier of L is non empty set

the carrier of L * is non empty functional FinSequence-membered FinSequenceSet of the carrier of L

(L) is non empty PFuncsDomHQN of the carrier of L

the charact of L is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of L *), the carrier of L) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of L *), the carrier of L)

PFuncs (( the carrier of L *), the carrier of L) is non empty functional set

rng the charact of L is set

dom the charact of U0 is Element of bool NAT

a is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)

arity a is V29() V30() V31() V35() V36() V41() Element of NAT

b is non empty Relation-like the carrier of L * -defined the carrier of L -valued Function-like homogeneous quasi_total Element of (L)

arity b is V29() V30() V31() V35() V36() V41() Element of NAT

x is V29() V30() V31() V35() V36() V41() set

the charact of U0 . x is homogeneous set

the charact of L . x is homogeneous set

bool the carrier of L is non empty set

y is non empty Element of bool the carrier of L

(L,y) is Relation-like NAT -defined PFuncs ((y *),y) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((y *),y)

y * is non empty functional FinSequence-membered FinSequenceSet of y

PFuncs ((y *),y) is non empty functional set

dom (L,y) is Element of bool NAT

(L,y) . x is set

(L,y,b) is non empty Relation-like y * -defined y -valued Function-like homogeneous quasi_total Element of bool [:(y *),y:]

[:(y *),y:] is non empty set

bool [:(y *),y:] is non empty set

(arity b) -tuples_on y is non empty functional FinSequence-membered FinSequenceSet of y

b | ((arity b) -tuples_on y) is Relation-like the carrier of L * -defined the carrier of L -valued Function-like Element of bool [:( the carrier of L *), the carrier of L:]

[:( the carrier of L *), the carrier of L:] is non empty set

bool [:( the carrier of L *), the carrier of L:] is non empty set

dom a is functional FinSequence-membered V89() set

dom b is functional FinSequence-membered V89() set

(dom b) /\ ((arity b) -tuples_on y) is set

(arity b) -tuples_on the carrier of L is non empty functional FinSequence-membered FinSequenceSet of the carrier of L

((arity b) -tuples_on the carrier of L) /\ ((arity b) -tuples_on y) is set

(arity a) -tuples_on y is non empty functional FinSequence-membered FinSequenceSet of y

U0 is non empty V84() quasi_total non-empty UAStr

the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)

the carrier of U0 is non empty set

the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0

PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set

dom the charact of U0 is Element of bool NAT

L is non empty V84() quasi_total non-empty UAStr

the charact of L is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of L *), the carrier of L) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of L *), the carrier of L)

the carrier of L is non empty set

the carrier of L * is non empty functional FinSequence-membered FinSequenceSet of the carrier of L

PFuncs (( the carrier of L *), the carrier of L) is non empty functional set

dom the charact of L is Element of bool NAT

bool the carrier of L is non empty set

a is non empty Element of bool the carrier of L

(L,a) is Relation-like NAT -defined PFuncs ((a *),a) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((a *),a)

a * is non empty functional FinSequence-membered FinSequenceSet of a

PFuncs ((a *),a) is non empty functional set

U0 is non empty V84() quasi_total non-empty UAStr

the carrier of U0 is non empty set

bool the carrier of U0 is non empty set

the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)

the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0

PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set

L is non empty Element of bool the carrier of U0

(U0,L) is Relation-like NAT -defined PFuncs ((L *),L) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((L *),L)

L * is non empty functional FinSequence-membered FinSequenceSet of L

PFuncs ((L *),L) is non empty functional set

dom the charact of U0 is Element of bool NAT

dom (U0,L) is Element of bool NAT

a is V29() V30() V31() V35() V36() V41() set

the charact of U0 . a is homogeneous set

(U0,L) . a is set

(U0) is non empty PFuncsDomHQN of the carrier of U0

rng the charact of U0 is set

b is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)

(U0,L,b) is non empty Relation-like L * -defined L -valued Function-like homogeneous quasi_total Element of bool [:(L *),L:]

[:(L *),L:] is non empty set

bool [:(L *),L:] is non empty set

U0 is non empty V84() quasi_total non-empty UAStr

L is non empty V84() quasi_total non-empty UAStr

a is non empty V84() quasi_total non-empty UAStr

the carrier of U0 is non empty set

the carrier of L is non empty set

bool the carrier of L is non empty set

the carrier of a is non empty set

bool the carrier of a is non empty set

the charact of L is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of L *), the carrier of L) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of L *), the carrier of L)

the carrier of L * is non empty functional FinSequence-membered FinSequenceSet of the carrier of L

PFuncs (( the carrier of L *), the carrier of L) is non empty functional set

b is non empty Element of bool the carrier of a

(a,b) is Relation-like NAT -defined PFuncs ((b *),b) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((b *),b)

b * is non empty functional FinSequence-membered FinSequenceSet of b

PFuncs ((b *),b) is non empty functional set

the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)

the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0

PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set

x is non empty Element of bool the carrier of a

(a,x) is Relation-like NAT -defined PFuncs ((x *),x) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((x *),x)

x * is non empty functional FinSequence-membered FinSequenceSet of x

PFuncs ((x *),x) is non empty functional set

y is non empty Element of bool the carrier of L

(L,y) is Relation-like NAT -defined PFuncs ((y *),y) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((y *),y)

y * is non empty functional FinSequence-membered FinSequenceSet of y

PFuncs ((y *),y) is non empty functional set

dom the charact of L is Element of bool NAT

dom (a,b) is Element of bool NAT

the charact of a is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of a *), the carrier of a) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of a *), the carrier of a)

the carrier of a * is non empty functional FinSequence-membered FinSequenceSet of the carrier of a

PFuncs (( the carrier of a *), the carrier of a) is non empty functional set

dom the charact of a is Element of bool NAT

(a) is non empty PFuncsDomHQN of the carrier of a

rng the charact of a is set

y is non empty Relation-like the carrier of a * -defined the carrier of a -valued Function-like homogeneous quasi_total Element of (a)

z is V29() V30() V31() V35() V36() V41() set

the charact of a . z is homogeneous set

(L) is non empty PFuncsDomHQN of the carrier of L

rng the charact of L is set

the charact of L . z is homogeneous set

u23 is non empty Relation-like the carrier of L * -defined the carrier of L -valued Function-like homogeneous quasi_total Element of (L)

dom u23 is functional FinSequence-membered V89() set

arity u23 is V29() V30() V31() V35() V36() V41() Element of NAT

(arity u23) -tuples_on the carrier of L is non empty functional FinSequence-membered FinSequenceSet of the carrier of L

dom (L,y) is Element of bool NAT

(U0) is non empty PFuncsDomHQN of the carrier of U0

rng the charact of U0 is set

the charact of U0 . z is homogeneous set

u12 is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)

dom u12 is functional FinSequence-membered V89() set

arity u12 is V29() V30() V31() V35() V36() V41() Element of NAT

(arity u12) -tuples_on the carrier of U0 is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0

dom y is functional FinSequence-membered V89() set

arity y is V29() V30() V31() V35() V36() V41() Element of NAT

(arity y) -tuples_on the carrier of a is non empty functional FinSequence-membered FinSequenceSet of the carrier of a

(arity y) -tuples_on b is non empty functional FinSequence-membered FinSequenceSet of b

y | ((arity y) -tuples_on b) is Relation-like the carrier of a * -defined the carrier of a -valued Function-like Element of bool [:( the carrier of a *), the carrier of a:]

[:( the carrier of a *), the carrier of a:] is non empty set

bool [:( the carrier of a *), the carrier of a:] is non empty set

dom (y | ((arity y) -tuples_on b)) is functional FinSequence-membered set

(dom y) /\ ((arity y) -tuples_on b) is set

(a,b,y) is non empty Relation-like b * -defined b -valued Function-like homogeneous quasi_total Element of bool [:(b *),b:]

[:(b *),b:] is non empty set

bool [:(b *),b:] is non empty set

(L,y,u23) is non empty Relation-like y * -defined y -valued Function-like homogeneous quasi_total Element of bool [:(y *),y:]

[:(y *),y:] is non empty set

bool [:(y *),y:] is non empty set

(arity u23) -tuples_on y is non empty functional FinSequence-membered FinSequenceSet of y

u23 | ((arity u23) -tuples_on y) is Relation-like the carrier of L * -defined the carrier of L -valued Function-like Element of bool [:( the carrier of L *), the carrier of L:]

[:( the carrier of L *), the carrier of L:] is non empty set

bool [:( the carrier of L *), the carrier of L:] is non empty set

(arity u12) -tuples_on y is non empty functional FinSequence-membered FinSequenceSet of y

((arity u23) -tuples_on the carrier of L) /\ ((arity u23) -tuples_on y) is set

C is Relation-like NAT -defined x -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of x

rng u12 is set

rng C is set

len C is V29() V30() V31() V35() V36() V41() Element of NAT

o1 is Relation-like NAT -defined b -valued Function-like V36() FinSequence-like FinSubsequence-like Element of b *

{ b

o0 is Relation-like NAT -defined the carrier of U0 -valued Function-like V36() FinSequence-like FinSubsequence-like Element of the carrier of U0 *

{ b

u12 . o0 is set

B is Relation-like NAT -defined y -valued Function-like V36() FinSequence-like FinSubsequence-like Element of y *

{ b

(u23 | ((arity u23) -tuples_on y)) . B is set

u23 . B is set

(y | ((arity y) -tuples_on b)) . o1 is set

y . C is set

dom the charact of U0 is Element of bool NAT

dom (a,x) is Element of bool NAT

y is V29() V30() V31() V35() V36() V41() set

the charact of a . y is homogeneous set

the charact of L . y is homogeneous set

z is non empty Relation-like the carrier of a * -defined the carrier of a -valued Function-like homogeneous quasi_total Element of (a)

u23 is non empty Relation-like the carrier of L * -defined the carrier of L -valued Function-like homogeneous quasi_total Element of (L)

(a,x) . y is set

(a,x,z) is non empty Relation-like x * -defined x -valued Function-like homogeneous quasi_total Element of bool [:(x *),x:]

[:(x *),x:] is non empty set

bool [:(x *),x:] is non empty set

arity z is V29() V30() V31() V35() V36() V41() Element of NAT

(arity z) -tuples_on x is non empty functional FinSequence-membered FinSequenceSet of x

z | ((arity z) -tuples_on x) is Relation-like the carrier of a * -defined the carrier of a -valued Function-like Element of bool [:( the carrier of a *), the carrier of a:]

(arity z) -tuples_on b is non empty functional FinSequence-membered FinSequenceSet of b

((arity z) -tuples_on b) /\ ((arity z) -tuples_on x) is set

z | (((arity z) -tuples_on b) /\ ((arity z) -tuples_on x)) is Relation-like the carrier of a * -defined the carrier of a -valued Function-like Element of bool [:( the carrier of a *), the carrier of a:]

z | ((arity z) -tuples_on b) is Relation-like the carrier of a * -defined the carrier of a -valued Function-like Element of bool [:( the carrier of a *), the carrier of a:]

(z | ((arity z) -tuples_on b)) | ((arity z) -tuples_on x) is Relation-like the carrier of a * -defined the carrier of a -valued Function-like Element of bool [:( the carrier of a *), the carrier of a:]

(a,b,z) is non empty Relation-like b * -defined b -valued Function-like homogeneous quasi_total Element of bool [:(b *),b:]

(a,b,z) | ((arity z) -tuples_on x) is Relation-like b * -defined b -valued Function-like Element of bool [:(b *),b:]

u23 | ((arity z) -tuples_on x) is Relation-like the carrier of L * -defined the carrier of L -valued Function-like Element of bool [:( the carrier of L *), the carrier of L:]

arity u23 is V29() V30() V31() V35() V36() V41() Element of NAT

(arity u23) -tuples_on y is non empty functional FinSequence-membered FinSequenceSet of y

u23 | ((arity u23) -tuples_on y) is Relation-like the carrier of L * -defined the carrier of L -valued Function-like Element of bool [:( the carrier of L *), the carrier of L:]

(L,y,u23) is non empty Relation-like y * -defined y -valued Function-like homogeneous quasi_total Element of bool [:(y *),y:]

the charact of U0 . y is homogeneous set

U0 is non empty V84() quasi_total non-empty UAStr

L is non empty V84() quasi_total non-empty UAStr

the carrier of L is non empty set

bool the carrier of L is non empty set

the carrier of U0 is non empty set

b is non empty Element of bool the carrier of L

(L,b) is Relation-like NAT -defined PFuncs ((b *),b) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((b *),b)

b * is non empty functional FinSequence-membered FinSequenceSet of b

PFuncs ((b *),b) is non empty functional set

dom (L,b) is Element of bool NAT

the charact of L is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of L *), the carrier of L) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of L *), the carrier of L)

the carrier of L * is non empty functional FinSequence-membered FinSequenceSet of the carrier of L

PFuncs (( the carrier of L *), the carrier of L) is non empty functional set

dom the charact of L is Element of bool NAT

x is V29() V30() V31() V35() V36() V41() set

the charact of L . x is homogeneous set

(L,b) . x is set

(L) is non empty PFuncsDomHQN of the carrier of L

rng the charact of L is set

y is non empty Relation-like the carrier of L * -defined the carrier of L -valued Function-like homogeneous quasi_total Element of (L)

(L,b,y) is non empty Relation-like b * -defined b -valued Function-like homogeneous quasi_total Element of bool [:(b *),b:]

[:(b *),b:] is non empty set

bool [:(b *),b:] is non empty set

bool the carrier of U0 is non empty set

a is non empty Element of bool the carrier of L

the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)

the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0

PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set

U0 is non empty V84() quasi_total non-empty UAStr

L is non empty V84() quasi_total non-empty (U0)

the carrier of L is non empty set

a is non empty V84() quasi_total non-empty (U0)

the carrier of a is non empty set

the charact of L is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of L *), the carrier of L) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of L *), the carrier of L)

the carrier of L * is non empty functional FinSequence-membered FinSequenceSet of the carrier of L

PFuncs (( the carrier of L *), the carrier of L) is non empty functional set

dom the charact of L is Element of bool NAT

the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)

the carrier of U0 is non empty set

the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0

PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set

dom the charact of U0 is Element of bool NAT

bool the carrier of U0 is non empty set

bool the carrier of a is non empty set

x is non empty Element of bool the carrier of a

(a,x) is Relation-like NAT -defined PFuncs ((x *),x) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((x *),x)

x * is non empty functional FinSequence-membered FinSequenceSet of x

PFuncs ((x *),x) is non empty functional set

the charact of a is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of a *), the carrier of a) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of a *), the carrier of a)

the carrier of a * is non empty functional FinSequence-membered FinSequenceSet of the carrier of a

PFuncs (( the carrier of a *), the carrier of a) is non empty functional set

y is non empty Element of bool the carrier of U0

(U0,y) is Relation-like NAT -defined PFuncs ((y *),y) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((y *),y)

y * is non empty functional FinSequence-membered FinSequenceSet of y

PFuncs ((y *),y) is non empty functional set

dom (a,x) is Element of bool NAT

dom the charact of a is Element of bool NAT

b is non empty Element of bool the carrier of U0

(a) is non empty PFuncsDomHQN of the carrier of a

rng the charact of a is set

y is non empty Relation-like the carrier of a * -defined the carrier of a -valued Function-like homogeneous quasi_total Element of (a)

z is Relation-like NAT -defined x -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of x

len z is V29() V30() V31() V35() V36() V41() Element of NAT

arity y is V29() V30() V31() V35() V36() V41() Element of NAT

y . z is set

u23 is V29() V30() V31() V35() V36() V41() set

the charact of a . u23 is homogeneous set

(U0) is non empty PFuncsDomHQN of the carrier of U0

rng the charact of U0 is set

the charact of U0 . u23 is homogeneous set

u12 is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)

arity u12 is V29() V30() V31() V35() V36() V41() Element of NAT

rng z is set

b * is non empty functional FinSequence-membered FinSequenceSet of b

(arity u12) -tuples_on y is non empty functional FinSequence-membered FinSequenceSet of y

(U0,y,u12) is non empty Relation-like y * -defined y -valued Function-like homogeneous quasi_total Element of bool [:(y *),y:]

[:(y *),y:] is non empty set

bool [:(y *),y:] is non empty set

u12 | ((arity u12) -tuples_on y) is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like Element of bool [:( the carrier of U0 *), the carrier of U0:]

[:( the carrier of U0 *), the carrier of U0:] is non empty set

bool [:( the carrier of U0 *), the carrier of U0:] is non empty set

{ b

C is Relation-like NAT -defined y -valued Function-like V36() FinSequence-like FinSubsequence-like Element of y *

B is Relation-like NAT -defined b -valued Function-like V36() FinSequence-like FinSubsequence-like Element of b *

u12 . B is set

(U0,b) is Relation-like NAT -defined PFuncs ((b *),b) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((b *),b)

b * is non empty functional FinSequence-membered FinSequenceSet of b

PFuncs ((b *),b) is non empty functional set

y is V29() V30() V31() V35() V36() V41() set

(U0) is non empty PFuncsDomHQN of the carrier of U0

rng the charact of U0 is set

the charact of U0 . y is homogeneous set

(a) is non empty PFuncsDomHQN of the carrier of a

rng the charact of a is set

the charact of a . y is homogeneous set

u23 is non empty Relation-like the carrier of a * -defined the carrier of a -valued Function-like homogeneous quasi_total Element of (a)

z is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)

(U0,y,z) is non empty Relation-like y * -defined y -valued Function-like homogeneous quasi_total Element of bool [:(y *),y:]

[:(y *),y:] is non empty set

bool [:(y *),y:] is non empty set

arity u23 is V29() V30() V31() V35() V36() V41() Element of NAT

arity z is V29() V30() V31() V35() V36() V41() Element of NAT

the charact of L . y is homogeneous set

(U0,b,z) is non empty Relation-like b * -defined b -valued Function-like homogeneous quasi_total Element of bool [:(b *),b:]

[:(b *),b:] is non empty set

bool [:(b *),b:] is non empty set

(arity z) -tuples_on b is non empty functional FinSequence-membered FinSequenceSet of b

z | ((arity z) -tuples_on b) is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like Element of bool [:( the carrier of U0 *), the carrier of U0:]

[:( the carrier of U0 *), the carrier of U0:] is non empty set

bool [:( the carrier of U0 *), the carrier of U0:] is non empty set

(arity z) -tuples_on y is non empty functional FinSequence-membered FinSequenceSet of y

((arity z) -tuples_on y) /\ ((arity z) -tuples_on b) is set

z | (((arity z) -tuples_on y) /\ ((arity z) -tuples_on b)) is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like Element of bool [:( the carrier of U0 *), the carrier of U0:]

z | ((arity z) -tuples_on y) is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like Element of bool [:( the carrier of U0 *), the carrier of U0:]

(arity z) -tuples_on x is non empty functional FinSequence-membered FinSequenceSet of x

(z | ((arity z) -tuples_on y)) | ((arity z) -tuples_on x) is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like Element of bool [:( the carrier of U0 *), the carrier of U0:]

(U0,y,z) | ((arity z) -tuples_on x) is Relation-like y * -defined y -valued Function-like Element of bool [:(y *),y:]

(a,x,u23) is non empty Relation-like x * -defined x -valued Function-like homogeneous quasi_total Element of bool [:(x *),x:]

[:(x *),x:] is non empty set

bool [:(x *),x:] is non empty set

(a,x) . y is set

U0 is non empty V84() quasi_total non-empty UAStr

L is non empty strict V84() quasi_total non-empty (U0)

the carrier of L is non empty set

a is non empty strict V84() quasi_total non-empty (U0)

the carrier of a is non empty set

U0 is non empty V84() quasi_total non-empty UAStr

L is non empty V84() quasi_total non-empty UAStr

signature U0 is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT

signature L is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT

dom (signature U0) is Element of bool NAT

len (signature U0) is V29() V30() V31() V35() V36() V41() Element of NAT

the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)

the carrier of U0 is non empty set

the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0

PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set

len the charact of U0 is non empty V29() V30() V31() V35() V36() V41() Element of NAT

dom the charact of U0 is Element of bool NAT

the carrier of L is non empty set

bool the carrier of L is non empty set

len (signature L) is V29() V30() V31() V35() V36() V41() Element of NAT

the charact of L is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of L *), the carrier of L) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of L *), the carrier of L)

the carrier of L * is non empty functional FinSequence-membered FinSequenceSet of the carrier of L

PFuncs (( the carrier of L *), the carrier of L) is non empty functional set

len the charact of L is non empty V29() V30() V31() V35() V36() V41() Element of NAT

dom (signature L) is Element of bool NAT

dom the charact of L is Element of bool NAT

y is non empty Element of bool the carrier of L

(L,y) is Relation-like NAT -defined PFuncs ((y *),y) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((y *),y)

y * is non empty functional FinSequence-membered FinSequenceSet of y

PFuncs ((y *),y) is non empty functional set

dom (L,y) is Element of bool NAT

y is V29() V30() V31() V35() V36() V41() set

(signature U0) . y is set

(signature L) . y is set

(U0) is non empty PFuncsDomHQN of the carrier of U0

rng the charact of U0 is set

the charact of U0 . y is homogeneous set

(L) is non empty PFuncsDomHQN of the carrier of L

rng the charact of L is set

the charact of L . y is homogeneous set

z is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)

arity z is V29() V30() V31() V35() V36() V41() Element of NAT

u23 is non empty Relation-like the carrier of L * -defined the carrier of L -valued Function-like homogeneous quasi_total Element of (L)

arity u23 is V29() V30() V31() V35() V36() V41() Element of NAT

U0 is non empty V84() quasi_total non-empty UAStr

the carrier of U0 is non empty set

bool the carrier of U0 is non empty set

L is non empty Element of bool the carrier of U0

(U0,L) is Relation-like NAT -defined PFuncs ((L *),L) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((L *),L)

L * is non empty functional FinSequence-membered FinSequenceSet of L

PFuncs ((L *),L) is non empty functional set

UAStr(# L,(U0,L) #) is non empty strict UAStr

the charact of UAStr(# L,(U0,L) #) is Relation-like NAT -defined PFuncs (( the carrier of UAStr(# L,(U0,L) #) *), the carrier of UAStr(# L,(U0,L) #)) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs (( the carrier of UAStr(# L,(U0,L) #) *), the carrier of UAStr(# L,(U0,L) #))

the carrier of UAStr(# L,(U0,L) #) is non empty set

the carrier of UAStr(# L,(U0,L) #) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of UAStr(# L,(U0,L) #)

PFuncs (( the carrier of UAStr(# L,(U0,L) #) *), the carrier of UAStr(# L,(U0,L) #)) is non empty functional set

dom the charact of UAStr(# L,(U0,L) #) is Element of bool NAT

the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)

the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0

PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set

dom the charact of U0 is Element of bool NAT

b is set

the charact of UAStr(# L,(U0,L) #) . b is set

(U0) is non empty PFuncsDomHQN of the carrier of U0

rng the charact of U0 is set

the charact of U0 . b is homogeneous set

x is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)

(U0,L,x) is non empty Relation-like L * -defined L -valued Function-like homogeneous quasi_total Element of bool [:(L *),L:]

[:(L *),L:] is non empty set

bool [:(L *),L:] is non empty set

[:( the carrier of UAStr(# L,(U0,L) #) *), the carrier of UAStr(# L,(U0,L) #):] is non empty set

bool [:( the carrier of UAStr(# L,(U0,L) #) *), the carrier of UAStr(# L,(U0,L) #):] is non empty set

b is V29() V30() V31() V35() V36() V41() set

the charact of UAStr(# L,(U0,L) #) . b is set

x is Relation-like the carrier of UAStr(# L,(U0,L) #) * -defined the carrier of UAStr(# L,(U0,L) #) -valued Function-like Element of bool [:( the carrier of UAStr(# L,(U0,L) #) *), the carrier of UAStr(# L,(U0,L) #):]

(U0) is non empty PFuncsDomHQN of the carrier of U0

rng the charact of U0 is set

the charact of U0 . b is homogeneous set

y is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)

(U0,L,y) is non empty Relation-like L * -defined L -valued Function-like homogeneous quasi_total Element of bool [:(L *),L:]

[:(L *),L:] is non empty set

bool [:(L *),L:] is non empty set

b is V29() V30() V31() V35() V36() V41() set

the charact of UAStr(# L,(U0,L) #) . b is set

x is Relation-like the carrier of UAStr(# L,(U0,L) #) * -defined the carrier of UAStr(# L,(U0,L) #) -valued Function-like Element of bool [:( the carrier of UAStr(# L,(U0,L) #) *), the carrier of UAStr(# L,(U0,L) #):]

(U0) is non empty PFuncsDomHQN of the carrier of U0

rng the charact of U0 is set

the charact of U0 . b is homogeneous set

y is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)

(U0,L,y) is non empty Relation-like L * -defined L -valued Function-like homogeneous quasi_total Element of bool [:(L *),L:]

[:(L *),L:] is non empty set

bool [:(L *),L:] is non empty set

U0 is non empty V84() quasi_total non-empty UAStr

the carrier of U0 is non empty set

bool the carrier of U0 is non empty set

L is non empty Element of bool the carrier of U0

(U0,L) is Relation-like NAT -defined PFuncs ((L *),L) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((L *),L)

L * is non empty functional FinSequence-membered FinSequenceSet of L

PFuncs ((L *),L) is non empty functional set

UAStr(# L,(U0,L) #) is non empty strict UAStr

a is non empty strict V84() quasi_total non-empty UAStr

the carrier of a is non empty set

the charact of a is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of a *), the carrier of a) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of a *), the carrier of a)

the carrier of a * is non empty functional FinSequence-membered FinSequenceSet of the carrier of a

PFuncs (( the carrier of a *), the carrier of a) is non empty functional set

b is non empty Element of bool the carrier of U0

(U0,b) is Relation-like NAT -defined PFuncs ((b *),b) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((b *),b)

b * is non empty functional FinSequence-membered FinSequenceSet of b

PFuncs ((b *),b) is non empty functional set

U0 is non empty V84() quasi_total non-empty UAStr

L is non empty V84() quasi_total non-empty (U0)

the carrier of L is non empty set

a is non empty V84() quasi_total non-empty (U0)

the carrier of a is non empty set

the carrier of L /\ the carrier of a is set

the carrier of U0 is non empty set

bool the carrier of U0 is non empty set

b is non empty Element of bool the carrier of U0

(U0,b) is Relation-like NAT -defined PFuncs ((b *),b) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((b *),b)

b * is non empty functional FinSequence-membered FinSequenceSet of b

PFuncs ((b *),b) is non empty functional set

UAStr(# b,(U0,b) #) is non empty strict UAStr

the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0

(U0) is non empty PFuncsDomHQN of the carrier of U0

the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)

PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set

rng the charact of U0 is set

u23 is Relation-like NAT -defined b -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of b

len u23 is V29() V30() V31() V35() V36() V41() Element of NAT

y is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)

arity y is V29() V30() V31() V35() V36() V41() Element of NAT

o0 is non empty Element of bool the carrier of U0

u12 is Relation-like NAT -defined the carrier of a -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of the carrier of a

y . u12 is set

B is non empty Element of bool the carrier of U0

C is Relation-like NAT -defined the carrier of L -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of the carrier of L

y . C is set

y . u23 is set

the carrier of UAStr(# b,(U0,b) #) is non empty set

the charact of UAStr(# b,(U0,b) #) is Relation-like NAT -defined PFuncs (( the carrier of UAStr(# b,(U0,b) #) *), the carrier of UAStr(# b,(U0,b) #)) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs (( the carrier of UAStr(# b,(U0,b) #) *), the carrier of UAStr(# b,(U0,b) #))

the carrier of UAStr(# b,(U0,b) #) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of UAStr(# b,(U0,b) #)

PFuncs (( the carrier of UAStr(# b,(U0,b) #) *), the carrier of UAStr(# b,(U0,b) #)) is non empty functional set

y is non empty Element of bool the carrier of U0

(U0,y) is Relation-like NAT -defined PFuncs ((y *),y) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((y *),y)

y * is non empty functional FinSequence-membered FinSequenceSet of y

PFuncs ((y *),y) is non empty functional set

y is non empty V84() quasi_total non-empty UAStr

y is non empty strict V84() quasi_total non-empty (U0)

the carrier of y is non empty set

the charact of y is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of y *), the carrier of y) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of y *), the carrier of y)

the carrier of y * is non empty functional FinSequence-membered FinSequenceSet of the carrier of y

PFuncs (( the carrier of y *), the carrier of y) is non empty functional set

z is non empty Element of bool the carrier of U0

(U0,z) is Relation-like NAT -defined PFuncs ((z *),z) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((z *),z)

z * is non empty functional FinSequence-membered FinSequenceSet of z

PFuncs ((z *),z) is non empty functional set

x is non empty strict V84() quasi_total non-empty (U0)

the carrier of x is non empty set

the charact of x is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of x *), the carrier of x) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of x *), the carrier of x)

the carrier of x * is non empty functional FinSequence-membered FinSequenceSet of the carrier of x

PFuncs (( the carrier of x *), the carrier of x) is non empty functional set

y is non empty strict V84() quasi_total non-empty (U0)

the carrier of y is non empty set

the charact of y is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of y *), the carrier of y) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of y *), the carrier of y)

the carrier of y * is non empty functional FinSequence-membered FinSequenceSet of the carrier of y

PFuncs (( the carrier of y *), the carrier of y) is non empty functional set

b is non empty Element of bool the carrier of U0

(U0,b) is Relation-like NAT -defined PFuncs ((b *),b) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((b *),b)

b * is non empty functional FinSequence-membered FinSequenceSet of b

PFuncs ((b *),b) is non empty functional set

U0 is non empty V84() quasi_total non-empty UAStr

the carrier of U0 is non empty set

the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0

(U0) is non empty PFuncsDomHQN of the carrier of U0

the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)

PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set

rng the charact of U0 is set

{ b

( arity b

bool the carrier of U0 is non empty set

a is set

b is Element of the carrier of U0

x is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)

arity x is V29() V30() V31() V35() V36() V41() Element of NAT

rng x is set

the non empty set is non empty set

the Element of the non empty set is Element of the non empty set

the non empty set * is non empty functional FinSequence-membered FinSequenceSet of the non empty set

PFuncs (( the non empty set *), the non empty set ) is non empty functional set

<*> the non empty set is empty proper Relation-like NAT -defined the non empty set -valued Function-like functional V29() V30() V31() V33() V34() V35() V36() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V89() FinSequence of the non empty set

[:NAT, the non empty set :] is non empty V36() set

(<*> the non empty set ) .--> the Element of the non empty set is set

{(<*> the non empty set )} is non empty trivial V43(1) set

{(<*> the non empty set )} --> the Element of the non empty set is Relation-like {(<*> the non empty set )} -defined { the Element of the non empty set } -valued Function-like V21({(<*> the non empty set )},{ the Element of the non empty set }) Element of bool [:{(<*> the non empty set )},{ the Element of the non empty set }:]

{ the Element of the non empty set } is non empty trivial V43(1) set

[:{(<*> the non empty set )},{ the Element of the non empty set }:] is non empty set

bool [:{(<*> the non empty set )},{ the Element of the non empty set }:] is non empty set

a is Element of PFuncs (( the non empty set *), the non empty set )

<*a*> is non empty trivial Relation-like NAT -defined PFuncs (( the non empty set *), the non empty set ) -valued Function-like V36() V43(1) FinSequence-like FinSubsequence-like FinSequence of PFuncs (( the non empty set *), the non empty set )

UAStr(# the non empty set ,<*a*> #) is non empty strict UAStr

the carrier of UAStr(# the non empty set ,<*a*> #) is non empty set

the charact of UAStr(# the non empty set ,<*a*> #) is Relation-like NAT -defined PFuncs (( the carrier of UAStr(# the non empty set ,<*a*> #) *), the carrier of UAStr(# the non empty set ,<*a*> #)) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs (( the carrier of UAStr(# the non empty set ,<*a*> #) *), the carrier of UAStr(# the non empty set ,<*a*> #))

the carrier of UAStr(# the non empty set ,<*a*> #) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of UAStr(# the non empty set ,<*a*> #)

PFuncs (( the carrier of UAStr(# the non empty set ,<*a*> #) *), the carrier of UAStr(# the non empty set ,<*a*> #)) is non empty functional set

x is non empty V84() quasi_total non-empty UAStr

dom <*a*> is Element of bool NAT

the carrier of x is non empty set

the carrier of x * is non empty functional FinSequence-membered FinSequenceSet of the carrier of x

(x) is non empty PFuncsDomHQN of the carrier of x

the charact of x is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of x *), the carrier of x) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of x *), the carrier of x)

PFuncs (( the carrier of x *), the carrier of x) is non empty functional set

rng the charact of x is set

the charact of x . 1 is homogeneous set

y is non empty Relation-like the carrier of x * -defined the carrier of x -valued Function-like homogeneous quasi_total Element of (x)

dom y is functional FinSequence-membered V89() set

y is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set

len y is V29() V30() V31() V35() V36() V41() Element of NAT

arity y is V29() V30() V31() V35() V36() V41() Element of NAT

U0 is non empty V84() quasi_total non-empty () UAStr

(U0) is Element of bool the carrier of U0

the carrier of U0 is non empty set

bool the carrier of U0 is non empty set

the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0

(U0) is non empty PFuncsDomHQN of the carrier of U0

the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)

PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set

rng the charact of U0 is set

{ b

( arity b

L is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)

arity L is V29() V30() V31() V35() V36() V41() Element of NAT

dom L is functional FinSequence-membered V89() set

0 -tuples_on the carrier of U0 is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0

<*> the carrier of U0 is empty proper Relation-like NAT -defined the carrier of U0 -valued Function-like functional V29() V30() V31() V33() V34() V35() V36() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V89() FinSequence of the carrier of U0

[:NAT, the carrier of U0:] is non empty V36() set

{(<*> the carrier of U0)} is non empty trivial V43(1) set

L . (<*> the carrier of U0) is set

rng L is set

a is Element of the carrier of U0

U0 is non empty V84() quasi_total non-empty UAStr

(U0) is Element of bool the carrier of U0

the carrier of U0 is non empty set

bool the carrier of U0 is non empty set

the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0

(U0) is non empty PFuncsDomHQN of the carrier of U0

the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)

PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set

rng the charact of U0 is set

{ b

( arity b

L is non empty V84() quasi_total non-empty (U0)

the carrier of L is non empty set

bool the carrier of L is non empty set

x is set

y is Element of the carrier of U0

y is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)

arity y is V29() V30() V31() V35() V36() V41() Element of NAT

rng y is set

y is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)

arity y is V29() V30() V31() V35() V36() V41() Element of NAT

rng y is set

dom y is functional FinSequence-membered V89() set

z is set

y . z is set

0 -tuples_on the carrier of U0 is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0

<*> the carrier of U0 is empty proper Relation-like NAT -defined the carrier of U0 -valued Function-like functional V29() V30() V31() V33() V34() V35() V36() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V89() FinSequence of the carrier of U0

[:NAT, the carrier of U0:] is non empty V36() set

{(<*> the carrier of U0)} is non empty trivial V43(1) set

b is non empty Element of bool the carrier of U0

<*> b is empty proper Relation-like NAT -defined b -valued Function-like functional V29() V30() V31() V33() V34() V35() V36() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V89() FinSequence of b

[:NAT,b:] is non empty V36() set

{(<*> b)} is non empty trivial V43(1) set

0 -tuples_on b is non empty functional FinSequence-membered FinSequenceSet of b

(arity y) -tuples_on b is non empty functional FinSequence-membered FinSequenceSet of b

(dom y) /\ ((arity y) -tuples_on b) is set

y | ((arity y) -tuples_on b) is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like Element of bool [:( the carrier of U0 *), the carrier of U0:]

[:( the carrier of U0 *), the carrier of U0:] is non empty set

bool [:( the carrier of U0 *), the carrier of U0:] is non empty set

dom (y | ((arity y) -tuples_on b)) is functional FinSequence-membered set

dom the charact of U0 is Element of bool NAT

u23 is V29() V30() V31() V35() V36() V41() set

the charact of U0 . u23 is homogeneous set

the charact of L is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of L *), the carrier of L) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of L *), the carrier of L)

the carrier of L * is non empty functional FinSequence-membered FinSequenceSet of the carrier of L

PFuncs (( the carrier of L *), the carrier of L) is non empty functional set

dom the charact of L is Element of bool NAT

(L) is non empty PFuncsDomHQN of the carrier of L

rng the charact of L is set

the charact of L . u23 is homogeneous set

(U0,b) is Relation-like NAT -defined PFuncs ((b *),b) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((b *),b)

b * is non empty functional FinSequence-membered FinSequenceSet of b

PFuncs ((b *),b) is non empty functional set

u12 is non empty Relation-like the carrier of L * -defined the carrier of L -valued Function-like homogeneous quasi_total Element of (L)

(U0,b,y) is non empty Relation-like b * -defined b -valued Function-like homogeneous quasi_total Element of bool [:(b *),b:]

[:(b *),b:] is non empty set

bool [:(b *),b:] is non empty set

dom (U0,b,y) is functional FinSequence-membered V89() set

u12 . z is set

rng u12 is set

(y | ((arity y) -tuples_on b)) . z is set

U0 is non empty V84() quasi_total non-empty () UAStr

(U0) is non empty Element of bool the carrier of U0

the carrier of U0 is non empty set

bool the carrier of U0 is non empty set

the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0

(U0) is non empty PFuncsDomHQN of the carrier of U0

the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)

PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set

rng the charact of U0 is set

{ b