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:]
{ b1 where b1 is Relation-like NAT -defined [:J,A:] -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of [:J,A:] * : len b1 = arity j } is set
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
{ b1 where b1 is Relation-like NAT -defined A -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of A * : len b1 = arity ua } is set
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
{ b1 where b1 is Relation-like NAT -defined J -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of J * : len b1 = arity j } is set
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
{ (b1 -tuples_on [:J,A:]) where b1 is V24() V25() V26() V30() V31() V36() countable Element of NAT : verum } is set
union { (b1 -tuples_on [:J,A:]) where b1 is V24() V25() V26() V30() V31() V36() countable Element of NAT : verum } is set
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:]
{ b1 where b1 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 b1 = arity j } is set
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:] *
{ b1 where b1 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:] * : len b1 = arity j } is set
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 (