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

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

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

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

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

rng (S2 * S1) is Element of bool P
bool P is non empty set

S1 is set
proj1 P is set
P . S1 is set

rng P is Element of bool A
bool A is non empty set
A is non empty set

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

S1 is Relation-like Function-like Element 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

S2 is V4() V5() V6() V10() V14() V44() V49() countable set

S2 is 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

proj1 A is set
proj1 P is set

proj1 S2 is set

proj1 G is set
S2 is set
A . S2 is set
P . S2 is set
G is set

proj1 R is set
SG is set
R . SG is set
G . SG is set
A . SG is set
R . S2 is set

proj1 SG is set

proj1 em is set

proj1 P is set
proj1 A is set
S2 is set
A . S2 is set
P . S2 is set

proj1 G is set

proj1 Q is set

proj1 S2 is set

proj1 G is set
A is non empty set

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

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

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

G is set
A is set
P is set

S2 is set
S1 . S2 is set
rng S1 is Element of bool A
bool A is non empty 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

A is set

[:P,S1:] is Relation-like set
bool [:P,S1:] is non empty set

bool [:NAT,S1:] is non empty set

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

G is set
G . G is set
Q . G is set

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

proj2 P is set
proj1 P is set
S1 is set
P . S1 is set
S2 is set

proj1 S1 is set
proj2 S1 is set

A is set

rng S1 is Element of bool A
bool A is non empty set
union P is Element of bool A

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
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
{ [:b1,b2:] where b1 is non empty Element of S1, b2 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:])

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

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

P is non empty with_non-empty_elements non empty-membered a_partition of A

{ } 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

Q is 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

bool P is non empty set
S2 is Element of bool (bool (A *))

G is set

rng Q is Element of bool A
bool A is non empty set
union P is non empty Element of bool A

proj1 G is set
proj2 G is 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

SG is set

proj1 em is set

em is set
em . em is set
Q . em is set
R . em is set

proj1 f is set

bool P is non empty set

proj1 f is set

proj1 em is set
A is non empty set
P is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT

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 b1) where b1 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 () is non empty Element of bool (bool ())
bool () is non empty set
bool (bool ()) is non empty set
G is set

SG is set
dom R is V51(P) countable Element of bool NAT

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

bool S1 is non empty set

len em is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
G is Element of bool (bool ())

R is set

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

proj1 em is set
proj2 em is 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

len f is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT

f is set
dom SG is V51(P) countable Element of bool NAT

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

proj1 s1 is set

bool S1 is non empty set

proj1 s1 is 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
{ (b1 /\ P) where b1 is non empty Element of S1 : not b1 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 () is non empty set
S1 is non empty with_non-empty_elements non empty-membered a_partition of proj1 A
{ (A | b1) where b1 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)

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 ()
SG is set

R is non empty Element of S1
A | R is non empty Relation-like Function-like set

em is non empty Element of S1
A | em is non empty Relation-like Function-like set
SG is non empty Element of bool ()
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

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

Union S1 is set
Funcs ((dom S1),(Union S1)) is functional set

bool is non empty set
union (rng S1) is set
union is Element of bool A
bool A is non empty set
proj2 G is set

proj1 Q is set
proj2 Q is set

{Q} is non empty trivial functional V51(1) with_common_domain set
G is 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
{ {b1} where b1 is Element of em : verum } is set
em is Element of em
{em} is non empty trivial V51(1) set
A is set

[::] is Relation-like set
bool [::] is non empty set
proj2 () is with_non-empty_elements set
A is set

proj2 P is set
A is set

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

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,P:] is Relation-like set
bool [:P,P:] is non empty set

bool P is non empty set
A is set
S1 is set

(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

Union P is set
proj1 P 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
S1 is set
union () 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

rng S2 is non empty with_non-empty_elements non empty-membered Element of bool S1
bool S1 is non empty set
F1() is non empty set
F2() is non empty set
[:F1(),F2():] is non empty Relation-like set
bool [:F1(),F2():] is non empty set
F3() is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
F4() is Relation-like F1() -defined F2() -valued Element of bool [:F1(),F2():]

proj1 A is set
A . 0 is 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 F1() -defined F2() -valued Element of bool [:F1(),F2():]
F5(S2,S1) is Relation-like F1() -defined F2() -valued Element of bool [:F1(),F2():]
P . F3() is set
S1 is Relation-like F1() -defined F2() -valued Element of bool [:F1(),F2():]
G is Relation-like F1() -defined F2() -valued Element of bool [:F1(),F2():]
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
F5(G,S2) is Relation-like F1() -defined F2() -valued Element of bool [:F1(),F2():]
F1() is non empty set
F2() is non empty set
[:F1(),F2():] is non empty Relation-like set
bool [:F1(),F2():] is non empty set
A is Relation-like F1() -defined F2() -valued Element of bool [:F1(),F2():]
P is Relation-like F1() -defined F2() -valued Element of bool [:F1(),F2():]
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 F1()
Q is Element of F2()
G is Element of F1()
Q is Element of F2()
F1() is non empty set
F2() is non empty set
[:F1(),F2():] is non empty Relation-like set
bool [:F1(),F2():] is non empty set
F3() is V4() V5() V6() V10() V14() V44() V49() countable Element of NAT
F4() is Relation-like F1() -defined F2() -valued Element of bool [:F1(),F2():]
A is Relation-like F1() -defined F2() -valued Element of bool [:F1(),F2():]
P is Relation-like F1() -defined F2() -valued Element of bool [:F1(),F2():]

S1 . F3() is set
S1 . 0 is set

S2 . F3() 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 F1() -defined F2() -valued Element of bool [:F1(),F2():]
F5(Q,G) is Relation-like F1() -defined F2() -valued Element of bool [:F1(),F2():]
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

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

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

Q is Element of the carrier of 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))
dom G is non empty functional FinSequence-membered Element of bool ( the carrier of A *)
bool ( the carrier of A *) is non empty 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 *)

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

Q is Element of the carrier of 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))
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

R is Element of 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:]
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 . 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 . 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

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

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 . ((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

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 *)

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

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 *),A:] is non empty Relation-like set
bool [:(A *),A:] is non empty set
A is non empty set

[:(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))

{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