:: 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