:: 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₁ where b₁ is Relation-like NAT -defined [:J,A:] -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of [:J,A:] * : len b₁ = 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
{ b₁ where b₁ is Relation-like NAT -defined A -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of A * : len b₁ = 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
{ b₁ where b₁ is Relation-like NAT -defined J -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of J * : len b₁ = 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
{ (b₁ -tuples_on [:J,A:]) where b₁ is V24() V25() V26() V30() V31() V36() countable Element of NAT : verum } is set
union { (b₁ -tuples_on [:J,A:]) where b₁ 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:]
{ b<sub>1</sub> where b<sub>1</sub> 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 b<sub>1</sub> = 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:] *
{ b<sub>1</sub> where b<sub>1</sub> 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 b<sub>1</sub> = 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 (o /. n) is V24() V25() V26() V30() V31() V36() countable Element of NAT
arity j is V24() V25() V26() V30() V31() V36() countable Element of NAT
(arity o1) -tuples_on pr is functional non empty FinSequence-membered FinSequenceSet of pr
{ b<sub>1</sub> where b<sub>1</sub> is Relation-like NAT -defined pr -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of pr * : len b<sub>1</sub> = arity o1 } is set
( the carrier of A, the carrier of ua,j,o) | ((arity o1) -tuples_on pr) is Relation-like [: the carrier of A, the carrier of ua:] * -defined (arity o1) -tuples_on pr -defined [: the carrier of A, the carrier of ua:] * -defined [: the carrier of A, the carrier of ua:] -valued Function-like Element of bool [:([: the carrier of A, the carrier of ua:] *),[: the carrier of A, the carrier of ua:]:]
proj1 (( the carrier of A, the carrier of ua,j,o) | ((arity o1) -tuples_on pr)) is functional FinSequence-membered set
proj1 ( the carrier of A, the carrier of ua,j,o) is functional non empty with_common_domain FinSequence-membered set
(arity j) -tuples_on pr is functional non empty FinSequence-membered FinSequenceSet of pr
{ b<sub>1</sub> where b<sub>1</sub> is Relation-like NAT -defined pr -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of pr * : len b<sub>1</sub> = arity j } is set
(proj1 ( the carrier of A, the carrier of ua,j,o)) /\ ((arity j) -tuples_on pr) is set
(arity j) -tuples_on the carrier of (A,ua) is functional non empty FinSequence-membered FinSequenceSet of the carrier of (A,ua)
{ b<sub>1</sub> where b<sub>1</sub> is Relation-like NAT -defined the carrier of (A,ua) -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of the carrier of (A,ua) * : len b<sub>1</sub> = arity j } is set
((arity j) -tuples_on the carrier of (A,ua)) /\ ((arity j) -tuples_on pr) is set
arity (j /. n9) is V24() V25() V26() V30() V31() V36() countable Element of NAT
(n9,n,(j /. n9),(o /. n)) is Relation-like [:n9,n:] * -defined [:n9,n:] -valued Function-like non empty homogeneous quasi_total Element of bool [:([:n9,n:] *),[:n9,n:]:]
[:n9,n:] is Relation-like non empty set
[:n9,n:] * is functional non empty FinSequence-membered FinSequenceSet of [:n9,n:]
[:([:n9,n:] *),[:n9,n:]:] is Relation-like non empty set
bool [:([:n9,n:] *),[:n9,n:]:] is non empty set
proj1 (n9,n,(j /. n9),(o /. n)) is functional non empty with_common_domain FinSequence-membered set
j is set
g is Relation-like NAT -defined pr -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of pr *
len g is V24() V25() V26() V30() V31() V36() countable Element of NAT
proj2 g is set
(( the carrier of A, the carrier of ua,j,o) | ((arity o1) -tuples_on pr)) . j is set
g is Relation-like NAT -defined [: the carrier of A, the carrier of ua:] -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of [: the carrier of A, the carrier of ua:]
( the carrier of A, the carrier of ua,j,o) . g is set
( 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
o . ( the carrier of A, the carrier of ua,g) is set
[(j . ( the carrier of A, the carrier of ua,g)),(o . ( the carrier of A, the carrier of ua,g))] is V15() set
{(j . ( the carrier of A, the carrier of ua,g)),(o . ( 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)),(o . ( the carrier of A, the carrier of ua,g))},{(j . ( the carrier of A, the carrier of ua,g))}} is non empty set
g is Relation-like NAT -defined [:n9,n:] -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of [:n9,n:]
(n9,n,g) is Relation-like NAT -defined n9 -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of n9
len (n9,n,g) is V24() V25() V26() V30() V31() V36() countable Element of NAT
len g is V24() V25() V26() V30() V31() V36() countable Element of NAT
g is Relation-like NAT -defined n9 -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of n9 *
{ b<sub>1</sub> where b<sub>1</sub> is Relation-like NAT -defined n9 -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of n9 * : len b<sub>1</sub> = arity j } is set
(n9,n,g) is Relation-like NAT -defined n -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of n
len (n9,n,g) is V24() V25() V26() V30() V31() V36() countable Element of NAT
a is Relation-like NAT -defined n -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of n *
{ b<sub>1</sub> where b<sub>1</sub> is Relation-like NAT -defined n -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of n * : len b<sub>1</sub> = arity o } is set
(arity o) -tuples_on n is functional non empty FinSequence-membered FinSequenceSet of n
o | ((arity o) -tuples_on n) is Relation-like the carrier of ua * -defined (arity o) -tuples_on n -defined the carrier of ua * -defined the carrier of ua -valued Function-like Element of bool [:( the carrier of ua *), the carrier of ua:]
[:( the carrier of ua *), the carrier of ua:] is Relation-like non empty set
bool [:( the carrier of ua *), the carrier of ua:] is non empty set
proj1 (o | ((arity o) -tuples_on n)) is functional FinSequence-membered set
proj1 o is functional non empty with_common_domain FinSequence-membered set
(proj1 o) /\ ((arity o) -tuples_on n) is set
(arity o) -tuples_on the carrier of ua is functional non empty FinSequence-membered FinSequenceSet of the carrier of ua
{ b<sub>1</sub> where b<sub>1</sub> is Relation-like NAT -defined the carrier of ua -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of the carrier of ua * : len b<sub>1</sub> = arity o } is set
((arity o) -tuples_on the carrier of ua) /\ ((arity o) -tuples_on n) is set
(arity j) -tuples_on n9 is functional non empty FinSequence-membered FinSequenceSet of n9
j | ((arity j) -tuples_on n9) is Relation-like the carrier of A * -defined (arity j) -tuples_on n9 -defined the carrier of A * -defined the carrier of A -valued Function-like Element of bool [:( the carrier of A *), the carrier of A:]
[:( the carrier of A *), the carrier of A:] is Relation-like non empty set
bool [:( the carrier of A *), the carrier of A:] is non empty set
proj1 (j | ((arity j) -tuples_on n9)) is functional FinSequence-membered set
proj1 j is functional non empty with_common_domain FinSequence-membered set
(proj1 j) /\ ((arity j) -tuples_on n9) is set
(arity j) -tuples_on the carrier of A is functional non empty FinSequence-membered FinSequenceSet of the carrier of A
{ b<sub>1</sub> where b<sub>1</sub> is Relation-like NAT -defined the carrier of A -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of the carrier of A * : len b<sub>1</sub> = arity j } is set
((arity j) -tuples_on the carrier of A) /\ ((arity j) -tuples_on n9) is set
(n9,n,(j /. n9),(o /. n)) . j is set
(j /. n9) . (n9,n,g) is set
(o /. n) . (n9,n,g) is set
[((j /. n9) . (n9,n,g)),((o /. n) . (n9,n,g))] is V15() set
{((j /. n9) . (n9,n,g)),((o /. n) . (n9,n,g))} is non empty set
{((j /. n9) . (n9,n,g))} is non empty trivial V38(1) set
{{((j /. n9) . (n9,n,g)),((o /. n) . (n9,n,g))},{((j /. n9) . (n9,n,g))}} is non empty set
(j | ((arity j) -tuples_on n9)) . g is set
[((j | ((arity j) -tuples_on n9)) . g),((o /. n) . (n9,n,g))] is V15() set
{((j | ((arity j) -tuples_on n9)) . g),((o /. n) . (n9,n,g))} is non empty set
{((j | ((arity j) -tuples_on n9)) . g)} is non empty trivial V38(1) set
{{((j | ((arity j) -tuples_on n9)) . g),((o /. n) . (n9,n,g))},{((j | ((arity j) -tuples_on n9)) . g)}} is non empty set
j . (n9,n,g) is set
[(j . (n9,n,g)),((o /. n) . (n9,n,g))] is V15() set
{(j . (n9,n,g)),((o /. n) . (n9,n,g))} is non empty set
{(j . (n9,n,g))} is non empty trivial V38(1) set
{{(j . (n9,n,g)),((o /. n) . (n9,n,g))},{(j . (n9,n,g))}} is non empty set
(o | ((arity o) -tuples_on n)) . (n9,n,g) is set
[(j . (n9,n,g)),((o | ((arity o) -tuples_on n)) . (n9,n,g))] is V15() set
{(j . (n9,n,g)),((o | ((arity o) -tuples_on n)) . (n9,n,g))} is non empty set
{{(j . (n9,n,g)),((o | ((arity o) -tuples_on n)) . (n9,n,g))},{(j . (n9,n,g))}} is non empty set
o . (n9,n,g) is set
[(j . (n9,n,g)),(o . (n9,n,g))] is V15() set
{(j . (n9,n,g)),(o . (n9,n,g))} is non empty set
{{(j . (n9,n,g)),(o . (n9,n,g))},{(j . (n9,n,g))}} is non empty set
o1 /. pr is Relation-like pr * -defined pr -valued Function-like non empty homogeneous quasi_total Element of bool [:(pr *),pr:]
[:(pr *),pr:] is Relation-like non empty set
bool [:(pr *),pr:] is non empty set
{{}} is functional non empty trivial V38(1) with_common_domain set
{{}} * is functional non empty FinSequence-membered FinSequenceSet of {{}}
[:({{}} *),{{}}:] is Relation-like non empty set
bool [:({{}} *),{{}}:] is non empty set
J is V24() V25() V26() V30() V31() V36() countable set
J |-> {} is Relation-like empty-yielding NAT -defined Function-like V31() V38(J) countable FinSequence-like FinSubsequence-like set
Seg J is V31() V38(J) countable Element of bool NAT
(Seg J) --> {} is Relation-like Seg J -defined Seg J -defined {{}} -valued Function-like constant total total quasi_total V31() Cardinal-yielding countable Function-yielding V45() FinSequence-like FinSubsequence-like Element of bool [:(Seg J),{{}}:]
[:(Seg J),{{}}:] is Relation-like set
bool [:(Seg J),{{}}:] is non empty set
{(J |-> {})} is functional non empty trivial V38(1) with_common_domain set
A is Relation-like Function-like set
proj1 A is set
proj2 A is set
ua is set
j is Relation-like Function-like Element of {{}}
J |-> j is Relation-like NAT -defined {{}} -valued Function-like V31() V38(J) countable Function-yielding V45() FinSequence-like FinSubsequence-like Element of J -tuples_on {{}}
J -tuples_on {{}} is functional non empty FinSequence-membered FinSequenceSet of {{}}
{ b<sub>1</sub> where b<sub>1</sub> is Relation-like NAT -defined {{}} -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of {{}} * : len b<sub>1</sub> = J } is set
(Seg J) --> j is Relation-like Seg J -defined Seg J -defined {{}} -valued {j} -valued Function-like constant total total quasi_total V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like Element of bool [:(Seg J),{j}:]
{j} is functional non empty trivial V38(1) with_common_domain set
[:(Seg J),{j}:] is Relation-like set
bool [:(Seg J),{j}:] is non empty set
j is Relation-like {{}} * -defined {{}} -valued Function-like Function-yielding V45() Element of bool [:({{}} *),{{}}:]
proj1 j is functional FinSequence-membered set
proj2 j is set
A is Relation-like {{}} * -defined {{}} -valued Function-like Function-yielding V45() Element of bool [:({{}} *),{{}}:]
proj1 A is functional FinSequence-membered set
proj2 A is set
j is Relation-like {{}} * -defined {{}} -valued Function-like Function-yielding V45() Element of bool [:({{}} *),{{}}:]
proj1 j is functional FinSequence-membered set
proj2 j is set
J is V24() V25() V26() V30() V31() V36() countable set
(J) is Relation-like {{}} * -defined {{}} -valued Function-like Function-yielding V45() Element of bool [:({{}} *),{{}}:]
proj1 (J) is functional FinSequence-membered set
J |-> {} is Relation-like empty-yielding NAT -defined Function-like V31() V38(J) countable FinSequence-like FinSubsequence-like set
Seg J is V31() V38(J) countable Element of bool NAT
(Seg J) --> {} is Relation-like Seg J -defined Seg J -defined {{}} -valued Function-like constant total total quasi_total V31() Cardinal-yielding countable Function-yielding V45() FinSequence-like FinSubsequence-like Element of bool [:(Seg J),{{}}:]
[:(Seg J),{{}}:] is Relation-like set
bool [:(Seg J),{{}}:] is non empty set
{(J |-> {})} is functional non empty trivial V38(1) with_common_domain set
j is Relation-like NAT -defined Function-like V31() countable FinSequence-like FinSubsequence-like set
ua 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 ua is V24() V25() V26() V30() V31() V36() countable Element of NAT
j is Relation-like NAT -defined {{}} -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence of {{}}
len j is V24() V25() V26() V30() V31() V36() countable Element of NAT
ua is Relation-like NAT -defined {{}} -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence of {{}}
len ua is V24() V25() V26() V30() V31() V36() countable Element of NAT
dom j is countable Element of bool NAT
Seg (len j) is V31() V38( len j) countable Element of bool NAT
pr is V24() V25() V26() V30() V31() V36() countable set
dom ua is countable Element of bool NAT
ua . pr is Relation-like Function-like set
j . pr is Relation-like Function-like set
J is V24() V25() V26() V30() V31() V36() countable set
(J) is Relation-like {{}} * -defined {{}} -valued Function-like non empty Function-yielding V45() homogeneous quasi_total Element of bool [:({{}} *),{{}}:]
arity (J) is V24() V25() V26() V30() V31() V36() countable Element of NAT
proj1 (J) is functional non empty with_common_domain FinSequence-membered set
J |-> {} is Relation-like empty-yielding NAT -defined Function-like V31() V38(J) countable FinSequence-like FinSubsequence-like set
Seg J is V31() V38(J) countable Element of bool NAT
(Seg J) --> {} is Relation-like Seg J -defined Seg J -defined {{}} -valued Function-like constant total total quasi_total V31() Cardinal-yielding countable Function-yielding V45() FinSequence-like FinSubsequence-like Element of bool [:(Seg J),{{}}:]
[:(Seg J),{{}}:] is Relation-like set
bool [:(Seg J),{{}}:] is non empty set
{(J |-> {})} is functional non empty trivial V38(1) with_common_domain set
A is Relation-like NAT -defined Function-like V31() countable FinSequence-like FinSubsequence-like set
len A is V24() V25() V26() V30() V31() V36() countable Element of NAT
A is Relation-like NAT -defined Function-like V31() countable FinSequence-like FinSubsequence-like set
PFuncs (({{}} *),{{}}) is functional non empty set
J is Relation-like NAT -defined NAT -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of NAT
len J is V24() V25() V26() V30() V31() V36() countable Element of NAT
Seg (len J) is V31() V38( len J) countable Element of bool NAT
A is V24() V25() V26() V30() V31() V36() countable set
J . A is set
dom J is countable Element of bool NAT
j is V24() V25() V26() V30() V31() V36() countable Element of NAT
(j) is Relation-like {{}} * -defined {{}} -valued Function-like non empty Function-yielding V45() homogeneous quasi_total Element of bool [:({{}} *),{{}}:]
ua is Relation-like Function-like Element of PFuncs (({{}} *),{{}})
pr is V24() V25() V26() V30() V31() V36() countable set
(pr) is Relation-like {{}} * -defined {{}} -valued Function-like non empty Function-yielding V45() homogeneous quasi_total Element of bool [:({{}} *),{{}}:]
A is Relation-like NAT -defined PFuncs (({{}} *),{{}}) -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence of PFuncs (({{}} *),{{}})
dom A is countable Element of bool NAT
j is Relation-like NAT -defined PFuncs (({{}} *),{{}}) -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence of PFuncs (({{}} *),{{}})
len j is V24() V25() V26() V30() V31() V36() countable Element of NAT
dom j is countable Element of bool NAT
ua is V24() V25() V26() V30() V31() V36() countable set
J . ua is set
j . ua is Relation-like Function-like set
pr is V24() V25() V26() V30() V31() V36() countable set
(pr) is Relation-like {{}} * -defined {{}} -valued Function-like non empty Function-yielding V45() homogeneous quasi_total Element of bool [:({{}} *),{{}}:]
A is Relation-like NAT -defined PFuncs (({{}} *),{{}}) -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence of PFuncs (({{}} *),{{}})
len A is V24() V25() V26() V30() V31() V36() countable Element of NAT
dom A is countable Element of bool NAT
j is Relation-like NAT -defined PFuncs (({{}} *),{{}}) -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence of PFuncs (({{}} *),{{}})
len j is V24() V25() V26() V30() V31() V36() countable Element of NAT
dom j is countable Element of bool NAT
Seg (len J) is V31() V38( len J) countable Element of bool NAT
ua is V24() V25() V26() V30() V31() V36() countable set
dom J is countable Element of bool NAT
J . ua is set
A . ua is Relation-like Function-like set
pr is V24() V25() V26() V30() V31() V36() countable Element of NAT
(pr) is Relation-like {{}} * -defined {{}} -valued Function-like non empty Function-yielding V45() homogeneous quasi_total Element of bool [:({{}} *),{{}}:]
j . ua is Relation-like Function-like set
J is Relation-like NAT -defined NAT -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of NAT
(J) is Relation-like NAT -defined PFuncs (({{}} *),{{}}) -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence of PFuncs (({{}} *),{{}})
dom (J) is countable Element of bool NAT
A is V24() V25() V26() V30() V31() V36() countable set
(J) . A is Relation-like Function-like set
j is Relation-like {{}} * -defined {{}} -valued Function-like Function-yielding V45() Element of bool [:({{}} *),{{}}:]
len (J) is V24() V25() V26() V30() V31() V36() countable Element of NAT
Seg (len (J)) is V31() V38( len (J)) countable Element of bool NAT
len J is V24() V25() V26() V30() V31() V36() countable Element of NAT
Seg (len J) is V31() V38( len J) countable Element of bool NAT
dom J is countable Element of bool NAT
J . A is set
ua is V24() V25() V26() V30() V31() V36() countable Element of NAT
(ua) is Relation-like {{}} * -defined {{}} -valued Function-like non empty Function-yielding V45() homogeneous quasi_total Element of bool [:({{}} *),{{}}:]
A is set
(J) . A is Relation-like Function-like set
len (J) is V24() V25() V26() V30() V31() V36() countable Element of NAT
Seg (len (J)) is V31() V38( len (J)) countable Element of bool NAT
len J is V24() V25() V26() V30() V31() V36() countable Element of NAT
Seg (len J) is V31() V38( len J) countable Element of bool NAT
dom J is countable Element of bool NAT
j is V24() V25() V26() V30() V31() V36() countable Element of NAT
J . j is set
(J) . j is Relation-like Function-like set
ua is V24() V25() V26() V30() V31() V36() countable Element of NAT
(ua) is Relation-like {{}} * -defined {{}} -valued Function-like non empty Function-yielding V45() homogeneous quasi_total Element of bool [:({{}} *),{{}}:]
A is V24() V25() V26() V30() V31() V36() countable set
(J) . A is Relation-like Function-like set
j is Relation-like {{}} * -defined {{}} -valued Function-like Function-yielding V45() Element of bool [:({{}} *),{{}}:]
len (J) is V24() V25() V26() V30() V31() V36() countable Element of NAT
Seg (len (J)) is V31() V38( len (J)) countable Element of bool NAT
len J is V24() V25() V26() V30() V31() V36() countable Element of NAT
Seg (len J) is V31() V38( len J) countable Element of bool NAT
dom J is countable Element of bool NAT
J . A is set
ua is V24() V25() V26() V30() V31() V36() countable Element of NAT
(ua) is Relation-like {{}} * -defined {{}} -valued Function-like non empty Function-yielding V45() homogeneous quasi_total Element of bool [:({{}} *),{{}}:]
J is Relation-like NAT -defined NAT -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of NAT
(J) is Relation-like NAT -defined PFuncs (({{}} *),{{}}) -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence of PFuncs (({{}} *),{{}})
UAStr(# {{}},(J) #) is non empty strict UAStr
the carrier of UAStr(# {{}},(J) #) is non empty set
the charact of UAStr(# {{}},(J) #) is Relation-like NAT -defined PFuncs (( the carrier of UAStr(# {{}},(J) #) *), the carrier of UAStr(# {{}},(J) #)) -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence of PFuncs (( the carrier of UAStr(# {{}},(J) #) *), the carrier of UAStr(# {{}},(J) #))
the carrier of UAStr(# {{}},(J) #) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of UAStr(# {{}},(J) #)
PFuncs (( the carrier of UAStr(# {{}},(J) #) *), the carrier of UAStr(# {{}},(J) #)) is functional non empty set
len the charact of UAStr(# {{}},(J) #) is V24() V25() V26() V30() V31() V36() countable Element of NAT
len J is V24() V25() V26() V30() V31() V36() countable Element of NAT
J is non empty set
J * is functional non empty FinSequence-membered FinSequenceSet of J
the Element of J is Element of J
<* the Element of J*> is Relation-like NAT -defined J -valued Function-like constant non empty trivial V31() V38(1) countable FinSequence-like FinSubsequence-like FinSequence of J
j is Relation-like NAT -defined J -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of J *
J is Relation-like NAT -defined NAT -valued Function-like non empty V31() countable FinSequence-like FinSubsequence-like FinSequence of NAT
(J) is Relation-like NAT -defined PFuncs (({{}} *),{{}}) -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence of PFuncs (({{}} *),{{}})
UAStr(# {{}},(J) #) is non empty strict UAStr
J is Relation-like Function-like set
A is set
proj1 J is set
J . A is set
J is Relation-like Function-like set
proj1 J is set
A is set
J . A is set
J is set
the 1-sorted is 1-sorted
J --> the 1-sorted is Relation-like J -defined { the 1-sorted } -valued Function-like constant total quasi_total Element of bool [:J,{ the 1-sorted }:]
{ the 1-sorted } is non empty trivial V38(1) set
[:J,{ the 1-sorted }:] is Relation-like set
bool [:J,{ the 1-sorted }:] is non empty set
proj1 (J --> the 1-sorted ) is set
ua is Relation-like J -defined Function-like total set
proj1 ua is set
pr is set
ua . pr is set
J is non empty set
the non empty V88() quasi_total non-empty UAStr is non empty V88() quasi_total non-empty UAStr
J --> the non empty V88() quasi_total non-empty UAStr is Relation-like J -defined { the non empty V88() quasi_total non-empty UAStr } -valued Function-like constant non empty total quasi_total Element of bool [:J,{ the non empty V88() quasi_total non-empty UAStr }:]
{ the non empty V88() quasi_total non-empty UAStr } is non empty trivial V38(1) set
[:J,{ the non empty V88() quasi_total non-empty UAStr }:] is Relation-like non empty set
bool [:J,{ the non empty V88() quasi_total non-empty UAStr }:] is non empty set
proj1 (J --> the non empty V88() quasi_total non-empty UAStr ) is non empty set
ua is Relation-like J -defined Function-like non empty total set
proj1 ua is non empty set
pr is set
ua . pr is set
n is set
ua . n is set
n9 is non empty V88() quasi_total non-empty UAStr
signature n9 is Relation-like NAT -defined NAT -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of NAT
o is non empty V88() quasi_total non-empty UAStr
signature o is Relation-like NAT -defined NAT -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of NAT
pr is set
ua . pr is set
J is non empty set
A is Relation-like J -defined Function-like non empty total () set
j is Element of J
A . j is set
proj1 A is non empty set
J is non empty set
A is Relation-like J -defined Function-like non empty total () () set
j is Element of J
A . j is set
proj1 A is non empty set
J is set
A is Relation-like J -defined Function-like total () set
j is set
A . j is set
ua is non empty set
n is Relation-like ua -defined Function-like non empty total () set
pr is Element of ua
(ua,n,pr) is 1-sorted
the carrier of (ua,n,pr) is set
j is Relation-like Function-like set
proj1 j is set
ua is Relation-like J -defined Function-like total set
pr is set
A . pr is set
ua . pr is set
j is Relation-like J -defined Function-like total set
ua is Relation-like J -defined Function-like total set
pr is set
j . pr is set
ua . pr is set
A . pr is set
n is 1-sorted
the carrier of n is set
n9 is 1-sorted
the carrier of n9 is set
J is non empty set
A is Relation-like J -defined Function-like non empty total () () set
(J,A) is Relation-like J -defined Function-like non empty total set
j is set
(J,A) . j is set
A . j is set
ua is 1-sorted
the carrier of ua is set
proj1 A is non empty set
J is non empty set
A is Relation-like J -defined Function-like non empty total () () () set
the Element of J is Element of J
(J,A, the Element of J) is non empty V88() quasi_total non-empty UAStr
ua is non empty V88() quasi_total non-empty UAStr
signature ua is Relation-like NAT -defined NAT -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of NAT
pr is Element of J
(J,A,pr) is non empty V88() quasi_total non-empty UAStr
signature (J,A,pr) is Relation-like NAT -defined NAT -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of NAT
proj1 A is non empty set
the Element of J is Element of J
ua is Relation-like NAT -defined NAT -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of NAT
pr is Relation-like NAT -defined NAT -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of NAT
(J,A, the Element of J) is non empty V88() quasi_total non-empty UAStr
n is non empty V88() quasi_total non-empty UAStr
signature n is Relation-like NAT -defined NAT -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of NAT
J is non empty set
A is Relation-like non-empty non empty-yielding J -defined Function-like non empty total set
product A is functional non empty with_common_domain product-like set
J is non empty set
A is Relation-like non-empty non empty-yielding J -defined Function-like non empty total set
j is set
A . j is set
j is Relation-like Function-like set
proj1 j is set
ua is Relation-like Function-like set
proj1 ua is set
pr is Relation-like J -defined Function-like non empty total set
proj1 pr is non empty set
n is set
pr . n is set
A . n is set
<*> (A . n) is Relation-like non-empty empty-yielding NAT -defined A . n -valued 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 FinSequence of A . n
j . n is set
(<*> (A . n)) .--> (j . n) is Relation-like bool [:NAT,(A . n):] -defined {(<*> (A . n))} -defined Function-like one-to-one set
[:NAT,(A . n):] is Relation-like set
bool [:NAT,(A . n):] is non empty set
{(<*> (A . n))} is functional non empty trivial V38(1) with_common_domain set
{(<*> (A . n))} --> (j . n) is Relation-like {(<*> (A . n))} -defined {(j . n)} -valued Function-like constant non empty total quasi_total Element of bool [:{(<*> (A . n))},{(j . n)}:]
{(j . n)} is non empty trivial V38(1) set
[:{(<*> (A . n))},{(j . n)}:] is Relation-like non empty set
bool [:{(<*> (A . n))},{(j . n)}:] is non empty set
n is Relation-like J -defined Function-like non empty total Function-yielding V45() set
n9 is Element of J
n . n9 is Relation-like Function-like set
A . n9 is non empty set
(A . n9) * is functional non empty FinSequence-membered FinSequenceSet of A . n9
[:((A . n9) *),(A . n9):] is Relation-like non empty set
bool [:((A . n9) *),(A . n9):] is non empty set
j . n9 is set
<*> (A . n9) is Relation-like non-empty empty-yielding NAT -defined A . n9 -valued Function-like one-to-one constant functional empty proper V24() V25() V26() V28() V29() V30() V31() V36() V38( {} ) Cardinal-yielding with_common_domain countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of A . n9
[:NAT,(A . n9):] is Relation-like non empty V31() set
o is Element of A . n9
(<*> (A . n9)) .--> o is Relation-like bool [:NAT,(A . n9):] -defined {(<*> (A . n9))} -defined A . n9 -valued Function-like one-to-one set
bool [:NAT,(A . n9):] is non empty V31() set
{(<*> (A . n9))} is functional non empty trivial V38(1) with_common_domain set
{(<*> (A . n9))} --> o is Relation-like {(<*> (A . n9))} -defined A . n9 -valued {o} -valued Function-like constant non empty total quasi_total Element of bool [:{(<*> (A . n9))},{o}:]
{o} is non empty trivial V38(1) set
[:{(<*> (A . n9))},{o}:] is Relation-like non empty set
bool [:{(<*> (A . n9))},{o}:] is non empty set
J is non empty set
A is Relation-like non-empty non empty-yielding J -defined Function-like non empty total set
j is Relation-like J -defined Function-like non empty total Function-yielding V45() (J,A)
ua is Element of J
j . ua is Relation-like Function-like set
A . ua is non empty set
(A . ua) * is functional non empty FinSequence-membered FinSequenceSet of A . ua
[:((A . ua) *),(A . ua):] is Relation-like non empty set
bool [:((A . ua) *),(A . ua):] is non empty set
J is non empty set
A is Relation-like non-empty non empty-yielding J -defined Function-like non empty total set
j is set
A . j is set
j is Relation-like Function-like set
proj1 j is set
ua is Relation-like Function-like set
proj1 ua is set
pr is Relation-like J -defined Function-like non empty total set
proj1 pr is non empty set
n is set
pr . n is set
A . n is set
<*> (A . n) is Relation-like non-empty empty-yielding NAT -defined A . n -valued 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 FinSequence of A . n
j . n is set
(<*> (A . n)) .--> (j . n) is Relation-like bool [:NAT,(A . n):] -defined {(<*> (A . n))} -defined Function-like one-to-one set
[:NAT,(A . n):] is Relation-like set
bool [:NAT,(A . n):] is non empty set
{(<*> (A . n))} is functional non empty trivial V38(1) with_common_domain set
{(<*> (A . n))} --> (j . n) is Relation-like {(<*> (A . n))} -defined {(j . n)} -valued Function-like constant non empty total quasi_total Element of bool [:{(<*> (A . n))},{(j . n)}:]
{(j . n)} is non empty trivial V38(1) set
[:{(<*> (A . n))},{(j . n)}:] is Relation-like non empty set
bool [:{(<*> (A . n))},{(j . n)}:] is non empty set
n9 is Element of J
A . n9 is non empty set
j . n9 is set
n is Relation-like J -defined Function-like non empty total Function-yielding V45() set
n . n9 is Relation-like Function-like set
<*> (A . n9) is Relation-like non-empty empty-yielding NAT -defined A . n9 -valued Function-like one-to-one constant functional empty proper V24() V25() V26() V28() V29() V30() V31() V36() V38( {} ) Cardinal-yielding with_common_domain countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of A . n9
[:NAT,(A . n9):] is Relation-like non empty V31() set
o is Element of A . n9
(<*> (A . n9)) .--> o is Relation-like bool [:NAT,(A . n9):] -defined {(<*> (A . n9))} -defined A . n9 -valued Function-like one-to-one set
bool [:NAT,(A . n9):] is non empty V31() set
{(<*> (A . n9))} is functional non empty trivial V38(1) with_common_domain set
{(<*> (A . n9))} --> o is Relation-like {(<*> (A . n9))} -defined A . n9 -valued {o} -valued Function-like constant non empty total quasi_total Element of bool [:{(<*> (A . n9))},{o}:]
{o} is non empty trivial V38(1) set
[:{(<*> (A . n9))},{o}:] is Relation-like non empty set
bool [:{(<*> (A . n9))},{o}:] is non empty set
(A . n9) * is functional non empty FinSequence-membered FinSequenceSet of A . n9
[:((A . n9) *),(A . n9):] is Relation-like non empty set
bool [:((A . n9) *),(A . n9):] is non empty set
n9 is Relation-like J -defined Function-like non empty total Function-yielding V45() (J,A)
proj1 n9 is non empty set
o is set
n9 . o is Relation-like Function-like set
j is set
n9 . j is Relation-like Function-like set
x1 is Relation-like Function-like set
y1 is Relation-like Function-like set
proj1 x1 is set
proj1 y1 is set
o is Element of J
A . o is non empty set
j . o is set
g is V24() V25() V26() V30() V31() V36() countable set
g is V24() V25() V26() V30() V31() V36() countable set
g is non empty set
g -tuples_on g is functional non empty FinSequence-membered FinSequenceSet of g
g * is functional non empty FinSequence-membered FinSequenceSet of g
{ b<sub>1</sub> where b<sub>1</sub> is Relation-like NAT -defined g -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of g * : len b<sub>1</sub> = g } is set
g is non empty set
g -tuples_on g is functional non empty FinSequence-membered FinSequenceSet of g
g * is functional non empty FinSequence-membered FinSequenceSet of g
{ b<sub>1</sub> where b<sub>1</sub> is Relation-like NAT -defined g -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of g * : len b<sub>1</sub> = g } is set
[:(g *),g:] is Relation-like non empty set
bool [:(g *),g:] is non empty set
[:(g *),g:] is Relation-like non empty set
bool [:(g *),g:] is non empty set
a is Relation-like g * -defined g -valued Function-like non empty homogeneous quasi_total Element of bool [:(g *),g:]
arity a is V24() V25() V26() V30() V31() V36() countable Element of NAT
f is Relation-like g * -defined g -valued Function-like non empty homogeneous quasi_total Element of bool [:(g *),g:]
arity f is V24() V25() V26() V30() V31() V36() countable Element of NAT
(A . o) * is functional non empty FinSequence-membered FinSequenceSet of A . o
[:((A . o) *),(A . o):] is Relation-like non empty set
bool [:((A . o) *),(A . o):] is non empty set
<*> (A . o) is Relation-like non-empty empty-yielding NAT -defined A . o -valued Function-like one-to-one constant functional empty proper V24() V25() V26() V28() V29() V30() V31() V36() V38( {} ) Cardinal-yielding with_common_domain countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of A . o
[:NAT,(A . o):] is Relation-like non empty V31() set
j is Element of A . o
(<*> (A . o)) .--> j is Relation-like bool [:NAT,(A . o):] -defined {(<*> (A . o))} -defined A . o -valued Function-like one-to-one set
bool [:NAT,(A . o):] is non empty V31() set
{(<*> (A . o))} is functional non empty trivial V38(1) with_common_domain set
{(<*> (A . o))} --> j is Relation-like {(<*> (A . o))} -defined A . o -valued {j} -valued Function-like constant non empty total quasi_total Element of bool [:{(<*> (A . o))},{j}:]
{j} is non empty trivial V38(1) set
[:{(<*> (A . o))},{j}:] is Relation-like non empty set
bool [:{(<*> (A . o))},{j}:] is non empty set
b is Relation-like (A . o) * -defined A . o -valued Function-like non empty homogeneous quasi_total Element of bool [:((A . o) *),(A . o):]
proj1 b is functional non empty with_common_domain FinSequence-membered set
bool (A . o) is non empty set
{} (A . o) is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty proper 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 bool (A . o)
{({} (A . o))} is functional non empty trivial V38(1) with_common_domain Element of bool (bool (A . o))
bool (bool (A . o)) is non empty set
proj1 a is functional non empty with_common_domain FinSequence-membered set
p1 is set
A . o is set
<*> (A . o) is Relation-like non-empty empty-yielding NAT -defined A . o -valued 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 FinSequence of A . o
j . o is set
(<*> (A . o)) .--> (j . o) is Relation-like bool [:NAT,(A . o):] -defined {(<*> (A . o))} -defined Function-like one-to-one set
[:NAT,(A . o):] is Relation-like set
bool [:NAT,(A . o):] is non empty set
{(<*> (A . o))} is functional non empty trivial V38(1) with_common_domain set
{(<*> (A . o))} --> (j . o) is Relation-like {(<*> (A . o))} -defined {(j . o)} -valued Function-like constant non empty total quasi_total Element of bool [:{(<*> (A . o))},{(j . o)}:]
{(j . o)} is non empty trivial V38(1) set
[:{(<*> (A . o))},{(j . o)}:] is Relation-like non empty set
bool [:{(<*> (A . o))},{(j . o)}:] is non empty set
p1 is Relation-like NAT -defined g -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of g *
len p1 is V24() V25() V26() V30() V31() V36() countable Element of NAT
o1 is Element of J
A . o1 is non empty set
j . o1 is set
(A . o1) * is functional non empty FinSequence-membered FinSequenceSet of A . o1
[:((A . o1) *),(A . o1):] is Relation-like non empty set
bool [:((A . o1) *),(A . o1):] is non empty set
<*> (A . o1) is Relation-like non-empty empty-yielding NAT -defined A . o1 -valued Function-like one-to-one constant functional empty proper V24() V25() V26() V28() V29() V30() V31() V36() V38( {} ) Cardinal-yielding with_common_domain countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of A . o1
[:NAT,(A . o1):] is Relation-like non empty V31() set
fy is Element of A . o1
(<*> (A . o1)) .--> fy is Relation-like bool [:NAT,(A . o1):] -defined {(<*> (A . o1))} -defined A . o1 -valued Function-like one-to-one set
bool [:NAT,(A . o1):] is non empty V31() set
{(<*> (A . o1))} is functional non empty trivial V38(1) with_common_domain set
{(<*> (A . o1))} --> fy is Relation-like {(<*> (A . o1))} -defined A . o1 -valued {fy} -valued Function-like constant non empty total quasi_total Element of bool [:{(<*> (A . o1))},{fy}:]
{fy} is non empty trivial V38(1) set
[:{(<*> (A . o1))},{fy}:] is Relation-like non empty set
bool [:{(<*> (A . o1))},{fy}:] is non empty set
o2y is Relation-like (A . o1) * -defined A . o1 -valued Function-like non empty homogeneous quasi_total Element of bool [:((A . o1) *),(A . o1):]
proj1 o2y is functional non empty with_common_domain FinSequence-membered set
bool (A . o1) is non empty set
{} (A . o1) is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty proper 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 bool (A . o1)
{({} (A . o1))} is functional non empty trivial V38(1) with_common_domain Element of bool (bool (A . o1))
bool (bool (A . o1)) is non empty set
proj1 f is functional non empty with_common_domain FinSequence-membered set
p2 is set
A . j is set
<*> (A . j) is Relation-like non-empty empty-yielding NAT -defined A . j -valued 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 FinSequence of A . j
j . j is set
(<*> (A . j)) .--> (j . j) is Relation-like bool [:NAT,(A . j):] -defined {(<*> (A . j))} -defined Function-like one-to-one set
[:NAT,(A . j):] is Relation-like set
bool [:NAT,(A . j):] is non empty set
{(<*> (A . j))} is functional non empty trivial V38(1) with_common_domain set
{(<*> (A . j))} --> (j . j) is Relation-like {(<*> (A . j))} -defined {(j . j)} -valued Function-like constant non empty total quasi_total Element of bool [:{(<*> (A . j))},{(j . j)}:]
{(j . j)} is non empty trivial V38(1) set
[:{(<*> (A . j))},{(j . j)}:] is Relation-like non empty set
bool [:{(<*> (A . j))},{(j . j)}:] is non empty set
p2 is Relation-like NAT -defined g -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of g *
len p2 is V24() V25() V26() V30() V31() V36() countable Element of NAT
J is non empty set
A is Relation-like non-empty non empty-yielding J -defined Function-like non empty total set
j is Relation-like J -defined Function-like non empty total Function-yielding V45() (J,A)
ua is Element of J
(J,A,j,ua) is Relation-like (A . ua) * -defined A . ua -valued Function-like non empty homogeneous quasi_total Element of bool [:((A . ua) *),(A . ua):]
A . ua is non empty set
(A . ua) * is functional non empty FinSequence-membered FinSequenceSet of A . ua
[:((A . ua) *),(A . ua):] is Relation-like non empty set
bool [:((A . ua) *),(A . ua):] is non empty set
arity (J,A,j,ua) is V24() V25() V26() V30() V31() V36() countable Element of NAT
pr is Element of J
(J,A,j,pr) is Relation-like (A . pr) * -defined A . pr -valued Function-like non empty homogeneous quasi_total Element of bool [:((A . pr) *),(A . pr):]
A . pr is non empty set
(A . pr) * is functional non empty FinSequence-membered FinSequenceSet of A . pr
[:((A . pr) *),(A . pr):] is Relation-like non empty set
bool [:((A . pr) *),(A . pr):] is non empty set
arity (J,A,j,pr) is V24() V25() V26() V30() V31() V36() countable Element of NAT
proj1 (J,A,j,pr) is functional non empty with_common_domain FinSequence-membered set
(arity (J,A,j,pr)) -tuples_on (A . pr) is functional non empty FinSequence-membered FinSequenceSet of A . pr
{ b<sub>1</sub> where b<sub>1</sub> is Relation-like NAT -defined A . pr -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of (A . pr) * : len b<sub>1</sub> = arity (J,A,j,pr) } is set
proj1 j is non empty set
proj1 (J,A,j,ua) is functional non empty with_common_domain FinSequence-membered set
(arity (J,A,j,ua)) -tuples_on (A . ua) is functional non empty FinSequence-membered FinSequenceSet of A . ua
{ b<sub>1</sub> where b<sub>1</sub> is Relation-like NAT -defined A . ua -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of (A . ua) * : len b<sub>1</sub> = arity (J,A,j,ua) } is set
ua is set
proj1 j is non empty set
pr is set
j . ua is Relation-like Function-like set
j . pr is Relation-like Function-like set
o is Relation-like Function-like set
j is Relation-like Function-like set
proj1 o is set
proj1 j is set
n is Element of J
(J,A,j,n) is Relation-like (A . n) * -defined A . n -valued Function-like non empty homogeneous quasi_total Element of bool [:((A . n) *),(A . n):]
A . n is non empty set
(A . n) * is functional non empty FinSequence-membered FinSequenceSet of A . n
[:((A . n) *),(A . n):] is Relation-like non empty set
bool [:((A . n) *),(A . n):] is non empty set
arity (J,A,j,n) is V24() V25() V26() V30() V31() V36() countable Element of NAT
n9 is Element of J
(J,A,j,n9) is Relation-like (A . n9) * -defined A . n9 -valued Function-like non empty homogeneous quasi_total Element of bool [:((A . n9) *),(A . n9):]
A . n9 is non empty set
(A . n9) * is functional non empty FinSequence-membered FinSequenceSet of A . n9
[:((A . n9) *),(A . n9):] is Relation-like non empty set
bool [:((A . n9) *),(A . n9):] is non empty set
arity (J,A,j,n9) is V24() V25() V26() V30() V31() V36() countable Element of NAT
(arity (J,A,j,n)) -tuples_on (A . n9) is functional non empty FinSequence-membered FinSequenceSet of A . n9
{ b<sub>1</sub> where b<sub>1</sub> is Relation-like NAT -defined A . n9 -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of (A . n9) * : len b<sub>1</sub> = arity (J,A,j,n) } is set
o is V24() V25() V26() V30() V31() V36() countable set
o1 is V24() V25() V26() V30() V31() V36() countable set
x1 is non empty set
o -tuples_on x1 is functional non empty FinSequence-membered FinSequenceSet of x1
x1 * is functional non empty FinSequence-membered FinSequenceSet of x1
{ b<sub>1</sub> where b<sub>1</sub> is Relation-like NAT -defined x1 -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of x1 * : len b<sub>1</sub> = o } is set
y1 is non empty set
o1 -tuples_on y1 is functional non empty FinSequence-membered FinSequenceSet of y1
y1 * is functional non empty FinSequence-membered FinSequenceSet of y1
{ b<sub>1</sub> where b<sub>1</sub> is Relation-like NAT -defined y1 -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of y1 * : len b<sub>1</sub> = o1 } is set
[:(x1 *),x1:] is Relation-like non empty set
bool [:(x1 *),x1:] is non empty set
[:(y1 *),y1:] is Relation-like non empty set
bool [:(y1 *),y1:] is non empty set
(arity (J,A,j,n)) -tuples_on (A . n) is functional non empty FinSequence-membered FinSequenceSet of A . n
{ b<sub>1</sub> where b<sub>1</sub> is Relation-like NAT -defined A . n -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of (A . n) * : len b<sub>1</sub> = arity (J,A,j,n) } is set
the Relation-like NAT -defined x1 -valued Function-like V31() V38(o) countable FinSequence-like FinSubsequence-like Element of o -tuples_on x1 is Relation-like NAT -defined x1 -valued Function-like V31() V38(o) countable FinSequence-like FinSubsequence-like Element of o -tuples_on x1
the Relation-like NAT -defined y1 -valued Function-like V31() V38(o1) countable FinSequence-like FinSubsequence-like Element of o1 -tuples_on y1 is Relation-like NAT -defined y1 -valued Function-like V31() V38(o1) countable FinSequence-like FinSubsequence-like Element of o1 -tuples_on y1
g is Relation-like x1 * -defined x1 -valued Function-like non empty homogeneous quasi_total Element of bool [:(x1 *),x1:]
arity g is V24() V25() V26() V30() V31() V36() countable Element of NAT
g is Relation-like y1 * -defined y1 -valued Function-like non empty homogeneous quasi_total Element of bool [:(y1 *),y1:]
arity g is V24() V25() V26() V30() V31() V36() countable Element of NAT
len the Relation-like NAT -defined y1 -valued Function-like V31() V38(o1) countable FinSequence-like FinSubsequence-like Element of o1 -tuples_on y1 is V24() V25() V26() V30() V31() V36() countable Element of NAT
len the Relation-like NAT -defined x1 -valued Function-like V31() V38(o) countable FinSequence-like FinSubsequence-like Element of o -tuples_on x1 is V24() V25() V26() V30() V31() V36() countable Element of NAT
J is Relation-like Function-like Function-yielding V45() set
proj1 J is set
A is Relation-like Function-like set
ua is set
J . ua is Relation-like Function-like set
A . ua is set
(J . ua) . (A . ua) is set
ua is Relation-like Function-like set
proj1 ua is set
pr is set
ua . pr is set
J . pr is Relation-like Function-like set
A . pr is set
(J . pr) . (A . pr) is set
j is Relation-like Function-like set
proj1 j is set
ua is Relation-like Function-like set
proj1 ua is set
pr is set
j . pr is set
ua . pr is set
J . pr is Relation-like Function-like set
n is set
n9 is Relation-like Function-like set
A . pr is set
n9 . (A . pr) is set
J is set
A is Relation-like J -defined Function-like total Function-yielding V45() set
j is Relation-like J -defined Function-like total set
(A,j) is Relation-like Function-like set
proj1 (A,j) is set
proj1 A is set
J is set
A is Relation-like J -defined Function-like total Function-yielding V45() set
j is Relation-like J -defined Function-like total set
(A,j) is Relation-like J -defined Function-like set
proj1 (A,j) is set
proj1 A is set
ua is Relation-like J -defined Function-like set
J is set
A is Relation-like J -defined Function-like total Function-yielding V45() set
j is Relation-like J -defined Function-like total set
(A,j) is Relation-like J -defined Function-like total set
ua is Relation-like Function-like set
proj1 ua is set
proj1 A is set
pr is set
n is Relation-like Function-like set
A . pr is Relation-like Function-like set
ua . pr is set
j . pr is set
n . (j . pr) is set
pr is set
ua . pr is set
A . pr is Relation-like Function-like set
j . pr is set
(A . pr) . (j . pr) is set
J is non empty set
A is Relation-like non-empty non empty-yielding J -defined Function-like non empty total set
product A is functional non empty with_common_domain product-like set
j is Relation-like NAT -defined product A -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence of product A
dom j is countable Element of bool NAT
[:(dom j),J:] is Relation-like set
uncurry j is Relation-like Function-like set
the Element of J is Element of J
proj1 A is non empty set
A . the Element of J is non empty set
proj2 A is non empty set
union (proj2 A) is set
proj2 j is set
pr is non empty set
Funcs (J,pr) is non empty FUNCTION_DOMAIN of J,pr
n is set
n9 is Relation-like Function-like set
proj1 n9 is set
proj2 n9 is set
o is set
j is set
n9 . j is set
A . j is set
proj1 (uncurry j) is set
J is non empty set
A is Relation-like non-empty non empty-yielding J -defined Function-like non empty total set
product A is functional non empty with_common_domain product-like set
j is Relation-like NAT -defined product A -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence of product A
dom j is countable Element of bool NAT
[:(dom j),J:] is Relation-like set
uncurry j is Relation-like [:(dom j),J:] -defined Function-like set
the Element of J is Element of J
proj1 A is non empty set
A . the Element of J is non empty set
proj2 A is non empty set
union (proj2 A) is set
proj2 j is set
pr is non empty set
Funcs (J,pr) is non empty FUNCTION_DOMAIN of J,pr
n is set
n9 is Relation-like Function-like set
proj1 n9 is set
proj2 n9 is set
o is set
j is set
n9 . j is set
A . j is set
proj1 (uncurry j) is set
n is Relation-like [:(dom j),J:] -defined Function-like set
ua is Relation-like [:(dom j),J:] -defined Function-like set
J is set
A is set
[:J,A:] is Relation-like set
[:A,J:] is Relation-like set
j is Relation-like [:J,A:] -defined Function-like total set
~ j is Relation-like Function-like set
proj1 j is set
proj1 (~ j) is set
J is set
A is set
[:J,A:] is Relation-like set
[:A,J:] is Relation-like set
j is Relation-like [:J,A:] -defined Function-like total set
~ j is Relation-like [:A,J:] -defined Function-like set
proj1 j is set
proj1 (~ j) is set
ua is Relation-like [:A,J:] -defined Function-like set
J is set
A is non empty set
[:J,A:] is Relation-like set
j is Relation-like [:J,A:] -defined Function-like total set
curry j is Relation-like Function-like set
proj1 j is set
proj1 (curry j) is set
proj1 (proj1 j) is set
J is set
A is non empty set
[:J,A:] is Relation-like set
j is Relation-like [:J,A:] -defined Function-like total set
curry j is Relation-like J -defined Function-like set
proj1 j is set
proj1 (curry j) is set
proj1 (proj1 j) is set
pr is Relation-like J -defined Function-like set
J is non empty set
A is Relation-like non-empty non empty-yielding J -defined Function-like non empty total set
j is Relation-like J -defined Function-like non empty total Function-yielding V45() () (J,A)
the Element of J is Element of J
(J,A,j, the Element of J) is Relation-like (A . the Element of J) * -defined A . the Element of J -valued Function-like non empty homogeneous quasi_total Element of bool [:((A . the Element of J) *),(A . the Element of J):]
A . the Element of J is non empty set
(A . the Element of J) * is functional non empty FinSequence-membered FinSequenceSet of A . the Element of J
[:((A . the Element of J) *),(A . the Element of J):] is Relation-like non empty set
bool [:((A . the Element of J) *),(A . the Element of J):] is non empty set
arity (J,A,j, the Element of J) is V24() V25() V26() V30() V31() V36() countable Element of NAT
pr is Element of J
(J,A,j,pr) is Relation-like (A . pr) * -defined A . pr -valued Function-like non empty homogeneous quasi_total Element of bool [:((A . pr) *),(A . pr):]
A . pr is non empty set
(A . pr) * is functional non empty FinSequence-membered FinSequenceSet of A . pr
[:((A . pr) *),(A . pr):] is Relation-like non empty set
bool [:((A . pr) *),(A . pr):] is non empty set
arity (J,A,j,pr) is V24() V25() V26() V30() V31() V36() countable Element of NAT
the Element of J is Element of J
pr is V24() V25() V26() V30() V31() V36() countable set
n is V24() V25() V26() V30() V31() V36() countable set
(J,A,j, the Element of J) is Relation-like (A . the Element of J) * -defined A . the Element of J -valued Function-like non empty homogeneous quasi_total Element of bool [:((A . the Element of J) *),(A . the Element of J):]
A . the Element of J is non empty set
(A . the Element of J) * is functional non empty FinSequence-membered FinSequenceSet of A . the Element of J
[:((A . the Element of J) *),(A . the Element of J):] is Relation-like non empty set
bool [:((A . the Element of J) *),(A . the Element of J):] is non empty set
arity (J,A,j, the Element of J) is V24() V25() V26() V30() V31() V36() countable Element of NAT
J is set
A is Relation-like J -defined Function-like total set
j is Relation-like Function-like set
proj1 j is set
ua is Relation-like J -defined Function-like total set
pr is set
ua . pr is set
A . pr is set
{} (A . pr) 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 bool (A . pr)
bool (A . pr) is non empty set
j is Relation-like J -defined Function-like total set
ua is Relation-like J -defined Function-like total set
pr is set
j . pr is set
ua . pr is set
A . pr is set
{} (A . pr) 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 bool (A . pr)
bool (A . pr) is non empty set
J is non empty set
A is Relation-like non-empty non empty-yielding J -defined Function-like non empty total set
product A is functional non empty with_common_domain product-like set
(product A) * is functional non empty FinSequence-membered FinSequenceSet of product A
[:((product A) *),(product A):] is Relation-like non empty set
bool [:((product A) *),(product A):] is non empty set
j is Relation-like J -defined Function-like non empty total Function-yielding V45() () (J,A)
(J,A,j) is V24() V25() V26() V30() V31() V36() countable set
(J,A,j) -tuples_on (product A) is functional non empty FinSequence-membered FinSequenceSet of product A
{ b<sub>1</sub> where b<sub>1</sub> is Relation-like NAT -defined product A -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of (product A) * : len b<sub>1</sub> = (J,A,j) } is set
(J,A) is Relation-like J -defined Function-like non empty total set
(J,j,(J,A)) is Relation-like J -defined Function-like non empty total set
o is set
j is Relation-like NAT -defined product A -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like Element of (product A) *
len j is V24() V25() V26() V30() V31() V36() countable Element of NAT
dom j is countable Element of bool NAT
proj1 A is non empty set
o is set
(J,j,(J,A)) . o is set
A . o is set
o1 is Element of J
(J,A,j,o1) is Relation-like (A . o1) * -defined A . o1 -valued Function-like non empty homogeneous quasi_total Element of bool [:((A . o1) *),(A . o1):]
A . o1 is non empty set
(A . o1) * is functional non empty FinSequence-membered FinSequenceSet of A . o1
[:((A . o1) *),(A . o1):] is Relation-like non empty set
bool [:((A . o1) *),(A . o1):] is non empty set
proj2 (J,A,j,o1) is non empty set
arity (J,A,j,o1) is V24() V25() V26() V30() V31() V36() countable Element of NAT
proj1 (J,A,j,o1) is functional non empty with_common_domain FinSequence-membered set
0 -tuples_on (A . o1) is functional non empty FinSequence-membered FinSequenceSet of A . o1
{ b<sub>1</sub> where b<sub>1</sub> is Relation-like NAT -defined A . o1 -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of (A . o1) * : len b<sub>1</sub> = 0 } is set
[:NAT,(A . o1):] is Relation-like non empty V31() set
bool [:NAT,(A . o1):] is non empty V31() set
<*> (A . o1) is Relation-like non-empty empty-yielding NAT -defined A . o1 -valued Function-like one-to-one constant functional empty proper V24() V25() V26() V28() V29() V30() V31() V36() V38( {} ) Cardinal-yielding with_common_domain countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of A . o1
{(<*> (A . o1))} is functional non empty trivial V38(1) with_common_domain Element of bool (bool [:NAT,(A . o1):])
bool (bool [:NAT,(A . o1):]) is non empty V31() set
{} (A . o1) is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty proper 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 bool (A . o1)
bool (A . o1) is non empty set
(J,A,j,o1) . ({} (A . o1)) is set
(J,A) . o1 is set
(J,A,j,o1) . ((J,A) . o1) is set
proj1 (J,j,(J,A)) is non empty set
o is Relation-like J -defined Function-like non empty total set
o1 is Relation-like NAT -defined product A -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like Element of (product A) *
dom o1 is countable Element of bool NAT
uncurry o1 is Relation-like [:(dom o1),J:] -defined Function-like total set
[:(dom o1),J:] is Relation-like set
~ (uncurry o1) is Relation-like [:J,(dom o1):] -defined Function-like total set
[:J,(dom o1):] is Relation-like set
x1 is non empty set
[:J,x1:] is Relation-like non empty set
y1 is Relation-like [:J,x1:] -defined Function-like non empty total set
curry y1 is Relation-like J -defined Function-like non empty total set
(J,j,(curry y1)) is Relation-like J -defined Function-like non empty total set
dom j is countable Element of bool NAT
o is non empty set
[:J,o:] is Relation-like non empty set
uncurry j is Relation-like [:(dom j),J:] -defined Function-like total set
[:(dom j),J:] is Relation-like set
~ (uncurry j) is Relation-like [:J,(dom j):] -defined Function-like total set
[:J,(dom j):] is Relation-like set
o1 is Relation-like [:J,o:] -defined Function-like non empty total set
curry o1 is Relation-like J -defined Function-like non empty total set
(J,j,(curry o1)) is Relation-like J -defined Function-like non empty total set
proj1 A is non empty set
y1 is set
(J,j,(curry o1)) . y1 is set
A . y1 is set
proj1 o1 is non empty set
proj1 (proj1 o1) is set
j is Element of J
(curry o1) . j is set
{j} is non empty trivial V38(1) Element of bool J
bool J is non empty set
proj2 (proj1 o1) is set
[:{j},(proj2 (proj1 o1)):] is Relation-like set
(proj1 o1) /\ [:{j},(proj2 (proj1 o1)):] is Relation-like set
proj2 ((proj1 o1) /\ [:{j},(proj2 (proj1 o1)):]) is set
g is Relation-like Function-like set
proj1 g is set
J /\ {j} is Element of bool J
o /\ o is set
[:(J /\ {j}),(o /\ o):] is Relation-like set
proj2 [:(J /\ {j}),(o /\ o):] is set
[:{j},o:] is Relation-like non empty set
proj2 [:{j},o:] is non empty set
Seg (len j) is V31() V38( len j) countable Element of bool NAT
g is Relation-like NAT -defined Function-like V31() countable FinSequence-like FinSubsequence-like set
proj2 g is set
A . j is non empty set
g is set
dom g is countable Element of bool NAT
g is set
g . g is set
proj1 (uncurry j) is set
[g,j] is V15() set
{g,j} is non empty set
{g} is non empty trivial V38(1) set
{{g,j},{g}} is non empty set
a is set
b is set
[a,b] is V15() set
{a,b} is non empty set
{a} is non empty trivial V38(1) set
{{a,b},{a}} is non empty set
f is Relation-like Function-like set
j . a is Relation-like Function-like set
proj1 f is set
(~ (uncurry j)) . (j,g) is set
[j,g] is V15() set
{j,g} is non empty set
{j} is non empty trivial V38(1) set
{{j,g},{j}} is non empty set
(~ (uncurry j)) . [j,g] is set
(uncurry j) . (g,j) is set
(uncurry j) . [g,j] is set
[a,b] `1 is set
[a,b] `2 is set
f . j is set
proj2 j is set
(A . j) * is functional non empty FinSequence-membered FinSequenceSet of A . j
g is Relation-like NAT -defined A . j -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of A . j
(J,A,j,j) is Relation-like (A . j) * -defined A . j -valued Function-like non empty homogeneous quasi_total Element of bool [:((A . j) *),(A . j):]
[:((A . j) *),(A . j):] is Relation-like non empty set
bool [:((A . j) *),(A . j):] is non empty set
arity (J,A,j,j) is V24() V25() V26() V30() V31() V36() countable Element of NAT
proj1 (J,A,j,j) is functional non empty with_common_domain FinSequence-membered set
(J,A,j) -tuples_on (A . j) is functional non empty FinSequence-membered FinSequenceSet of A . j
{ b₁ where b₁ is Relation-like NAT -defined A . j -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of (A . j) * : len b₁ = (J,A,j) } is set
g is Relation-like NAT -defined A . j -valued Function-like V31() countable FinSequence-like FinSubsequence-like Element of (A . j) *
len g is V24() V25() V26() V30() V31() V36() countable Element of NAT
(J,A,j,j) . g is set
proj2 (J,A,j,j) is non empty set
(J,A,j,j) . ((curry o1) . j) is set
proj1 (J,j,(curry o1)) is non empty set
x1 is Relation-like J -defined Function-like non empty total set
y1 is Relation-like NAT -defined product A -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like Element of (product A) *
dom y1 is countable Element of bool NAT
uncurry y1 is Relation-like [:(dom y1),J:] -defined Function-like total set
[:(dom y1),J:] is Relation-like set
~ (uncurry y1) is Relation-like [:J,(dom y1):] -defined Function-like total set
[:J,(dom y1):] is Relation-like set
j is non empty set
[:J,j:] is Relation-like non empty set
g is Relation-like [:J,j:] -defined Function-like non empty total set
curry g is Relation-like J -defined Function-like non empty total set
(J,j,(curry g)) is Relation-like J -defined Function-like non empty total set
dom j is countable Element of bool NAT
dom j is countable Element of bool NAT
o is Relation-like J -defined Function-like non empty total set
o1 is Relation-like J -defined Function-like non empty total set
o is Relation-like Function-like set
proj1 o is set
proj2 o is set
{ (b₁ -tuples_on (product A)) where b₁ is V24() V25() V26() V30() V31() V36() countable Element of NAT : verum } is set
union { (b₁ -tuples_on (product A)) where b₁ is V24() V25() V26() V30() V31() V36() countable Element of NAT : verum } is set
j is Relation-like (product A) * -defined product A -valued Function-like Function-yielding V45() Element of bool [:((product A) *),(product A):]
o is Relation-like NAT -defined Function-like V31() countable FinSequence-like FinSubsequence-like set
proj1 j is functional FinSequence-membered set
o1 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
len o1 is V24() V25() V26() V30() V31() V36() countable Element of NAT
x1 is Relation-like NAT -defined product A -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like Element of (product A) *
y1 is Relation-like NAT -defined product A -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like Element of (product A) *
j is Relation-like NAT -defined product A -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like Element of (product A) *
len j is V24() V25() V26() V30() V31() V36() countable Element of NAT
g is Relation-like NAT -defined product A -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like Element of (product A) *
len g is V24() V25() V26() V30() V31() V36() countable Element of NAT
o is Relation-like NAT -defined product A -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence of product A
len o is V24() V25() V26() V30() V31() V36() countable Element of NAT
o1 is Relation-like NAT -defined product A -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence of product A
len o1 is V24() V25() V26() V30() V31() V36() countable Element of NAT
proj1 j is functional FinSequence-membered set
x1 is Relation-like NAT -defined product A -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like Element of (product A) *
y1 is Relation-like NAT -defined product A -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like Element of (product A) *
j is Relation-like NAT -defined product A -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like Element of (product A) *
len j is V24() V25() V26() V30() V31() V36() countable Element of NAT
o is Relation-like (product A) * -defined product A -valued Function-like non empty Function-yielding V45() homogeneous quasi_total Element of bool [:((product A) *),(product A):]
proj1 o is functional non empty with_common_domain FinSequence-membered set
o1 is Relation-like NAT -defined product A -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like Element of (product A) *
dom o1 is countable Element of bool NAT
o . o1 is Relation-like Function-like set
uncurry o1 is Relation-like [:(dom o1),J:] -defined Function-like total set
[:(dom o1),J:] is Relation-like set
~ (uncurry o1) is Relation-like [:J,(dom o1):] -defined Function-like total set
[:J,(dom o1):] is Relation-like set
x1 is non empty set
[:J,x1:] is Relation-like non empty set
y1 is Relation-like [:J,x1:] -defined Function-like non empty total set
curry y1 is Relation-like J -defined Function-like non empty total set
(J,j,(curry y1)) is Relation-like J -defined Function-like non empty total set
n is Relation-like (product A) * -defined product A -valued Function-like non empty Function-yielding V45() homogeneous quasi_total Element of bool [:((product A) *),(product A):]
proj1 n is functional non empty with_common_domain FinSequence-membered set
n9 is Relation-like (product A) * -defined product A -valued Function-like non empty Function-yielding V45() homogeneous quasi_total Element of bool [:((product A) *),(product A):]
proj1 n9 is functional non empty with_common_domain FinSequence-membered set
o is set
n . o is Relation-like Function-like set
n9 . o is Relation-like Function-like set
j is Relation-like NAT -defined product A -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like Element of (product A) *
len j is V24() V25() V26() V30() V31() V36() countable Element of NAT
dom j is countable Element of bool NAT
n . j is Relation-like Function-like set
dom j is countable Element of bool NAT
o is non empty set
[:J,o:] is Relation-like non empty set
uncurry j is Relation-like [:(dom j),J:] -defined Function-like total set
[:(dom j),J:] is Relation-like set
~ (uncurry j) is Relation-like [:J,(dom j):] -defined Function-like total set
[:J,(dom j):] is Relation-like set
n . j is Relation-like Function-like set
o1 is Relation-like [:J,o:] -defined Function-like non empty total set
curry o1 is Relation-like J -defined Function-like non empty total set
(J,j,(curry o1)) is Relation-like J -defined Function-like non empty total set
dom j is countable Element of bool NAT
dom j is countable Element of bool NAT
J is non empty set
j is V24() V25() V26() V30() V31() V36() countable set
A is Relation-like J -defined Function-like non empty total () () () set
(J,A) is Relation-like NAT -defined NAT -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of NAT
dom (J,A) is countable Element of bool NAT
(J,A) is Relation-like non-empty non empty-yielding J -defined Function-like non empty total set
ua is set
pr is Element of J
(J,A,pr) is non empty V88() quasi_total non-empty UAStr
signature (J,A,pr) is Relation-like NAT -defined NAT -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of NAT
dom (signature (J,A,pr)) is countable Element of bool NAT
len (signature (J,A,pr)) is V24() V25() V26() V30() V31() V36() countable Element of NAT
Seg (len (signature (J,A,pr))) is V31() V38( len (signature (J,A,pr))) countable Element of bool NAT
the charact of (J,A,pr) is Relation-like non-empty NAT -defined PFuncs (( the carrier of (J,A,pr) *), the carrier of (J,A,pr)) -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,pr) *), the carrier of (J,A,pr))
the carrier of (J,A,pr) is non empty set
the carrier of (J,A,pr) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (J,A,pr)
PFuncs (( the carrier of (J,A,pr) *), the carrier of (J,A,pr)) is functional non empty set
len the charact of (J,A,pr) is non empty V24() V25() V26() V30() V31() V36() countable Element of NAT
Seg (len the charact of (J,A,pr)) is non empty V31() V38( len the charact of (J,A,pr)) countable Element of bool NAT
dom the charact of (J,A,pr) is non empty countable Element of bool NAT
Operations (J,A,pr) is non empty PFuncsDomHQN of the carrier of (J,A,pr)
proj2 the charact of (J,A,pr) is non empty set
the charact of (J,A,pr) . j is Relation-like Function-like homogeneous set
n is Relation-like the carrier of (J,A,pr) * -defined the carrier of (J,A,pr) -valued Function-like non empty homogeneous quasi_total Element of Operations (J,A,pr)
n9 is Element of J
(J,A,n9) is non empty V88() quasi_total non-empty UAStr
the carrier of (J,A,n9) is non empty set
the carrier of (J,A,n9) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (J,A,n9)
Operations (J,A,n9) is non empty PFuncsDomHQN of the carrier of (J,A,n9)
the charact of (J,A,n9) is Relation-like non-empty NAT -defined PFuncs (( the carrier of (J,A,n9) *), the carrier of (J,A,n9)) -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,n9) *), the carrier of (J,A,n9))
PFuncs (( the carrier of (J,A,n9) *), the carrier of (J,A,n9)) is functional non empty set
proj2 the charact of (J,A,n9) is non empty set
the charact of (J,A,n9) . j is Relation-like Function-like homogeneous set
o is Relation-like the carrier of (J,A,n9) * -defined the carrier of (J,A,n9) -valued Function-like non empty homogeneous quasi_total Element of Operations (J,A,n9)
ua is Relation-like Function-like set
proj1 ua is set
pr is Relation-like J -defined Function-like non empty total set
proj1 pr is non empty set
n is set
pr . n is set
n9 is Element of J
(J,A,n9) is non empty V88() quasi_total non-empty UAStr
signature (J,A,n9) is Relation-like NAT -defined NAT -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of NAT
dom (signature (J,A,n9)) is countable Element of bool NAT
len (signature (J,A,n9)) is V24() V25() V26() V30() V31() V36() countable Element of NAT
Seg (len (signature (J,A,n9))) is V31() V38( len (signature (J,A,n9))) countable Element of bool NAT
the charact of (J,A,n9) is Relation-like non-empty NAT -defined PFuncs (( the carrier of (J,A,n9) *), the carrier of (J,A,n9)) -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,n9) *), the carrier of (J,A,n9))
the carrier of (J,A,n9) is non empty set
the carrier of (J,A,n9) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (J,A,n9)
PFuncs (( the carrier of (J,A,n9) *), the carrier of (J,A,n9)) is functional non empty set
len the charact of (J,A,n9) is non empty V24() V25() V26() V30() V31() V36() countable Element of NAT
Seg (len the charact of (J,A,n9)) is non empty V31() V38( len the charact of (J,A,n9)) countable Element of bool NAT
dom the charact of (J,A,n9) is non empty countable Element of bool NAT
Operations (J,A,n9) is non empty PFuncsDomHQN of the carrier of (J,A,n9)
proj2 the charact of (J,A,n9) is non empty set
the charact of (J,A,n9) . j is Relation-like Function-like homogeneous set
o is Relation-like the carrier of (J,A,n9) * -defined the carrier of (J,A,n9) -valued Function-like non empty homogeneous quasi_total Element of Operations (J,A,n9)
n is Relation-like J -defined Function-like non empty total Function-yielding V45() set
n9 is Element of J
n . n9 is Relation-like Function-like set
(J,A) . n9 is non empty set
((J,A) . n9) * is functional non empty FinSequence-membered FinSequenceSet of (J,A) . n9
[:(((J,A) . n9) *),((J,A) . n9):] is Relation-like non empty set
bool [:(((J,A) . n9) *),((J,A) . n9):] is non empty set
(J,A,n9) is non empty V88() quasi_total non-empty UAStr
signature (J,A,n9) is Relation-like NAT -defined NAT -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of NAT
dom (signature (J,A,n9)) is countable Element of bool NAT
len (signature (J,A,n9)) is V24() V25() V26() V30() V31() V36() countable Element of NAT
Seg (len (signature (J,A,n9))) is V31() V38( len (signature (J,A,n9))) countable Element of bool NAT
the charact of (J,A,n9) is Relation-like non-empty NAT -defined PFuncs (( the carrier of (J,A,n9) *), the carrier of (J,A,n9)) -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,n9) *), the carrier of (J,A,n9))
the carrier of (J,A,n9) is non empty set
the carrier of (J,A,n9) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (J,A,n9)
PFuncs (( the carrier of (J,A,n9) *), the carrier of (J,A,n9)) is functional non empty set
len the charact of (J,A,n9) is non empty V24() V25() V26() V30() V31() V36() countable Element of NAT
Seg (len the charact of (J,A,n9)) is non empty V31() V38( len the charact of (J,A,n9)) countable Element of bool NAT
dom the charact of (J,A,n9) is non empty countable Element of bool NAT
Operations (J,A,n9) is non empty PFuncsDomHQN of the carrier of (J,A,n9)
proj2 the charact of (J,A,n9) is non empty set
the charact of (J,A,n9) . j is Relation-like Function-like homogeneous set
o is Relation-like the carrier of (J,A,n9) * -defined the carrier of (J,A,n9) -valued Function-like non empty homogeneous quasi_total Element of Operations (J,A,n9)
j is 1-sorted
the carrier of j is set
n9 is Relation-like J -defined Function-like non empty total Function-yielding V45() (J,(J,A))
o is Element of J
(J,(J,A),n9,o) is Relation-like ((J,A) . o) * -defined (J,A) . o -valued Function-like non empty homogeneous quasi_total Element of bool [:(((J,A) . o) *),((J,A) . o):]
(J,A) . o is non empty set
((J,A) . o) * is functional non empty FinSequence-membered FinSequenceSet of (J,A) . o
[:(((J,A) . o) *),((J,A) . o):] is Relation-like non empty set
bool [:(((J,A) . o) *),((J,A) . o):] is non empty set
arity (J,(J,A),n9,o) is V24() V25() V26() V30() V31() V36() countable Element of NAT
j is Element of J
(J,(J,A),n9,j) is Relation-like ((J,A) . j) * -defined (J,A) . j -valued Function-like non empty homogeneous quasi_total Element of bool [:(((J,A) . j) *),((J,A) . j):]
(J,A) . j is non empty set
((J,A) . j) * is functional non empty FinSequence-membered FinSequenceSet of (J,A) . j
[:(((J,A) . j) *),((J,A) . j):] is Relation-like non empty set
bool [:(((J,A) . j) *),((J,A) . j):] is non empty set
arity (J,(J,A),n9,j) is V24() V25() V26() V30() V31() V36() countable Element of NAT
(J,A,j) is non empty V88() quasi_total non-empty UAStr
signature (J,A,j) is Relation-like NAT -defined NAT -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of NAT
dom (signature (J,A,j)) is countable Element of bool NAT
len (signature (J,A,j)) is V24() V25() V26() V30() V31() V36() countable Element of NAT
Seg (len (signature (J,A,j))) is V31() V38( len (signature (J,A,j))) countable Element of bool NAT
the charact of (J,A,j) is Relation-like non-empty NAT -defined PFuncs (( the carrier of (J,A,j) *), the carrier of (J,A,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,A,j) *), the carrier of (J,A,j))
the carrier of (J,A,j) is non empty set
the carrier of (J,A,j) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (J,A,j)
PFuncs (( the carrier of (J,A,j) *), the carrier of (J,A,j)) is functional non empty set
len the charact of (J,A,j) is non empty V24() V25() V26() V30() V31() V36() countable Element of NAT
Seg (len the charact of (J,A,j)) is non empty V31() V38( len the charact of (J,A,j)) countable Element of bool NAT
dom the charact of (J,A,j) is non empty countable Element of bool NAT
Operations (J,A,j) is non empty PFuncsDomHQN of the carrier of (J,A,j)
proj2 the charact of (J,A,j) is non empty set
the charact of (J,A,j) . j is Relation-like Function-like homogeneous set
(signature (J,A,j)) . j is set
o is Relation-like the carrier of (J,A,j) * -defined the carrier of (J,A,j) -valued Function-like non empty homogeneous quasi_total Element of Operations (J,A,j)
arity o is V24() V25() V26() V30() V31() V36() countable Element of NAT
proj1 A is non empty set
(J,A,o) is non empty V88() quasi_total non-empty UAStr
signature (J,A,o) is Relation-like NAT -defined NAT -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of NAT
the charact of (J,A,o) is Relation-like non-empty NAT -defined PFuncs (( the carrier of (J,A,o) *), the carrier of (J,A,o)) -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,o) *), the carrier of (J,A,o))
the carrier of (J,A,o) is non empty set
the carrier of (J,A,o) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (J,A,o)
PFuncs (( the carrier of (J,A,o) *), the carrier of (J,A,o)) is functional non empty set
len the charact of (J,A,o) is non empty V24() V25() V26() V30() V31() V36() countable Element of NAT
Seg (len the charact of (J,A,o)) is non empty V31() V38( len the charact of (J,A,o)) countable Element of bool NAT
dom the charact of (J,A,o) is non empty countable Element of bool NAT
Operations (J,A,o) is non empty PFuncsDomHQN of the carrier of (J,A,o)
proj2 the charact of (J,A,o) is non empty set
the charact of (J,A,o) . j is Relation-like Function-like homogeneous set
o1 is Relation-like the carrier of (J,A,o) * -defined the carrier of (J,A,o) -valued Function-like non empty homogeneous quasi_total Element of Operations (J,A,o)
o is Relation-like J -defined Function-like non empty total Function-yielding V45() () (J,(J,A))
j is Element of J
(J,A,j) is non empty V88() quasi_total non-empty UAStr
the carrier of (J,A,j) is non empty set
the carrier of (J,A,j) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (J,A,j)
Operations (J,A,j) is non empty PFuncsDomHQN of the carrier of (J,A,j)
the charact of (J,A,j) is Relation-like non-empty NAT -defined PFuncs (( the carrier of (J,A,j) *), the carrier of (J,A,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,A,j) *), the carrier of (J,A,j))
PFuncs (( the carrier of (J,A,j) *), the carrier of (J,A,j)) is functional non empty set
proj2 the charact of (J,A,j) is non empty set
the charact of (J,A,j) . j is Relation-like Function-like homogeneous set
(J,(J,A),o,j) is Relation-like ((J,A) . j) * -defined (J,A) . j -valued Function-like non empty homogeneous quasi_total Element of bool [:(((J,A) . j) *),((J,A) . j):]
(J,A) . j is non empty set
((J,A) . j) * is functional non empty FinSequence-membered FinSequenceSet of (J,A) . j
[:(((J,A) . j) *),((J,A) . j):] is Relation-like non empty set
bool [:(((J,A) . j) *),((J,A) . j):] is non empty set
o is Relation-like the carrier of (J,A,j) * -defined the carrier of (J,A,j) -valued Function-like non empty homogeneous quasi_total Element of Operations (J,A,j)
ua is Relation-like J -defined Function-like non empty total Function-yielding V45() () (J,(J,A))
pr is Relation-like J -defined Function-like non empty total Function-yielding V45() () (J,(J,A))
n is set
ua . n is Relation-like Function-like set
pr . n is Relation-like Function-like set
n9 is Element of J
(J,A,n9) is non empty V88() quasi_total non-empty UAStr
signature (J,A,n9) is Relation-like NAT -defined NAT -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of NAT
dom (signature (J,A,n9)) is countable Element of bool NAT
len (signature (J,A,n9)) is V24() V25() V26() V30() V31() V36() countable Element of NAT
Seg (len (signature (J,A,n9))) is V31() V38( len (signature (J,A,n9))) countable Element of bool NAT
the charact of (J,A,n9) is Relation-like non-empty NAT -defined PFuncs (( the carrier of (J,A,n9) *), the carrier of (J,A,n9)) -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,n9) *), the carrier of (J,A,n9))
the carrier of (J,A,n9) is non empty set
the carrier of (J,A,n9) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (J,A,n9)
PFuncs (( the carrier of (J,A,n9) *), the carrier of (J,A,n9)) is functional non empty set
len the charact of (J,A,n9) is non empty V24() V25() V26() V30() V31() V36() countable Element of NAT
Seg (len the charact of (J,A,n9)) is non empty V31() V38( len the charact of (J,A,n9)) countable Element of bool NAT
dom the charact of (J,A,n9) is non empty countable Element of bool NAT
Operations (J,A,n9) is non empty PFuncsDomHQN of the carrier of (J,A,n9)
proj2 the charact of (J,A,n9) is non empty set
the charact of (J,A,n9) . j is Relation-like Function-like homogeneous set
(J,(J,A),ua,n9) is Relation-like ((J,A) . n9) * -defined (J,A) . n9 -valued Function-like non empty homogeneous quasi_total Element of bool [:(((J,A) . n9) *),((J,A) . n9):]
(J,A) . n9 is non empty set
((J,A) . n9) * is functional non empty FinSequence-membered FinSequenceSet of (J,A) . n9
[:(((J,A) . n9) *),((J,A) . n9):] is Relation-like non empty set
bool [:(((J,A) . n9) *),((J,A) . n9):] is non empty set
o is Relation-like the carrier of (J,A,n9) * -defined the carrier of (J,A,n9) -valued Function-like non empty homogeneous quasi_total Element of Operations (J,A,n9)
J is non empty set
A is Relation-like J -defined Function-like non empty total () () () set
(J,A) is Relation-like non-empty non empty-yielding J -defined Function-like non empty total set
product (J,A) is functional non empty with_common_domain product-like set
(product (J,A)) * is functional non empty FinSequence-membered FinSequenceSet of product (J,A)
PFuncs (((product (J,A)) *),(product (J,A))) is functional non empty set
(J,A) is Relation-like NAT -defined NAT -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of 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
ua is V24() V25() V26() V30() V31() V36() countable set
(J,A,ua) is Relation-like J -defined Function-like non empty total Function-yielding V45() () (J,(J,A))
(J,(J,A),(J,A,ua)) is Relation-like (product (J,A)) * -defined product (J,A) -valued Function-like non empty Function-yielding V45() homogeneous quasi_total Element of bool [:((product (J,A)) *),(product (J,A)):]
[:((product (J,A)) *),(product (J,A)):] is Relation-like non empty set
bool [:((product (J,A)) *),(product (J,A)):] is non empty set
pr is Relation-like Function-like Element of PFuncs (((product (J,A)) *),(product (J,A)))
ua is Relation-like NAT -defined PFuncs (((product (J,A)) *),(product (J,A))) -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((product (J,A)) *),(product (J,A)))
dom ua is countable Element of bool NAT
pr is Relation-like NAT -defined PFuncs (((product (J,A)) *),(product (J,A))) -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((product (J,A)) *),(product (J,A)))
len pr is V24() V25() V26() V30() V31() V36() countable Element of NAT
dom pr is countable Element of bool NAT
n is V24() V25() V26() V30() V31() V36() countable set
pr . n is Relation-like Function-like set
(J,A,n) is Relation-like J -defined Function-like non empty total Function-yielding V45() () (J,(J,A))
(J,(J,A),(J,A,n)) is Relation-like (product (J,A)) * -defined product (J,A) -valued Function-like non empty Function-yielding V45() homogeneous quasi_total Element of bool [:((product (J,A)) *),(product (J,A)):]
[:((product (J,A)) *),(product (J,A)):] is Relation-like non empty set
bool [:((product (J,A)) *),(product (J,A)):] is non empty set
j is Relation-like NAT -defined PFuncs (((product (J,A)) *),(product (J,A))) -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((product (J,A)) *),(product (J,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 (((product (J,A)) *),(product (J,A))) -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((product (J,A)) *),(product (J,A)))
len ua is V24() V25() V26() V30() V31() V36() countable Element of NAT
dom ua is countable Element of bool NAT
Seg (len (J,A)) is V31() V38( len (J,A)) countable Element of bool NAT
pr is V24() V25() V26() V30() V31() V36() countable set
j . pr is Relation-like Function-like set
(J,A,pr) is Relation-like J -defined Function-like non empty total Function-yielding V45() () (J,(J,A))
(J,(J,A),(J,A,pr)) is Relation-like (product (J,A)) * -defined product (J,A) -valued Function-like non empty Function-yielding V45() homogeneous quasi_total Element of bool [:((product (J,A)) *),(product (J,A)):]
[:((product (J,A)) *),(product (J,A)):] is Relation-like non empty set
bool [:((product (J,A)) *),(product (J,A)):] is non empty set
ua . pr is Relation-like Function-like set
J is non empty set
A is Relation-like J -defined Function-like non empty total () () () set
(J,A) is Relation-like non-empty non empty-yielding J -defined Function-like non empty total set
product (J,A) is functional non empty with_common_domain product-like set
(J,A) is Relation-like NAT -defined PFuncs (((product (J,A)) *),(product (J,A))) -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((product (J,A)) *),(product (J,A)))
(product (J,A)) * is functional non empty FinSequence-membered FinSequenceSet of product (J,A)
PFuncs (((product (J,A)) *),(product (J,A))) is functional non empty set
UAStr(# (product (J,A)),(J,A) #) is non empty strict UAStr
the Element of J is Element of J
[:((product (J,A)) *),(product (J,A)):] is Relation-like non empty set
bool [:((product (J,A)) *),(product (J,A)):] is non empty set
the charact of UAStr(# (product (J,A)),(J,A) #) is Relation-like NAT -defined PFuncs (( the carrier of UAStr(# (product (J,A)),(J,A) #) *), the carrier of UAStr(# (product (J,A)),(J,A) #)) -valued Function-like V31() countable Function-yielding V45() FinSequence-like FinSubsequence-like FinSequence of PFuncs (( the carrier of UAStr(# (product (J,A)),(J,A) #) *), the carrier of UAStr(# (product (J,A)),(J,A) #))
the carrier of UAStr(# (product (J,A)),(J,A) #) is non empty set
the carrier of UAStr(# (product (J,A)),(J,A) #) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of UAStr(# (product (J,A)),(J,A) #)
PFuncs (( the carrier of UAStr(# (product (J,A)),(J,A) #) *), the carrier of UAStr(# (product (J,A)),(J,A) #)) is functional non empty set
dom the charact of UAStr(# (product (J,A)),(J,A) #) is countable Element of bool NAT
n is V24() V25() V26() V30() V31() V36() countable set
the charact of UAStr(# (product (J,A)),(J,A) #) . n is Relation-like Function-like set
n9 is Relation-like (product (J,A)) * -defined product (J,A) -valued Function-like Function-yielding V45() Element of bool [:((product (J,A)) *),(product (J,A)):]
(J,A,n) is Relation-like J -defined Function-like non empty total Function-yielding V45() () (J,(J,A))
(J,(J,A),(J,A,n)) is Relation-like (product (J,A)) * -defined product (J,A) -valued Function-like non empty Function-yielding V45() homogeneous quasi_total Element of bool [:((product (J,A)) *),(product (J,A)):]
n is V24() V25() V26() V30() V31() V36() countable set
the charact of UAStr(# (product (J,A)),(J,A) #) . n is Relation-like Function-like set
n9 is Relation-like (product (J,A)) * -defined product (J,A) -valued Function-like Function-yielding V45() Element of bool [:((product (J,A)) *),(product (J,A)):]
(J,A,n) is Relation-like J -defined Function-like non empty total Function-yielding V45() () (J,(J,A))
(J,(J,A),(J,A,n)) is Relation-like (product (J,A)) * -defined product (J,A) -valued Function-like non empty Function-yielding V45() homogeneous quasi_total Element of bool [:((product (J,A)) *),(product (J,A)):]
n is set
the charact of UAStr(# (product (J,A)),(J,A) #) . n is Relation-like Function-like set
n9 is V24() V25() V26() V30() V31() V36() countable Element of NAT
(J,A,n9) is Relation-like J -defined Function-like non empty total Function-yielding V45() () (J,(J,A))
(J,(J,A),(J,A,n9)) is Relation-like (product (J,A)) * -defined product (J,A) -valued Function-like non empty Function-yielding V45() homogeneous quasi_total Element of bool [:((product (J,A)) *),(product (J,A)):]
len the charact of UAStr(# (product (J,A)),(J,A) #) is V24() V25() V26() V30() V31() V36() countable Element of NAT
(J,A) is Relation-like NAT -defined NAT -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of NAT
len (J,A) is V24() V25() V26() V30() V31() V36() countable Element of NAT
(J,A, the Element of J) is non empty V88() quasi_total non-empty UAStr
signature (J,A, the Element of J) is Relation-like NAT -defined NAT -valued Function-like V31() countable FinSequence-like FinSubsequence-like FinSequence of NAT
len (signature (J,A, the Element of J)) is V24() V25() V26() V30() V31() V36() countable Element of NAT
the charact of (J,A, the Element of J) is Relation-like non-empty NAT -defined PFuncs (( the carrier of (J,A, the Element of J) *), the carrier of (J,A, the Element 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,A, the Element of J) *), the carrier of (J,A, the Element of J))
the carrier of (J,A, the Element of J) is non empty set
the carrier of (J,A, the Element of J) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (J,A, the Element of J)
PFuncs (( the carrier of (J,A, the Element of J) *), the carrier of (J,A, the Element of J)) is functional non empty set
len the charact of (J,A, the Element of J) is non empty V24() V25() V26() V30() V31() V36() countable Element of NAT