:: PUA2MSS1 semantic presentation

REAL is set
NAT is non empty V4() V5() V6() V44() V49() V50() countable denumerable Element of bool REAL
bool REAL is non empty set
NAT is non empty V4() V5() V6() V44() V49() V50() countable denumerable set
bool NAT is non empty V44() set
bool NAT is non empty V44() set
BOOLEAN is non empty set
0 is empty V4() V5() V6() V8() V9() V10() V14() Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V44() V49() V51( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding with_common_domain countable Element of NAT
{} is empty V4() V5() V6() V8() V9() V10() V14() Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V44() V49() V51( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding with_common_domain countable set
the empty V4() V5() V6() V8() V9() V10() V14() Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V44() V49() V51( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding with_common_domain countable set is empty V4() V5() V6() V8() V9() V10() V14() Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V44() V49() V51( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding with_common_domain countable set
1 is non empty V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
{0,1} is non empty set
2 is non empty V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
3 is non empty V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
Seg 1 is non empty trivial V44() V51(1) countable Element of bool NAT
{1} is non empty trivial with_non-empty_elements non empty-membered V51(1) set
Seg 2 is non empty V44() V51(2) countable Element of bool NAT
{1,2} is non empty with_non-empty_elements non empty-membered set
A is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
dom A is countable Element of bool NAT
len A is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
Seg (len A) is V44() V51( len A) countable Element of bool NAT
P is Relation-like Function-like set
proj1 P is set
A is set
P is non empty set
[:A,P:] is Relation-like set
bool [:A,P:] is non empty set
S1 is Relation-like NAT -defined A -valued Function-like V44() FinSequence-like FinSubsequence-like countable FinSequence of A
S2 is Relation-like A -defined P -valued Function-like total quasi_total Element of bool [:A,P:]
S2 * S1 is Relation-like NAT -defined P -valued Function-like Element of bool [:NAT,P:]
[:NAT,P:] is non empty Relation-like V44() set
bool [:NAT,P:] is non empty V44() set
rng S1 is Element of bool A
bool A is non empty set
dom S2 is Element of bool A
dom (S2 * S1) is countable Element of bool NAT
dom S1 is countable Element of bool NAT
rng (S2 * S1) is Element of bool P
bool P is non empty set
A is with_non-empty_elements set
P is Relation-like NAT -defined A -valued Function-like V44() FinSequence-like FinSubsequence-like countable FinSequence of A
S1 is set
proj1 P is set
P . S1 is set
dom P is countable Element of bool NAT
rng P is Element of bool A
bool A is non empty set
A is non empty set
A * is non empty functional FinSequence-membered FinSequenceSet of A
PFuncs ((A *),A) is non empty functional set
[:(A *),A:] is non empty Relation-like set
bool [:(A *),A:] is non empty set
the non empty Relation-like A * -defined A -valued Function-like homogeneous quasi_total Element of bool [:(A *),A:] is non empty Relation-like A * -defined A -valued Function-like homogeneous quasi_total Element of bool [:(A *),A:]
S1 is Relation-like Function-like Element of PFuncs ((A *),A)
<*S1*> is non empty trivial Relation-like NAT -defined PFuncs ((A *),A) -valued Function-like constant V44() V51(1) FinSequence-like FinSubsequence-like countable FinSequence of PFuncs ((A *),A)
S2 is V4() V5() V6() V10() V14() V44() V49() countable set
dom <*S1*> is non empty trivial V51(1) countable Element of bool NAT
G is Relation-like A * -defined A -valued Function-like Element of bool [:(A *),A:]
<*S1*> . S2 is Relation-like Function-like set
S2 is V4() V5() V6() V10() V14() V44() V49() countable set
G is Relation-like A * -defined A -valued Function-like Element of bool [:(A *),A:]
<*S1*> . S2 is Relation-like Function-like set
S2 is set
<*S1*> . S2 is Relation-like Function-like set
A is UAStr
the charact of A is Relation-like NAT -defined PFuncs (( the carrier of A *), the carrier of A) -valued Function-like V44() FinSequence-like FinSubsequence-like countable FinSequence of PFuncs (( the carrier of A *), the carrier of A)
the carrier of A is set
the carrier of A * is non empty functional FinSequence-membered FinSequenceSet of the carrier of A
PFuncs (( the carrier of A *), the carrier of A) is non empty functional set
P is non empty Relation-like Function-like set
proj1 P is non empty set
the Element of proj1 P is Element of proj1 P
P . the Element of proj1 P is set
S2 is non empty set
proj2 P is non empty set
[:( the carrier of A *), the carrier of A:] is Relation-like set
bool [:( the carrier of A *), the carrier of A:] is non empty set
A is Relation-like non-empty Function-like set
product A is non empty functional with_common_domain product-like set
P is Relation-like non-empty Function-like set
product P is non empty functional with_common_domain product-like set
proj1 A is set
proj1 P is set
the Relation-like Function-like A -compatible Element of product A is Relation-like Function-like A -compatible Element of product A
S2 is Relation-like Function-like set
proj1 S2 is set
G is Relation-like Function-like set
proj1 G is set
S2 is set
A . S2 is set
P . S2 is set
G is set
G is Relation-like Function-like set
R is Relation-like Function-like set
proj1 R is set
SG is set
R . SG is set
G . SG is set
A . SG is set
R . S2 is set
SG is Relation-like Function-like set
proj1 SG is set
em is Relation-like Function-like set
proj1 em is set
A is Relation-like non-empty Function-like set
product A is non empty functional with_common_domain product-like set
P is Relation-like non-empty Function-like set
product P is non empty functional with_common_domain product-like set
the Relation-like Function-like A -compatible Element of product A is Relation-like Function-like A -compatible Element of product A
proj1 P is set
proj1 A is set
S2 is set
A . S2 is set
P . S2 is set
G is Relation-like Function-like set
proj1 G is set
Q is Relation-like Function-like set
proj1 Q is set
S2 is Relation-like Function-like set
proj1 S2 is set
G is Relation-like Function-like set
proj1 G is set
A is non empty set
A * is non empty functional FinSequence-membered FinSequenceSet of A
PFuncs ((A *),A) is non empty functional set
P is Relation-like NAT -defined PFuncs ((A *),A) -valued Function-like V44() FinSequence-like FinSubsequence-like countable FinSequence of PFuncs ((A *),A)
proj2 P is set
bool (PFuncs ((A *),A)) is non empty set
A is non empty set
P is non empty set
PFuncs (A,P) is non empty functional set
bool (PFuncs (A,P)) is non empty set
S1 is non empty functional Element of bool (PFuncs (A,P))
[:A,P:] is non empty Relation-like set
bool [:A,P:] is non empty set
S2 is Relation-like Function-like Element of S1
A is non empty non-empty UAStr
the charact of A is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of A *), the carrier of A) -valued Function-like V44() FinSequence-like FinSubsequence-like countable FinSequence of PFuncs (( the carrier of A *), the carrier of A)
the carrier of A is non empty set
the carrier of A * is non empty functional FinSequence-membered FinSequenceSet of the carrier of A
PFuncs (( the carrier of A *), the carrier of A) is non empty functional set
dom the charact of A is non empty countable Element of bool NAT
P is Element of dom the charact of A
the charact of A . P is non empty Relation-like Function-like set
( the carrier of A, the charact of A) is non empty functional with_non-empty_elements non empty-membered Element of bool (PFuncs (( the carrier of A *), the carrier of A))
bool (PFuncs (( the carrier of A *), the carrier of A)) is non empty set
A is set
S1 is set
S2 is set
P is with_non-empty_elements a_partition of A
G is set
A is set
P is set
S1 is Relation-like NAT -defined A -valued Function-like V44() FinSequence-like FinSubsequence-like countable FinSequence of A
product S1 is functional with_common_domain product-like set
dom S1 is countable Element of bool NAT
S2 is set
S1 . S2 is set
rng S1 is Element of bool A
bool A is non empty set
S2 is Relation-like Function-like set
proj1 S2 is set
proj2 S2 is set
len S1 is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
Seg (len S1) is V44() V51( len S1) countable Element of bool NAT
product S2 is functional with_common_domain product-like set
A is set
P is with_non-empty_elements a_partition of A
S1 is with_non-empty_elements a_partition of A
[:P,S1:] is Relation-like set
bool [:P,S1:] is non empty set
S2 is Relation-like non-empty P -defined S1 -valued Function-like quasi_total Element of bool [:P,S1:]
G is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable FinSequence of P
product G is non empty functional with_common_domain product-like set
S2 * G is Relation-like non-empty NAT -defined S1 -valued Function-like Element of bool [:NAT,S1:]
[:NAT,S1:] is Relation-like set
bool [:NAT,S1:] is non empty set
Q is Relation-like non-empty NAT -defined S1 -valued Function-like V44() FinSequence-like FinSubsequence-like countable FinSequence of S1
product Q is non empty functional with_common_domain product-like set
rng G is with_non-empty_elements Element of bool P
bool P is non empty set
G is non empty set
dom S2 is Element of bool P
dom (S2 * G) is countable Element of bool NAT
dom G is countable Element of bool NAT
dom Q is countable Element of bool NAT
G is set
G . G is set
Q . G is set
rng Q is with_non-empty_elements Element of bool S1
bool S1 is non empty set
R is non empty set
bool R is non empty set
SG is non empty with_non-empty_elements non empty-membered a_partition of R
em is non empty Element of SG
the Element of em is Element of em
S2 . em is set
em is non empty with_non-empty_elements non empty-membered a_partition of R
(S2 * G) . G is set
G is set
Q . G is set
G . G is set
S2 . (G . G) is set
A is set
union A is set
P is Relation-like Function-like set
proj2 P is set
proj1 P is set
S1 is set
P . S1 is set
S2 is set
S1 is Relation-like Function-like set
proj1 S1 is set
proj2 S1 is set
product S1 is functional with_common_domain product-like set
A is set
P is with_non-empty_elements a_partition of A
S1 is Relation-like NAT -defined A -valued Function-like V44() FinSequence-like FinSubsequence-like countable FinSequence of A
rng S1 is Element of bool A
bool A is non empty set
union P is Element of bool A
dom S1 is countable Element of bool NAT
S2 is Relation-like Function-like set
proj1 S2 is set
proj2 S2 is set
product S2 is functional with_common_domain product-like set
len S1 is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
Seg (len S1) is V44() V51( len S1) countable Element of bool NAT
A is non empty set
P is non empty set
bool A is non empty set
bool P is non empty set
[:A,P:] is non empty Relation-like set
S1 is non empty with_non-empty_elements non empty-membered a_partition of A
S2 is non empty with_non-empty_elements non empty-membered a_partition of P
{ [:b₁,b₂:] where b₁ is non empty Element of S1, b₂ is non empty Element of S2 : verum } is set
bool [:A,P:] is non empty Element of bool (bool [:A,P:])
bool [:A,P:] is non empty set
bool (bool [:A,P:]) is non empty set
Q is set
G is non empty Element of S1
R is non empty Element of S2
[:G,R:] is non empty Relation-like A -defined P -valued Element of bool [:A,P:]
Q is Element of bool (bool [:A,P:])
union Q is Relation-like A -defined P -valued Element of bool [:A,P:]
G is set
R is set
[G,R] is V26() set
{G,R} is non empty set
{G} is non empty trivial V51(1) set
{{G,R},{G}} is non empty with_non-empty_elements non empty-membered set
union S1 is non empty Element of bool A
SG is set
union S2 is non empty Element of bool P
em is set
[:SG,em:] is Relation-like set
G is Relation-like A -defined P -valued Element of bool [:A,P:]
R is non empty Element of S1
SG is non empty Element of S2
[:R,SG:] is non empty Relation-like A -defined P -valued Element of bool [:A,P:]
em is Relation-like A -defined P -valued Element of bool [:A,P:]
em is non empty Element of S1
f is non empty Element of S2
[:em,f:] is non empty Relation-like A -defined P -valued Element of bool [:A,P:]
R /\ em is Element of bool A
SG /\ f is Element of bool P
G /\ em is Relation-like A -defined P -valued Element of bool [:A,P:]
[:{},(SG /\ f):] is Relation-like set
[:(R /\ em),{}:] is Relation-like set
A is non empty set
A * is non empty functional FinSequence-membered FinSequenceSet of A
P is non empty with_non-empty_elements non empty-membered a_partition of A
P * is non empty functional FinSequence-membered FinSequenceSet of P
{ (product b₁) where b₁ is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P * : verum } is set
bool (A *) is non empty Element of bool (bool (A *))
bool (A *) is non empty set
bool (bool (A *)) is non empty set
S2 is set
G is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P *
product G is non empty functional with_common_domain product-like set
Q is set
dom G is countable Element of bool NAT
G is Relation-like Function-like set
proj1 G is set
len G is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
Seg (len G) is V44() V51( len G) countable Element of bool NAT
proj2 G is set
R is set
SG is set
G . SG is set
G . SG is set
rng G is with_non-empty_elements Element of bool P
bool P is non empty set
S2 is Element of bool (bool (A *))
union S2 is functional FinSequence-membered Element of bool (A *)
G is set
Q is Relation-like NAT -defined A -valued Function-like V44() FinSequence-like FinSubsequence-like countable FinSequence of A
rng Q is Element of bool A
bool A is non empty set
union P is non empty Element of bool A
dom Q is countable Element of bool NAT
G is Relation-like Function-like set
proj1 G is set
proj2 G is set
product G is functional with_common_domain product-like set
len Q is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
Seg (len Q) is V44() V51( len Q) countable Element of bool NAT
R is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
SG is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable FinSequence of P
em is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P *
product em is non empty functional with_common_domain product-like set
G is functional FinSequence-membered Element of bool (A *)
Q is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P *
product Q is non empty functional with_common_domain product-like set
G is functional FinSequence-membered Element of bool (A *)
R is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P *
product R is non empty functional with_common_domain product-like set
SG is set
dom Q is countable Element of bool NAT
em is Relation-like Function-like set
proj1 em is set
dom R is countable Element of bool NAT
em is set
em . em is set
Q . em is set
R . em is set
f is Relation-like Function-like set
proj1 f is set
rng Q is with_non-empty_elements Element of bool P
bool P is non empty set
rng R is with_non-empty_elements Element of bool P
f is Relation-like Function-like set
proj1 f is set
em is Relation-like Function-like set
proj1 em is set
A is non empty set
P is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
P -tuples_on A is non empty functional FinSequence-membered FinSequenceSet of A
S1 is non empty with_non-empty_elements non empty-membered a_partition of A
P -tuples_on S1 is non empty functional FinSequence-membered FinSequenceSet of S1
{ (product b₁) where b₁ is Relation-like non-empty NAT -defined S1 -valued Function-like V44() V51(P) FinSequence-like FinSubsequence-like countable Element of P -tuples_on S1 : verum } is set
bool (P -tuples_on A) is non empty Element of bool (bool (P -tuples_on A))
bool (P -tuples_on A) is non empty set
bool (bool (P -tuples_on A)) is non empty set
G is set
R is Relation-like non-empty NAT -defined S1 -valued Function-like V44() V51(P) FinSequence-like FinSubsequence-like countable Element of P -tuples_on S1
product R is non empty functional with_common_domain product-like set
SG is set
dom R is V51(P) countable Element of bool NAT
em is Relation-like Function-like set
proj1 em is set
len R is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
Seg (len R) is V44() V51( len R) countable Element of bool NAT
proj2 em is set
f is set
g is set
em . g is set
R . g is set
rng R is with_non-empty_elements Element of bool S1
bool S1 is non empty set
em is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
len em is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
G is Element of bool (bool (P -tuples_on A))
union G is functional FinSequence-membered Element of bool (P -tuples_on A)
R is set
SG is Relation-like NAT -defined A -valued Function-like V44() V51(P) FinSequence-like FinSubsequence-like countable Element of P -tuples_on A
rng SG is Element of bool A
bool A is non empty set
union S1 is non empty Element of bool A
dom SG is V51(P) countable Element of bool NAT
em is Relation-like Function-like set
proj1 em is set
proj2 em is set
product em is functional with_common_domain product-like set
len SG is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
Seg (len SG) is V44() V51( len SG) countable Element of bool NAT
em is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
f is Relation-like non-empty NAT -defined S1 -valued Function-like V44() FinSequence-like FinSubsequence-like countable FinSequence of S1
len f is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
g is Relation-like non-empty NAT -defined S1 -valued Function-like V44() V51(P) FinSequence-like FinSubsequence-like countable Element of P -tuples_on S1
product g is non empty functional with_common_domain product-like set
R is functional FinSequence-membered Element of bool (P -tuples_on A)
SG is Relation-like non-empty NAT -defined S1 -valued Function-like V44() V51(P) FinSequence-like FinSubsequence-like countable Element of P -tuples_on S1
product SG is non empty functional with_common_domain product-like set
em is functional FinSequence-membered Element of bool (P -tuples_on A)
em is Relation-like non-empty NAT -defined S1 -valued Function-like V44() V51(P) FinSequence-like FinSubsequence-like countable Element of P -tuples_on S1
product em is non empty functional with_common_domain product-like set
f is set
dom SG is V51(P) countable Element of bool NAT
g is Relation-like Function-like set
proj1 g is set
dom em is V51(P) countable Element of bool NAT
g is set
g . g is set
SG . g is set
em . g is set
s1 is Relation-like Function-like set
proj1 s1 is set
rng SG is with_non-empty_elements Element of bool S1
bool S1 is non empty set
rng em is with_non-empty_elements Element of bool S1
s1 is Relation-like Function-like set
proj1 s1 is set
g is Relation-like Function-like set
proj1 g is set
A is non empty set
bool A is non empty set
P is set
S1 is non empty with_non-empty_elements non empty-membered a_partition of A
{ (b₁ /\ P) where b₁ is non empty Element of S1 : not b₁ misses P } is set
bool P is non empty Element of bool (bool P)
bool P is non empty set
bool (bool P) is non empty set
G is set
A /\ P is set
Q is non empty Element of S1
Q /\ P is Element of bool A
G is Element of bool (bool P)
union G is Element of bool P
Q is set
union S1 is non empty Element of bool A
G is set
G /\ P is set
Q is Element of bool P
G is non empty Element of S1
G /\ P is Element of bool A
R is Element of bool P
SG is non empty Element of S1
SG /\ P is Element of bool A
A is non empty Relation-like Function-like set
proj1 A is non empty set
bool (proj1 A) is non empty set
S1 is non empty with_non-empty_elements non empty-membered a_partition of proj1 A
{ (A | b₁) where b₁ is non empty Element of S1 : verum } is set
bool A is non empty Element of bool (bool A)
bool A is non empty set
bool (bool A) is non empty set
Q is set
G is non empty Element of S1
A | G is non empty Relation-like Function-like set
Q is Element of bool (bool A)
union Q is Relation-like Function-like Element of bool A
G is set
R is set
[G,R] is V26() set
{G,R} is non empty set
{G} is non empty trivial V51(1) set
{{G,R},{G}} is non empty with_non-empty_elements non empty-membered set
union S1 is non empty Element of bool (proj1 A)
SG is set
A | SG is Relation-like Function-like set
G is Relation-like Function-like Element of bool A
R is non empty Element of S1
A | R is non empty Relation-like Function-like set
em is Relation-like Function-like Element of bool A
em is non empty Element of S1
A | em is non empty Relation-like Function-like set
SG is non empty Element of bool (proj1 A)
f is set
g is set
g is set
[g,g] is V26() set
{g,g} is non empty set
{g} is non empty trivial V51(1) set
{{g,g},{g}} is non empty with_non-empty_elements non empty-membered set
A is set
SmallestPartition A is with_non-empty_elements a_partition of A
id A is Relation-like A -defined A -valued Function-like one-to-one total quasi_total onto bijective reflexive symmetric antisymmetric transitive Element of bool [:A,A:]
[:A,A:] is Relation-like set
bool [:A,A:] is non empty set
Class (id A) is with_non-empty_elements a_partition of A
S1 is Relation-like non-empty NAT -defined SmallestPartition A -valued Function-like V44() FinSequence-like FinSubsequence-like countable FinSequence of SmallestPartition A
product S1 is non empty functional with_common_domain product-like set
the Relation-like NAT -defined Function-like S1 -compatible Element of product S1 is Relation-like NAT -defined Function-like S1 -compatible Element of product S1
dom the Relation-like NAT -defined Function-like S1 -compatible Element of product S1 is countable Element of bool NAT
dom S1 is countable Element of bool NAT
G is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
Union S1 is set
Funcs ((dom S1),(Union S1)) is functional set
rng S1 is with_non-empty_elements Element of bool (SmallestPartition A)
bool (SmallestPartition A) is non empty set
union (rng S1) is set
union (SmallestPartition A) is Element of bool A
bool A is non empty set
proj2 G is set
Q is Relation-like Function-like set
proj1 Q is set
proj2 Q is set
Q is Relation-like NAT -defined A -valued Function-like V44() FinSequence-like FinSubsequence-like countable FinSequence of A
{Q} is non empty trivial functional V51(1) with_common_domain set
G is set
R is Relation-like Function-like set
proj1 R is set
SG is set
R . SG is set
S1 . SG is set
Q . SG is set
em is non empty set
{ {b₁} where b₁ is Element of em : verum } is set
em is Element of em
{em} is non empty trivial V51(1) set
A is set
the with_non-empty_elements a_partition of A is with_non-empty_elements a_partition of A
id the with_non-empty_elements a_partition of A is Relation-like non-empty the with_non-empty_elements a_partition of A -defined the with_non-empty_elements a_partition of A -valued Function-like one-to-one total quasi_total onto bijective reflexive symmetric antisymmetric transitive Element of bool [: the with_non-empty_elements a_partition of A, the with_non-empty_elements a_partition of A:]
[: the with_non-empty_elements a_partition of A, the with_non-empty_elements a_partition of A:] is Relation-like set
bool [: the with_non-empty_elements a_partition of A, the with_non-empty_elements a_partition of A:] is non empty set
proj2 (id the with_non-empty_elements a_partition of A) is with_non-empty_elements set
A is set
P is Relation-like Function-like (A)
proj2 P is set
A is set
P is Relation-like Function-like (A)
S1 is set
proj1 P is set
P . S1 is set
(A,P) is with_non-empty_elements a_partition of A
A is non empty set
P is Relation-like non-empty Function-like one-to-one (A)
bool A is non empty set
(A,P) is non empty with_non-empty_elements non empty-membered a_partition of A
the non empty Element of (A,P) is non empty Element of (A,P)
S2 is set
[S2, the non empty Element of (A,P)] is V26() set
{S2, the non empty Element of (A,P)} is non empty set
{S2} is non empty trivial V51(1) set
{{S2, the non empty Element of (A,P)},{S2}} is non empty with_non-empty_elements non empty-membered set
A is set
P is with_non-empty_elements a_partition of A
id P is Relation-like P -defined P -valued Function-like one-to-one total reflexive symmetric antisymmetric transitive set
id P is Relation-like non-empty P -defined P -valued Function-like one-to-one total quasi_total onto bijective reflexive symmetric antisymmetric transitive Element of bool [:P,P:]
[:P,P:] is Relation-like set
bool [:P,P:] is non empty set
rng (id P) is with_non-empty_elements Element of bool P
bool P is non empty set
A is set
S1 is set
P is Relation-like non-empty Function-like one-to-one (A)
(A,P) is with_non-empty_elements a_partition of A
union (A,P) is Element of bool A
bool A is non empty set
proj1 P is set
S2 is set
G is set
P . G is set
S2 is set
P . S2 is set
G is set
P . G is set
A is set
P is Relation-like non-empty Function-like set
Union P is set
proj1 P is set
proj2 P is with_non-empty_elements set
bool A is non empty Element of bool (bool A)
bool A is non empty set
bool (bool A) is non empty set
S1 is set
union (proj2 P) is set
S1 is Element of bool (bool A)
union S1 is Element of bool A
S2 is Element of bool A
G is Element of bool A
Q is set
P . Q is set
G is set
P . G is set
S2 is set
G is set
P . S2 is set
P . G is set
Q is non empty set
the Element of Q is Element of Q
G is non empty set
P is non empty set
A is non empty set
S1 is non empty with_non-empty_elements non empty-membered a_partition of P
[:A,S1:] is non empty Relation-like set
bool [:A,S1:] is non empty set
S2 is non empty Relation-like non-empty non empty-yielding A -defined S1 -valued Function-like total quasi_total Element of bool [:A,S1:]
rng S2 is non empty with_non-empty_elements non empty-membered Element of bool S1
bool S1 is non empty set
F₁() is non empty set
F₂() is non empty set
[:F₁(),F₂():] is non empty Relation-like set
bool [:F₁(),F₂():] is non empty set
F₃() is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
F₄() is Relation-like F₁() -defined F₂() -valued Element of bool [:F₁(),F₂():]
A is Relation-like Function-like set
proj1 A is set
A . 0 is set
P is non empty Relation-like NAT -defined Function-like total set
P . 0 is set
S1 is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
P . S1 is set
S1 + 1 is non empty V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
P . (S1 + 1) is set
S2 is Relation-like F₁() -defined F₂() -valued Element of bool [:F₁(),F₂():]
F₅(S2,S1) is Relation-like F₁() -defined F₂() -valued Element of bool [:F₁(),F₂():]
P . F₃() is set
S1 is Relation-like F₁() -defined F₂() -valued Element of bool [:F₁(),F₂():]
G is Relation-like F₁() -defined F₂() -valued Element of bool [:F₁(),F₂():]
S2 is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
P . S2 is set
S2 + 1 is non empty V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
P . (S2 + 1) is set
F₅(G,S2) is Relation-like F₁() -defined F₂() -valued Element of bool [:F₁(),F₂():]
F₁() is non empty set
F₂() is non empty set
[:F₁(),F₂():] is non empty Relation-like set
bool [:F₁(),F₂():] is non empty set
A is Relation-like F₁() -defined F₂() -valued Element of bool [:F₁(),F₂():]
P is Relation-like F₁() -defined F₂() -valued Element of bool [:F₁(),F₂():]
S1 is set
S2 is set
[S1,S2] is V26() set
{S1,S2} is non empty set
{S1} is non empty trivial V51(1) set
{{S1,S2},{S1}} is non empty with_non-empty_elements non empty-membered set
G is Element of F₁()
Q is Element of F₂()
G is Element of F₁()
Q is Element of F₂()
F₁() is non empty set
F₂() is non empty set
[:F₁(),F₂():] is non empty Relation-like set
bool [:F₁(),F₂():] is non empty set
F₃() is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
F₄() is Relation-like F₁() -defined F₂() -valued Element of bool [:F₁(),F₂():]
A is Relation-like F₁() -defined F₂() -valued Element of bool [:F₁(),F₂():]
P is Relation-like F₁() -defined F₂() -valued Element of bool [:F₁(),F₂():]
S1 is non empty Relation-like NAT -defined Function-like total set
S1 . F₃() is set
S1 . 0 is set
S2 is non empty Relation-like NAT -defined Function-like total set
S2 . F₃() is set
S2 . 0 is set
G is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
S1 . G is set
S2 . G is set
G + 1 is non empty V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
S1 . (G + 1) is set
Q is Relation-like F₁() -defined F₂() -valued Element of bool [:F₁(),F₂():]
F₅(Q,G) is Relation-like F₁() -defined F₂() -valued Element of bool [:F₁(),F₂():]
S2 . (G + 1) is set
A is non empty partial non-empty UAStr
the carrier of A is non empty set
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
the carrier of A * is non empty functional FinSequence-membered FinSequenceSet of the carrier of A
the charact of A is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of A *), the carrier of A) -valued Function-like V44() FinSequence-like FinSubsequence-like countable homogeneous FinSequence of PFuncs (( the carrier of A *), the carrier of A)
PFuncs (( the carrier of A *), the carrier of A) is non empty functional set
( the carrier of A, the charact of A) is non empty functional with_non-empty_elements non empty-membered Element of bool (PFuncs (( the carrier of A *), the carrier of A))
bool (PFuncs (( the carrier of A *), the carrier of A)) is non empty set
A is non empty partial non-empty UAStr
the carrier of A is non empty set
(A) is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
S1 is set
[S1,S1] is V26() set
{S1,S1} is non empty set
{S1} is non empty trivial V51(1) set
{{S1,S1},{S1}} is non empty with_non-empty_elements non empty-membered set
the carrier of A * is non empty functional FinSequence-membered FinSequenceSet of the carrier of A
the charact of A is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of A *), the carrier of A) -valued Function-like V44() FinSequence-like FinSubsequence-like countable homogeneous FinSequence of PFuncs (( the carrier of A *), the carrier of A)
PFuncs (( the carrier of A *), the carrier of A) is non empty functional set
( the carrier of A, the charact of A) is non empty functional with_non-empty_elements non empty-membered Element of bool (PFuncs (( the carrier of A *), the carrier of A))
bool (PFuncs (( the carrier of A *), the carrier of A)) is non empty set
<*S1*> is non empty trivial Relation-like NAT -defined Function-like constant V44() V51(1) FinSequence-like FinSubsequence-like countable set
G is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
G ^ <*S1*> is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
Q is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
(G ^ <*S1*>) ^ Q is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
S2 is non empty Relation-like the carrier of A * -defined the carrier of A -valued Function-like ( the carrier of A * , the carrier of A,( the carrier of A, the charact of A))
dom S2 is non empty functional FinSequence-membered Element of bool ( the carrier of A *)
bool ( the carrier of A *) is non empty set
R is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
R ^ <*S1*> is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
SG is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
(R ^ <*S1*>) ^ SG is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
G is non empty Relation-like the carrier of A * -defined the carrier of A -valued Function-like ( the carrier of A * , the carrier of A,( the carrier of A, the charact of A))
dom G is non empty functional FinSequence-membered Element of bool ( the carrier of A *)
dom (A) is Element of bool the carrier of A
bool the carrier of A is non empty set
field (A) is set
proj1 (A) is set
proj2 (A) is set
(proj1 (A)) \/ (proj2 (A)) is set
S1 is set
S2 is set
[S1,S2] is V26() set
{S1,S2} is non empty set
{S1} is non empty trivial V51(1) set
{{S1,S2},{S1}} is non empty with_non-empty_elements non empty-membered set
[S2,S1] is V26() set
{S2,S1} is non empty set
{S2} is non empty trivial V51(1) set
{{S2,S1},{S2}} is non empty with_non-empty_elements non empty-membered set
the carrier of A * is non empty functional FinSequence-membered FinSequenceSet of the carrier of A
the charact of A is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of A *), the carrier of A) -valued Function-like V44() FinSequence-like FinSubsequence-like countable homogeneous FinSequence of PFuncs (( the carrier of A *), the carrier of A)
PFuncs (( the carrier of A *), the carrier of A) is non empty functional set
( the carrier of A, the charact of A) is non empty functional with_non-empty_elements non empty-membered Element of bool (PFuncs (( the carrier of A *), the carrier of A))
bool (PFuncs (( the carrier of A *), the carrier of A)) is non empty set
G is Element of the carrier of A
<*G*> is non empty trivial Relation-like NAT -defined the carrier of A -valued Function-like constant V44() V51(1) FinSequence-like FinSubsequence-like countable FinSequence of the carrier of A
Q is Element of the carrier of A
<*Q*> is non empty trivial Relation-like NAT -defined the carrier of A -valued Function-like constant V44() V51(1) FinSequence-like FinSubsequence-like countable FinSequence of the carrier of A
R is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
R ^ <*G*> is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
SG is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
(R ^ <*G*>) ^ SG is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
G is non empty Relation-like the carrier of A * -defined the carrier of A -valued Function-like ( the carrier of A * , the carrier of A,( the carrier of A, the charact of A))
dom G is non empty functional FinSequence-membered Element of bool ( the carrier of A *)
bool ( the carrier of A *) is non empty set
R ^ <*Q*> is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
(R ^ <*Q*>) ^ SG is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
em is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
em ^ <*Q*> is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
f is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
(em ^ <*Q*>) ^ f is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
em is non empty Relation-like the carrier of A * -defined the carrier of A -valued Function-like ( the carrier of A * , the carrier of A,( the carrier of A, the charact of A))
dom em is non empty functional FinSequence-membered Element of bool ( the carrier of A *)
em ^ <*G*> is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
(em ^ <*G*>) ^ f is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
S1 is set
S2 is set
G is set
[S1,S2] is V26() set
{S1,S2} is non empty set
{S1} is non empty trivial V51(1) set
{{S1,S2},{S1}} is non empty with_non-empty_elements non empty-membered set
[S2,G] is V26() set
{S2,G} is non empty set
{S2} is non empty trivial V51(1) set
{{S2,G},{S2}} is non empty with_non-empty_elements non empty-membered set
[S1,G] is V26() set
{S1,G} is non empty set
{{S1,G},{S1}} is non empty with_non-empty_elements non empty-membered set
the carrier of A * is non empty functional FinSequence-membered FinSequenceSet of the carrier of A
the charact of A is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of A *), the carrier of A) -valued Function-like V44() FinSequence-like FinSubsequence-like countable homogeneous FinSequence of PFuncs (( the carrier of A *), the carrier of A)
PFuncs (( the carrier of A *), the carrier of A) is non empty functional set
( the carrier of A, the charact of A) is non empty functional with_non-empty_elements non empty-membered Element of bool (PFuncs (( the carrier of A *), the carrier of A))
bool (PFuncs (( the carrier of A *), the carrier of A)) is non empty set
em is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
Q is Element of the carrier of A
<*Q*> is non empty trivial Relation-like NAT -defined the carrier of A -valued Function-like constant V44() V51(1) FinSequence-like FinSubsequence-like countable FinSequence of the carrier of A
em ^ <*Q*> is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
em is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
(em ^ <*Q*>) ^ em is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
SG is non empty Relation-like the carrier of A * -defined the carrier of A -valued Function-like ( the carrier of A * , the carrier of A,( the carrier of A, the charact of A))
dom SG is non empty functional FinSequence-membered Element of bool ( the carrier of A *)
bool ( the carrier of A *) is non empty set
G is Element of the carrier of A
<*G*> is non empty trivial Relation-like NAT -defined the carrier of A -valued Function-like constant V44() V51(1) FinSequence-like FinSubsequence-like countable FinSequence of the carrier of A
em ^ <*G*> is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
(em ^ <*G*>) ^ em is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
R is Element of the carrier of A
<*R*> is non empty trivial Relation-like NAT -defined the carrier of A -valued Function-like constant V44() V51(1) FinSequence-like FinSubsequence-like countable FinSequence of the carrier of A
em ^ <*R*> is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
(em ^ <*R*>) ^ em is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
A is non empty partial non-empty UAStr
the carrier of A is non empty set
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
P is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
the carrier of A * is non empty functional FinSequence-membered FinSequenceSet of the carrier of A
the charact of A is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of A *), the carrier of A) -valued Function-like V44() FinSequence-like FinSubsequence-like countable homogeneous FinSequence of PFuncs (( the carrier of A *), the carrier of A)
PFuncs (( the carrier of A *), the carrier of A) is non empty functional set
( the carrier of A, the charact of A) is non empty functional with_non-empty_elements non empty-membered Element of bool (PFuncs (( the carrier of A *), the carrier of A))
bool (PFuncs (( the carrier of A *), the carrier of A)) is non empty set
A is non empty partial non-empty UAStr
the carrier of A is non empty set
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
S1 is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
P is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
A is non empty partial non-empty UAStr
the carrier of A is non empty set
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
P is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
(A,P,0) is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
(A,P,1) is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
(A,P) is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
S1 is non empty Relation-like NAT -defined Function-like total set
S1 . 0 is set
0 + 1 is non empty V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
S1 . (0 + 1) is set
A is non empty partial non-empty UAStr
the carrier of A is non empty set
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
P is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
P + 1 is non empty V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
S1 is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
(A,S1,(P + 1)) is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
(A,S1,P) is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
(A,(A,S1,P)) is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
S2 is non empty Relation-like NAT -defined Function-like total set
S2 . P is set
S2 . 0 is set
S2 . (P + 1) is set
A is non empty partial non-empty UAStr
the carrier of A is non empty set
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
P is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
S1 is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
P + S1 is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
S2 is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
(A,S2,(P + S1)) is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
(A,S2,P) is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
(A,(A,S2,P),S1) is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
P + 0 is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
(A,S2,(P + 0)) is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
(A,(A,S2,P),0) is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
G is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
P + G is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
(A,S2,(P + G)) is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
(A,(A,S2,P),G) is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
G + 1 is non empty V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
P + (G + 1) is non empty V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
(A,S2,(P + (G + 1))) is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
(P + G) + 1 is non empty V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
(A,S2,((P + G) + 1)) is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
(A,(A,S2,(P + G))) is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
(A,(A,S2,P),(G + 1)) is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
A is non empty partial non-empty UAStr
the carrier of A is non empty set
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
(A) is Relation-like the carrier of A -defined the carrier of A -valued total quasi_total reflexive symmetric transitive Element of bool [: the carrier of A, the carrier of A:]
P is Relation-like the carrier of A -defined the carrier of A -valued total quasi_total reflexive symmetric transitive Element of bool [: the carrier of A, the carrier of A:]
(A,P) is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
S1 is set
S2 is Element of the carrier of A
[S2,S2] is V26() set
{S2,S2} is non empty set
{S2} is non empty trivial V51(1) set
{{S2,S2},{S2}} is non empty with_non-empty_elements non empty-membered set
the carrier of A * is non empty functional FinSequence-membered FinSequenceSet of the carrier of A
the charact of A is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of A *), the carrier of A) -valued Function-like V44() FinSequence-like FinSubsequence-like countable homogeneous FinSequence of PFuncs (( the carrier of A *), the carrier of A)
PFuncs (( the carrier of A *), the carrier of A) is non empty functional set
( the carrier of A, the charact of A) is non empty functional with_non-empty_elements non empty-membered Element of bool (PFuncs (( the carrier of A *), the carrier of A))
bool (PFuncs (( the carrier of A *), the carrier of A)) is non empty set
Q is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
<*S2*> is non empty trivial Relation-like NAT -defined the carrier of A -valued Function-like constant V44() V51(1) FinSequence-like FinSubsequence-like countable FinSequence of the carrier of A
Q ^ <*S2*> is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
G is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
(Q ^ <*S2*>) ^ G is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
G is non empty Relation-like the carrier of A * -defined the carrier of A -valued Function-like ( the carrier of A * , the carrier of A,( the carrier of A, the charact of A))
dom G is non empty functional FinSequence-membered Element of bool ( the carrier of A *)
bool ( the carrier of A *) is non empty set
G . ((Q ^ <*S2*>) ^ G) is set
rng G is non empty Element of bool the carrier of A
bool the carrier of A is non empty set
[(G . ((Q ^ <*S2*>) ^ G)),(G . ((Q ^ <*S2*>) ^ G))] is V26() set
{(G . ((Q ^ <*S2*>) ^ G)),(G . ((Q ^ <*S2*>) ^ G))} is non empty set
{(G . ((Q ^ <*S2*>) ^ G))} is non empty trivial V51(1) set
{{(G . ((Q ^ <*S2*>) ^ G)),(G . ((Q ^ <*S2*>) ^ G))},{(G . ((Q ^ <*S2*>) ^ G))}} is non empty with_non-empty_elements non empty-membered set
[S1,S1] is V26() set
{S1,S1} is non empty set
{S1} is non empty trivial V51(1) set
{{S1,S1},{S1}} is non empty with_non-empty_elements non empty-membered set
dom (A,P) is Element of bool the carrier of A
field (A,P) is set
proj1 (A,P) is set
proj2 (A,P) is set
(proj1 (A,P)) \/ (proj2 (A,P)) is set
S1 is set
S2 is set
[S1,S2] is V26() set
{S1,S2} is non empty set
{S1} is non empty trivial V51(1) set
{{S1,S2},{S1}} is non empty with_non-empty_elements non empty-membered set
G is Element of the carrier of A
Q is Element of the carrier of A
[G,Q] is V26() set
{G,Q} is non empty set
{G} is non empty trivial V51(1) set
{{G,Q},{G}} is non empty with_non-empty_elements non empty-membered set
[Q,G] is V26() set
{Q,G} is non empty set
{Q} is non empty trivial V51(1) set
{{Q,G},{Q}} is non empty with_non-empty_elements non empty-membered set
R is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
<*Q*> is non empty trivial Relation-like NAT -defined the carrier of A -valued Function-like constant V44() V51(1) FinSequence-like FinSubsequence-like countable FinSequence of the carrier of A
R ^ <*Q*> is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
SG is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
(R ^ <*Q*>) ^ SG is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
G is non empty Relation-like the carrier of A * -defined the carrier of A -valued Function-like ( the carrier of A * , the carrier of A,( the carrier of A, the charact of A))
dom G is non empty functional FinSequence-membered Element of bool ( the carrier of A *)
<*G*> is non empty trivial Relation-like NAT -defined the carrier of A -valued Function-like constant V44() V51(1) FinSequence-like FinSubsequence-like countable FinSequence of the carrier of A
R ^ <*G*> is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
(R ^ <*G*>) ^ SG is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
G . ((R ^ <*G*>) ^ SG) is set
G . ((R ^ <*Q*>) ^ SG) is set
[(G . ((R ^ <*G*>) ^ SG)),(G . ((R ^ <*Q*>) ^ SG))] is V26() set
{(G . ((R ^ <*G*>) ^ SG)),(G . ((R ^ <*Q*>) ^ SG))} is non empty set
{(G . ((R ^ <*G*>) ^ SG))} is non empty trivial V51(1) set
{{(G . ((R ^ <*G*>) ^ SG)),(G . ((R ^ <*Q*>) ^ SG))},{(G . ((R ^ <*G*>) ^ SG))}} is non empty with_non-empty_elements non empty-membered set
[(G . ((R ^ <*Q*>) ^ SG)),(G . ((R ^ <*G*>) ^ SG))] is V26() set
{(G . ((R ^ <*Q*>) ^ SG)),(G . ((R ^ <*G*>) ^ SG))} is non empty set
{(G . ((R ^ <*Q*>) ^ SG))} is non empty trivial V51(1) set
{{(G . ((R ^ <*Q*>) ^ SG)),(G . ((R ^ <*G*>) ^ SG))},{(G . ((R ^ <*Q*>) ^ SG))}} is non empty with_non-empty_elements non empty-membered set
[S2,S1] is V26() set
{S2,S1} is non empty set
{S2} is non empty trivial V51(1) set
{{S2,S1},{S2}} is non empty with_non-empty_elements non empty-membered set
S1 is set
S2 is set
G is set
[S1,S2] is V26() set
{S1,S2} is non empty set
{S1} is non empty trivial V51(1) set
{{S1,S2},{S1}} is non empty with_non-empty_elements non empty-membered set
[S2,G] is V26() set
{S2,G} is non empty set
{S2} is non empty trivial V51(1) set
{{S2,G},{S2}} is non empty with_non-empty_elements non empty-membered set
Q is Element of the carrier of A
G is Element of the carrier of A
[Q,G] is V26() set
{Q,G} is non empty set
{Q} is non empty trivial V51(1) set
{{Q,G},{Q}} is non empty with_non-empty_elements non empty-membered set
em is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
<*Q*> is non empty trivial Relation-like NAT -defined the carrier of A -valued Function-like constant V44() V51(1) FinSequence-like FinSubsequence-like countable FinSequence of the carrier of A
em ^ <*Q*> is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
em is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
(em ^ <*Q*>) ^ em is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
SG is non empty Relation-like the carrier of A * -defined the carrier of A -valued Function-like ( the carrier of A * , the carrier of A,( the carrier of A, the charact of A))
dom SG is non empty functional FinSequence-membered Element of bool ( the carrier of A *)
<*G*> is non empty trivial Relation-like NAT -defined the carrier of A -valued Function-like constant V44() V51(1) FinSequence-like FinSubsequence-like countable FinSequence of the carrier of A
em ^ <*G*> is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
(em ^ <*G*>) ^ em is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
SG . ((em ^ <*Q*>) ^ em) is set
SG . ((em ^ <*G*>) ^ em) is set
[(SG . ((em ^ <*Q*>) ^ em)),(SG . ((em ^ <*G*>) ^ em))] is V26() set
{(SG . ((em ^ <*Q*>) ^ em)),(SG . ((em ^ <*G*>) ^ em))} is non empty set
{(SG . ((em ^ <*Q*>) ^ em))} is non empty trivial V51(1) set
{{(SG . ((em ^ <*Q*>) ^ em)),(SG . ((em ^ <*G*>) ^ em))},{(SG . ((em ^ <*Q*>) ^ em))}} is non empty with_non-empty_elements non empty-membered set
R is Element of the carrier of A
<*R*> is non empty trivial Relation-like NAT -defined the carrier of A -valued Function-like constant V44() V51(1) FinSequence-like FinSubsequence-like countable FinSequence of the carrier of A
em ^ <*R*> is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
(em ^ <*R*>) ^ em is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
SG . ((em ^ <*R*>) ^ em) is set
[(SG . ((em ^ <*G*>) ^ em)),(SG . ((em ^ <*R*>) ^ em))] is V26() set
{(SG . ((em ^ <*G*>) ^ em)),(SG . ((em ^ <*R*>) ^ em))} is non empty set
{(SG . ((em ^ <*G*>) ^ em))} is non empty trivial V51(1) set
{{(SG . ((em ^ <*G*>) ^ em)),(SG . ((em ^ <*R*>) ^ em))},{(SG . ((em ^ <*G*>) ^ em))}} is non empty with_non-empty_elements non empty-membered set
[(SG . ((em ^ <*Q*>) ^ em)),(SG . ((em ^ <*R*>) ^ em))] is V26() set
{(SG . ((em ^ <*Q*>) ^ em)),(SG . ((em ^ <*R*>) ^ em))} is non empty set
{{(SG . ((em ^ <*Q*>) ^ em)),(SG . ((em ^ <*R*>) ^ em))},{(SG . ((em ^ <*Q*>) ^ em))}} is non empty with_non-empty_elements non empty-membered set
[G,R] is V26() set
{G,R} is non empty set
{G} is non empty trivial V51(1) set
{{G,R},{G}} is non empty with_non-empty_elements non empty-membered set
[Q,R] is V26() set
{Q,R} is non empty set
{{Q,R},{Q}} is non empty with_non-empty_elements non empty-membered set
[S1,G] is V26() set
{S1,G} is non empty set
{{S1,G},{S1}} is non empty with_non-empty_elements non empty-membered set
A is non empty partial non-empty UAStr
the carrier of A is non empty set
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
P is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
(A,P) is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
S1 is set
S2 is set
[S1,S2] is V26() set
{S1,S2} is non empty set
{S1} is non empty trivial V51(1) set
{{S1,S2},{S1}} is non empty with_non-empty_elements non empty-membered set
A is non empty partial non-empty UAStr
the carrier of A is non empty set
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
(A) is Relation-like the carrier of A -defined the carrier of A -valued total quasi_total reflexive symmetric transitive Element of bool [: the carrier of A, the carrier of A:]
P is Relation-like the carrier of A -defined the carrier of A -valued total quasi_total reflexive symmetric transitive Element of bool [: the carrier of A, the carrier of A:]
(A,P,0) is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
S1 is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
(A,P,S1) is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
(A,(A,P,S1)) is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
S1 + 1 is non empty V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
(A,P,(S1 + 1)) is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
S1 is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
(A,P,S1) is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
S2 is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
(A,P,S2) is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
G is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
(A,P,G) is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
A is non empty partial non-empty UAStr
(A) is Relation-like the carrier of A -defined the carrier of A -valued total quasi_total reflexive symmetric transitive Element of bool [: the carrier of A, the carrier of A:]
the carrier of A is non empty set
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
A is non empty partial non-empty UAStr
the carrier of A is non empty set
(A) is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
(A) is Relation-like the carrier of A -defined the carrier of A -valued total quasi_total reflexive symmetric transitive Element of bool [: the carrier of A, the carrier of A:]
P is set
S1 is set
[P,S1] is V26() set
{P,S1} is non empty set
{P} is non empty trivial V51(1) set
{{P,S1},{P}} is non empty with_non-empty_elements non empty-membered set
(A,(A),0) is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
A is non empty partial non-empty UAStr
the carrier of A is non empty set
(A) is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
P is set
(A) is Relation-like the carrier of A -defined the carrier of A -valued total quasi_total reflexive symmetric transitive Element of bool [: the carrier of A, the carrier of A:]
S2 is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
(A,(A),S2) is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
S1 is Element of the carrier of A
[S1,S1] is V26() set
{S1,S1} is non empty set
{S1} is non empty trivial V51(1) set
{{S1,S1},{S1}} is non empty with_non-empty_elements non empty-membered set
[P,P] is V26() set
{P,P} is non empty set
{P} is non empty trivial V51(1) set
{{P,P},{P}} is non empty with_non-empty_elements non empty-membered set
dom (A) is Element of bool the carrier of A
bool the carrier of A is non empty set
field (A) is set
proj1 (A) is set
proj2 (A) is set
(proj1 (A)) \/ (proj2 (A)) is set
P is set
S1 is set
[P,S1] is V26() set
{P,S1} is non empty set
{P} is non empty trivial V51(1) set
{{P,S1},{P}} is non empty with_non-empty_elements non empty-membered set
Q is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
(A,(A),Q) is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
S2 is Element of the carrier of A
G is Element of the carrier of A
[S2,G] is V26() set
{S2,G} is non empty set
{S2} is non empty trivial V51(1) set
{{S2,G},{S2}} is non empty with_non-empty_elements non empty-membered set
[G,S2] is V26() set
{G,S2} is non empty set
{G} is non empty trivial V51(1) set
{{G,S2},{G}} is non empty with_non-empty_elements non empty-membered set
[S1,P] is V26() set
{S1,P} is non empty set
{S1} is non empty trivial V51(1) set
{{S1,P},{S1}} is non empty with_non-empty_elements non empty-membered set
P is set
S1 is set
S2 is set
[P,S1] is V26() set
{P,S1} is non empty set
{P} is non empty trivial V51(1) set
{{P,S1},{P}} is non empty with_non-empty_elements non empty-membered set
[S1,S2] is V26() set
{S1,S2} is non empty set
{S1} is non empty trivial V51(1) set
{{S1,S2},{S1}} is non empty with_non-empty_elements non empty-membered set
R is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
(A,(A),R) is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
G is Element of the carrier of A
Q is Element of the carrier of A
[G,Q] is V26() set
{G,Q} is non empty set
{G} is non empty trivial V51(1) set
{{G,Q},{G}} is non empty with_non-empty_elements non empty-membered set
G is Element of the carrier of A
[Q,G] is V26() set
{Q,G} is non empty set
{Q} is non empty trivial V51(1) set
{{Q,G},{Q}} is non empty with_non-empty_elements non empty-membered set
[G,G] is V26() set
{G,G} is non empty set
{{G,G},{G}} is non empty with_non-empty_elements non empty-membered set
[P,S2] is V26() set
{P,S2} is non empty set
{{P,S2},{P}} is non empty with_non-empty_elements non empty-membered set
A is non empty set
A * is non empty functional FinSequence-membered FinSequenceSet of A
[:(A *),A:] is non empty Relation-like set
bool [:(A *),A:] is non empty set
A is non empty set
A * is non empty functional FinSequence-membered FinSequenceSet of A
[:(A *),A:] is non empty Relation-like set
bool [:(A *),A:] is non empty set
A is non empty partial non-empty UAStr
the carrier of A is non empty set
the carrier of A * is non empty functional FinSequence-membered FinSequenceSet of the carrier of A
the charact of A is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of A *), the carrier of A) -valued Function-like V44() FinSequence-like FinSubsequence-like countable homogeneous FinSequence of PFuncs (( the carrier of A *), the carrier of A)
PFuncs (( the carrier of A *), the carrier of A) is non empty functional set
( the carrier of A, the charact of A) is non empty functional with_non-empty_elements non empty-membered Element of bool (PFuncs (( the carrier of A *), the carrier of A))
bool (PFuncs (( the carrier of A *), the carrier of A)) is non empty set
SmallestPartition the carrier of A is non empty with_non-empty_elements non empty-membered a_partition of the carrier of A
id the carrier of A is non empty Relation-like the carrier of A -defined the carrier of A -valued Function-like one-to-one total quasi_total onto bijective reflexive symmetric antisymmetric transitive Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
Class (id the carrier of A) is non empty with_non-empty_elements non empty-membered a_partition of the carrier of A
S1 is non empty Relation-like the carrier of A * -defined the carrier of A -valued Function-like ( the carrier of A * , the carrier of A,( the carrier of A, the charact of A))
S2 is Relation-like non-empty NAT -defined SmallestPartition the carrier of A -valued Function-like V44() FinSequence-like FinSubsequence-like countable FinSequence of SmallestPartition the carrier of A
product S2 is non empty functional with_common_domain product-like set
G is Relation-like NAT -defined the carrier of A -valued Function-like V44() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of A
{G} is non empty trivial functional V51(1) with_common_domain set
dom S1 is non empty functional FinSequence-membered Element of bool ( the carrier of A *)
bool ( the carrier of A *) is non empty set
S1 . G is set
rng S1 is non empty Element of bool the carrier of A
bool the carrier of A is non empty set
Q is Element of the carrier of A
{ {b₁} where b₁ is Element of the carrier of A : verum } is set
{Q} is non empty trivial V51(1) set
G is non empty Element of SmallestPartition the carrier of A
S1 .: (product S2) is Element of bool the carrier of A
R is non empty Element of SmallestPartition the carrier of A
SG is set
em is set
S1 . em is set
S2 is Relation-like non-empty NAT -defined SmallestPartition the carrier of A -valued Function-like V44() FinSequence-like FinSubsequence-like countable FinSequence of SmallestPartition the carrier of A
product S2 is non empty functional with_common_domain product-like set
G is Relation-like NAT -defined the carrier of A -valued Function-like V44() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of A
{G} is non empty trivial functional V51(1) with_common_domain set
Q is set
G is set
F₁() is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
len F₁() is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
F₂() is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
len F₂() is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
dom F₁() is countable Element of bool NAT
A is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
len A is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
P is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
A ^ P is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
S1 is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
len S1 is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
S2 is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
S1 ^ S2 is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
S1 ^ P is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
A is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
A + 1 is non empty V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
P is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
len P is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
S1 is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
P ^ S1 is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
S2 is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
len S2 is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
G is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
S2 ^ G is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
S2 ^ S1 is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
Q is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
G is set
<*G*> is non empty trivial Relation-like NAT -defined Function-like constant V44() V51(1) FinSequence-like FinSubsequence-like countable set
Q ^ <*G*> is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
R is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
SG is set
<*SG*> is non empty trivial Relation-like NAT -defined Function-like constant V44() V51(1) FinSequence-like FinSubsequence-like countable set
R ^ <*SG*> is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
dom P is countable Element of bool NAT
Seg (len P) is V44() V51( len P) countable Element of bool NAT
dom S2 is countable Element of bool NAT
Seg (len S2) is V44() V51( len S2) countable Element of bool NAT
len <*G*> is non empty V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
len <*SG*> is non empty V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
len Q is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
(len Q) + 1 is non empty V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
len R is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
(len R) + 1 is non empty V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
<*G*> ^ S1 is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
Q ^ (<*G*> ^ S1) is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
<*SG*> ^ G is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
R ^ (<*SG*> ^ G) is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
P . ((len Q) + 1) is set
S2 . ((len R) + 1) is set
R ^ (<*G*> ^ S1) is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
F₁() . (A + 1) is set
F₂() . (A + 1) is set
R ^ <*G*> is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
(R ^ <*G*>) ^ S1 is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
F₁() ^ {} is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
F₂() ^ {} is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
A is non empty partial non-empty UAStr
the carrier of A is non empty set
the carrier of A * is non empty functional FinSequence-membered FinSequenceSet of the carrier of A
the charact of A is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of A *), the carrier of A) -valued Function-like V44() FinSequence-like FinSubsequence-like countable homogeneous FinSequence of PFuncs (( the carrier of A *), the carrier of A)
PFuncs (( the carrier of A *), the carrier of A) is non empty functional set
( the carrier of A, the charact of A) is non empty functional with_non-empty_elements non empty-membered Element of bool (PFuncs (( the carrier of A *), the carrier of A))
bool (PFuncs (( the carrier of A *), the carrier of A)) is non empty set
(A) is Relation-like the carrier of A -defined the carrier of A -valued total quasi_total reflexive symmetric transitive Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
Class (A) is non empty with_non-empty_elements non empty-membered a_partition of the carrier of A
S1 is non empty Relation-like the carrier of A * -defined the carrier of A -valued Function-like ( the carrier of A * , the carrier of A,( the carrier of A, the charact of A))
bool the carrier of A is non empty set
the non empty Element of Class (A) is non empty Element of Class (A)
S2 is Relation-like non-empty NAT -defined Class (A) -valued Function-like V44() FinSequence-like FinSubsequence-like countable FinSequence of Class (A)
product S2 is non empty functional with_common_domain product-like set
dom S1 is non empty functional FinSequence-membered Element of bool ( the carrier of A *)
bool ( the carrier of A *) is non empty set
Q is set
S1 . Q is set
Class ((A),(S1 . Q)) is Element of bool the carrier of A
{(S1 . Q)} is non empty trivial V51(1) set
(A) .: {(S1 . Q)} is set
G is non empty Element of Class (A)
S1 .: (product S2) is Element of bool the carrier of A
R is non empty Element of Class (A)
SG is set
em is set
S1 . em is set
dom S2 is countable Element of bool NAT
Union S2 is set
Funcs ((dom S2),(Union S2)) is functional set
len S2 is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
Seg (len S2) is V44() V51( len S2) countable Element of bool NAT
em is Relation-like Function-like set
f is Relation-like Function-like set
s1 is Relation-like Function-like set
proj1 s1 is set
proj2 s1 is set
o is Relation-like Function-like set
proj1 o is set
proj2 o is set
g is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
len g is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
s1 is Relation-like Function-like set
proj1 s1 is set
proj2 s1 is set
g is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
len g is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
s1 is Relation-like Function-like set
proj1 s1 is set
proj2 s1 is set
S1 . g is set
s1 is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
o is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
p is set
<*p*> is non empty trivial Relation-like NAT -defined Function-like constant V44() V51(1) FinSequence-like FinSubsequence-like countable set
s1 ^ <*p*> is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
(s1 ^ <*p*>) ^ o is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
S1 . ((s1 ^ <*p*>) ^ o) is set
a is set
[p,a] is V26() set
{p,a} is non empty set
{p} is non empty trivial V51(1) set
{{p,a},{p}} is non empty with_non-empty_elements non empty-membered set
<*a*> is non empty trivial Relation-like NAT -defined Function-like constant V44() V51(1) FinSequence-like FinSubsequence-like countable set
s1 ^ <*a*> is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
(s1 ^ <*a*>) ^ o is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
S1 . ((s1 ^ <*a*>) ^ o) is set
[(S1 . ((s1 ^ <*p*>) ^ o)),(S1 . g)] is V26() set
{(S1 . ((s1 ^ <*p*>) ^ o)),(S1 . g)} is non empty set
{(S1 . ((s1 ^ <*p*>) ^ o))} is non empty trivial V51(1) set
{{(S1 . ((s1 ^ <*p*>) ^ o)),(S1 . g)},{(S1 . ((s1 ^ <*p*>) ^ o))}} is non empty with_non-empty_elements non empty-membered set
(A) is Relation-like the carrier of A -defined the carrier of A -valued total quasi_total reflexive symmetric transitive Element of bool [: the carrier of A, the carrier of A:]
rng S1 is non empty Element of bool the carrier of A
h is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
h + 1 is non empty V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
(A,(A),(h + 1)) is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
(A,(A),h) is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
(A,(A,(A),h)) is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
[(S1 . ((s1 ^ <*p*>) ^ o)),(S1 . ((s1 ^ <*a*>) ^ o))] is V26() set
{(S1 . ((s1 ^ <*p*>) ^ o)),(S1 . ((s1 ^ <*a*>) ^ o))} is non empty set
{{(S1 . ((s1 ^ <*p*>) ^ o)),(S1 . ((s1 ^ <*a*>) ^ o))},{(S1 . ((s1 ^ <*p*>) ^ o))}} is non empty with_non-empty_elements non empty-membered set
[(S1 . ((s1 ^ <*a*>) ^ o)),(S1 . ((s1 ^ <*p*>) ^ o))] is V26() set
{(S1 . ((s1 ^ <*a*>) ^ o)),(S1 . ((s1 ^ <*p*>) ^ o))} is non empty set
{(S1 . ((s1 ^ <*a*>) ^ o))} is non empty trivial V51(1) set
{{(S1 . ((s1 ^ <*a*>) ^ o)),(S1 . ((s1 ^ <*p*>) ^ o))},{(S1 . ((s1 ^ <*a*>) ^ o))}} is non empty with_non-empty_elements non empty-membered set
[(S1 . ((s1 ^ <*a*>) ^ o)),(S1 . g)] is V26() set
{(S1 . ((s1 ^ <*a*>) ^ o)),(S1 . g)} is non empty set
{{(S1 . ((s1 ^ <*a*>) ^ o)),(S1 . g)},{(S1 . ((s1 ^ <*a*>) ^ o))}} is non empty with_non-empty_elements non empty-membered set
dom g is countable Element of bool NAT
s1 is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
g . s1 is set
g . s1 is set
[(g . s1),(g . s1)] is V26() set
{(g . s1),(g . s1)} is non empty set
{(g . s1)} is non empty trivial V51(1) set
{{(g . s1),(g . s1)},{(g . s1)}} is non empty with_non-empty_elements non empty-membered set
S2 . s1 is set
rng S2 is with_non-empty_elements Element of bool (Class (A))
bool (Class (A)) is non empty set
o is Relation-like Function-like set
proj1 o is set
proj2 o is set
o is non empty Element of Class (A)
p is Relation-like Function-like set
proj1 p is set
p is Relation-like Function-like set
proj1 p is set
a is Relation-like Function-like set
proj1 a is set
p is set
Class ((A),p) is Element of bool the carrier of A
{p} is non empty trivial V51(1) set
(A) .: {p} is set
S1 . g is set
S2 is Relation-like non-empty NAT -defined Class (A) -valued Function-like V44() FinSequence-like FinSubsequence-like countable FinSequence of Class (A)
product S2 is non empty functional with_common_domain product-like set
dom S1 is non empty functional FinSequence-membered Element of bool ( the carrier of A *)
bool ( the carrier of A *) is non empty set
(product S2) /\ (dom S1) is functional FinSequence-membered Element of bool ( the carrier of A *)
S1 .: (product S2) is Element of bool the carrier of A
S1 .: {} is empty proper V4() V5() V6() V8() V9() V10() V14() Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V44() V49() V51( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding with_common_domain countable Element of bool the carrier of A
S2 is Relation-like non-empty NAT -defined Class (A) -valued Function-like V44() FinSequence-like FinSubsequence-like countable FinSequence of Class (A)
product S2 is non empty functional with_common_domain product-like set
dom S1 is non empty functional FinSequence-membered Element of bool ( the carrier of A *)
bool ( the carrier of A *) is non empty set
dom S1 is non empty functional FinSequence-membered Element of bool ( the carrier of A *)
bool ( the carrier of A *) is non empty set
S2 is Relation-like non-empty NAT -defined Class (A) -valued Function-like V44() FinSequence-like FinSubsequence-like countable FinSequence of Class (A)
product S2 is non empty functional with_common_domain product-like set
G is set
Q is set
dom S2 is countable Element of bool NAT
Union S2 is set
Funcs ((dom S2),(Union S2)) is functional set
len S2 is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
Seg (len S2) is V44() V51( len S2) countable Element of bool NAT
G is Relation-like Function-like set
R is Relation-like Function-like set
em is Relation-like Function-like set
proj1 em is set
proj2 em is set
f is Relation-like Function-like set
proj1 f is set
proj2 f is set
SG is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
len SG is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
em is Relation-like Function-like set
proj1 em is set
proj2 em is set
em is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
len em is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
em is Relation-like Function-like set
proj1 em is set
proj2 em is set
em is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
f is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
g is set
<*g*> is non empty trivial Relation-like NAT -defined Function-like constant V44() V51(1) FinSequence-like FinSubsequence-like countable set
em ^ <*g*> is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
(em ^ <*g*>) ^ f is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
g is set
[g,g] is V26() set
{g,g} is non empty set
{g} is non empty trivial V51(1) set
{{g,g},{g}} is non empty with_non-empty_elements non empty-membered set
<*g*> is non empty trivial Relation-like NAT -defined Function-like constant V44() V51(1) FinSequence-like FinSubsequence-like countable set
em ^ <*g*> is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
(em ^ <*g*>) ^ f is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
(A) is Relation-like the carrier of A -defined the carrier of A -valued total quasi_total reflexive symmetric transitive Element of bool [: the carrier of A, the carrier of A:]
dom SG is countable Element of bool NAT
em is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
SG . em is set
em . em is set
[(SG . em),(em . em)] is V26() set
{(SG . em),(em . em)} is non empty set
{(SG . em)} is non empty trivial V51(1) set
{{(SG . em),(em . em)},{(SG . em)}} is non empty with_non-empty_elements non empty-membered set
S2 . em is set
rng S2 is with_non-empty_elements Element of bool (Class (A))
bool (Class (A)) is non empty set
f is Relation-like Function-like set
proj1 f is set
proj2 f is set
f is non empty Element of Class (A)
g is Relation-like Function-like set
proj1 g is set
g is Relation-like Function-like set
proj1 g is set
g is Relation-like Function-like set
proj1 g is set
g is set
Class ((A),g) is Element of bool the carrier of A
{g} is non empty trivial V51(1) set
(A) .: {g} is set
A is non empty partial non-empty UAStr
the carrier of A is non empty set
the carrier of A * is non empty functional FinSequence-membered FinSequenceSet of the carrier of A
the charact of A is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of A *), the carrier of A) -valued Function-like V44() FinSequence-like FinSubsequence-like countable homogeneous FinSequence of PFuncs (( the carrier of A *), the carrier of A)
PFuncs (( the carrier of A *), the carrier of A) is non empty functional set
( the carrier of A, the charact of A) is non empty functional with_non-empty_elements non empty-membered Element of bool (PFuncs (( the carrier of A *), the carrier of A))
bool (PFuncs (( the carrier of A *), the carrier of A)) is non empty set
(A) is Relation-like the carrier of A -defined the carrier of A -valued total quasi_total reflexive symmetric transitive Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
Class (A) is non empty with_non-empty_elements non empty-membered a_partition of the carrier of A
P is non empty Relation-like the carrier of A * -defined the carrier of A -valued Function-like ( the carrier of A * , the carrier of A,( the carrier of A, the charact of A))
A is non empty partial non-empty UAStr
the carrier of A is non empty set
the non empty with_non-empty_elements non empty-membered (A) is non empty with_non-empty_elements non empty-membered (A)
( the carrier of A, the non empty with_non-empty_elements non empty-membered (A)) is non empty Relation-like non-empty non empty-yielding the non empty with_non-empty_elements non empty-membered (A) -defined the non empty with_non-empty_elements non empty-membered (A) -valued Function-like one-to-one total reflexive symmetric antisymmetric transitive ( the carrier of A)
( the carrier of A,( the carrier of A, the non empty with_non-empty_elements non empty-membered (A))) is non empty with_non-empty_elements non empty-membered a_partition of the carrier of A
A is non empty partial non-empty UAStr
P is non empty Relation-like non-empty Function-like one-to-one (A)
proj2 P is non empty with_non-empty_elements non empty-membered set
A is non empty partial non-empty UAStr
the carrier of A is non empty set
(A) is Relation-like the carrier of A -defined the carrier of A -valued total quasi_total reflexive symmetric transitive Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
Class (A) is non empty with_non-empty_elements non empty-membered a_partition of the carrier of A
the carrier of A * is non empty functional FinSequence-membered FinSequenceSet of the carrier of A
the charact of A is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of A *), the carrier of A) -valued Function-like V44() FinSequence-like FinSubsequence-like countable homogeneous FinSequence of PFuncs (( the carrier of A *), the carrier of A)
PFuncs (( the carrier of A *), the carrier of A) is non empty functional set
( the carrier of A, the charact of A) is non empty functional with_non-empty_elements non empty-membered Element of bool (PFuncs (( the carrier of A *), the carrier of A))
bool (PFuncs (( the carrier of A *), the carrier of A)) is non empty set
P is non empty Relation-like the carrier of A * -defined the carrier of A -valued Function-like ( the carrier of A * , the carrier of A,( the carrier of A, the charact of A))
A is non empty set
bool A is non empty set
P is non empty with_non-empty_elements non empty-membered a_partition of A
S1 is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable FinSequence of P
product S1 is non empty functional with_common_domain product-like set
S2 is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
G is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
Q is set
<*Q*> is non empty trivial Relation-like NAT -defined Function-like constant V44() V51(1) FinSequence-like FinSubsequence-like countable set
S2 ^ <*Q*> is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
(S2 ^ <*Q*>) ^ G is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
G is set
<*G*> is non empty trivial Relation-like NAT -defined Function-like constant V44() V51(1) FinSequence-like FinSubsequence-like countable set
S2 ^ <*G*> is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
(S2 ^ <*G*>) ^ G is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
R is non empty Element of P
SG is Element of R
<*SG*> is non empty trivial Relation-like NAT -defined R -valued Function-like constant V44() V51(1) FinSequence-like FinSubsequence-like countable FinSequence of R
S2 ^ <*SG*> is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
(S2 ^ <*SG*>) ^ G is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
dom S1 is countable Element of bool NAT
em is Element of R
<*em*> is non empty trivial Relation-like NAT -defined R -valued Function-like constant V44() V51(1) FinSequence-like FinSubsequence-like countable FinSequence of R
S2 ^ <*em*> is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
(S2 ^ <*em*>) ^ G is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
dom ((S2 ^ <*em*>) ^ G) is non empty countable Element of bool NAT
len ((S2 ^ <*em*>) ^ G) is non empty V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
Seg (len ((S2 ^ <*em*>) ^ G)) is non empty V44() V51( len ((S2 ^ <*em*>) ^ G)) countable Element of bool NAT
len (S2 ^ <*em*>) is non empty V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
len G is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
(len (S2 ^ <*em*>)) + (len G) is non empty V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
Seg ((len (S2 ^ <*em*>)) + (len G)) is non empty V44() V51((len (S2 ^ <*em*>)) + (len G)) countable Element of bool NAT
len S2 is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
len <*em*> is non empty V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
(len S2) + (len <*em*>) is non empty V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
((len S2) + (len <*em*>)) + (len G) is non empty V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
Seg (((len S2) + (len <*em*>)) + (len G)) is non empty V44() V51(((len S2) + (len <*em*>)) + (len G)) countable Element of bool NAT
(len S2) + 1 is non empty V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
((len S2) + 1) + (len G) is non empty V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
Seg (((len S2) + 1) + (len G)) is non empty V44() V51(((len S2) + 1) + (len G)) countable Element of bool NAT
len <*SG*> is non empty V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
(len S2) + (len <*SG*>) is non empty V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
((len S2) + (len <*SG*>)) + (len G) is non empty V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
Seg (((len S2) + (len <*SG*>)) + (len G)) is non empty V44() V51(((len S2) + (len <*SG*>)) + (len G)) countable Element of bool NAT
len (S2 ^ <*SG*>) is non empty V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
(len (S2 ^ <*SG*>)) + (len G) is non empty V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
Seg ((len (S2 ^ <*SG*>)) + (len G)) is non empty V44() V51((len (S2 ^ <*SG*>)) + (len G)) countable Element of bool NAT
len ((S2 ^ <*SG*>) ^ G) is non empty V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
Seg (len ((S2 ^ <*SG*>) ^ G)) is non empty V44() V51( len ((S2 ^ <*SG*>) ^ G)) countable Element of bool NAT
em is Relation-like Function-like set
proj1 em is set
em is set
dom <*SG*> is non empty trivial V51(1) countable Element of bool NAT
dom (S2 ^ <*SG*>) is non empty countable Element of bool NAT
Seg ((len S2) + 1) is non empty V44() V51((len S2) + 1) countable Element of bool NAT
dom (S2 ^ <*em*>) is non empty countable Element of bool NAT
f is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
dom G is countable Element of bool NAT
g is Relation-like Function-like set
proj1 g is set
dom S2 is countable Element of bool NAT
(S2 ^ <*em*>) . em is set
S2 . em is set
(S2 ^ <*SG*>) . em is set
((S2 ^ <*em*>) ^ G) . em is set
((S2 ^ <*SG*>) ^ G) . em is set
S1 . em is set
g is Relation-like Function-like set
proj1 g is set
g is V4() V5() V6() V10() V14() V44() V49() countable set
(len S2) + g is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
g is V4() V5() V6() V10() V14() V44() V49() countable set
(len S2) + g is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
(S2 ^ <*SG*>) . f is set
(S2 ^ <*em*>) . f is set
((S2 ^ <*SG*>) ^ G) . f is set
((S2 ^ <*em*>) ^ G) . f is set
S1 . em is set
g is Relation-like Function-like set
proj1 g is set
rng S1 is with_non-empty_elements Element of bool P
bool P is non empty set
((S2 ^ <*em*>) ^ G) . em is set
g is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
(len (S2 ^ <*SG*>)) + g is non empty V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
g is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
(len (S2 ^ <*SG*>)) + g is non empty V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
((S2 ^ <*em*>) ^ G) . em is set
G . g is set
((S2 ^ <*SG*>) ^ G) . em is set
S1 . em is set
g is Relation-like Function-like set
proj1 g is set
g is V4() V5() V6() V10() V14() V44() V49() countable set
(len (S2 ^ <*SG*>)) + g is non empty V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
A is non empty partial non-empty UAStr
the carrier of A is non empty set
(A) is Relation-like the carrier of A -defined the carrier of A -valued total quasi_total reflexive symmetric transitive Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
Class (A) is non empty with_non-empty_elements non empty-membered a_partition of the carrier of A
P is non empty with_non-empty_elements non empty-membered (A)
S1 is Relation-like the carrier of A -defined the carrier of A -valued total quasi_total reflexive symmetric transitive Element of bool [: the carrier of A, the carrier of A:]
Class S1 is non empty with_non-empty_elements non empty-membered a_partition of the carrier of A
S2 is set
bool the carrier of A is non empty set
G is non empty Element of P
the Element of G is Element of G
Class ((A), the Element of G) is Element of bool the carrier of A
{ the Element of G} is non empty trivial V51(1) set
(A) .: { the Element of G} is set
G is set
R is Element of G
(A) is Relation-like the carrier of A -defined the carrier of A -valued total quasi_total reflexive symmetric transitive Element of bool [: the carrier of A, the carrier of A:]
(A,(A),0) is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
em is set
f is set
[em,f] is V26() set
{em,f} is non empty set
{em} is non empty trivial V51(1) set
{{em,f},{em}} is non empty with_non-empty_elements non empty-membered set
g is Element of the carrier of A
Class (S1,g) is Element of bool the carrier of A
{g} is non empty trivial V51(1) set
S1 .: {g} is set
g is Element of the carrier of A
s1 is non empty Element of P
the carrier of A * is non empty functional FinSequence-membered FinSequenceSet of the carrier of A
the charact of A is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of A *), the carrier of A) -valued Function-like V44() FinSequence-like FinSubsequence-like countable homogeneous FinSequence of PFuncs (( the carrier of A *), the carrier of A)
PFuncs (( the carrier of A *), the carrier of A) is non empty functional set
( the carrier of A, the charact of A) is non empty functional with_non-empty_elements non empty-membered Element of bool (PFuncs (( the carrier of A *), the carrier of A))
bool (PFuncs (( the carrier of A *), the carrier of A)) is non empty set
<*g*> is non empty trivial Relation-like NAT -defined the carrier of A -valued Function-like constant V44() V51(1) FinSequence-like FinSubsequence-like countable FinSequence of the carrier of A
<*g*> is non empty trivial Relation-like NAT -defined the carrier of A -valued Function-like constant V44() V51(1) FinSequence-like FinSubsequence-like countable FinSequence of the carrier of A
o is non empty Relation-like the carrier of A * -defined the carrier of A -valued Function-like ( the carrier of A * , the carrier of A,( the carrier of A, the charact of A))
dom o is non empty functional FinSequence-membered Element of bool ( the carrier of A *)
bool ( the carrier of A *) is non empty set
p is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
p ^ <*g*> is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
a is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
(p ^ <*g*>) ^ a is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
p ^ <*g*> is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
(p ^ <*g*>) ^ a is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
h is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
r is Element of s1
<*r*> is non empty trivial Relation-like NAT -defined s1 -valued Function-like constant V44() V51(1) FinSequence-like FinSubsequence-like countable FinSequence of s1
h ^ <*r*> is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
h is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
(h ^ <*r*>) ^ h is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
p9 is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable FinSequence of P
product p9 is non empty functional with_common_domain product-like set
s2 is Element of s1
<*s2*> is non empty trivial Relation-like NAT -defined s1 -valued Function-like constant V44() V51(1) FinSequence-like FinSubsequence-like countable FinSequence of s1
h ^ <*s2*> is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
(h ^ <*s2*>) ^ h is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
[g,g] is V26() set
{g,g} is non empty set
{g} is non empty trivial V51(1) set
{{g,g},{g}} is non empty with_non-empty_elements non empty-membered set
em is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
(A,(A),em) is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
em + 1 is non empty V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
(A,(A),(em + 1)) is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
f is set
g is set
[f,g] is V26() set
{f,g} is non empty set
{f} is non empty trivial V51(1) set
{{f,g},{f}} is non empty with_non-empty_elements non empty-membered set
s1 is Element of the carrier of A
Class (S1,s1) is Element of bool the carrier of A
{s1} is non empty trivial V51(1) set
S1 .: {s1} is set
the carrier of A * is non empty functional FinSequence-membered FinSequenceSet of the carrier of A
the charact of A is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of A *), the carrier of A) -valued Function-like V44() FinSequence-like FinSubsequence-like countable homogeneous FinSequence of PFuncs (( the carrier of A *), the carrier of A)
PFuncs (( the carrier of A *), the carrier of A) is non empty functional set
( the carrier of A, the charact of A) is non empty functional with_non-empty_elements non empty-membered Element of bool (PFuncs (( the carrier of A *), the carrier of A))
bool (PFuncs (( the carrier of A *), the carrier of A)) is non empty set
a is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
g is Element of the carrier of A
<*g*> is non empty trivial Relation-like NAT -defined the carrier of A -valued Function-like constant V44() V51(1) FinSequence-like FinSubsequence-like countable FinSequence of the carrier of A
a ^ <*g*> is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
h is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
(a ^ <*g*>) ^ h is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
p is non empty Relation-like the carrier of A * -defined the carrier of A -valued Function-like ( the carrier of A * , the carrier of A,( the carrier of A, the charact of A))
dom p is non empty functional FinSequence-membered Element of bool ( the carrier of A *)
bool ( the carrier of A *) is non empty set
<*s1*> is non empty trivial Relation-like NAT -defined the carrier of A -valued Function-like constant V44() V51(1) FinSequence-like FinSubsequence-like countable FinSequence of the carrier of A
a ^ <*s1*> is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
(a ^ <*s1*>) ^ h is non empty Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
h is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable FinSequence of P
product h is non empty functional with_common_domain product-like set
p .: (product h) is Element of bool the carrier of A
r is non empty Element of P
o is non empty Element of P
p . ((a ^ <*g*>) ^ h) is set
p . ((a ^ <*s1*>) ^ h) is set
[(p . ((a ^ <*g*>) ^ h)),(p . ((a ^ <*s1*>) ^ h))] is V26() set
{(p . ((a ^ <*g*>) ^ h)),(p . ((a ^ <*s1*>) ^ h))} is non empty set
{(p . ((a ^ <*g*>) ^ h))} is non empty trivial V51(1) set
{{(p . ((a ^ <*g*>) ^ h)),(p . ((a ^ <*s1*>) ^ h))},{(p . ((a ^ <*g*>) ^ h))}} is non empty with_non-empty_elements non empty-membered set
s2 is set
Class (S1,s2) is Element of bool the carrier of A
{s2} is non empty trivial V51(1) set
S1 .: {s2} is set
[g,s1] is V26() set
{g,s1} is non empty set
{g} is non empty trivial V51(1) set
{{g,s1},{g}} is non empty with_non-empty_elements non empty-membered set
(A,(A,(A),em)) is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
SG is Element of the carrier of A
em is Element of the carrier of A
[SG,em] is V26() set
{SG,em} is non empty set
{SG} is non empty trivial V51(1) set
{{SG,em},{SG}} is non empty with_non-empty_elements non empty-membered set
f is set
Class (S1,f) is Element of bool the carrier of A
{f} is non empty trivial V51(1) set
S1 .: {f} is set
em is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
(A,(A),em) is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
[em,SG] is V26() set
{em,SG} is non empty set
{em} is non empty trivial V51(1) set
{{em,SG},{em}} is non empty with_non-empty_elements non empty-membered set
A is non empty non void V72() ManySortedSign
the carrier of A is non empty set
id the carrier of A is non empty Relation-like the carrier of A -defined the carrier of A -valued Function-like one-to-one total quasi_total onto bijective reflexive symmetric antisymmetric transitive Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
the carrier' of A is non empty set
id the carrier' of A is non empty Relation-like the carrier' of A -defined the carrier' of A -valued Function-like one-to-one total quasi_total onto bijective reflexive symmetric antisymmetric transitive Element of bool [: the carrier' of A, the carrier' of A:]
[: the carrier' of A, the carrier' of A:] is non empty Relation-like set
bool [: the carrier' of A, the carrier' of A:] is non empty set
the ResultSort of A is non empty Relation-like the carrier' of A -defined the carrier of A -valued Function-like total quasi_total Element of bool [: the carrier' of A, the carrier of A:]
[: the carrier' of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier' of A, the carrier of A:] is non empty set
dom the ResultSort of A is non empty Element of bool the carrier' of A
bool the carrier' of A is non empty set
rng the ResultSort of A is non empty Element of bool the carrier of A
bool the carrier of A is non empty set
(id the carrier of A) * the ResultSort of A is non empty Relation-like the carrier' of A -defined the carrier of A -valued Function-like total quasi_total Element of bool [: the carrier' of A, the carrier of A:]
dom (id the carrier of A) is non empty Element of bool the carrier of A
dom (id the carrier' of A) is non empty Element of bool the carrier' of A
rng (id the carrier of A) is non empty Element of bool the carrier of A
rng (id the carrier' of A) is non empty Element of bool the carrier' of A
the ResultSort of A * (id the carrier' of A) is non empty Relation-like the carrier' of A -defined the carrier of A -valued Function-like total quasi_total Element of bool [: the carrier' of A, the carrier of A:]
the Arity of A is non empty Relation-like the carrier' of A -defined the carrier of A * -valued Function-like total quasi_total Element of bool [: the carrier' of A,( the carrier of A *):]
the carrier of A * is non empty functional FinSequence-membered FinSequenceSet of the carrier of A
[: the carrier' of A,( the carrier of A *):] is non empty Relation-like set
bool [: the carrier' of A,( the carrier of A *):] is non empty set
S2 is set
the Arity of A . S2 is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
(id the carrier' of A) . S2 is set
the Arity of A . ((id the carrier' of A) . S2) is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
G is Relation-like Function-like set
G * (id the carrier of A) is Relation-like the carrier of A -valued Function-like set
proj2 G is set
A is ManySortedSign
P is ManySortedSign
S1 is ManySortedSign
S2 is Relation-like Function-like set
Q is Relation-like Function-like set
G is Relation-like Function-like set
G is Relation-like Function-like set
S2 * G is Relation-like Function-like set
Q * G is Relation-like Function-like set
proj1 S2 is set
the carrier of A is set
proj1 Q is set
the carrier' of A is set
proj2 S2 is set
the carrier of P is set
proj2 Q is set
the carrier' of P is set
the ResultSort of A is Relation-like the carrier' of A -defined the carrier of A -valued Function-like quasi_total Element of bool [: the carrier' of A, the carrier of A:]
[: the carrier' of A, the carrier of A:] is Relation-like set
bool [: the carrier' of A, the carrier of A:] is non empty set
the ResultSort of A * S2 is Relation-like the carrier' of A -defined Function-like set
the ResultSort of P is Relation-like the carrier' of P -defined the carrier of P -valued Function-like quasi_total Element of bool [: the carrier' of P, the carrier of P:]
[: the carrier' of P, the carrier of P:] is Relation-like set
bool [: the carrier' of P, the carrier of P:] is non empty set
Q * the ResultSort of P is Relation-like the carrier of P -valued Function-like set
the Arity of A is Relation-like the carrier' of A -defined the carrier of A * -valued Function-like total quasi_total Element of bool [: the carrier' of A,( the carrier of A *):]
the carrier of A * is non empty functional FinSequence-membered FinSequenceSet of the carrier of A
[: the carrier' of A,( the carrier of A *):] is Relation-like set
bool [: the carrier' of A,( the carrier of A *):] is non empty set
the Arity of P is Relation-like the carrier' of P -defined the carrier of P * -valued Function-like total quasi_total Element of bool [: the carrier' of P,( the carrier of P *):]
the carrier of P * is non empty functional FinSequence-membered FinSequenceSet of the carrier of P
[: the carrier' of P,( the carrier of P *):] is Relation-like set
bool [: the carrier' of P,( the carrier of P *):] is non empty set
proj1 G is set
proj1 G is set
proj2 G is set
the carrier of S1 is set
proj2 G is set
the carrier' of S1 is set
the ResultSort of P * G is Relation-like the carrier' of P -defined Function-like set
the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like quasi_total Element of bool [: the carrier' of S1, the carrier of S1:]
[: the carrier' of S1, the carrier of S1:] is Relation-like set
bool [: the carrier' of S1, the carrier of S1:] is non empty set
G * the ResultSort of S1 is Relation-like the carrier of S1 -valued Function-like set
the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total quasi_total Element of bool [: the carrier' of S1,( the carrier of S1 *):]
the carrier of S1 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of S1
[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set
bool [: the carrier' of S1,( the carrier of S1 *):] is non empty set
proj1 (S2 * G) is set
proj1 (Q * G) is set
proj2 (S2 * G) is set
proj2 (Q * G) is set
the ResultSort of A * (S2 * G) is Relation-like the carrier' of A -defined Function-like set
(Q * G) * the ResultSort of S1 is Relation-like the carrier of S1 -valued Function-like set
(Q * the ResultSort of P) * G is Relation-like Function-like set
Q * ( the ResultSort of P * G) is Relation-like Function-like set
em is set
the Arity of A . em is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
(Q * G) . em is set
the Arity of S1 . ((Q * G) . em) is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
em is Relation-like Function-like set
em * (S2 * G) is Relation-like Function-like set
em * S2 is Relation-like Function-like set
Q . em is set
the Arity of P . (Q . em) is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
(em * S2) * G is Relation-like Function-like set
G . (Q . em) is set
S1 is non empty non void V72() ManySortedSign
the carrier of S1 is non empty set
[: the carrier of S1, the carrier of S1:] is non empty Relation-like set
bool [: the carrier of S1, the carrier of S1:] is non empty set
id the carrier of S1 is non empty Relation-like the carrier of S1 -defined the carrier of S1 -valued Function-like one-to-one total quasi_total onto bijective reflexive symmetric antisymmetric transitive Element of bool [: the carrier of S1, the carrier of S1:]
S2 is non empty Relation-like the carrier of S1 -defined the carrier of S1 -valued Function-like one-to-one total quasi_total onto bijective reflexive symmetric antisymmetric transitive Element of bool [: the carrier of S1, the carrier of S1:]
proj2 S2 is non empty set
the carrier' of S1 is non empty set
[: the carrier' of S1, the carrier' of S1:] is non empty Relation-like set
bool [: the carrier' of S1, the carrier' of S1:] is non empty set
id the carrier' of S1 is non empty Relation-like the carrier' of S1 -defined the carrier' of S1 -valued Function-like one-to-one total quasi_total onto bijective reflexive symmetric antisymmetric transitive Element of bool [: the carrier' of S1, the carrier' of S1:]
G is non empty Relation-like the carrier' of S1 -defined the carrier' of S1 -valued Function-like one-to-one total quasi_total onto bijective reflexive symmetric antisymmetric transitive Element of bool [: the carrier' of S1, the carrier' of S1:]
proj2 G is non empty set
rng S2 is non empty Element of bool the carrier of S1
bool the carrier of S1 is non empty set
rng G is non empty Element of bool the carrier' of S1
bool the carrier' of S1 is non empty set
A is ManySortedSign
P is ManySortedSign
S1 is ManySortedSign
the carrier of A is set
the carrier' of A is set
S2 is Relation-like Function-like set
G is Relation-like Function-like set
proj2 S2 is set
proj2 G is set
the carrier of P is set
the carrier' of P is set
Q is Relation-like Function-like set
G is Relation-like Function-like set
proj2 Q is set
proj2 G is set
Q * S2 is Relation-like Function-like set
R is Relation-like Function-like set
proj2 R is set
G * G is Relation-like Function-like set
SG is Relation-like Function-like set
proj2 SG is set
proj1 S2 is set
proj1 G is set
A is non empty partial non-empty UAStr
P is non empty with_non-empty_elements non empty-membered (A)
the charact of A is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of A *), the carrier of A) -valued Function-like V44() FinSequence-like FinSubsequence-like countable homogeneous FinSequence of PFuncs (( the carrier of A *), the carrier of A)
the carrier of A is non empty set
the carrier of A * is non empty functional FinSequence-membered FinSequenceSet of the carrier of A
PFuncs (( the carrier of A *), the carrier of A) is non empty functional set
dom the charact of A is non empty countable Element of bool NAT
P * is non empty functional FinSequence-membered FinSequenceSet of P
{ [b₁,b₂] where b₁ is Element of dom the charact of A, b₂ is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P * : product b₂ meets dom (A,b₁) } is set
S2 is set
G is Element of dom the charact of A
Q is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P *
[G,Q] is V26() set
{G,Q} is non empty set
{G} is non empty trivial V51(1) set
{{G,Q},{G}} is non empty with_non-empty_elements non empty-membered set
product Q is non empty functional with_common_domain product-like set
(A,G) is non empty Relation-like the carrier of A * -defined the carrier of A -valued Function-like ( the carrier of A * , the carrier of A,( the carrier of A, the charact of A))
( the carrier of A, the charact of A) is non empty functional with_non-empty_elements non empty-membered Element of bool (PFuncs (( the carrier of A *), the carrier of A))
bool (PFuncs (( the carrier of A *), the carrier of A)) is non empty set
the charact of A . G is non empty Relation-like Function-like homogeneous set
dom (A,G) is non empty functional FinSequence-membered Element of bool ( the carrier of A *)
bool ( the carrier of A *) is non empty set
S2 is set
G is Element of dom the charact of A
Q is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P *
[G,Q] is V26() set
{G,Q} is non empty set
{G} is non empty trivial V51(1) set
{{G,Q},{G}} is non empty with_non-empty_elements non empty-membered set
product Q is non empty functional with_common_domain product-like set
(A,G) is non empty Relation-like the carrier of A * -defined the carrier of A -valued Function-like ( the carrier of A * , the carrier of A,( the carrier of A, the charact of A))
( the carrier of A, the charact of A) is non empty functional with_non-empty_elements non empty-membered Element of bool (PFuncs (( the carrier of A *), the carrier of A))
bool (PFuncs (( the carrier of A *), the carrier of A)) is non empty set
the charact of A . G is non empty Relation-like Function-like homogeneous set
dom (A,G) is non empty functional FinSequence-membered Element of bool ( the carrier of A *)
bool ( the carrier of A *) is non empty set
bool the carrier of A is non empty set
(A,G) .: (product Q) is Element of bool the carrier of A
G is non empty Element of P
S2 is Relation-like Function-like set
proj1 S2 is set
proj2 S2 is set
[: { [b₁,b₂] where b₁ is Element of dom the charact of A, b₂ is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P * : product b₂ meets dom (A,b₁) } ,(P *):] is Relation-like set
bool [: { [b₁,b₂] where b₁ is Element of dom the charact of A, b₂ is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P * : product b₂ meets dom (A,b₁) } ,(P *):] is non empty set
Q is Relation-like Function-like set
proj1 Q is set
proj2 Q is set
[: { [b₁,b₂] where b₁ is Element of dom the charact of A, b₂ is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P * : product b₂ meets dom (A,b₁) } ,P:] is Relation-like set
bool [: { [b₁,b₂] where b₁ is Element of dom the charact of A, b₂ is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P * : product b₂ meets dom (A,b₁) } ,P:] is non empty set
G is Relation-like { [b₁,b₂] where b₁ is Element of dom the charact of A, b₂ is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P * : product b₂ meets dom (A,b₁) } -defined P * -valued Function-like total quasi_total Element of bool [: { [b₁,b₂] where b₁ is Element of dom the charact of A, b₂ is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P * : product b₂ meets dom (A,b₁) } ,(P *):]
G is Relation-like non-empty { [b₁,b₂] where b₁ is Element of dom the charact of A, b₂ is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P * : product b₂ meets dom (A,b₁) } -defined P -valued Function-like total quasi_total Element of bool [: { [b₁,b₂] where b₁ is Element of dom the charact of A, b₂ is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P * : product b₂ meets dom (A,b₁) } ,P:]
ManySortedSign(# P, { [b₁,b₂] where b₁ is Element of dom the charact of A, b₂ is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P * : product b₂ meets dom (A,b₁) } ,G,G #) is strict ManySortedSign
R is strict ManySortedSign
the carrier of R is set
the carrier' of R is set
the Arity of R is Relation-like the carrier' of R -defined the carrier of R * -valued Function-like total quasi_total Element of bool [: the carrier' of R,( the carrier of R *):]
the carrier of R * is non empty functional FinSequence-membered FinSequenceSet of the carrier of R
[: the carrier' of R,( the carrier of R *):] is Relation-like set
bool [: the carrier' of R,( the carrier of R *):] is non empty set
the ResultSort of R is Relation-like the carrier' of R -defined the carrier of R -valued Function-like quasi_total Element of bool [: the carrier' of R, the carrier of R:]
[: the carrier' of R, the carrier of R:] is Relation-like set
bool [: the carrier' of R, the carrier of R:] is non empty set
SG is Element of dom the charact of A
(A,SG) is non empty Relation-like the carrier of A * -defined the carrier of A -valued Function-like ( the carrier of A * , the carrier of A,( the carrier of A, the charact of A))
( the carrier of A, the charact of A) is non empty functional with_non-empty_elements non empty-membered Element of bool (PFuncs (( the carrier of A *), the carrier of A))
bool (PFuncs (( the carrier of A *), the carrier of A)) is non empty set
the charact of A . SG is non empty Relation-like Function-like homogeneous set
dom (A,SG) is non empty functional FinSequence-membered Element of bool ( the carrier of A *)
bool ( the carrier of A *) is non empty set
em is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P *
product em is non empty functional with_common_domain product-like set
[SG,em] is V26() set
{SG,em} is non empty set
{SG} is non empty trivial V51(1) set
{{SG,em},{SG}} is non empty with_non-empty_elements non empty-membered set
the Arity of R . [SG,em] is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
(A,SG) .: (product em) is Element of bool the carrier of A
bool the carrier of A is non empty set
the ResultSort of R . [SG,em] is set
G . [SG,em] is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
G . [SG,em] is set
f is Element of dom the charact of A
g is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P *
[f,g] is V26() set
{f,g} is non empty set
{f} is non empty trivial V51(1) set
{{f,g},{f}} is non empty with_non-empty_elements non empty-membered set
(A,f) is non empty Relation-like the carrier of A * -defined the carrier of A -valued Function-like ( the carrier of A * , the carrier of A,( the carrier of A, the charact of A))
the charact of A . f is non empty Relation-like Function-like homogeneous set
product g is non empty functional with_common_domain product-like set
(A,f) .: (product g) is Element of bool the carrier of A
s1 is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P *
g is Element of dom the charact of A
[g,s1] is V26() set
{g,s1} is non empty set
{g} is non empty trivial V51(1) set
{{g,s1},{g}} is non empty with_non-empty_elements non empty-membered set
S2 is strict ManySortedSign
the carrier of S2 is set
the carrier' of S2 is set
the Arity of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 * -valued Function-like total quasi_total Element of bool [: the carrier' of S2,( the carrier of S2 *):]
the carrier of S2 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of S2
[: the carrier' of S2,( the carrier of S2 *):] is Relation-like set
bool [: the carrier' of S2,( the carrier of S2 *):] is non empty set
the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like quasi_total Element of bool [: the carrier' of S2, the carrier of S2:]
[: the carrier' of S2, the carrier of S2:] is Relation-like set
bool [: the carrier' of S2, the carrier of S2:] is non empty set
G is strict ManySortedSign
the carrier of G is set
the carrier' of G is set
the Arity of G is Relation-like the carrier' of G -defined the carrier of G * -valued Function-like total quasi_total Element of bool [: the carrier' of G,( the carrier of G *):]
the carrier of G * is non empty functional FinSequence-membered FinSequenceSet of the carrier of G
[: the carrier' of G,( the carrier of G *):] is Relation-like set
bool [: the carrier' of G,( the carrier of G *):] is non empty set
the ResultSort of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like quasi_total Element of bool [: the carrier' of G, the carrier of G:]
[: the carrier' of G, the carrier of G:] is Relation-like set
bool [: the carrier' of G, the carrier of G:] is non empty set
dom the Arity of S2 is Element of bool the carrier' of S2
bool the carrier' of S2 is non empty set
dom the Arity of G is Element of bool the carrier' of G
bool the carrier' of G is non empty set
Q is set
G is Element of dom the charact of A
R is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P *
[G,R] is V26() set
{G,R} is non empty set
{G} is non empty trivial V51(1) set
{{G,R},{G}} is non empty with_non-empty_elements non empty-membered set
product R is non empty functional with_common_domain product-like set
(A,G) is non empty Relation-like the carrier of A * -defined the carrier of A -valued Function-like ( the carrier of A * , the carrier of A,( the carrier of A, the charact of A))
( the carrier of A, the charact of A) is non empty functional with_non-empty_elements non empty-membered Element of bool (PFuncs (( the carrier of A *), the carrier of A))
bool (PFuncs (( the carrier of A *), the carrier of A)) is non empty set
the charact of A . G is non empty Relation-like Function-like homogeneous set
dom (A,G) is non empty functional FinSequence-membered Element of bool ( the carrier of A *)
bool ( the carrier of A *) is non empty set
the Arity of S2 . Q is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
the Arity of G . Q is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
dom the ResultSort of S2 is Element of bool the carrier' of S2
dom the ResultSort of G is Element of bool the carrier' of G
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
Q is Relation-like the carrier of A -defined the carrier of A -valued total quasi_total reflexive symmetric transitive Element of bool [: the carrier of A, the carrier of A:]
Class Q is non empty with_non-empty_elements non empty-membered a_partition of the carrier of A
G is set
R is Element of dom the charact of A
SG is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P *
[R,SG] is V26() set
{R,SG} is non empty set
{R} is non empty trivial V51(1) set
{{R,SG},{R}} is non empty with_non-empty_elements non empty-membered set
product SG is non empty functional with_common_domain product-like set
(A,R) is non empty Relation-like the carrier of A * -defined the carrier of A -valued Function-like ( the carrier of A * , the carrier of A,( the carrier of A, the charact of A))
the charact of A . R is non empty Relation-like Function-like homogeneous set
dom (A,R) is non empty functional FinSequence-membered Element of bool ( the carrier of A *)
em is set
(A,R) . em is set
(A,R) .: (product SG) is Element of bool the carrier of A
bool the carrier of A is non empty set
the ResultSort of S2 . G is set
the ResultSort of G . G is set
Class (Q,((A,R) . em)) is Element of bool the carrier of A
{((A,R) . em)} is non empty trivial V51(1) set
Q .: {((A,R) . em)} is set
em is set
Class (Q,em) is Element of bool the carrier of A
{em} is non empty trivial V51(1) set
Q .: {em} is set
em is set
Class (Q,em) is Element of bool the carrier of A
{em} is non empty trivial V51(1) set
Q .: {em} is set
A is non empty partial non-empty UAStr
P is non empty with_non-empty_elements non empty-membered (A)
(A,P) is strict ManySortedSign
the carrier of (A,P) is set
the charact of A is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of A *), the carrier of A) -valued Function-like V44() FinSequence-like FinSubsequence-like countable homogeneous FinSequence of PFuncs (( the carrier of A *), the carrier of A)
the carrier of A is non empty set
the carrier of A * is non empty functional FinSequence-membered FinSequenceSet of the carrier of A
PFuncs (( the carrier of A *), the carrier of A) is non empty functional set
dom the charact of A is non empty countable Element of bool NAT
the Element of dom the charact of A is Element of dom the charact of A
(A, the Element of dom the charact of A) is non empty Relation-like the carrier of A * -defined the carrier of A -valued Function-like ( the carrier of A * , the carrier of A,( the carrier of A, the charact of A))
( the carrier of A, the charact of A) is non empty functional with_non-empty_elements non empty-membered Element of bool (PFuncs (( the carrier of A *), the carrier of A))
bool (PFuncs (( the carrier of A *), the carrier of A)) is non empty set
the charact of A . the Element of dom the charact of A is non empty Relation-like Function-like homogeneous set
dom (A, the Element of dom the charact of A) is non empty functional FinSequence-membered Element of bool ( the carrier of A *)
bool ( the carrier of A *) is non empty set
the Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable Element of dom (A, the Element of dom the charact of A) is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable Element of dom (A, the Element of dom the charact of A)
union P is non empty Element of bool the carrier of A
bool the carrier of A is non empty set
G is Relation-like NAT -defined the carrier of A -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of the carrier of A *
rng G is Element of bool the carrier of A
dom G is countable Element of bool NAT
Q is Relation-like Function-like set
proj1 Q is set
proj2 Q is set
product Q is functional with_common_domain product-like set
len G is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
Seg (len G) is V44() V51( len G) countable Element of bool NAT
G is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
P * is non empty functional FinSequence-membered FinSequenceSet of P
R is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable FinSequence of P
SG is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P *
product SG is non empty functional with_common_domain product-like set
the carrier' of (A,P) is set
{ [b₁,b₂] where b₁ is Element of dom the charact of A, b₂ is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P * : product b₂ meets dom (A,b₁) } is set
[ the Element of dom the charact of A,SG] is V26() set
{ the Element of dom the charact of A,SG} is non empty set
{ the Element of dom the charact of A} is non empty trivial V51(1) set
{{ the Element of dom the charact of A,SG},{ the Element of dom the charact of A}} is non empty with_non-empty_elements non empty-membered set
A is non empty partial non-empty UAStr
P is non empty with_non-empty_elements non empty-membered (A)
(A,P) is non empty non void V72() strict ManySortedSign
the carrier' of (A,P) is non empty set
S1 is Element of the carrier' of (A,P)
S1 `1 is set
the charact of A is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of A *), the carrier of A) -valued Function-like V44() FinSequence-like FinSubsequence-like countable homogeneous FinSequence of PFuncs (( the carrier of A *), the carrier of A)
the carrier of A is non empty set
the carrier of A * is non empty functional FinSequence-membered FinSequenceSet of the carrier of A
PFuncs (( the carrier of A *), the carrier of A) is non empty functional set
dom the charact of A is non empty countable Element of bool NAT
P * is non empty functional FinSequence-membered FinSequenceSet of P
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub> is Element of dom the charact of A, b<sub>2</sub> is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P * : product b<sub>2</sub> meets dom (A,b<sub>1</sub>) } is set
S2 is Element of dom the charact of A
G is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P *
[S2,G] is V26() set
{S2,G} is non empty set
{S2} is non empty trivial V51(1) set
{{S2,G},{S2}} is non empty with_non-empty_elements non empty-membered set
product G is non empty functional with_common_domain product-like set
(A,S2) is non empty Relation-like the carrier of A * -defined the carrier of A -valued Function-like ( the carrier of A * , the carrier of A,( the carrier of A, the charact of A))
( the carrier of A, the charact of A) is non empty functional with_non-empty_elements non empty-membered Element of bool (PFuncs (( the carrier of A *), the carrier of A))
bool (PFuncs (( the carrier of A *), the carrier of A)) is non empty set
the charact of A . S2 is non empty Relation-like Function-like homogeneous set
dom (A,S2) is non empty functional FinSequence-membered Element of bool ( the carrier of A *)
bool ( the carrier of A *) is non empty set
S1 `2 is set
P * is non empty functional FinSequence-membered FinSequenceSet of P
{ [b₁,b₂] where b₁ is Element of dom the charact of A, b₂ is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P * : product b₂ meets dom (A,b₁) } is set
S2 is Element of dom the charact of A
G is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P *
[S2,G] is V26() set
{S2,G} is non empty set
{S2} is non empty trivial V51(1) set
{{S2,G},{S2}} is non empty with_non-empty_elements non empty-membered set
product G is non empty functional with_common_domain product-like set
(A,S2) is non empty Relation-like the carrier of A * -defined the carrier of A -valued Function-like ( the carrier of A * , the carrier of A,( the carrier of A, the charact of A))
( the carrier of A, the charact of A) is non empty functional with_non-empty_elements non empty-membered Element of bool (PFuncs (( the carrier of A *), the carrier of A))
bool (PFuncs (( the carrier of A *), the carrier of A)) is non empty set
the charact of A . S2 is non empty Relation-like Function-like homogeneous set
dom (A,S2) is non empty functional FinSequence-membered Element of bool ( the carrier of A *)
bool ( the carrier of A *) is non empty set
P is non empty non void V72() ManySortedSign
the carrier' of P is non empty set
A is non empty partial non-empty UAStr
P is non empty with_non-empty_elements non empty-membered (A)
(A,P) is non empty non void V72() strict ManySortedSign
the carrier of (A,P) is non empty set
the carrier of A is non empty set
( the carrier of A,P) is non empty Relation-like non-empty non empty-yielding P -defined P -valued Function-like one-to-one total reflexive symmetric antisymmetric transitive ( the carrier of A)
the carrier' of (A,P) is non empty set
the carrier of A * is non empty functional FinSequence-membered FinSequenceSet of the carrier of A
[:( the carrier of A *), the carrier of A:] is non empty Relation-like set
bool [:( the carrier of A *), the carrier of A:] is non empty set
G is non empty Relation-like the carrier' of (A,P) -defined Function-like total set
the charact of A is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of A *), the carrier of A) -valued Function-like V44() FinSequence-like FinSubsequence-like countable homogeneous FinSequence of PFuncs (( the carrier of A *), the carrier of A)
PFuncs (( the carrier of A *), the carrier of A) is non empty functional set
dom the charact of A is non empty countable Element of bool NAT
{ b₁ where b₁ is Element of the carrier' of (A,P) : (A,P,b₁) = a₁ } is set
Q is non empty Relation-like dom the charact of A -defined Function-like total set
dom Q is non empty countable Element of bool (dom the charact of A)
bool (dom the charact of A) is non empty set
P * is non empty functional FinSequence-membered FinSequenceSet of P
{ [b₁,b₂] where b₁ is Element of dom the charact of A, b₂ is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P * : product b₂ meets dom (A,b₁) } is set
G is set
proj1 Q is non empty set
Q . G is set
R is Element of dom the charact of A
(A,R) is non empty Relation-like the carrier of A * -defined the carrier of A -valued Function-like ( the carrier of A * , the carrier of A,( the carrier of A, the charact of A))
( the carrier of A, the charact of A) is non empty functional with_non-empty_elements non empty-membered Element of bool (PFuncs (( the carrier of A *), the carrier of A))
bool (PFuncs (( the carrier of A *), the carrier of A)) is non empty set
the charact of A . R is non empty Relation-like Function-like homogeneous set
dom (A,R) is non empty functional FinSequence-membered Element of bool ( the carrier of A *)
bool ( the carrier of A *) is non empty set
the Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable Element of dom (A,R) is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable Element of dom (A,R)
em is Relation-like NAT -defined the carrier of A -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of the carrier of A *
rng em is Element of bool the carrier of A
bool the carrier of A is non empty set
union P is non empty Element of bool the carrier of A
dom em is countable Element of bool NAT
em is Relation-like Function-like set
proj1 em is set
proj2 em is set
product em is functional with_common_domain product-like set
len em is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
Seg (len em) is V44() V51( len em) countable Element of bool NAT
f is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P *
product f is non empty functional with_common_domain product-like set
[R,f] is V26() set
{R,f} is non empty set
{R} is non empty trivial V51(1) set
{{R,f},{R}} is non empty with_non-empty_elements non empty-membered set
[R,f] `1 is set
Q . R is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier' of (A,P) : (A,P,b<sub>1</sub>) = R } is set
the Arity of (A,P) is non empty Relation-like the carrier' of (A,P) -defined the carrier of (A,P) * -valued Function-like total quasi_total Element of bool [: the carrier' of (A,P),( the carrier of (A,P) *):]
the carrier of (A,P) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of (A,P)
[: the carrier' of (A,P),( the carrier of (A,P) *):] is non empty Relation-like set
bool [: the carrier' of (A,P),( the carrier of (A,P) *):] is non empty set
S2 is non empty Relation-like the carrier of (A,P) -defined Function-like total set
S2 # is non empty Relation-like the carrier of (A,P) * -defined Function-like total set
the Arity of (A,P) * (S2 #) is non empty Relation-like the carrier' of (A,P) -defined Function-like total set
the ResultSort of (A,P) is non empty Relation-like the carrier' of (A,P) -defined the carrier of (A,P) -valued Function-like total quasi_total Element of bool [: the carrier' of (A,P), the carrier of (A,P):]
[: the carrier' of (A,P), the carrier of (A,P):] is non empty Relation-like set
bool [: the carrier' of (A,P), the carrier of (A,P):] is non empty set
the ResultSort of (A,P) * S2 is non empty Relation-like the carrier' of (A,P) -defined Function-like total set
R is set
G . R is set
( the Arity of (A,P) * (S2 #)) . R is set
( the ResultSort of (A,P) * S2) . R is set
[:(( the Arity of (A,P) * (S2 #)) . R),(( the ResultSort of (A,P) * S2) . R):] is Relation-like set
bool [:(( the Arity of (A,P) * (S2 #)) . R),(( the ResultSort of (A,P) * S2) . R):] is non empty set
SG is Element of dom the charact of A
em is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P *
[SG,em] is V26() set
{SG,em} is non empty set
{SG} is non empty trivial V51(1) set
{{SG,em},{SG}} is non empty with_non-empty_elements non empty-membered set
product em is non empty functional with_common_domain product-like set
(A,SG) is non empty Relation-like the carrier of A * -defined the carrier of A -valued Function-like ( the carrier of A * , the carrier of A,( the carrier of A, the charact of A))
( the carrier of A, the charact of A) is non empty functional with_non-empty_elements non empty-membered Element of bool (PFuncs (( the carrier of A *), the carrier of A))
bool (PFuncs (( the carrier of A *), the carrier of A)) is non empty set
the charact of A . SG is non empty Relation-like Function-like homogeneous set
dom (A,SG) is non empty functional FinSequence-membered Element of bool ( the carrier of A *)
bool ( the carrier of A *) is non empty set
rng the ResultSort of (A,P) is non empty Element of bool the carrier of (A,P)
bool the carrier of (A,P) is non empty set
dom the Arity of (A,P) is non empty Element of bool the carrier' of (A,P)
bool the carrier' of (A,P) is non empty set
rng em is with_non-empty_elements Element of bool P
bool P is non empty set
the Arity of (A,P) . R is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
(S2 #) . em is set
em * S2 is Relation-like NAT -defined Function-like set
product (em * S2) is functional with_common_domain product-like set
(A,SG) .: (product em) is Element of bool the carrier of A
bool the carrier of A is non empty set
the ResultSort of (A,P) . R is set
em is Element of the carrier' of (A,P)
(A,P,em) is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P *
(A,P,em) is Element of dom the charact of A
(A,SG) | (product em) is Relation-like the carrier of A * -defined product em -defined the carrier of A * -defined the carrier of A -valued Function-like homogeneous Element of bool [:( the carrier of A *), the carrier of A:]
rng ((A,SG) | (product em)) is Element of bool the carrier of A
G . em is set
dom ((A,SG) | (product em)) is functional FinSequence-membered with_common_domain Element of bool ( the carrier of A *)
G is Relation-like non-empty Function-like set
Union G is set
SG is set
proj1 G is set
em is set
G . em is set
em is Element of dom the charact of A
G . em is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier' of (A,P) : (A,P,b<sub>1</sub>) = em } is set
f is Element of the carrier' of (A,P)
(A,P,f) is Element of dom the charact of A
SG is set
em is Element of the carrier' of (A,P)
(A,P,em) is Element of dom the charact of A
G . (A,P,em) is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier' of (A,P) : (A,P,b<sub>1</sub>) = (A,P,em) } is set
SG is set
proj1 G is set
em is set
G . SG is set
G . em is set
g is set
em is Element of dom the charact of A
G . em is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier' of (A,P) : (A,P,b<sub>1</sub>) = em } is set
f is Element of dom the charact of A
G . f is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier' of (A,P) : (A,P,b<sub>1</sub>) = f } is set
g is Element of the carrier' of (A,P)
(A,P,g) is Element of dom the charact of A
s1 is Element of the carrier' of (A,P)
(A,P,s1) is Element of dom the charact of A
R is non empty Relation-like the carrier' of (A,P) -defined Function-like total V52() ManySortedFunction of the Arity of (A,P) * (S2 #), the ResultSort of (A,P) * S2
MSAlgebra(# S2,R #) is strict MSAlgebra over (A,P)
em is strict MSAlgebra over (A,P)
SG is non empty Relation-like non-empty Function-like one-to-one ( the carrier' of (A,P))
( the carrier of A,( the carrier of A,P)) is non empty with_non-empty_elements non empty-membered a_partition of the carrier of A
the Sorts of em is non empty Relation-like the carrier of (A,P) -defined Function-like total set
proj1 SG is non empty set
the Charact of em is non empty Relation-like the carrier' of (A,P) -defined Function-like total V52() ManySortedFunction of the Arity of (A,P) * ( the Sorts of em #), the ResultSort of (A,P) * the Sorts of em
the Sorts of em # is non empty Relation-like the carrier of (A,P) * -defined Function-like total set
the Arity of (A,P) * ( the Sorts of em #) is non empty Relation-like the carrier' of (A,P) -defined Function-like total set
the ResultSort of (A,P) * the Sorts of em is non empty Relation-like the carrier' of (A,P) -defined Function-like total set
em is Element of dom the charact of A
SG . em is set
the Charact of em | (SG . em) is Relation-like SG . em -defined the carrier' of (A,P) -defined Function-like set
(A,em) is non empty Relation-like the carrier of A * -defined the carrier of A -valued Function-like ( the carrier of A * , the carrier of A,( the carrier of A, the charact of A))
( the carrier of A, the charact of A) is non empty functional with_non-empty_elements non empty-membered Element of bool (PFuncs (( the carrier of A *), the carrier of A))
bool (PFuncs (( the carrier of A *), the carrier of A)) is non empty set
the charact of A . em is non empty Relation-like Function-like homogeneous set
{ (product b<sub>1</sub>) where b<sub>1</sub> is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P * : verum } is set
dom (A,em) is non empty functional FinSequence-membered Element of bool ( the carrier of A *)
bool ( the carrier of A *) is non empty set
f is non empty with_non-empty_elements non empty-membered a_partition of the carrier of A *
{ (b<sub>1</sub> /\ (dom (A,em))) where b<sub>1</sub> is non empty Element of f : b<sub>1</sub> meets dom (A,em) } is set
( the carrier' of (A,P),SG) is non empty with_non-empty_elements non empty-membered a_partition of the carrier' of (A,P)
dom R is non empty Element of bool the carrier' of (A,P)
bool the carrier' of (A,P) is non empty set
dom ( the Charact of em | (SG . em)) is Element of bool (SG . em)
bool (SG . em) is non empty set
bool (dom (A,em)) is non empty set
g is non empty with_non-empty_elements non empty-membered a_partition of dom (A,em)
{ ((A,em) | b<sub>1</sub>) where b<sub>1</sub> is non empty Element of g : verum } is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier' of (A,P) : (A,P,b<sub>1</sub>) = em } is set
s1 is non empty Relation-like Function-like set
proj2 s1 is non empty set
p is non empty with_non-empty_elements non empty-membered a_partition of (A,em)
a is set
proj1 s1 is non empty set
h is set
s1 . h is set
dom the Charact of em is non empty Element of bool the carrier' of (A,P)
(dom the Charact of em) /\ (SG . em) is Element of bool the carrier' of (A,P)
h is Element of the carrier' of (A,P)
(A,P,h) is Element of dom the charact of A
r is Element of dom the charact of A
s2 is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P *
[r,s2] is V26() set
{r,s2} is non empty set
{r} is non empty trivial V51(1) set
{{r,s2},{r}} is non empty with_non-empty_elements non empty-membered set
product s2 is non empty functional with_common_domain product-like set
(A,r) is non empty Relation-like the carrier of A * -defined the carrier of A -valued Function-like ( the carrier of A * , the carrier of A,( the carrier of A, the charact of A))
the charact of A . r is non empty Relation-like Function-like homogeneous set
dom (A,r) is non empty functional FinSequence-membered Element of bool ( the carrier of A *)
(A,P,h) is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P *
(product s2) /\ (dom (A,em)) is functional FinSequence-membered Element of bool ( the carrier of A *)
(A,em) | (product s2) is Relation-like the carrier of A * -defined product s2 -defined the carrier of A * -defined the carrier of A -valued Function-like homogeneous Element of bool [:( the carrier of A *), the carrier of A:]
R . h is set
o is non empty set
[:o,p:] is non empty Relation-like set
bool [:o,p:] is non empty set
a is non empty Relation-like non-empty non empty-yielding o -defined p -valued Function-like total quasi_total Element of bool [:o,p:]
rng a is non empty with_non-empty_elements non empty-membered Element of bool p
bool p is non empty set
h is set
h is non empty Element of g
(A,em) | h is non empty Relation-like the carrier of A * -defined h -defined the carrier of A * -defined the carrier of A -valued Function-like Element of bool [:( the carrier of A *), the carrier of A:]
r is non empty Element of f
r /\ (dom (A,em)) is functional FinSequence-membered Element of bool ( the carrier of A *)
s2 is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P *
product s2 is non empty functional with_common_domain product-like set
[em,s2] is V26() set
{em,s2} is non empty set
{em} is non empty trivial V51(1) set
{{em,s2},{em}} is non empty with_non-empty_elements non empty-membered set
[em,s2] `1 is set
[em,s2] `2 is set
R . [em,s2] is set
h is set
proj1 a is non empty set
h is set
a . h is set
a . h is set
dom a is non empty Element of bool o
bool o is non empty set
r is Element of the carrier' of (A,P)
(A,P,r) is Element of dom the charact of A
s2 is Element of the carrier' of (A,P)
(A,P,s2) is Element of dom the charact of A
p9 is Element of dom the charact of A
o9 is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P *
[p9,o9] is V26() set
{p9,o9} is non empty set
{p9} is non empty trivial V51(1) set
{{p9,o9},{p9}} is non empty with_non-empty_elements non empty-membered set
product o9 is non empty functional with_common_domain product-like set
(A,p9) is non empty Relation-like the carrier of A * -defined the carrier of A -valued Function-like ( the carrier of A * , the carrier of A,( the carrier of A, the charact of A))
the charact of A . p9 is non empty Relation-like Function-like homogeneous set
dom (A,p9) is non empty functional FinSequence-membered Element of bool ( the carrier of A *)
o2 is Element of dom the charact of A
p2 is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P *
[o2,p2] is V26() set
{o2,p2} is non empty set
{o2} is non empty trivial V51(1) set
{{o2,p2},{o2}} is non empty with_non-empty_elements non empty-membered set
product p2 is non empty functional with_common_domain product-like set
(A,o2) is non empty Relation-like the carrier of A * -defined the carrier of A -valued Function-like ( the carrier of A * , the carrier of A,( the carrier of A, the charact of A))
the charact of A . o2 is non empty Relation-like Function-like homogeneous set
dom (A,o2) is non empty functional FinSequence-membered Element of bool ( the carrier of A *)
R . r is set
R . s2 is set
(A,P,r) is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P *
(A,P,s2) is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P *
(A,em) | (product o9) is Relation-like the carrier of A * -defined product o9 -defined the carrier of A * -defined the carrier of A -valued Function-like homogeneous Element of bool [:( the carrier of A *), the carrier of A:]
(A,em) | (product p2) is Relation-like the carrier of A * -defined product p2 -defined the carrier of A * -defined the carrier of A -valued Function-like homogeneous Element of bool [:( the carrier of A *), the carrier of A:]
dom ((A,em) | (product o9)) is functional FinSequence-membered with_common_domain Element of bool ( the carrier of A *)
A is non empty partial non-empty UAStr
the charact of A is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of A *), the carrier of A) -valued Function-like V44() FinSequence-like FinSubsequence-like countable homogeneous FinSequence of PFuncs (( the carrier of A *), the carrier of A)
the carrier of A is non empty set
the carrier of A * is non empty functional FinSequence-membered FinSequenceSet of the carrier of A
PFuncs (( the carrier of A *), the carrier of A) is non empty functional set
dom the charact of A is non empty countable Element of bool NAT
P is non empty non void V72() ManySortedSign
the carrier' of P is non empty set
S1 is MSAlgebra over P
the Sorts of S1 is non empty Relation-like the carrier of P -defined Function-like total set
the carrier of P is non empty set
proj2 the Sorts of S1 is non empty set
S2 is non empty Relation-like non-empty Function-like one-to-one ( the carrier' of P)
proj1 S2 is non empty set
the Charact of S1 is non empty Relation-like the carrier' of P -defined Function-like total V52() ManySortedFunction of the Arity of P * ( the Sorts of S1 #), the ResultSort of P * the Sorts of S1
the Arity of P is non empty Relation-like the carrier' of P -defined the carrier of P * -valued Function-like total quasi_total Element of bool [: the carrier' of P,( the carrier of P *):]
the carrier of P * is non empty functional FinSequence-membered FinSequenceSet of the carrier of P
[: the carrier' of P,( the carrier of P *):] is non empty Relation-like set
bool [: the carrier' of P,( the carrier of P *):] is non empty set
the Sorts of S1 # is non empty Relation-like the carrier of P * -defined Function-like total set
the Arity of P * ( the Sorts of S1 #) is non empty Relation-like the carrier' of P -defined Function-like total set
the ResultSort of P is non empty Relation-like the carrier' of P -defined the carrier of P -valued Function-like total quasi_total Element of bool [: the carrier' of P, the carrier of P:]
[: the carrier' of P, the carrier of P:] is non empty Relation-like set
bool [: the carrier' of P, the carrier of P:] is non empty set
the ResultSort of P * the Sorts of S1 is non empty Relation-like the carrier' of P -defined Function-like total set
G is non empty Relation-like non-empty Function-like one-to-one (A)
proj1 G is non empty set
(A,G) is non empty with_non-empty_elements non empty-membered (A)
[: the carrier of P,(A,G):] is non empty Relation-like set
bool [: the carrier of P,(A,G):] is non empty set
G is Element of dom the charact of A
(A,G) is non empty Relation-like the carrier of A * -defined the carrier of A -valued Function-like ( the carrier of A * , the carrier of A,( the carrier of A, the charact of A))
( the carrier of A, the charact of A) is non empty functional with_non-empty_elements non empty-membered Element of bool (PFuncs (( the carrier of A *), the carrier of A))
bool (PFuncs (( the carrier of A *), the carrier of A)) is non empty set
the charact of A . G is non empty Relation-like Function-like homogeneous set
dom (A,G) is non empty functional FinSequence-membered Element of bool ( the carrier of A *)
bool ( the carrier of A *) is non empty set
S2 . G is set
R is Relation-like NAT -defined proj2 the Sorts of S1 -valued Function-like V44() FinSequence-like FinSubsequence-like countable FinSequence of proj2 the Sorts of S1
product R is functional with_common_domain product-like set
(A,G) * is non empty functional FinSequence-membered FinSequenceSet of (A,G)
the Charact of S1 | (S2 . G) is Relation-like S2 . G -defined the carrier' of P -defined Function-like set
SG is Relation-like non-empty NAT -defined (A,G) -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of (A,G) *
product SG is non empty functional with_common_domain product-like set
the Relation-like NAT -defined Function-like SG -compatible Element of product SG is Relation-like NAT -defined Function-like SG -compatible Element of product SG
(A,G) . the Relation-like NAT -defined Function-like SG -compatible Element of product SG is set
[ the Relation-like NAT -defined Function-like SG -compatible Element of product SG,((A,G) . the Relation-like NAT -defined Function-like SG -compatible Element of product SG)] is V26() set
{ the Relation-like NAT -defined Function-like SG -compatible Element of product SG,((A,G) . the Relation-like NAT -defined Function-like SG -compatible Element of product SG)} is non empty set
{ the Relation-like NAT -defined Function-like SG -compatible Element of product SG} is non empty trivial functional V51(1) with_common_domain set
{{ the Relation-like NAT -defined Function-like SG -compatible Element of product SG,((A,G) . the Relation-like NAT -defined Function-like SG -compatible Element of product SG)},{ the Relation-like NAT -defined Function-like SG -compatible Element of product SG}} is non empty with_non-empty_elements non empty-membered set
em is non empty Relation-like non-empty Function-like one-to-one ((A,G))
((A,G),em,[ the Relation-like NAT -defined Function-like SG -compatible Element of product SG,((A,G) . the Relation-like NAT -defined Function-like SG -compatible Element of product SG)]) is set
proj1 em is non empty set
em . ((A,G),em,[ the Relation-like NAT -defined Function-like SG -compatible Element of product SG,((A,G) . the Relation-like NAT -defined Function-like SG -compatible Element of product SG)]) is set
bool the carrier' of P is non empty set
( the carrier' of P,S2) is non empty with_non-empty_elements non empty-membered a_partition of the carrier' of P
dom the Charact of S1 is non empty Element of bool the carrier' of P
f is non empty Element of ( the carrier' of P,S2)
g is Element of f
the_arity_of g is Relation-like NAT -defined the carrier of P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of the carrier of P *
the Arity of P . g is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable Element of the carrier of P *
Q is non empty Relation-like non-empty non empty-yielding the carrier of P -defined (A,G) -valued Function-like total quasi_total Element of bool [: the carrier of P,(A,G):]
Q * (the_arity_of g) is Relation-like non-empty NAT -defined (A,G) -valued Function-like Element of bool [:NAT,(A,G):]
[:NAT,(A,G):] is non empty Relation-like V44() set
bool [:NAT,(A,G):] is non empty V44() set
g is Relation-like non-empty NAT -defined (A,G) -valued Function-like V44() FinSequence-like FinSubsequence-like countable FinSequence of (A,G)
{ (product b₁) where b₁ is Relation-like non-empty NAT -defined (A,G) -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of (A,G) * : verum } is set
(the_arity_of g) * the Sorts of S1 is Relation-like NAT -defined Function-like set
dom the Arity of P is non empty Element of bool the carrier' of P
Args (g,S1) is Element of proj2 ( the Sorts of S1 #)
proj2 ( the Sorts of S1 #) is non empty set
( the Arity of P * ( the Sorts of S1 #)) . g is set
( the Sorts of S1 #) . ( the Arity of P . g) is set
s1 is Relation-like non-empty NAT -defined (A,G) -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of (A,G) *
product s1 is non empty functional with_common_domain product-like set
o is non empty with_non-empty_elements non empty-membered a_partition of the carrier of A *
em . g is set
the Charact of S1 . g is set
Den (g,S1) is Relation-like Args (g,S1) -defined Result (g,S1) -valued Function-like quasi_total Element of bool [:(Args (g,S1)),(Result (g,S1)):]
Result (g,S1) is Element of proj2 the Sorts of S1
( the ResultSort of P * the Sorts of S1) . g is set
[:(Args (g,S1)),(Result (g,S1)):] is Relation-like set
bool [:(Args (g,S1)),(Result (g,S1)):] is non empty set
dom (Den (g,S1)) is Element of bool (Args (g,S1))
bool (Args (g,S1)) is non empty set
A is non empty partial non-empty UAStr
the carrier of A is non empty set
(A) is Relation-like the carrier of A -defined the carrier of A -valued total quasi_total reflexive symmetric transitive Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
Class (A) is non empty with_non-empty_elements non empty-membered a_partition of the carrier of A
P is non empty with_non-empty_elements non empty-membered (A)
(A,P) is non empty non void V72() strict ManySortedSign
S2 is non empty non void V72() ManySortedSign
the carrier' of S2 is non empty set
G is MSAlgebra over S2
Q is non empty Relation-like non-empty Function-like one-to-one ( the carrier' of S2)
the Sorts of G is non empty Relation-like the carrier of S2 -defined Function-like total set
the carrier of S2 is non empty set
proj1 Q is non empty set
the charact of A is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of A *), the carrier of A) -valued Function-like V44() FinSequence-like FinSubsequence-like countable homogeneous FinSequence of PFuncs (( the carrier of A *), the carrier of A)
the carrier of A * is non empty functional FinSequence-membered FinSequenceSet of the carrier of A
PFuncs (( the carrier of A *), the carrier of A) is non empty functional set
dom the charact of A is non empty countable Element of bool NAT
G is non-empty MSAlgebra over S2
the Sorts of G is non empty Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like total set
R is non empty Relation-like non-empty Function-like one-to-one (A)
proj1 R is non empty set
(A,R) is non empty with_non-empty_elements non empty-membered (A)
[: the carrier of S2,(A,R):] is non empty Relation-like set
bool [: the carrier of S2,(A,R):] is non empty set
the carrier' of (A,P) is non empty set
P * is non empty functional FinSequence-membered FinSequenceSet of P
{ [b₁,b₂] where b₁ is Element of dom the charact of A, b₂ is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P * : product b₂ meets dom (A,b₁) } is set
the carrier of (A,P) is non empty set
em is set
em is Relation-like Function-like set
proj1 em is set
proj2 em is set
[:(A,R),P:] is non empty Relation-like set
bool [:(A,R),P:] is non empty set
em is non empty Relation-like non-empty non empty-yielding (A,R) -defined P -valued Function-like total quasi_total Element of bool [:(A,R),P:]
R * em is Relation-like non-empty P -valued Function-like set
proj1 (R * em) is set
rng (R * em) is with_non-empty_elements Element of bool P
bool P is non empty set
rng em is non empty with_non-empty_elements non empty-membered Element of bool P
[: the carrier of S2, the carrier of (A,P):] is non empty Relation-like set
bool [: the carrier of S2, the carrier of (A,P):] is non empty set
f is non empty Relation-like the carrier of S2 -defined the carrier of (A,P) -valued Function-like total quasi_total Element of bool [: the carrier of S2, the carrier of (A,P):]
proj2 f is non empty set
g is set
( the carrier' of S2,Q,g) is set
g is Element of the carrier' of S2
the_arity_of g is Relation-like NAT -defined the carrier of S2 -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of the carrier of S2 *
the carrier of S2 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of S2
the Arity of S2 is non empty Relation-like the carrier' of S2 -defined the carrier of S2 * -valued Function-like total quasi_total Element of bool [: the carrier' of S2,( the carrier of S2 *):]
[: the carrier' of S2,( the carrier of S2 *):] is non empty Relation-like set
bool [: the carrier' of S2,( the carrier of S2 *):] is non empty set
the Arity of S2 . g is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable Element of the carrier of S2 *
SG is non empty Relation-like non-empty non empty-yielding the carrier of S2 -defined (A,R) -valued Function-like total quasi_total Element of bool [: the carrier of S2,(A,R):]
SG * (the_arity_of g) is Relation-like non-empty NAT -defined (A,R) -valued Function-like Element of bool [:NAT,(A,R):]
[:NAT,(A,R):] is non empty Relation-like V44() set
bool [:NAT,(A,R):] is non empty V44() set
product (SG * (the_arity_of g)) is non empty functional with_common_domain product-like set
s1 is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable FinSequence of P
product s1 is non empty functional with_common_domain product-like set
( the carrier' of S2,Q,g) is set
o is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P *
[( the carrier' of S2,Q,g),o] is V26() set
{( the carrier' of S2,Q,g),o} is non empty set
{( the carrier' of S2,Q,g)} is non empty trivial V51(1) set
{{( the carrier' of S2,Q,g),o},{( the carrier' of S2,Q,g)}} is non empty with_non-empty_elements non empty-membered set
p is V26() set
Args (g,G) is non empty Element of proj2 ( the Sorts of G #)
the Sorts of G # is non empty Relation-like non-empty non empty-yielding the carrier of S2 * -defined Function-like total set
proj2 ( the Sorts of G #) is non empty with_non-empty_elements non empty-membered set
the Arity of S2 * ( the Sorts of G #) is non empty Relation-like non-empty non empty-yielding the carrier' of S2 -defined Function-like total set
( the Arity of S2 * ( the Sorts of G #)) . g is non empty set
the Element of Args (g,G) is Element of Args (g,G)
Den (g,G) is non empty Relation-like Args (g,G) -defined Result (g,G) -valued Function-like total quasi_total Element of bool [:(Args (g,G)),(Result (g,G)):]
Result (g,G) is non empty Element of proj2 the Sorts of G
proj2 the Sorts of G is non empty with_non-empty_elements non empty-membered set
the ResultSort of S2 is non empty Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like total quasi_total Element of bool [: the carrier' of S2, the carrier of S2:]
[: the carrier' of S2, the carrier of S2:] is non empty Relation-like set
bool [: the carrier' of S2, the carrier of S2:] is non empty set
the ResultSort of S2 * the Sorts of G is non empty Relation-like non-empty non empty-yielding the carrier' of S2 -defined Function-like total set
( the ResultSort of S2 * the Sorts of G) . g is non empty set
[:(Args (g,G)),(Result (g,G)):] is non empty Relation-like set
bool [:(Args (g,G)),(Result (g,G)):] is non empty set
the Charact of G is non empty Relation-like the carrier' of S2 -defined Function-like total V52() ManySortedFunction of the Arity of S2 * ( the Sorts of G #), the ResultSort of S2 * the Sorts of G
the Charact of G . g is set
dom (Den (g,G)) is non empty Element of bool (Args (g,G))
bool (Args (g,G)) is non empty set
dom the Arity of S2 is non empty Element of bool the carrier' of S2
bool the carrier' of S2 is non empty set
dom the Charact of G is non empty Element of bool the carrier' of S2
a is Element of dom the charact of A
Q . a is set
the Charact of G | (Q . a) is Relation-like Q . a -defined the carrier' of S2 -defined Function-like set
(A,a) is non empty Relation-like the carrier of A * -defined the carrier of A -valued Function-like ( the carrier of A * , the carrier of A,( the carrier of A, the charact of A))
( the carrier of A, the charact of A) is non empty functional with_non-empty_elements non empty-membered Element of bool (PFuncs (( the carrier of A *), the carrier of A))
bool (PFuncs (( the carrier of A *), the carrier of A)) is non empty set
the charact of A . a is non empty Relation-like Function-like homogeneous set
proj2 ( the Charact of G | (Q . a)) is set
the Charact of G .: (Q . a) is set
dom (A,a) is non empty functional FinSequence-membered Element of bool ( the carrier of A *)
bool ( the carrier of A *) is non empty set
( the Sorts of G #) . ( the Arity of S2 . g) is non empty set
product o is non empty functional with_common_domain product-like set
[( the carrier' of S2,Q,g),o] is V26() set
{( the carrier' of S2,Q,g),o} is non empty set
{( the carrier' of S2,Q,g)} is non empty trivial V51(1) set
{{( the carrier' of S2,Q,g),o},{( the carrier' of S2,Q,g)}} is non empty with_non-empty_elements non empty-membered set
g is Relation-like Function-like set
proj1 g is set
proj2 g is set
[: the carrier' of S2, the carrier' of (A,P):] is non empty Relation-like set
bool [: the carrier' of S2, the carrier' of (A,P):] is non empty set
g is non empty Relation-like the carrier' of S2 -defined the carrier' of (A,P) -valued Function-like total quasi_total Element of bool [: the carrier' of S2, the carrier' of (A,P):]
proj2 g is non empty set
dom f is non empty Element of bool the carrier of S2
bool the carrier of S2 is non empty set
dom g is non empty Element of bool the carrier' of S2
bool the carrier' of S2 is non empty set
rng f is non empty Element of bool the carrier of (A,P)
bool the carrier of (A,P) is non empty set
rng g is non empty Element of bool the carrier' of (A,P)
bool the carrier' of (A,P) is non empty set
the ResultSort of S2 is non empty Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like total quasi_total Element of bool [: the carrier' of S2, the carrier of S2:]
[: the carrier' of S2, the carrier of S2:] is non empty Relation-like set
bool [: the carrier' of S2, the carrier of S2:] is non empty set
the ResultSort of S2 * f is non empty Relation-like the carrier' of S2 -defined the carrier of (A,P) -valued Function-like total set
the ResultSort of (A,P) is non empty Relation-like the carrier' of (A,P) -defined the carrier of (A,P) -valued Function-like total quasi_total Element of bool [: the carrier' of (A,P), the carrier of (A,P):]
[: the carrier' of (A,P), the carrier of (A,P):] is non empty Relation-like set
bool [: the carrier' of (A,P), the carrier of (A,P):] is non empty set
g * the ResultSort of (A,P) is non empty Relation-like the carrier' of S2 -defined the carrier of (A,P) -valued Function-like total set
the Arity of S2 is non empty Relation-like the carrier' of S2 -defined the carrier of S2 * -valued Function-like total quasi_total Element of bool [: the carrier' of S2,( the carrier of S2 *):]
the carrier of S2 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of S2
[: the carrier' of S2,( the carrier of S2 *):] is non empty Relation-like set
bool [: the carrier' of S2,( the carrier of S2 *):] is non empty set
the Arity of (A,P) is non empty Relation-like the carrier' of (A,P) -defined the carrier of (A,P) * -valued Function-like total quasi_total Element of bool [: the carrier' of (A,P),( the carrier of (A,P) *):]
the carrier of (A,P) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of (A,P)
[: the carrier' of (A,P),( the carrier of (A,P) *):] is non empty Relation-like set
bool [: the carrier' of (A,P),( the carrier of (A,P) *):] is non empty set
s1 is Element of the carrier' of S2
the ResultSort of S2 . s1 is Element of the carrier of S2
R . ( the ResultSort of S2 . s1) is set
the ResultSort of S2 * the Sorts of G is non empty Relation-like non-empty non empty-yielding the carrier' of S2 -defined Function-like total set
( the ResultSort of S2 * the Sorts of G) . s1 is non empty set
f * the ResultSort of S2 is non empty Relation-like the carrier' of S2 -defined the carrier of (A,P) -valued Function-like total quasi_total Element of bool [: the carrier' of S2, the carrier of (A,P):]
[: the carrier' of S2, the carrier of (A,P):] is non empty Relation-like set
bool [: the carrier' of S2, the carrier of (A,P):] is non empty set
(f * the ResultSort of S2) . s1 is Element of the carrier of (A,P)
f . ( the ResultSort of S2 . s1) is Element of the carrier of (A,P)
em . (R . ( the ResultSort of S2 . s1)) is set
g . s1 is Element of the carrier' of (A,P)
( the carrier' of S2,Q,s1) is set
p is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable FinSequence of P
[( the carrier' of S2,Q,s1),p] is V26() set
{( the carrier' of S2,Q,s1),p} is non empty set
{( the carrier' of S2,Q,s1)} is non empty trivial V51(1) set
{{( the carrier' of S2,Q,s1),p},{( the carrier' of S2,Q,s1)}} is non empty with_non-empty_elements non empty-membered set
a is Element of the carrier' of S2
Args (a,G) is non empty Element of proj2 ( the Sorts of G #)
the Sorts of G # is non empty Relation-like non-empty non empty-yielding the carrier of S2 * -defined Function-like total set
proj2 ( the Sorts of G #) is non empty with_non-empty_elements non empty-membered set
the Arity of S2 * ( the Sorts of G #) is non empty Relation-like non-empty non empty-yielding the carrier' of S2 -defined Function-like total set
( the Arity of S2 * ( the Sorts of G #)) . a is non empty set
product p is non empty functional with_common_domain product-like set
the Element of Args (a,G) is Element of Args (a,G)
the Charact of G is non empty Relation-like the carrier' of S2 -defined Function-like total V52() ManySortedFunction of the Arity of S2 * ( the Sorts of G #), the ResultSort of S2 * the Sorts of G
h is Element of dom the charact of A
Q . h is set
the Charact of G | (Q . h) is Relation-like Q . h -defined the carrier' of S2 -defined Function-like set
(A,h) is non empty Relation-like the carrier of A * -defined the carrier of A -valued Function-like ( the carrier of A * , the carrier of A,( the carrier of A, the charact of A))
( the carrier of A, the charact of A) is non empty functional with_non-empty_elements non empty-membered Element of bool (PFuncs (( the carrier of A *), the carrier of A))
bool (PFuncs (( the carrier of A *), the carrier of A)) is non empty set
the charact of A . h is non empty Relation-like Function-like homogeneous set
proj2 ( the Charact of G | (Q . h)) is set
dom the Charact of G is non empty Element of bool the carrier' of S2
the Charact of G .: (Q . h) is set
the Charact of G . a is set
Den (a,G) is non empty Relation-like Args (a,G) -defined Result (a,G) -valued Function-like total quasi_total Element of bool [:(Args (a,G)),(Result (a,G)):]
Result (a,G) is non empty Element of proj2 the Sorts of G
proj2 the Sorts of G is non empty with_non-empty_elements non empty-membered set
( the ResultSort of S2 * the Sorts of G) . a is non empty set
[:(Args (a,G)),(Result (a,G)):] is non empty Relation-like set
bool [:(Args (a,G)),(Result (a,G)):] is non empty set
dom (Den (a,G)) is non empty Element of bool (Args (a,G))
bool (Args (a,G)) is non empty set
dom (A,h) is non empty functional FinSequence-membered Element of bool ( the carrier of A *)
bool ( the carrier of A *) is non empty set
h is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P *
product h is non empty functional with_common_domain product-like set
(A,h) .: (product h) is Element of bool the carrier of A
bool the carrier of A is non empty set
the ResultSort of (A,P) . (g . s1) is Element of the carrier of (A,P)
Result (s1,G) is non empty Element of proj2 the Sorts of G
Den (s1,G) is non empty Relation-like Args (s1,G) -defined Result (s1,G) -valued Function-like total quasi_total Element of bool [:(Args (s1,G)),(Result (s1,G)):]
Args (s1,G) is non empty Element of proj2 ( the Sorts of G #)
( the Arity of S2 * ( the Sorts of G #)) . s1 is non empty set
[:(Args (s1,G)),(Result (s1,G)):] is non empty Relation-like set
bool [:(Args (s1,G)),(Result (s1,G)):] is non empty set
the Charact of G . s1 is set
rng (Den (s1,G)) is non empty Element of bool (Result (s1,G))
bool (Result (s1,G)) is non empty set
(Den (s1,G)) .: (Args (s1,G)) is Element of bool (Result (s1,G))
(Den (s1,G)) .: (product h) is Element of bool (Result (s1,G))
(Den (s1,G)) . the Element of Args (a,G) is set
the ResultSort of (A,P) * g is non empty Relation-like the carrier' of S2 -defined the carrier of (A,P) -valued Function-like total quasi_total Element of bool [: the carrier' of S2, the carrier of (A,P):]
( the ResultSort of (A,P) * g) . s1 is Element of the carrier of (A,P)
s1 is set
o is Relation-like Function-like set
the Arity of S2 . s1 is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
p is Element of the carrier' of S2
the Arity of S2 . p is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable Element of the carrier of S2 *
a is Relation-like NAT -defined the carrier of S2 -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of the carrier of S2 *
SG is non empty Relation-like non-empty non empty-yielding the carrier of S2 -defined (A,R) -valued Function-like total quasi_total Element of bool [: the carrier of S2,(A,R):]
SG * a is Relation-like non-empty NAT -defined (A,R) -valued Function-like Element of bool [:NAT,(A,R):]
[:NAT,(A,R):] is non empty Relation-like V44() set
bool [:NAT,(A,R):] is non empty V44() set
g . p is Element of the carrier' of (A,P)
( the carrier' of S2,Q,p) is set
h is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable FinSequence of P
[( the carrier' of S2,Q,p),h] is V26() set
{( the carrier' of S2,Q,p),h} is non empty set
{( the carrier' of S2,Q,p)} is non empty trivial V51(1) set
{{( the carrier' of S2,Q,p),h},{( the carrier' of S2,Q,p)}} is non empty with_non-empty_elements non empty-membered set
r is Element of the carrier' of S2
Args (r,G) is non empty Element of proj2 ( the Sorts of G #)
( the Arity of S2 * ( the Sorts of G #)) . r is non empty set
product h is non empty functional with_common_domain product-like set
s2 is Element of dom the charact of A
p9 is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P *
[s2,p9] is V26() set
{s2,p9} is non empty set
{s2} is non empty trivial V51(1) set
{{s2,p9},{s2}} is non empty with_non-empty_elements non empty-membered set
product p9 is non empty functional with_common_domain product-like set
(A,s2) is non empty Relation-like the carrier of A * -defined the carrier of A -valued Function-like ( the carrier of A * , the carrier of A,( the carrier of A, the charact of A))
the charact of A . s2 is non empty Relation-like Function-like homogeneous set
dom (A,s2) is non empty functional FinSequence-membered Element of bool ( the carrier of A *)
g . s1 is set
the Arity of (A,P) . (g . s1) is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
( the Sorts of G #) . a is non empty set
h is Relation-like non-empty NAT -defined (A,R) -valued Function-like V44() FinSequence-like FinSubsequence-like countable FinSequence of (A,R)
product h is non empty functional with_common_domain product-like set
em * h is Relation-like non-empty NAT -defined P -valued Function-like Element of bool [:NAT,P:]
[:NAT,P:] is non empty Relation-like V44() set
bool [:NAT,P:] is non empty V44() set
o * f is Relation-like the carrier of (A,P) -valued Function-like set
s1 is set
o is non empty Element of P
the Element of o is Element of o
( the carrier of A,R, the Element of o) is set
R . ( the carrier of A,R, the Element of o) is set
em . (R . ( the carrier of A,R, the Element of o)) is set
f . ( the carrier of A,R, the Element of o) is set
s1 is set
o is Element of dom the charact of A
p is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of P *
[o,p] is V26() set
{o,p} is non empty set
{o} is non empty trivial V51(1) set
{{o,p},{o}} is non empty with_non-empty_elements non empty-membered set
product p is non empty functional with_common_domain product-like set
(A,o) is non empty Relation-like the carrier of A * -defined the carrier of A -valued Function-like ( the carrier of A * , the carrier of A,( the carrier of A, the charact of A))
the charact of A . o is non empty Relation-like Function-like homogeneous set
dom (A,o) is non empty functional FinSequence-membered Element of bool ( the carrier of A *)
a is set
dom p is countable Element of bool NAT
h is Relation-like Function-like set
proj1 h is set
Union p is set
Funcs ((dom p),(Union p)) is functional set
h is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable set
rng p is with_non-empty_elements Element of bool P
union (rng p) is set
union P is non empty Element of bool the carrier of A
proj2 h is set
r is Relation-like Function-like set
proj1 r is set
proj2 r is set
r is Relation-like non-empty NAT -defined (A,R) -valued Function-like V44() FinSequence-like FinSubsequence-like countable FinSequence of (A,R)
product r is non empty functional with_common_domain product-like set
dom h is countable Element of bool NAT
dom r is countable Element of bool NAT
s2 is set
h . s2 is set
p . s2 is set
r . s2 is set
rng r is with_non-empty_elements Element of bool (A,R)
bool (A,R) is non empty set
p9 is set
Q . o is set
s2 is Element of the carrier' of S2
the_arity_of s2 is Relation-like NAT -defined the carrier of S2 -valued Function-like V44() FinSequence-like FinSubsequence-like countable Element of the carrier of S2 *
the Arity of S2 . s2 is Relation-like NAT -defined Function-like V44() FinSequence-like FinSubsequence-like countable Element of the carrier of S2 *
(the_arity_of s2) * the Sorts of G is Relation-like non-empty NAT -defined Function-like set
g . s2 is Element of the carrier' of (A,P)
( the carrier' of S2,Q,s2) is set
p9 is Relation-like non-empty NAT -defined P -valued Function-like V44() FinSequence-like FinSubsequence-like countable FinSequence of P
[( the carrier' of S2,Q,s2),p9] is V26() set
{( the carrier' of S2,Q,s2),p9} is non empty set
{( the carrier' of S2,Q,s2)} is non empty trivial V51(1) set
{{( the carrier' of S2,Q,s2),p9},{( the carrier' of S2,Q,s2)}} is non empty with_non-empty_elements non empty-membered set
o9 is Element of the carrier' of S2
Args (o9,G) is non empty Element of proj2 ( the Sorts of G #)
( the Arity of S2 * ( the Sorts of G #)) . o9 is non empty set
product p9 is non empty functional with_common_domain product-like set
dom the Arity of S2 is non empty Element of bool the carrier' of S2
Args (s2,G) is non empty Element of proj2 ( the Sorts of G #)
( the Arity of S2 * ( the Sorts of G #)) . s2 is non empty set
( the Sorts of G #) . ( the Arity of S2 . s2) is non empty set
em * r is Relation-like non-empty NAT -defined P -valued Function-like Element of bool [:NAT,P:]