:: PRALG_1 semantic presentation

NAT is non empty V24() V25() V26() V31() V36() V37() countable denumerable Element of bool REAL

REAL is set

bool REAL is non empty set

1 is non empty set

[:1,1:] is Relation-like non empty set

bool [:1,1:] is non empty set

[:[:1,1:],1:] is Relation-like non empty set

bool [:[:1,1:],1:] is non empty set

NAT is non empty V24() V25() V26() V31() V36() V37() countable denumerable set

bool NAT is non empty V31() set

bool NAT is non empty V31() set

K249() is non empty set

0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V24() V25() V26() V28() V29() V30() V31() V36() V38( {} ) Cardinal-yielding with_common_domain countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT

{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V24() V25() V26() V28() V29() V30() V31() V36() V38( {} ) Cardinal-yielding with_common_domain countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence-membered set

the Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V24() V25() V26() V28() V29() V30() V31() V36() V38( {} ) Cardinal-yielding with_common_domain countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence-membered set is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V24() V25() V26() V28() V29() V30() V31() V36() V38( {} ) Cardinal-yielding with_common_domain countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence-membered set

{0,1} is non empty set

{{},1} is non empty set

K317() is set

bool K317() is non empty set

K318() is Element of bool K317()

K358() is non empty V110() L10()

the carrier of K358() is non empty set

K321( the carrier of K358()) is non empty M25( the carrier of K358())

K357(K358()) is Element of bool K321( the carrier of K358())

bool K321( the carrier of K358()) is non empty set

[:K357(K358()),NAT:] is Relation-like set

bool [:K357(K358()),NAT:] is non empty set

[:NAT,K357(K358()):] is Relation-like set

bool [:NAT,K357(K358()):] is non empty set

2 is non empty set

3 is non empty set

J is non empty set

A is non empty set

[:J,A:] is Relation-like non empty set

j is Relation-like NAT -defined [:J,A:] -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of [:J,A:]

pr1 j is Relation-like Function-like set

len j is V24() V25() V26() V30() V31() V36() countable Element of NAT

ua is Relation-like NAT -defined J -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of J

len ua is V24() V25() V26() V30() V31() V36() countable Element of NAT

dom ua is countable Element of bool NAT

pr1 j is Relation-like NAT -defined J -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of J

dom j is countable Element of bool NAT

pr is V24() V25() V26() V30() V31() V36() countable set

ua . pr is set

j . pr is set

(j . pr) `1 is set

pr is set

ua . pr is set

j . pr is set

(j . pr) `1 is set

pr1 j is Relation-like NAT -defined J -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of J

pr2 j is Relation-like Function-like set

ua is Relation-like NAT -defined A -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of A

len ua is V24() V25() V26() V30() V31() V36() countable Element of NAT

dom ua is countable Element of bool NAT

pr2 j is Relation-like NAT -defined A -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of A

dom j is countable Element of bool NAT

pr is V24() V25() V26() V30() V31() V36() countable set

ua . pr is set

j . pr is set

(j . pr) `2 is set

pr is set

ua . pr is set

j . pr is set

(j . pr) `2 is set

pr2 j is Relation-like NAT -defined A -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of A

J is non empty set

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

[:(J *),J:] is Relation-like non empty set

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

A is non empty set

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

[:(A *),A:] is Relation-like non empty set

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

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

arity j is V24() V25() V26() V30() V31() V36() countable Element of NAT

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

arity ua is V24() V25() V26() V30() V31() V36() countable Element of NAT

[:J,A:] is Relation-like non empty set

[:J,A:] * is functional non empty FinSequence-membered FinSequenceSet of [:J,A:]

[:([:J,A:] *),[:J,A:]:] is Relation-like non empty set

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

(arity j) -tuples_on [:J,A:] is functional non empty FinSequence-membered FinSequenceSet of [:J,A:]

{ b

proj1 ua is functional non empty with_common_domain FinSequence-membered set

(arity ua) -tuples_on A is functional non empty FinSequence-membered FinSequenceSet of A

{ b

proj2 j is non empty set

proj2 ua is non empty set

proj1 j is functional non empty with_common_domain FinSequence-membered set

(arity j) -tuples_on J is functional non empty FinSequence-membered FinSequenceSet of J

{ b

n9 is set

o is set

j is Relation-like NAT -defined [:J,A:] -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of [:J,A:] *

len j is V24() V25() V26() V30() V31() V36() countable Element of NAT

(J,A,j) is Relation-like NAT -defined J -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of J

len (J,A,j) is V24() V25() V26() V30() V31() V36() countable Element of NAT

o is Relation-like NAT -defined J -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of J *

j . o is set

(J,A,j) is Relation-like NAT -defined A -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of A

len (J,A,j) is V24() V25() V26() V30() V31() V36() countable Element of NAT

o1 is Relation-like NAT -defined A -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of A *

ua . o1 is set

j . (J,A,j) is set

ua . (J,A,j) is set

[(j . (J,A,j)),(ua . (J,A,j))] is V15() set

{(j . (J,A,j)),(ua . (J,A,j))} is non empty set

{(j . (J,A,j))} is non empty trivial V38(1) set

{{(j . (J,A,j)),(ua . (J,A,j))},{(j . (J,A,j))}} is non empty set

n9 is set

o is set

j is set

o is Relation-like NAT -defined [:J,A:] -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of [:J,A:] *

len o is V24() V25() V26() V30() V31() V36() countable Element of NAT

(J,A,o) is Relation-like NAT -defined J -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of J

j . (J,A,o) is set

(J,A,o) is Relation-like NAT -defined A -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of A

ua . (J,A,o) is set

[(j . (J,A,o)),(ua . (J,A,o))] is V15() set

{(j . (J,A,o)),(ua . (J,A,o))} is non empty set

{(j . (J,A,o))} is non empty trivial V38(1) set

{{(j . (J,A,o)),(ua . (J,A,o))},{(j . (J,A,o))}} is non empty set

[:((arity j) -tuples_on [:J,A:]),[:J,A:]:] is Relation-like non empty set

bool [:((arity j) -tuples_on [:J,A:]),[:J,A:]:] is non empty set

n9 is Relation-like (arity j) -tuples_on [:J,A:] -defined [:J,A:] -valued Function-like Element of bool [:((arity j) -tuples_on [:J,A:]),[:J,A:]:]

proj1 n9 is set

o is set

o is set

j is Relation-like NAT -defined [:J,A:] -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of [:J,A:] *

len j is V24() V25() V26() V30() V31() V36() countable Element of NAT

(J,A,j) is Relation-like NAT -defined J -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of J

j . (J,A,j) is set

(J,A,j) is Relation-like NAT -defined A -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of A

ua . (J,A,j) is set

[(j . (J,A,j)),(ua . (J,A,j))] is V15() set

{(j . (J,A,j)),(ua . (J,A,j))} is non empty set

{(j . (J,A,j))} is non empty trivial V38(1) set

{{(j . (J,A,j)),(ua . (J,A,j))},{(j . (J,A,j))}} is non empty set

o1 is Relation-like NAT -defined [:J,A:] -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of [:J,A:]

o is V15() set

(J,A,o1) is Relation-like NAT -defined J -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of J

j . (J,A,o1) is set

(J,A,o1) is Relation-like NAT -defined A -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of A

ua . (J,A,o1) is set

[(j . (J,A,o1)),(ua . (J,A,o1))] is V15() set

{(j . (J,A,o1)),(ua . (J,A,o1))} is non empty set

{(j . (J,A,o1))} is non empty trivial V38(1) set

{{(j . (J,A,o1)),(ua . (J,A,o1))},{(j . (J,A,o1))}} is non empty set

o is V15() set

{ (b

union { (b

o is Relation-like [:J,A:] * -defined [:J,A:] -valued Function-like Element of bool [:([:J,A:] *),[:J,A:]:]

j is Relation-like NAT -defined [:J,A:] -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of [:J,A:]

len j is V24() V25() V26() V30() V31() V36() countable Element of NAT

o is Relation-like NAT -defined [:J,A:] -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of [:J,A:]

len o is V24() V25() V26() V30() V31() V36() countable Element of NAT

proj1 o is functional FinSequence-membered set

o1 is Relation-like NAT -defined [:J,A:] -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of [:J,A:] *

x1 is Relation-like NAT -defined [:J,A:] -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of [:J,A:] *

len x1 is V24() V25() V26() V30() V31() V36() countable Element of NAT

j is Relation-like NAT -defined Function-like V31() countable FinSequence-like FinSubsequence-like set

proj1 o is functional FinSequence-membered set

o is Relation-like NAT -defined Function-like V31() countable FinSequence-like FinSubsequence-like set

len j is V24() V25() V26() V30() V31() V36() countable Element of NAT

len o is V24() V25() V26() V30() V31() V36() countable Element of NAT

o1 is Relation-like NAT -defined [:J,A:] -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of [:J,A:] *

len o1 is V24() V25() V26() V30() V31() V36() countable Element of NAT

x1 is Relation-like NAT -defined [:J,A:] -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of [:J,A:] *

len x1 is V24() V25() V26() V30() V31() V36() countable Element of NAT

j is Relation-like [:J,A:] * -defined [:J,A:] -valued Function-like non empty homogeneous quasi_total Element of bool [:([:J,A:] *),[:J,A:]:]

proj1 j is functional non empty with_common_domain FinSequence-membered set

o is Relation-like NAT -defined [:J,A:] -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of [:J,A:]

j . o is set

(J,A,o) is Relation-like NAT -defined J -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of J

j . (J,A,o) is set

(J,A,o) is Relation-like NAT -defined A -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of A

ua . (J,A,o) is set

[(j . (J,A,o)),(ua . (J,A,o))] is V15() set

{(j . (J,A,o)),(ua . (J,A,o))} is non empty set

{(j . (J,A,o))} is non empty trivial V38(1) set

{{(j . (J,A,o)),(ua . (J,A,o))},{(j . (J,A,o))}} is non empty set

pr is Relation-like [:J,A:] * -defined [:J,A:] -valued Function-like non empty homogeneous quasi_total Element of bool [:([:J,A:] *),[:J,A:]:]

proj1 pr is functional non empty with_common_domain FinSequence-membered set

n is Relation-like [:J,A:] * -defined [:J,A:] -valued Function-like non empty homogeneous quasi_total Element of bool [:([:J,A:] *),[:J,A:]:]

proj1 n is functional non empty with_common_domain FinSequence-membered set

n9 is Relation-like NAT -defined [:J,A:] -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of [:J,A:] *

o is Relation-like NAT -defined [:J,A:] -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of [:J,A:]

pr . o is set

(J,A,o) is Relation-like NAT -defined J -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of J

j . (J,A,o) is set

(J,A,o) is Relation-like NAT -defined A -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of A

ua . (J,A,o) is set

[(j . (J,A,o)),(ua . (J,A,o))] is V15() set

{(j . (J,A,o)),(ua . (J,A,o))} is non empty set

{(j . (J,A,o))} is non empty trivial V38(1) set

{{(j . (J,A,o)),(ua . (J,A,o))},{(j . (J,A,o))}} is non empty set

pr . n9 is set

n . n9 is set

J is non empty V88() quasi_total non-empty UAStr

A is non empty V88() quasi_total non-empty UAStr

the carrier of J is non empty set

the carrier of A is non empty set

[: the carrier of J, the carrier of A:] is Relation-like non empty set

[: the carrier of J, the carrier of A:] * is functional non empty FinSequence-membered FinSequenceSet of [: the carrier of J, the carrier of A:]

PFuncs (([: the carrier of J, the carrier of A:] *),[: the carrier of J, the carrier of A:]) is functional non empty set

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

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

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

len the charact of J is non empty V24() V25() V26() V30() V31() V36() countable Element of NAT

[:( the carrier of J *), the carrier of J:] is Relation-like non empty set

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

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

[:( the carrier of A *), the carrier of A:] is Relation-like non empty set

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

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

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

dom the charact of A is non empty countable Element of bool NAT

len the charact of A is non empty V24() V25() V26() V30() V31() V36() countable Element of NAT

Seg (len the charact of A) is non empty V31() V38( len the charact of A) countable Element of bool NAT

Seg (len the charact of J) is non empty V31() V38( len the charact of J) countable Element of bool NAT

dom the charact of J is non empty countable Element of bool NAT

pr is V24() V25() V26() V30() V31() V36() countable set

the charact of J . pr is Relation-like Function-like homogeneous set

the charact of A . pr is Relation-like Function-like homogeneous set

n is Relation-like the carrier of J * -defined the carrier of J -valued Function-like non empty homogeneous quasi_total Element of bool [:( the carrier of J *), the carrier of J:]

n9 is Relation-like the carrier of A * -defined the carrier of A -valued Function-like non empty homogeneous quasi_total Element of bool [:( the carrier of A *), the carrier of A:]

( the carrier of J, the carrier of A,n,n9) is Relation-like [: the carrier of J, the carrier of A:] * -defined [: the carrier of J, the carrier of A:] -valued Function-like non empty homogeneous quasi_total Element of bool [:([: the carrier of J, the carrier of A:] *),[: the carrier of J, the carrier of A:]:]

[:([: the carrier of J, the carrier of A:] *),[: the carrier of J, the carrier of A:]:] is Relation-like non empty set

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

o is Relation-like Function-like Element of PFuncs (([: the carrier of J, the carrier of A:] *),[: the carrier of J, the carrier of A:])

j is Relation-like the carrier of J * -defined the carrier of J -valued Function-like non empty homogeneous quasi_total Element of bool [:( the carrier of J *), the carrier of J:]

o is Relation-like the carrier of A * -defined the carrier of A -valued Function-like non empty homogeneous quasi_total Element of bool [:( the carrier of A *), the carrier of A:]

( the carrier of J, the carrier of A,j,o) is Relation-like [: the carrier of J, the carrier of A:] * -defined [: the carrier of J, the carrier of A:] -valued Function-like non empty homogeneous quasi_total Element of bool [:([: the carrier of J, the carrier of A:] *),[: the carrier of J, the carrier of A:]:]

pr is Relation-like NAT -defined PFuncs (([: the carrier of J, the carrier of A:] *),[: the carrier of J, the carrier of A:]) -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence of PFuncs (([: the carrier of J, the carrier of A:] *),[: the carrier of J, the carrier of A:])

dom pr is countable Element of bool NAT

n is Relation-like NAT -defined PFuncs (([: the carrier of J, the carrier of A:] *),[: the carrier of J, the carrier of A:]) -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence of PFuncs (([: the carrier of J, the carrier of A:] *),[: the carrier of J, the carrier of A:])

len n is V24() V25() V26() V30() V31() V36() countable Element of NAT

dom n is countable Element of bool NAT

n9 is V24() V25() V26() V30() V31() V36() countable set

the charact of J . n9 is Relation-like Function-like homogeneous set

the charact of A . n9 is Relation-like Function-like homogeneous set

n . n9 is Relation-like Function-like set

o is Relation-like the carrier of J * -defined the carrier of J -valued Function-like non empty homogeneous quasi_total Element of bool [:( the carrier of J *), the carrier of J:]

j is Relation-like the carrier of A * -defined the carrier of A -valued Function-like non empty homogeneous quasi_total Element of bool [:( the carrier of A *), the carrier of A:]

( the carrier of J, the carrier of A,o,j) is Relation-like [: the carrier of J, the carrier of A:] * -defined [: the carrier of J, the carrier of A:] -valued Function-like non empty homogeneous quasi_total Element of bool [:([: the carrier of J, the carrier of A:] *),[: the carrier of J, the carrier of A:]:]

[:([: the carrier of J, the carrier of A:] *),[: the carrier of J, the carrier of A:]:] is Relation-like non empty set

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

j is Relation-like NAT -defined PFuncs (([: the carrier of J, the carrier of A:] *),[: the carrier of J, the carrier of A:]) -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence of PFuncs (([: the carrier of J, the carrier of A:] *),[: the carrier of J, the carrier of A:])

len j is V24() V25() V26() V30() V31() V36() countable Element of NAT

dom j is countable Element of bool NAT

ua is Relation-like NAT -defined PFuncs (([: the carrier of J, the carrier of A:] *),[: the carrier of J, the carrier of A:]) -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence of PFuncs (([: the carrier of J, the carrier of A:] *),[: the carrier of J, the carrier of A:])

len ua is V24() V25() V26() V30() V31() V36() countable Element of NAT

dom ua is countable Element of bool NAT

Seg (len the charact of J) is non empty V31() V38( len the charact of J) countable Element of bool NAT

pr is V24() V25() V26() V30() V31() V36() countable set

dom the charact of J is non empty countable Element of bool NAT

the charact of J . pr is Relation-like Function-like homogeneous set

len the charact of A is non empty V24() V25() V26() V30() V31() V36() countable Element of NAT

Seg (len the charact of A) is non empty V31() V38( len the charact of A) countable Element of bool NAT

dom the charact of A is non empty countable Element of bool NAT

the charact of A . pr is Relation-like Function-like homogeneous set

j . pr is Relation-like Function-like set

n is Relation-like the carrier of J * -defined the carrier of J -valued Function-like non empty homogeneous quasi_total Element of bool [:( the carrier of J *), the carrier of J:]

n9 is Relation-like the carrier of A * -defined the carrier of A -valued Function-like non empty homogeneous quasi_total Element of bool [:( the carrier of A *), the carrier of A:]

( the carrier of J, the carrier of A,n,n9) is Relation-like [: the carrier of J, the carrier of A:] * -defined [: the carrier of J, the carrier of A:] -valued Function-like non empty homogeneous quasi_total Element of bool [:([: the carrier of J, the carrier of A:] *),[: the carrier of J, the carrier of A:]:]

[:([: the carrier of J, the carrier of A:] *),[: the carrier of J, the carrier of A:]:] is Relation-like non empty set

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

ua . pr is Relation-like Function-like set

J is non empty V88() quasi_total non-empty UAStr

the carrier of J is non empty set

A is non empty V88() quasi_total non-empty UAStr

the carrier of A is non empty set

[: the carrier of J, the carrier of A:] is Relation-like non empty set

(J,A) is Relation-like NAT -defined PFuncs (([: the carrier of J, the carrier of A:] *),[: the carrier of J, the carrier of A:]) -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence of PFuncs (([: the carrier of J, the carrier of A:] *),[: the carrier of J, the carrier of A:])

[: the carrier of J, the carrier of A:] * is functional non empty FinSequence-membered FinSequenceSet of [: the carrier of J, the carrier of A:]

PFuncs (([: the carrier of J, the carrier of A:] *),[: the carrier of J, the carrier of A:]) is functional non empty set

UAStr(# [: the carrier of J, the carrier of A:],(J,A) #) is non empty strict UAStr

dom (J,A) is countable Element of bool NAT

len (J,A) is V24() V25() V26() V30() V31() V36() countable Element of NAT

Seg (len (J,A)) is V31() V38( len (J,A)) countable Element of bool NAT

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

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

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

dom the charact of A is non empty countable Element of bool NAT

len the charact of A is non empty V24() V25() V26() V30() V31() V36() countable Element of NAT

Seg (len the charact of A) is non empty V31() V38( len the charact of A) countable Element of bool NAT

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

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

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

len the charact of J is non empty V24() V25() V26() V30() V31() V36() countable Element of NAT

dom the charact of J is non empty countable Element of bool NAT

Seg (len the charact of J) is non empty V31() V38( len the charact of J) countable Element of bool NAT

the carrier of UAStr(# [: the carrier of J, the carrier of A:],(J,A) #) is non empty set

the charact of UAStr(# [: the carrier of J, the carrier of A:],(J,A) #) is Relation-like NAT -defined PFuncs (( the carrier of UAStr(# [: the carrier of J, the carrier of A:],(J,A) #) *), the carrier of UAStr(# [: the carrier of J, the carrier of A:],(J,A) #)) -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence of PFuncs (( the carrier of UAStr(# [: the carrier of J, the carrier of A:],(J,A) #) *), the carrier of UAStr(# [: the carrier of J, the carrier of A:],(J,A) #))

the carrier of UAStr(# [: the carrier of J, the carrier of A:],(J,A) #) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of UAStr(# [: the carrier of J, the carrier of A:],(J,A) #)

PFuncs (( the carrier of UAStr(# [: the carrier of J, the carrier of A:],(J,A) #) *), the carrier of UAStr(# [: the carrier of J, the carrier of A:],(J,A) #)) is functional non empty set

[:( the carrier of UAStr(# [: the carrier of J, the carrier of A:],(J,A) #) *), the carrier of UAStr(# [: the carrier of J, the carrier of A:],(J,A) #):] is Relation-like non empty set

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

ua is V24() V25() V26() V30() V31() V36() countable set

dom the charact of UAStr(# [: the carrier of J, the carrier of A:],(J,A) #) is countable Element of bool NAT

the charact of UAStr(# [: the carrier of J, the carrier of A:],(J,A) #) . ua is Relation-like Function-like set

pr is Relation-like the carrier of UAStr(# [: the carrier of J, the carrier of A:],(J,A) #) * -defined the carrier of UAStr(# [: the carrier of J, the carrier of A:],(J,A) #) -valued Function-like Element of bool [:( the carrier of UAStr(# [: the carrier of J, the carrier of A:],(J,A) #) *), the carrier of UAStr(# [: the carrier of J, the carrier of A:],(J,A) #):]

[:( the carrier of A *), the carrier of A:] is Relation-like non empty set

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

the charact of A . ua is Relation-like Function-like homogeneous set

[:( the carrier of J *), the carrier of J:] is Relation-like non empty set

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

the charact of J . ua is Relation-like Function-like homogeneous set

n9 is Relation-like the carrier of J * -defined the carrier of J -valued Function-like non empty homogeneous quasi_total Element of bool [:( the carrier of J *), the carrier of J:]

n is Relation-like the carrier of A * -defined the carrier of A -valued Function-like non empty homogeneous quasi_total Element of bool [:( the carrier of A *), the carrier of A:]

( the carrier of J, the carrier of A,n9,n) is Relation-like [: the carrier of J, the carrier of A:] * -defined [: the carrier of J, the carrier of A:] -valued Function-like non empty homogeneous quasi_total Element of bool [:([: the carrier of J, the carrier of A:] *),[: the carrier of J, the carrier of A:]:]

[:([: the carrier of J, the carrier of A:] *),[: the carrier of J, the carrier of A:]:] is Relation-like non empty set

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

ua is set

proj1 the charact of UAStr(# [: the carrier of J, the carrier of A:],(J,A) #) is set

the charact of UAStr(# [: the carrier of J, the carrier of A:],(J,A) #) . ua is Relation-like Function-like set

dom the charact of UAStr(# [: the carrier of J, the carrier of A:],(J,A) #) is countable Element of bool NAT

[:( the carrier of A *), the carrier of A:] is Relation-like non empty set

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

n is V24() V25() V26() V30() V31() V36() countable Element of NAT

the charact of A . n is Relation-like Function-like homogeneous set

[:( the carrier of J *), the carrier of J:] is Relation-like non empty set

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

the charact of J . n is Relation-like Function-like homogeneous set

o is Relation-like the carrier of J * -defined the carrier of J -valued Function-like non empty homogeneous quasi_total Element of bool [:( the carrier of J *), the carrier of J:]

n9 is Relation-like the carrier of A * -defined the carrier of A -valued Function-like non empty homogeneous quasi_total Element of bool [:( the carrier of A *), the carrier of A:]

( the carrier of J, the carrier of A,o,n9) is Relation-like [: the carrier of J, the carrier of A:] * -defined [: the carrier of J, the carrier of A:] -valued Function-like non empty homogeneous quasi_total Element of bool [:([: the carrier of J, the carrier of A:] *),[: the carrier of J, the carrier of A:]:]

[:([: the carrier of J, the carrier of A:] *),[: the carrier of J, the carrier of A:]:] is Relation-like non empty set

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

[:( the carrier of UAStr(# [: the carrier of J, the carrier of A:],(J,A) #) *), the carrier of UAStr(# [: the carrier of J, the carrier of A:],(J,A) #):] is Relation-like non empty set

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

ua is V24() V25() V26() V30() V31() V36() countable set

dom the charact of UAStr(# [: the carrier of J, the carrier of A:],(J,A) #) is countable Element of bool NAT

the charact of UAStr(# [: the carrier of J, the carrier of A:],(J,A) #) . ua is Relation-like Function-like set

pr is Relation-like the carrier of UAStr(# [: the carrier of J, the carrier of A:],(J,A) #) * -defined the carrier of UAStr(# [: the carrier of J, the carrier of A:],(J,A) #) -valued Function-like Element of bool [:( the carrier of UAStr(# [: the carrier of J, the carrier of A:],(J,A) #) *), the carrier of UAStr(# [: the carrier of J, the carrier of A:],(J,A) #):]

[:( the carrier of A *), the carrier of A:] is Relation-like non empty set

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

the charact of A . ua is Relation-like Function-like homogeneous set

[:( the carrier of J *), the carrier of J:] is Relation-like non empty set

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

the charact of J . ua is Relation-like Function-like homogeneous set

n9 is Relation-like the carrier of J * -defined the carrier of J -valued Function-like non empty homogeneous quasi_total Element of bool [:( the carrier of J *), the carrier of J:]

n is Relation-like the carrier of A * -defined the carrier of A -valued Function-like non empty homogeneous quasi_total Element of bool [:( the carrier of A *), the carrier of A:]

( the carrier of J, the carrier of A,n9,n) is Relation-like [: the carrier of J, the carrier of A:] * -defined [: the carrier of J, the carrier of A:] -valued Function-like non empty homogeneous quasi_total Element of bool [:([: the carrier of J, the carrier of A:] *),[: the carrier of J, the carrier of A:]:]

[:([: the carrier of J, the carrier of A:] *),[: the carrier of J, the carrier of A:]:] is Relation-like non empty set

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

J is non empty V88() quasi_total non-empty UAStr

A is non empty V88() quasi_total non-empty UAStr

the carrier of J is non empty set

the carrier of A is non empty set

[: the carrier of J, the carrier of A:] is Relation-like non empty set

(J,A) is Relation-like NAT -defined PFuncs (([: the carrier of J, the carrier of A:] *),[: the carrier of J, the carrier of A:]) -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence of PFuncs (([: the carrier of J, the carrier of A:] *),[: the carrier of J, the carrier of A:])

[: the carrier of J, the carrier of A:] * is functional non empty FinSequence-membered FinSequenceSet of [: the carrier of J, the carrier of A:]

PFuncs (([: the carrier of J, the carrier of A:] *),[: the carrier of J, the carrier of A:]) is functional non empty set

UAStr(# [: the carrier of J, the carrier of A:],(J,A) #) is non empty strict UAStr

J is non empty set

A is non empty set

[:J,A:] is Relation-like non empty set

[:A,J:] is Relation-like non empty set

[:[:J,A:],[:A,J:]:] is Relation-like non empty set

bool [:[:J,A:],[:A,J:]:] is non empty set

j is Relation-like [:J,A:] -defined [:A,J:] -valued Function-like quasi_total Element of bool [:[:J,A:],[:A,J:]:]

ua is Relation-like [:J,A:] -defined [:A,J:] -valued Function-like quasi_total Element of bool [:[:J,A:],[:A,J:]:]

pr is Element of [:J,A:]

j . pr is Element of [:A,J:]

pr `2 is Element of A

pr `1 is Element of J

[(pr `2),(pr `1)] is V15() Element of [:A,J:]

{(pr `2),(pr `1)} is non empty set

{(pr `2)} is non empty trivial V38(1) set

{{(pr `2),(pr `1)},{(pr `2)}} is non empty set

ua . pr is Element of [:A,J:]

J is non empty set

A is non empty set

[:J,A:] is Relation-like non empty set

(J,A) is Relation-like [:J,A:] -defined [:A,J:] -valued Function-like quasi_total Element of bool [:[:J,A:],[:A,J:]:]

[:A,J:] is Relation-like non empty set

[:[:J,A:],[:A,J:]:] is Relation-like non empty set

bool [:[:J,A:],[:A,J:]:] is non empty set

rng (J,A) is Relation-like A -defined J -valued Element of bool [:A,J:]

bool [:A,J:] is non empty set

j is set

proj1 (J,A) is Relation-like set

ua is Element of [:A,J:]

ua `2 is Element of J

ua `1 is Element of A

[(ua `2),(ua `1)] is V15() Element of [:J,A:]

{(ua `2),(ua `1)} is non empty set

{(ua `2)} is non empty trivial V38(1) set

{{(ua `2),(ua `1)},{(ua `2)}} is non empty set

(J,A) . [(ua `2),(ua `1)] is Element of [:A,J:]

[(ua `2),(ua `1)] `2 is Element of A

[(ua `2),(ua `1)] `1 is Element of J

[([(ua `2),(ua `1)] `2),([(ua `2),(ua `1)] `1)] is V15() Element of [:A,J:]

{([(ua `2),(ua `1)] `2),([(ua `2),(ua `1)] `1)} is non empty set

{([(ua `2),(ua `1)] `2)} is non empty trivial V38(1) set

{{([(ua `2),(ua `1)] `2),([(ua `2),(ua `1)] `1)},{([(ua `2),(ua `1)] `2)}} is non empty set

[(ua `1),([(ua `2),(ua `1)] `1)] is V15() Element of [:A,J:]

{(ua `1),([(ua `2),(ua `1)] `1)} is non empty set

{(ua `1)} is non empty trivial V38(1) set

{{(ua `1),([(ua `2),(ua `1)] `1)},{(ua `1)}} is non empty set

[(ua `1),(ua `2)] is V15() Element of [:A,J:]

{(ua `1),(ua `2)} is non empty set

{{(ua `1),(ua `2)},{(ua `1)}} is non empty set

J is non empty set

A is non empty set

(J,A) is Relation-like [:J,A:] -defined [:A,J:] -valued Function-like quasi_total Element of bool [:[:J,A:],[:A,J:]:]

[:J,A:] is Relation-like non empty set

[:A,J:] is Relation-like non empty set

[:[:J,A:],[:A,J:]:] is Relation-like non empty set

bool [:[:J,A:],[:A,J:]:] is non empty set

j is set

proj1 (J,A) is Relation-like set

(J,A) . j is set

ua is set

(J,A) . ua is set

pr is Element of [:J,A:]

(J,A) . pr is Element of [:A,J:]

pr `2 is Element of A

pr `1 is Element of J

[(pr `2),(pr `1)] is V15() Element of [:A,J:]

{(pr `2),(pr `1)} is non empty set

{(pr `2)} is non empty trivial V38(1) set

{{(pr `2),(pr `1)},{(pr `2)}} is non empty set

n is Element of [:J,A:]

(J,A) . n is Element of [:A,J:]

n `2 is Element of A

n `1 is Element of J

[(n `2),(n `1)] is V15() Element of [:A,J:]

{(n `2),(n `1)} is non empty set

{(n `2)} is non empty trivial V38(1) set

{{(n `2),(n `1)},{(n `2)}} is non empty set

J is non empty V88() quasi_total non-empty UAStr

the carrier of J is non empty set

A is non empty V88() quasi_total non-empty UAStr

the carrier of A is non empty set

( the carrier of J, the carrier of A) is Relation-like [: the carrier of J, the carrier of A:] -defined [: the carrier of A, the carrier of J:] -valued Function-like quasi_total Element of bool [:[: the carrier of J, the carrier of A:],[: the carrier of A, the carrier of J:]:]

[: the carrier of J, the carrier of A:] is Relation-like non empty set

[: the carrier of A, the carrier of J:] is Relation-like non empty set

[:[: the carrier of J, the carrier of A:],[: the carrier of A, the carrier of J:]:] is Relation-like non empty set

bool [:[: the carrier of J, the carrier of A:],[: the carrier of A, the carrier of J:]:] is non empty set

(J,A) is non empty strict V88() quasi_total non-empty UAStr

the carrier of (J,A) is non empty set

(A,J) is non empty strict V88() quasi_total non-empty UAStr

the carrier of (A,J) is non empty set

[: the carrier of (J,A), the carrier of (A,J):] is Relation-like non empty set

bool [: the carrier of (J,A), the carrier of (A,J):] is non empty set

(J,A) is Relation-like NAT -defined PFuncs (([: the carrier of J, the carrier of A:] *),[: the carrier of J, the carrier of A:]) -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence of PFuncs (([: the carrier of J, the carrier of A:] *),[: the carrier of J, the carrier of A:])

[: the carrier of J, the carrier of A:] * is functional non empty FinSequence-membered FinSequenceSet of [: the carrier of J, the carrier of A:]

PFuncs (([: the carrier of J, the carrier of A:] *),[: the carrier of J, the carrier of A:]) is functional non empty set

UAStr(# [: the carrier of J, the carrier of A:],(J,A) #) is non empty strict UAStr

(A,J) is Relation-like NAT -defined PFuncs (([: the carrier of A, the carrier of J:] *),[: the carrier of A, the carrier of J:]) -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence of PFuncs (([: the carrier of A, the carrier of J:] *),[: the carrier of A, the carrier of J:])

[: the carrier of A, the carrier of J:] * is functional non empty FinSequence-membered FinSequenceSet of [: the carrier of A, the carrier of J:]

PFuncs (([: the carrier of A, the carrier of J:] *),[: the carrier of A, the carrier of J:]) is functional non empty set

UAStr(# [: the carrier of A, the carrier of J:],(A,J) #) is non empty strict UAStr

J is non empty V88() quasi_total non-empty UAStr

the carrier of J is non empty set

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

Operations J is non empty PFuncsDomHQN of the carrier of J

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

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

proj2 the charact of J is non empty set

dom the charact of J is non empty countable Element of bool NAT

A is non empty V88() quasi_total non-empty UAStr

the carrier of A is non empty set

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

Operations A is non empty PFuncsDomHQN of the carrier of A

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

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

proj2 the charact of A is non empty set

(J,A) is non empty strict V88() quasi_total non-empty UAStr

the carrier of (J,A) is non empty set

the carrier of (J,A) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (J,A)

Operations (J,A) is non empty PFuncsDomHQN of the carrier of (J,A)

the charact of (J,A) is Relation-like non-empty NAT -defined PFuncs (( the carrier of (J,A) *), the carrier of (J,A)) -valued Function-like non empty V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of (J,A) *), the carrier of (J,A))

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

proj2 the charact of (J,A) is non empty set

(J,A) is Relation-like NAT -defined PFuncs (([: the carrier of J, the carrier of A:] *),[: the carrier of J, the carrier of A:]) -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence of PFuncs (([: the carrier of J, the carrier of A:] *),[: the carrier of J, the carrier of A:])

[: the carrier of J, the carrier of A:] is Relation-like non empty set

[: the carrier of J, the carrier of A:] * is functional non empty FinSequence-membered FinSequenceSet of [: the carrier of J, the carrier of A:]

PFuncs (([: the carrier of J, the carrier of A:] *),[: the carrier of J, the carrier of A:]) is functional non empty set

dom (J,A) is countable Element of bool NAT

len (J,A) is V24() V25() V26() V30() V31() V36() countable Element of NAT

Seg (len (J,A)) is V31() V38( len (J,A)) countable Element of bool NAT

len the charact of J is non empty V24() V25() V26() V30() V31() V36() countable Element of NAT

Seg (len the charact of J) is non empty V31() V38( len the charact of J) countable Element of bool NAT

j is Relation-like the carrier of J * -defined the carrier of J -valued Function-like non empty homogeneous quasi_total Element of Operations J

arity j is V24() V25() V26() V30() V31() V36() countable Element of NAT

ua is Relation-like the carrier of A * -defined the carrier of A -valued Function-like non empty homogeneous quasi_total Element of Operations A

arity ua is V24() V25() V26() V30() V31() V36() countable Element of NAT

( the carrier of J, the carrier of A,j,ua) is Relation-like [: the carrier of J, the carrier of A:] * -defined [: the carrier of J, the carrier of A:] -valued Function-like non empty homogeneous quasi_total Element of bool [:([: the carrier of J, the carrier of A:] *),[: the carrier of J, the carrier of A:]:]

[:([: the carrier of J, the carrier of A:] *),[: the carrier of J, the carrier of A:]:] is Relation-like non empty set

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

pr is Relation-like the carrier of (J,A) * -defined the carrier of (J,A) -valued Function-like non empty homogeneous quasi_total Element of Operations (J,A)

arity pr is V24() V25() V26() V30() V31() V36() countable Element of NAT

n is V24() V25() V26() V30() V31() V36() countable set

the charact of J . n is Relation-like Function-like homogeneous set

the charact of A . n is Relation-like Function-like homogeneous set

the charact of (J,A) . n is Relation-like Function-like homogeneous set

signature J is Relation-like NAT -defined NAT -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of NAT

dom (signature J) is countable Element of bool NAT

len (signature J) is V24() V25() V26() V30() V31() V36() countable Element of NAT

Seg (len (signature J)) is V31() V38( len (signature J)) countable Element of bool NAT

(signature J) . n is set

signature A is Relation-like NAT -defined NAT -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of NAT

(signature A) . n is set

UAStr(# [: the carrier of J, the carrier of A:],(J,A) #) is non empty strict UAStr

proj1 pr is functional non empty with_common_domain FinSequence-membered set

(arity j) -tuples_on [: the carrier of J, the carrier of A:] is functional non empty FinSequence-membered FinSequenceSet of [: the carrier of J, the carrier of A:]

{ b

the Relation-like NAT -defined [: the carrier of J, the carrier of A:] -valued Function-like V31() V38( arity j) countable FinSequence-like FinSubsequence-like Element of (arity j) -tuples_on [: the carrier of J, the carrier of A:] is Relation-like NAT -defined [: the carrier of J, the carrier of A:] -valued Function-like V31() V38( arity j) countable FinSequence-like FinSubsequence-like Element of (arity j) -tuples_on [: the carrier of J, the carrier of A:]

o is Relation-like NAT -defined Function-like V31() countable FinSequence-like FinSubsequence-like set

len o is V24() V25() V26() V30() V31() V36() countable Element of NAT

j is Relation-like NAT -defined [: the carrier of J, the carrier of A:] -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of [: the carrier of J, the carrier of A:] *

len j is V24() V25() V26() V30() V31() V36() countable Element of NAT

n9 is Relation-like NAT -defined Function-like V31() countable FinSequence-like FinSubsequence-like set

J is non empty V88() quasi_total non-empty UAStr

A is non empty V88() quasi_total non-empty UAStr

(J,A) is non empty strict V88() quasi_total non-empty UAStr

signature J is Relation-like NAT -defined NAT -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of NAT

dom (signature J) is countable Element of bool NAT

len (signature J) is V24() V25() V26() V30() V31() V36() countable Element of NAT

Seg (len (signature J)) is V31() V38( len (signature J)) countable Element of bool NAT

the charact of (J,A) is Relation-like non-empty NAT -defined PFuncs (( the carrier of (J,A) *), the carrier of (J,A)) -valued Function-like non empty V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of (J,A) *), the carrier of (J,A))

the carrier of (J,A) is non empty set

the carrier of (J,A) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (J,A)

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

dom the charact of (J,A) is non empty countable Element of bool NAT

len the charact of (J,A) is non empty V24() V25() V26() V30() V31() V36() countable Element of NAT

Seg (len the charact of (J,A)) is non empty V31() V38( len the charact of (J,A)) countable Element of bool NAT

the charact of A is Relation-like non-empty NAT -defined PFuncs (( the carrier of A *), the carrier of A) -valued Function-like non empty V31() countable Function-yielding V45() 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 set

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

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

dom the charact of A is non empty countable Element of bool NAT

len the charact of A is non empty V24() V25() V26() V30() V31() V36() countable Element of NAT

Seg (len the charact of A) is non empty V31() V38( len the charact of A) countable Element of bool NAT

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

the carrier of J is non empty set

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

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

dom the charact of J is non empty countable Element of bool NAT

len the charact of J is non empty V24() V25() V26() V30() V31() V36() countable Element of NAT

Seg (len the charact of J) is non empty V31() V38( len the charact of J) countable Element of bool NAT

[: the carrier of J, the carrier of A:] is Relation-like non empty set

(J,A) is Relation-like NAT -defined PFuncs (([: the carrier of J, the carrier of A:] *),[: the carrier of J, the carrier of A:]) -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence of PFuncs (([: the carrier of J, the carrier of A:] *),[: the carrier of J, the carrier of A:])

[: the carrier of J, the carrier of A:] * is functional non empty FinSequence-membered FinSequenceSet of [: the carrier of J, the carrier of A:]

PFuncs (([: the carrier of J, the carrier of A:] *),[: the carrier of J, the carrier of A:]) is functional non empty set

UAStr(# [: the carrier of J, the carrier of A:],(J,A) #) is non empty strict UAStr

signature (J,A) is Relation-like NAT -defined NAT -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of NAT

len (signature (J,A)) is V24() V25() V26() V30() V31() V36() countable Element of NAT

dom (signature (J,A)) is countable Element of bool NAT

Seg (len (signature (J,A))) is V31() V38( len (signature (J,A))) countable Element of bool NAT

j is V24() V25() V26() V30() V31() V36() countable set

Operations (J,A) is non empty PFuncsDomHQN of the carrier of (J,A)

proj2 the charact of (J,A) is non empty set

the charact of (J,A) . j is Relation-like Function-like homogeneous set

signature A is Relation-like NAT -defined NAT -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of NAT

len (signature A) is V24() V25() V26() V30() V31() V36() countable Element of NAT

Operations A is non empty PFuncsDomHQN of the carrier of A

proj2 the charact of A is non empty set

the charact of A . j is Relation-like Function-like homogeneous set

pr is Relation-like the carrier of A * -defined the carrier of A -valued Function-like non empty homogeneous quasi_total Element of Operations A

Operations J is non empty PFuncsDomHQN of the carrier of J

proj2 the charact of J is non empty set

the charact of J . j is Relation-like Function-like homogeneous set

(signature J) . j is set

n is Relation-like the carrier of J * -defined the carrier of J -valued Function-like non empty homogeneous quasi_total Element of Operations J

arity n is V24() V25() V26() V30() V31() V36() countable Element of NAT

(signature (J,A)) . j is set

ua is Relation-like the carrier of (J,A) * -defined the carrier of (J,A) -valued Function-like non empty homogeneous quasi_total Element of Operations (J,A)

arity ua is V24() V25() V26() V30() V31() V36() countable Element of NAT

J is non empty V88() quasi_total non-empty UAStr

A is non empty V88() quasi_total non-empty UAStr

j is non empty V88() quasi_total non-empty UAStr

ua is non empty V88() quasi_total non-empty UAStr

(J,j) is non empty strict V88() quasi_total non-empty UAStr

(A,ua) is non empty strict V88() quasi_total non-empty UAStr

the carrier of A is non empty set

the carrier of ua is non empty set

[: the carrier of A, the carrier of ua:] is Relation-like non empty set

(A,ua) is Relation-like NAT -defined PFuncs (([: the carrier of A, the carrier of ua:] *),[: the carrier of A, the carrier of ua:]) -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence of PFuncs (([: the carrier of A, the carrier of ua:] *),[: the carrier of A, the carrier of ua:])

[: the carrier of A, the carrier of ua:] * is functional non empty FinSequence-membered FinSequenceSet of [: the carrier of A, the carrier of ua:]

PFuncs (([: the carrier of A, the carrier of ua:] *),[: the carrier of A, the carrier of ua:]) is functional non empty set

UAStr(# [: the carrier of A, the carrier of ua:],(A,ua) #) is non empty strict UAStr

the carrier of J is non empty set

the carrier of j is non empty set

[: the carrier of J, the carrier of j:] is Relation-like non empty set

(J,j) is Relation-like NAT -defined PFuncs (([: the carrier of J, the carrier of j:] *),[: the carrier of J, the carrier of j:]) -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence of PFuncs (([: the carrier of J, the carrier of j:] *),[: the carrier of J, the carrier of j:])

[: the carrier of J, the carrier of j:] * is functional non empty FinSequence-membered FinSequenceSet of [: the carrier of J, the carrier of j:]

PFuncs (([: the carrier of J, the carrier of j:] *),[: the carrier of J, the carrier of j:]) is functional non empty set

UAStr(# [: the carrier of J, the carrier of j:],(J,j) #) is non empty strict UAStr

bool the carrier of A is non empty set

bool the carrier of ua is non empty set

the carrier of (J,j) is non empty set

the carrier of (A,ua) is non empty set

bool the carrier of (A,ua) is non empty set

the charact of (J,j) is Relation-like non-empty NAT -defined PFuncs (( the carrier of (J,j) *), the carrier of (J,j)) -valued Function-like non empty V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of (J,j) *), the carrier of (J,j))

the carrier of (J,j) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (J,j)

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

pr is non empty Element of bool the carrier of (A,ua)

Opers ((A,ua),pr) is Relation-like NAT -defined PFuncs ((pr *),pr) -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((pr *),pr)

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

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

signature ua is Relation-like NAT -defined NAT -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of NAT

signature A is Relation-like NAT -defined NAT -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of NAT

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

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

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

len the charact of ua is non empty V24() V25() V26() V30() V31() V36() countable Element of NAT

len (signature A) is V24() V25() V26() V30() V31() V36() countable Element of NAT

dom the charact of ua is non empty countable Element of bool NAT

Seg (len the charact of ua) is non empty V31() V38( len the charact of ua) countable Element of bool NAT

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

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

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

len the charact of A is non empty V24() V25() V26() V30() V31() V36() countable Element of NAT

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

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

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

dom the charact of J is non empty countable Element of bool NAT

len the charact of J is non empty V24() V25() V26() V30() V31() V36() countable Element of NAT

Seg (len the charact of J) is non empty V31() V38( len the charact of J) countable Element of bool NAT

dom the charact of A is non empty countable Element of bool NAT

Seg (len the charact of A) is non empty V31() V38( len the charact of A) countable Element of bool NAT

len the charact of (J,j) is non empty V24() V25() V26() V30() V31() V36() countable Element of NAT

signature J is Relation-like NAT -defined NAT -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of NAT

signature j is Relation-like NAT -defined NAT -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of NAT

len (signature j) is V24() V25() V26() V30() V31() V36() countable Element of NAT

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

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

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

dom the charact of j is non empty countable Element of bool NAT

len the charact of j is non empty V24() V25() V26() V30() V31() V36() countable Element of NAT

Seg (len the charact of j) is non empty V31() V38( len the charact of j) countable Element of bool NAT

dom (Opers ((A,ua),pr)) is countable Element of bool NAT

len (Opers ((A,ua),pr)) is V24() V25() V26() V30() V31() V36() countable Element of NAT

Seg (len (Opers ((A,ua),pr))) is V31() V38( len (Opers ((A,ua),pr))) countable Element of bool NAT

the charact of (A,ua) is Relation-like non-empty NAT -defined PFuncs (( the carrier of (A,ua) *), the carrier of (A,ua)) -valued Function-like non empty V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of (A,ua) *), the carrier of (A,ua))

the carrier of (A,ua) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (A,ua)

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

dom the charact of (A,ua) is non empty countable Element of bool NAT

len the charact of (A,ua) is non empty V24() V25() V26() V30() V31() V36() countable Element of NAT

n is non empty Element of bool the carrier of ua

n9 is non empty Element of bool the carrier of A

Operations (A,ua) is non empty PFuncsDomHQN of the carrier of (A,ua)

proj2 the charact of (A,ua) is non empty set

o is Relation-like the carrier of (A,ua) * -defined the carrier of (A,ua) -valued Function-like non empty homogeneous quasi_total Element of Operations (A,ua)

j is Relation-like NAT -defined pr -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of pr

len j is V24() V25() V26() V30() V31() V36() countable Element of NAT

arity o is V24() V25() V26() V30() V31() V36() countable Element of NAT

o . j is set

o1 is V24() V25() V26() V30() V31() V36() countable set

the charact of (A,ua) . o1 is Relation-like Function-like homogeneous set

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

o is Relation-like NAT -defined [: the carrier of J, the carrier of j:] -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of [: the carrier of J, the carrier of j:] *

( the carrier of J, the carrier of j,o) is Relation-like NAT -defined the carrier of j -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of the carrier of j

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

( the carrier of J, the carrier of j,o) is Relation-like NAT -defined the carrier of J -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of the carrier of J

Seg (len the charact of (A,ua)) is non empty V31() V38( len the charact of (A,ua)) countable Element of bool NAT

Operations A is non empty PFuncsDomHQN of the carrier of A

proj2 the charact of A is non empty set

the charact of A . o1 is Relation-like Function-like homogeneous set

Operations ua is non empty PFuncsDomHQN of the carrier of ua

proj2 the charact of ua is non empty set

the charact of ua . o1 is Relation-like Function-like homogeneous set

j is Relation-like the carrier of A * -defined the carrier of A -valued Function-like non empty homogeneous quasi_total Element of Operations A

g is Relation-like the carrier of ua * -defined the carrier of ua -valued Function-like non empty homogeneous quasi_total Element of Operations ua

( the carrier of A, the carrier of ua,j,g) is Relation-like [: the carrier of A, the carrier of ua:] * -defined [: the carrier of A, the carrier of ua:] -valued Function-like non empty homogeneous quasi_total Element of bool [:([: the carrier of A, the carrier of ua:] *),[: the carrier of A, the carrier of ua:]:]

[:([: the carrier of A, the carrier of ua:] *),[: the carrier of A, the carrier of ua:]:] is Relation-like non empty set

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

arity j is V24() V25() V26() V30() V31() V36() countable Element of NAT

proj2 o is Relation-like set

arity g is V24() V25() V26() V30() V31() V36() countable Element of NAT

g is Relation-like NAT -defined [: the carrier of A, the carrier of ua:] -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of [: the carrier of A, the carrier of ua:] *

{ b

x1 is Relation-like NAT -defined n -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of n *

len x1 is V24() V25() V26() V30() V31() V36() countable Element of NAT

len o is V24() V25() V26() V30() V31() V36() countable Element of NAT

g . x1 is set

y1 is Relation-like NAT -defined n9 -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of n9 *

len y1 is V24() V25() V26() V30() V31() V36() countable Element of NAT

j . y1 is set

proj1 ( the carrier of A, the carrier of ua,j,g) is functional non empty with_common_domain FinSequence-membered set

(arity j) -tuples_on [: the carrier of A, the carrier of ua:] is functional non empty FinSequence-membered FinSequenceSet of [: the carrier of A, the carrier of ua:]

( the carrier of A, the carrier of ua,g) is Relation-like NAT -defined the carrier of A -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of the carrier of A

j . ( the carrier of A, the carrier of ua,g) is set

( the carrier of A, the carrier of ua,g) is Relation-like NAT -defined the carrier of ua -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of the carrier of ua

g . ( the carrier of A, the carrier of ua,g) is set

[(j . ( the carrier of A, the carrier of ua,g)),(g . ( the carrier of A, the carrier of ua,g))] is V15() set

{(j . ( the carrier of A, the carrier of ua,g)),(g . ( the carrier of A, the carrier of ua,g))} is non empty set

{(j . ( the carrier of A, the carrier of ua,g))} is non empty trivial V38(1) set

{{(j . ( the carrier of A, the carrier of ua,g)),(g . ( the carrier of A, the carrier of ua,g))},{(j . ( the carrier of A, the carrier of ua,g))}} is non empty set

Opers (ua,n) is Relation-like NAT -defined PFuncs ((n *),n) -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((n *),n)

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

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

dom (Opers (ua,n)) is countable Element of bool NAT

dom the charact of (J,j) is non empty countable Element of bool NAT

Seg (len the charact of (J,j)) is non empty V31() V38( len the charact of (J,j)) countable Element of bool NAT

Opers (A,n9) is Relation-like NAT -defined PFuncs ((n9 *),n9) -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((n9 *),n9)

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

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

dom (Opers (A,n9)) is countable Element of bool NAT

o is V24() V25() V26() V30() V31() V36() countable set

the charact of (J,j) . o is Relation-like Function-like homogeneous set

(Opers ((A,ua),pr)) . o is Relation-like Function-like set

Operations A is non empty PFuncsDomHQN of the carrier of A

proj2 the charact of A is non empty set

the charact of A . o is Relation-like Function-like homogeneous set

Operations ua is non empty PFuncsDomHQN of the carrier of ua

proj2 the charact of ua is non empty set

the charact of ua . o is Relation-like Function-like homogeneous set

the charact of (A,ua) . o is Relation-like Function-like homogeneous set

o1 is Relation-like the carrier of (A,ua) * -defined the carrier of (A,ua) -valued Function-like non empty homogeneous quasi_total Element of Operations (A,ua)

j is Relation-like the carrier of A * -defined the carrier of A -valued Function-like non empty homogeneous quasi_total Element of Operations A

o is Relation-like the carrier of ua * -defined the carrier of ua -valued Function-like non empty homogeneous quasi_total Element of Operations ua

( the carrier of A, the carrier of ua,j,o) is Relation-like [: the carrier of A, the carrier of ua:] * -defined [: the carrier of A, the carrier of ua:] -valued Function-like non empty homogeneous quasi_total Element of bool [:([: the carrier of A, the carrier of ua:] *),[: the carrier of A, the carrier of ua:]:]

[:([: the carrier of A, the carrier of ua:] *),[: the carrier of A, the carrier of ua:]:] is Relation-like non empty set

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

Operations j is non empty PFuncsDomHQN of the carrier of j

proj2 the charact of j is non empty set

the charact of j . o is Relation-like Function-like homogeneous set

(Opers (ua,n)) . o is Relation-like Function-like set

o /. n is Relation-like n * -defined n -valued Function-like non empty homogeneous quasi_total Element of bool [:(n *),n:]

[:(n *),n:] is Relation-like non empty set

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

x1 is Relation-like the carrier of j * -defined the carrier of j -valued Function-like non empty homogeneous quasi_total Element of Operations j

arity o1 is V24() V25() V26() V30() V31() V36() countable Element of NAT

arity o is V24() V25() V26() V30() V31() V36() countable Element of NAT

Operations J is non empty PFuncsDomHQN of the carrier of J

proj2 the charact of J is non empty set

the charact of J . o is Relation-like Function-like homogeneous set

(Opers (A,n9)) . o is Relation-like Function-like set

j /. n9 is Relation-like n9 * -defined n9 -valued Function-like non empty homogeneous quasi_total Element of bool [:(n9 *),n9:]

[:(n9 *),n9:] is Relation-like non empty set

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

y1 is Relation-like the carrier of J * -defined the carrier of J -valued Function-like non empty homogeneous quasi_total Element of Operations J

arity (