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

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

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

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

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

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

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

F

[:F

bool [:F

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

F

P . F

S1 is Relation-like F

G is Relation-like 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

F

F

[:F

bool [:F

A is Relation-like F

P is Relation-like 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

F

[:F

bool [:F

F

F

A is Relation-like F

P is Relation-like F

S1 is non empty Relation-like NAT -defined Function-like total set

S1 . F

S1 . 0 is set

S2 is non empty Relation-like NAT -defined Function-like total set

S2 . F

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

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