:: HILBERT2 semantic presentation

REAL is set

NAT is non empty epsilon-transitive epsilon-connected ordinal Element of bool REAL

bool REAL is non empty set

NAT is non empty epsilon-transitive epsilon-connected ordinal set

bool NAT is non empty set

bool NAT is non empty set

{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V29() ext-real non negative V33() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V50() constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding set

1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

{{},1} is non empty set

Trees is non empty constituted-Trees set

bool Trees is non empty set

FinTrees is non empty constituted-Trees constituted-FinTrees Element of bool Trees

HP-WFF is functional non empty with_VERUM with_implication with_conjunction with_propositional_variables HP-closed set

bool HP-WFF is non empty set

2 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

3 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V29() ext-real non negative V33() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V50() constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Element of NAT

<*0*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT

<*1*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT

<*2*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT

NAT * is functional non empty FinSequence-membered set

Seg 1 is non empty V33() V40(1) Element of bool NAT

<*> NAT is Relation-like non-empty empty-yielding NAT -defined NAT -valued Function-like one-to-one constant functional empty proper V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V29() ext-real non negative V33() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V50() constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding FinSequence of NAT

[:NAT,NAT:] is Relation-like non empty set

elementary_tree 0 is non empty Tree-like set

{{}} is functional non empty set

tree {} is non empty V33() Tree-like set

dom {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V29() ext-real non negative V33() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V50() constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding set

rng {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty trivial V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V29() ext-real non negative V33() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V50() constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding set

len {} is V38() set

p is set

union p is set

q is Relation-like p -defined Function-like total set

Union q is set

x is Relation-like Function-like set

dom x is set

rng q is set

union (rng q) is set

f is set

x . f is set

[f,(x . f)] is set

{f,(x . f)} is non empty set

{f} is non empty set

{{f,(x . f)},{f}} is non empty set

r is set

dom q is set

s is set

q . s is set

s is Relation-like s -defined Function-like total set

dom s is set

r is set

q . r is set

s is Relation-like r -defined Function-like total set

dom s is set

s . f is set

[f,(s . f)] is set

{f,(s . f)} is non empty set

{f} is non empty set

{{f,(s . f)},{f}} is non empty set

dom q is set

p is set

<*p*> is Relation-like NAT -defined Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like set

q is set

<*q*> is Relation-like NAT -defined Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like set

x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

<*p*> ^ x is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

<*q*> ^ f is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*q*> ^ f) . 1 is set

p is set

<*p*> is Relation-like NAT -defined Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like set

q is set

rng <*p*> is non empty set

{p} is non empty set

p is set

q is Relation-like NAT -defined p -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of p

x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

f is set

<*f*> is Relation-like NAT -defined Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like set

x ^ <*f*> is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

r is Relation-like NAT -defined p -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of p

r ^ <*f*> is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

p is set

<*p*> is Relation-like NAT -defined Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like set

q is non empty Tree-like set

x is non empty Tree-like set

tree (q,x) is non empty Tree-like set

<*q,x*> is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like Tree-yielding set

len <*q,x*> is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

tree <*q,x*> is non empty Tree-like set

f is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

r is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

f + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

<*q,x*> . (f + 1) is set

<*f*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT

<*f*> ^ r is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

<*p*> . 1 is set

f is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

f + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

<*q,x*> . (f + 1) is set

<*f*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT

<*f*> ^ {} is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

F

p is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

q is set

<*q*> is Relation-like NAT -defined Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like set

p ^ <*q*> is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

x is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT

f is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT

r is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

<*r*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT

f ^ <*r*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() FinSequence-like FinSubsequence-like FinSequence of NAT

s is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like Element of F

p is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like Element of F

p is set

q is Relation-like Function-like DecoratedTree-like set

x is Relation-like Function-like DecoratedTree-like set

p -tree (q,x) is Relation-like Function-like DecoratedTree-like set

(p -tree (q,x)) . {} is set

<*q,x*> is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like DTree-yielding set

p -tree <*q,x*> is Relation-like Function-like DecoratedTree-like set

p is set

q is Relation-like Function-like DecoratedTree-like set

q . {} is set

x is Relation-like Function-like DecoratedTree-like set

p -tree (q,x) is Relation-like Function-like DecoratedTree-like set

(p -tree (q,x)) . <*0*> is set

(p -tree (q,x)) . <*1*> is set

x . {} is set

<*q,x*> is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like DTree-yielding set

len <*q,x*> is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

dom q is non empty Tree-like set

0 + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

<*q,x*> . (0 + 1) is set

p -tree <*q,x*> is Relation-like Function-like DecoratedTree-like set

(p -tree <*q,x*>) . <*0*> is set

f is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like Element of dom q

<*0*> ^ f is Relation-like NAT -defined NAT -valued Function-like non empty V33() FinSequence-like FinSubsequence-like FinSequence of NAT

(p -tree <*q,x*>) . (<*0*> ^ f) is set

dom x is non empty Tree-like set

1 + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

<*q,x*> . (1 + 1) is set

(p -tree <*q,x*>) . <*1*> is set

r is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like Element of dom x

<*1*> ^ r is Relation-like NAT -defined NAT -valued Function-like non empty V33() FinSequence-like FinSubsequence-like FinSequence of NAT

(p -tree <*q,x*>) . (<*1*> ^ r) is set

p is set

q is Relation-like Function-like DecoratedTree-like set

x is Relation-like Function-like DecoratedTree-like set

p -tree (q,x) is Relation-like Function-like DecoratedTree-like set

(p -tree (q,x)) | <*0*> is Relation-like Function-like DecoratedTree-like set

(p -tree (q,x)) | <*1*> is Relation-like Function-like DecoratedTree-like set

<*q,x*> is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like DTree-yielding set

len <*q,x*> is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

p -tree <*q,x*> is Relation-like Function-like DecoratedTree-like set

(p -tree <*q,x*>) | <*0*> is Relation-like Function-like DecoratedTree-like set

0 + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

<*q,x*> . (0 + 1) is set

(p -tree <*q,x*>) | <*1*> is Relation-like Function-like DecoratedTree-like set

1 + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

<*q,x*> . (1 + 1) is set

p is set

q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like DTree-yielding set

p -tree q is Relation-like Function-like DecoratedTree-like set

dom (p -tree q) is non empty Tree-like set

dom q is non empty Element of bool NAT

doms q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Tree-yielding set

x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like DTree-yielding set

doms x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Tree-yielding set

tree (doms x) is non empty Tree-like set

p is set

q is Relation-like Function-like DecoratedTree-like set

p -tree q is Relation-like Function-like DecoratedTree-like set

<*q*> is Relation-like NAT -defined Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like DTree-yielding set

p -tree <*q*> is Relation-like Function-like non trivial DecoratedTree-like set

x is Relation-like Function-like DecoratedTree-like set

p -tree (q,x) is Relation-like Function-like DecoratedTree-like set

<*q,x*> is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like DTree-yielding set

p -tree <*q,x*> is Relation-like Function-like non trivial DecoratedTree-like set

p is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

3 + p is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

<*(3 + p)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT

p is set

VERUM is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

q is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

(q) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

3 + q is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

<*(3 + q)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT

q is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

3 + q is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

<*(3 + q)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT

(q) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

p is functional Element of bool HP-WFF

q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

q => x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

<*1*> ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*1*> ^ q) ^ x is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

<*1*> ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*1*> ^ q) ^ x is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

r is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

f => r is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

<*1*> ^ f is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*1*> ^ f) ^ r is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

q '&' x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

<*2*> ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*2*> ^ q) ^ x is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

<*2*> ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*2*> ^ q) ^ x is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

r is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

f '&' r is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

<*2*> ^ f is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*2*> ^ f) ^ r is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

{ b

q is set

x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

q is functional Element of bool HP-WFF

f is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

(f) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

3 + f is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

<*(3 + f)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT

f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

r is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

f => r is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

<*1*> ^ f is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*1*> ^ f) ^ r is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

f is set

f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

r is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

f '&' r is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

<*2*> ^ f is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*2*> ^ f) ^ r is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

p is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

q is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

(q) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

3 + q is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

<*(3 + q)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT

q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

q '&' x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

<*2*> ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*2*> ^ q) ^ x is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

q => x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

<*1*> ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*1*> ^ q) ^ x is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

p is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

len p is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

q '&' x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

<*2*> ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*2*> ^ q) ^ x is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

q ^ x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

<*2*> ^ (q ^ x) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

len (<*2*> ^ (q ^ x)) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

len <*2*> is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

len (q ^ x) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

(len <*2*>) + (len (q ^ x)) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

1 + (len (q ^ x)) is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

q => x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

<*1*> ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*1*> ^ q) ^ x is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

q ^ x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

<*1*> ^ (q ^ x) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

len (<*1*> ^ (q ^ x)) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

len <*1*> is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

len (q ^ x) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

(len <*1*>) + (len (q ^ x)) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

1 + (len (q ^ x)) is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

q is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

(q) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

3 + q is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

<*(3 + q)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT

p is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

p . 1 is set

q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

q '&' x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

<*2*> ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*2*> ^ q) ^ x is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

q ^ x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

<*2*> ^ (q ^ x) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

q is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

(q) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

3 + q is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

<*(3 + q)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT

1 + 0 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

2 + q is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

1 + (2 + q) is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

p is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

p . 1 is set

q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

q => x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

<*1*> ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*1*> ^ q) ^ x is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

q ^ x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

<*1*> ^ (q ^ x) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

q is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

(q) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

3 + q is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

<*(3 + q)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT

2 + 0 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

1 + q is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

2 + (1 + q) is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

p is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

3 + p is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

q . 1 is set

x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

x '&' f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

<*2*> ^ x is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*2*> ^ x) ^ f is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

x ^ f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

<*2*> ^ (x ^ f) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

2 + 0 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

1 + p is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

2 + (1 + p) is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

x => f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

<*1*> ^ x is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*1*> ^ x) ^ f is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

x ^ f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

<*1*> ^ (x ^ f) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

1 + 0 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

2 + p is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

1 + (2 + p) is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

p is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

p . 1 is set

q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

q '&' x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

<*2*> ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*2*> ^ q) ^ x is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

q ^ x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

<*2*> ^ (q ^ x) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

q => x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

<*1*> ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*1*> ^ q) ^ x is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

q ^ x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

<*1*> ^ (q ^ x) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

q is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

(q) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

3 + q is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

<*(3 + q)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT

p is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

len p is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

p '&' q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

<*2*> ^ p is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*2*> ^ p) ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

len (p '&' q) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

len q is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

len (<*2*> ^ p) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

(len (<*2*> ^ p)) + (len q) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

len <*2*> is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

(len <*2*>) + (len p) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

((len <*2*>) + (len p)) + (len q) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

1 + (len p) is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

(1 + (len p)) + (len q) is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

(len p) + (len q) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

1 + ((len p) + (len q)) is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

p is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

len p is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

p => q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

<*1*> ^ p is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*1*> ^ p) ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

len (p => q) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

len q is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

len (<*1*> ^ p) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

(len (<*1*> ^ p)) + (len q) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

len <*1*> is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

(len <*1*>) + (len p) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

((len <*1*>) + (len p)) + (len q) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

1 + (len p) is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

(1 + (len p)) + (len q) is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

(len p) + (len q) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

1 + ((len p) + (len q)) is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

p is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

q ^ x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

f is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative set

r is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

len r is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

s ^ s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

len s is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

r . 1 is set

s . 1 is set

s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

c

s '&' c

<*2*> ^ s is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*2*> ^ s) ^ c

s ^ c

<*2*> ^ (s ^ c

(<*2*> ^ (s ^ c

Y9 is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

IMrMs is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

Y9 '&' IMrMs is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

<*2*> ^ Y9 is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*2*> ^ Y9) ^ IMrMs is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

Y9 ^ IMrMs is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

(Y9 ^ IMrMs) ^ s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

<*2*> ^ ((Y9 ^ IMrMs) ^ s) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

<*2*> ^ (Y9 ^ IMrMs) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*2*> ^ (Y9 ^ IMrMs)) ^ s is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

IMrMs ^ s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

Y9 ^ (IMrMs ^ s) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

len s is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

len Y9 is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

len s is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

(len s) + (len s) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

N is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

s ^ N is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

len c

len Y9 is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

len s is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

N is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

Y9 ^ N is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

len c

len s is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

len Y9 is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

c

s => c

<*1*> ^ s is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*1*> ^ s) ^ c

s ^ c

<*1*> ^ (s ^ c

(<*1*> ^ (s ^ c

Y9 is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

IMrMs is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

Y9 => IMrMs is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

<*1*> ^ Y9 is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*1*> ^ Y9) ^ IMrMs is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

Y9 ^ IMrMs is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

(Y9 ^ IMrMs) ^ s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

<*1*> ^ ((Y9 ^ IMrMs) ^ s) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

<*1*> ^ (Y9 ^ IMrMs) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*1*> ^ (Y9 ^ IMrMs)) ^ s is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

IMrMs ^ s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

Y9 ^ (IMrMs ^ s) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

len s is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

len Y9 is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

len s is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

(len s) + (len s) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

N is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

s ^ N is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

len c

len Y9 is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

len s is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

N is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

Y9 ^ N is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

len c

len s is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

len Y9 is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

s is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

(s) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

3 + s is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

<*(3 + s)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT

len p is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

p is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

p ^ q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

x ^ f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

len p is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

len x is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

r is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

p ^ r is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

len x is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

len p is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

r is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

x ^ r is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

len p is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

len x is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

p is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

p '&' q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

<*2*> ^ p is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*2*> ^ p) ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

x '&' f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

<*2*> ^ x is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*2*> ^ x) ^ f is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

p ^ q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

<*2*> ^ (p ^ q) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

x ^ f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

<*2*> ^ (x ^ f) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

p is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

p => q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

<*1*> ^ p is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*1*> ^ p) ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

x => f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

<*1*> ^ x is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*1*> ^ x) ^ f is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

p ^ q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

<*1*> ^ (p ^ q) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

x ^ f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

<*1*> ^ (x ^ f) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

p is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

(p) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

3 + p is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

<*(3 + p)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT

q is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

(q) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

3 + q is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

<*(3 + q)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT

p is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

p '&' q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

<*2*> ^ p is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*2*> ^ p) ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

x => f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

<*1*> ^ x is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*1*> ^ x) ^ f is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

p ^ q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

<*2*> ^ (p ^ q) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

x ^ f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

<*1*> ^ (x ^ f) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(p '&' q) . 1 is set

p is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

p '&' q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

<*2*> ^ p is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*2*> ^ p) ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

p ^ q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

<*2*> ^ (p ^ q) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(p '&' q) . 1 is set

p is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

(p) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

3 + p is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

<*(3 + p)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT

q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

q '&' x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

<*2*> ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*2*> ^ q) ^ x is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

2 + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

(2 + 1) + p is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

2 + 0 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

1 + p is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

2 + (1 + p) is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

q ^ x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

<*2*> ^ (q ^ x) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(q '&' x) . 1 is set

p is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

p => q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

<*1*> ^ p is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*1*> ^ p) ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

p ^ q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

<*1*> ^ (p ^ q) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(p => q) . 1 is set

p is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

(p) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

3 + p is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

<*(3 + p)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT

q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

q => x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

<*1*> ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*1*> ^ q) ^ x is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

1 + 2 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

(1 + 2) + p is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

1 + 0 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

2 + p is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

1 + (2 + p) is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

q ^ x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set

<*1*> ^ (q ^ x) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(q => x) . 1 is set

p is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

p '&' q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

<*2*> ^ p is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*2*> ^ p) ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

len (p '&' q) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

len p is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

p is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

p => q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

<*1*> ^ p is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*1*> ^ p) ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

len (p => q) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

len p is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

p is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

(p) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

3 + p is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

<*(3 + p)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT

VERUM . 1 is set

F

{ (b

{ b

( ( not b

( b

( not b

( not b

( not b

( not b

x is set

f is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

(f) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

3 + f is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

<*(3 + f)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT

{VERUM} is functional non empty set

{ (b

x is functional Element of bool HP-WFF

f is set

r is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

(r) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

3 + r is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

<*(3 + r)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT

F

s is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

(s) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

3 + s is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

<*(3 + s)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT

F

r is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

(r) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

3 + r is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

<*(3 + r)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT

F

f is Relation-like x -defined Function-like total set

r is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

r '&' s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

<*2*> ^ r is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*2*> ^ r) ^ s is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

r => s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

<*1*> ^ r is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*1*> ^ r) ^ s is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

s is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

(s) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

3 + s is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

<*(3 + s)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT

s is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

(s) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

3 + s is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

<*(3 + s)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT

r is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

r '&' s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

<*2*> ^ r is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*2*> ^ r) ^ s is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

r => s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

<*1*> ^ r is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*1*> ^ r) ^ s is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

s '&' s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

<*2*> ^ s is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*2*> ^ s) ^ s is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

c

f . s is set

Y9 is set

f . s is set

IMrMs is set

f . (s '&' s) is set

r is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

(r) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

3 + r is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

<*(3 + r)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT

r is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

(r) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

3 + r is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

<*(3 + r)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT

f . (r) is set

F

r is set

union r is set

s is set

s is functional Element of bool HP-WFF

s is Relation-like s -defined Function-like total set

s . VERUM is set

s is set

s is set

c

Y9 is Relation-like c

Y9 . VERUM is set

Y9 is Relation-like c

Y9 . VERUM is set

s is Relation-like r -defined Function-like total set

rng s is set

c

dom s is set

Y9 is set

s . Y9 is set

IMrMs is Relation-like Y9 -defined Function-like total set

IMrMs . VERUM is set

c

Y9 is Relation-like Function-like set

IMrMs is Relation-like Function-like set

dom Y9 is set

dom IMrMs is set

dom s is set

N is set

s . N is set

N is Relation-like N -defined Function-like total set

N . VERUM is set

N is set

s . N is set

p is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT

(p) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

3 + p is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT

<*(3 + p)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT

Y9 . (p) is set

IMrMs . (p) is set

F

q is Relation-like N -defined Function-like total set

q . VERUM is set

q is Relation-like N -defined Function-like total set

q . VERUM is set

p is Relation-like N -defined Function-like total set

p . VERUM is set

p is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

Y9 . p is set

IMrMs . p is set

q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

Y9 . q is set

IMrMs . q is set

p '&' q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

<*2*> ^ p is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*2*> ^ p) ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

Y9 . (p '&' q) is set

IMrMs . (p '&' q) is set

p => q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

<*1*> ^ p is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*1*> ^ p) ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

Y9 . (p => q) is set

IMrMs . (p => q) is set

z is functional Element of bool HP-WFF

x is Relation-like N -defined Function-like total set

x . VERUM is set

y is Relation-like N -defined Function-like total set

y . VERUM is set

MZ1 is Relation-like z -defined Function-like total set

MZ1 . VERUM is set

z is functional Element of bool HP-WFF

x is Relation-like N -defined Function-like total set

x . VERUM is set

y is Relation-like N -defined Function-like total set

y . VERUM is set

MZ1 is Relation-like z -defined Function-like total set

MZ1 . VERUM is set

p is set

(dom Y9) /\ (dom IMrMs) is set

Y9 . p is set

IMrMs . p is set

Y9 . VERUM is set

IMrMs . VERUM is set

q is Relation-like N -defined Function-like total set

q . VERUM is set

x is Relation-like N -defined Function-like total set

x . VERUM is set

Y9 is Relation-like Function-like set

IMrMs is Relation-like Function-like set

dom s is set

N is set

s . N is set

dom Y9 is set

N is Relation-like N -defined Function-like total set

N . VERUM is set

N is set

s . N is set

dom IMrMs is set

p is Relation-like N -defined Function-like total set

p . VERUM is set

union c

Union s is set

IMrMs is set

s . IMrMs is set

N is Relation-like IMrMs -defined Function-like total set

N . VERUM is set

Y9 is Relation-like Function-like set

dom Y9 is set

s is functional Element of bool HP-WFF

IMrMs is Relation-like s -defined Function-like total set

N is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

IMrMs . N is set

N is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

N '&' N is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF

<*2*> ^ N is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

(<*2*> ^ N) ^ N is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set

IMrMs . N is set

IMrMs . (N '&' N) is set

p is set

dom s is set

s . p is set

q is set

x is set

y is set

z is Relation-like p -defined Function-like total set

z . VERUM is set

dom z is set

z . (N '&' N) is set

MZ1 is functional Element of bool HP-WFF

c

c

z . N is set

MZ1 is functional Element of bool HP-WFF

c

c

z . N is set

dom s is set

s . s is set

N is Relation-like s -defined Function-like total set

N . VERUM is set

N is set

p is functional Element of bool HP-WFF

q is Relation-like p</