:: PRE_CIRC semantic presentation

REAL is V66() V67() V68() V72() V79() V80() V82() set

NAT is V6() V7() V8() non empty non trivial non finite cardinal limit_cardinal countable denumerable V66() V67() V68() V69() V70() V71() V72() V77() V79() Element of bool REAL

bool REAL is non empty set

{} is Relation-like non-empty empty-yielding NAT -defined V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty ext-real V39() finite finite-yielding V44() cardinal {} -element Cardinal-yielding countable V53() V66() V67() V68() V69() V70() V71() V72() V79() V80() V81() V82() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V89() constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding set

the Relation-like non-empty empty-yielding NAT -defined V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty ext-real V39() finite finite-yielding V44() cardinal {} -element Cardinal-yielding countable V53() V66() V67() V68() V69() V70() V71() V72() V79() V80() V81() V82() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V89() constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding set is Relation-like non-empty empty-yielding NAT -defined V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty ext-real V39() finite finite-yielding V44() cardinal {} -element Cardinal-yielding countable V53() V66() V67() V68() V69() V70() V71() V72() V79() V80() V81() V82() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V89() constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding set

1 is V6() V7() V8() V12() non empty ext-real positive V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V77() V78() V79() V80() V81() Element of NAT

[:1,1:] is Relation-like non empty finite countable set

bool [:1,1:] is non empty finite V44() countable set

[:[:1,1:],1:] is Relation-like non empty finite countable set

bool [:[:1,1:],1:] is non empty finite V44() countable set

NAT is V6() V7() V8() non empty non trivial non finite cardinal limit_cardinal countable denumerable V66() V67() V68() V69() V70() V71() V72() V77() V79() set

bool NAT is non empty non trivial non finite set

COMPLEX is V66() V72() set

RAT is V66() V67() V68() V69() V72() set

INT is V66() V67() V68() V69() V70() V72() set

bool NAT is non empty non trivial non finite set

[:COMPLEX,COMPLEX:] is Relation-like set

bool [:COMPLEX,COMPLEX:] is non empty set

[:COMPLEX,REAL:] is Relation-like set

bool [:COMPLEX,REAL:] is non empty set

{{},1} is non empty finite V44() countable V66() V67() V68() V69() V70() V71() V77() V78() V79() V80() V81() 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

[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set

[:REAL,REAL:] is Relation-like set

bool [:REAL,REAL:] is non empty set

[:[:REAL,REAL:],REAL:] is Relation-like set

bool [:[:REAL,REAL:],REAL:] is non empty set

[:RAT,RAT:] is Relation-like set

bool [:RAT,RAT:] is non empty set

[:[:RAT,RAT:],RAT:] is Relation-like set

bool [:[:RAT,RAT:],RAT:] is non empty set

[:INT,INT:] is Relation-like set

bool [:INT,INT:] is non empty set

[:[:INT,INT:],INT:] is Relation-like set

bool [:[:INT,INT:],INT:] is non empty set

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

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

bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite set

K474() is set

2 is V6() V7() V8() V12() non empty ext-real positive V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V77() V78() V79() V80() V81() Element of NAT

3 is V6() V7() V8() V12() non empty ext-real positive V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V77() V78() V79() V80() V81() Element of NAT

Seg 1 is non empty trivial finite 1 -element countable V66() V67() V68() V69() V70() V71() V77() V78() V79() V80() V81() Element of bool NAT

curry {} is Relation-like Function-like set

curry' {} is Relation-like Function-like set

uncurry {} is Relation-like Function-like set

uncurry' {} is Relation-like Function-like set

{{}} is functional non empty trivial finite V44() 1 -element with_common_domain countable V66() V67() V68() V69() V70() V71() V77() V78() V79() V80() V81() Tree-like set

NAT * is functional non empty FinSequence-membered FinSequenceSet of NAT

<*> NAT is Relation-like non-empty empty-yielding NAT -defined NAT -valued V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty proper ext-real V39() finite finite-yielding V44() cardinal {} -element Cardinal-yielding countable V53() V66() V67() V68() V69() V70() V71() V72() V79() V80() V81() V82() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V89() constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding FinSequence of NAT

0 is Relation-like non-empty empty-yielding NAT -defined V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty ext-real V39() finite finite-yielding V44() cardinal {} -element Cardinal-yielding countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V72() V79() V80() V81() V82() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V89() constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Element of NAT

product {} is functional non empty with_common_domain product-like set

F

{ F

{ F

X is set

X is Element of F

F

n is Relation-like Function-like set

proj1 n is set

proj2 n is set

X is set

{X} is non empty trivial finite 1 -element countable set

X is set

{X} is non empty trivial finite 1 -element countable set

[X,X] is V22() set

{X,X} is non empty finite countable set

{{X,X},{X}} is non empty finite V44() countable set

{[X,X]} is Relation-like Function-like constant non empty trivial finite 1 -element countable set

{X} --> X is Relation-like {X} -defined {X} -valued Function-like constant non empty total quasi_total finite countable Element of bool [:{X},{X}:]

[:{X},{X}:] is Relation-like non empty finite countable set

bool [:{X},{X}:] is non empty finite V44() countable set

n is set

<*> n is Relation-like non-empty empty-yielding NAT -defined n -valued V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty ext-real V39() finite finite-yielding V44() cardinal {} -element Cardinal-yielding countable V53() V66() V67() V68() V69() V70() V71() V72() V79() V80() V81() V82() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V89() constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding FinSequence of n

X is Relation-like n -defined Function-like total set

X # is Relation-like n * -defined Function-like non empty total set

n * is functional non empty FinSequence-membered FinSequenceSet of n

(X #) . (<*> n) is set

X is Relation-like NAT -defined n -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n *

X * X is Relation-like NAT -defined Function-like finite countable set

product (X * X) is functional with_common_domain product-like set

F

n is set

F

F

n is Relation-like F

X is Element of F

n . X is set

F

F

n is set

n --> {{}} is Relation-like non-empty n -defined {{{}}} -valued Function-like constant total quasi_total Element of bool [:n,{{{}}}:]

{{{}}} is non empty trivial finite V44() 1 -element countable set

[:n,{{{}}}:] is Relation-like set

bool [:n,{{{}}}:] is non empty set

X is Relation-like Function-like set

X is Relation-like n -defined Function-like total set

m is set

X . m is set

n is set

bool n is non empty set

X is Element of bool n

X is Relation-like n -defined Function-like total set

X | X is Relation-like X -defined n -defined Function-like set

proj1 (X | X) is set

proj1 X is set

(proj1 X) /\ X is Element of bool n

k is Relation-like X -defined Function-like set

n is set

bool n is non empty set

X is Element of bool n

X is Relation-like n -defined Function-like total set

X | X is Relation-like X -defined n -defined Function-like total set

n is Relation-like non-empty Function-like set

X is set

n | X is Relation-like Function-like set

proj2 (n | X) is set

proj2 n is set

n is non empty set

X is Relation-like non-empty non empty-yielding n -defined Function-like non empty total set

proj2 X is non empty set

union (proj2 X) is set

the Element of n is Element of n

proj1 X is non empty set

X . the Element of n is non empty set

n is set

n --> {} is Relation-like n -defined {{}} -valued Function-like constant total quasi_total Cardinal-yielding Function-yielding V89() Element of bool [:n,{{}}:]

[:n,{{}}:] is Relation-like set

bool [:n,{{}}:] is non empty set

uncurry (n --> {}) is Relation-like Function-like set

proj2 (n --> {}) is trivial finite countable set

Funcs ({},{}) is set

proj1 (uncurry (n --> {})) is set

proj1 (n --> {}) is set

[:(proj1 (n --> {})),{}:] is Relation-like set

n is non empty set

X is set

n --> X is Relation-like n -defined {X} -valued Function-like constant non empty total quasi_total Element of bool [:n,{X}:]

{X} is non empty trivial finite 1 -element countable set

[:n,{X}:] is Relation-like non empty set

bool [:n,{X}:] is non empty set

X is Relation-like non-empty non empty-yielding n -defined Function-like non empty total set

m is Relation-like n -defined Function-like non empty total Function-yielding V89() ManySortedFunction of n --> X,X

commute m is Relation-like Function-like Function-yielding V89() set

proj1 (commute m) is set

proj1 X is non empty set

proj1 m is non empty set

proj2 m is non empty set

k is set

C is set

m . C is Relation-like Function-like set

(n --> X) . C is set

X . C is set

[:((n --> X) . C),(X . C):] is Relation-like set

bool [:((n --> X) . C),(X . C):] is non empty set

n --> {} is Relation-like n -defined {{}} -valued Function-like constant non empty total quasi_total Cardinal-yielding Function-yielding V89() Element of bool [:n,{{}}:]

[:n,{{}}:] is Relation-like non empty set

bool [:n,{{}}:] is non empty set

uncurry m is Relation-like Function-like set

curry' (uncurry m) is Relation-like Function-like set

proj2 m is non empty set

proj2 X is non empty set

union (proj2 X) is set

Funcs (X,(union (proj2 X))) is set

k is set

C is set

m . C is Relation-like Function-like set

(n --> X) . C is set

X . C is set

[:X,(X . C):] is Relation-like set

bool [:X,(X . C):] is non empty set

A is Relation-like X -defined X . C -valued Function-like quasi_total Element of bool [:X,(X . C):]

proj2 A is set

proj1 A is set

Funcs (n,(Funcs (X,(union (proj2 X))))) is set

Funcs (n,(union (proj2 X))) is set

Funcs (X,(Funcs (n,(union (proj2 X))))) is set

[:X,(Funcs (n,(union (proj2 X)))):] is Relation-like set

bool [:X,(Funcs (n,(union (proj2 X)))):] is non empty set

F

[:NAT,F

bool [:NAT,F

F

n is Relation-like NAT -defined F

n . {} is Element of F

X is Relation-like NAT -defined F

X . {} is Element of F

F

bool F

F

F

F

n is Relation-like F

X is set

proj1 n is set

n . X is set

F

X is Relation-like F

X is set

X . X is Relation-like Function-like set

F

F

[:(F

bool [:(F

F

X is Relation-like F

m is Element of F

X . m is Relation-like Function-like set

F

n is set

X is Relation-like non-empty n -defined Function-like total set

product X is functional non empty with_common_domain product-like set

proj1 X is set

X is Relation-like Function-like set

proj1 X is set

m is Relation-like n -defined Function-like X -compatible total Element of product X

m +* X is Relation-like Function-like set

k is set

(m +* X) . k is set

X . k is set

X . k is set

(m +* X) . k is set

m . k is set

X . k is set

C is Relation-like Function-like set

proj1 C is set

proj1 (m +* X) is set

proj1 m is set

(proj1 m) \/ (proj1 X) is set

n is non empty set

X is non empty set

n --> X is Relation-like non-empty non empty-yielding n -defined {X} -valued Function-like constant non empty total quasi_total Element of bool [:n,{X}:]

{X} is non empty trivial finite 1 -element countable set

[:n,{X}:] is Relation-like non empty set

bool [:n,{X}:] is non empty set

X is Relation-like non-empty non empty-yielding n -defined Function-like non empty total set

m is Relation-like n -defined Function-like non empty total Function-yielding V89() ManySortedFunction of n --> X,X

commute m is Relation-like Function-like Function-yielding V89() set

k is Element of X

(commute m) . k is Relation-like Function-like set

proj1 m is non empty set

uncurry m is Relation-like Function-like set

proj1 (uncurry m) is set

[:n,X:] is Relation-like non empty set

C is set

A is set

C is set

[A,C] is V22() set

{A,C} is non empty finite countable set

{A} is non empty trivial finite 1 -element countable set

{{A,C},{A}} is non empty finite V44() countable set

B is Relation-like Function-like set

m . A is Relation-like Function-like set

proj1 B is set

(n --> X) . A is set

X . A is set

[:((n --> X) . A),(X . A):] is Relation-like set

bool [:((n --> X) . A),(X . A):] is non empty set

C is set

A is set

[C,A] is V22() set

{C,A} is non empty finite countable set

{C} is non empty trivial finite 1 -element countable set

{{C,A},{C}} is non empty finite V44() countable set

[C,A] `1 is set

m . ([C,A] `1) is Relation-like Function-like set

B is Relation-like Function-like set

(n --> X) . ([C,A] `1) is set

X . ([C,A] `1) is set

[:((n --> X) . ([C,A] `1)),(X . ([C,A] `1)):] is Relation-like set

bool [:((n --> X) . ([C,A] `1)),(X . ([C,A] `1)):] is non empty set

proj1 B is set

[C,A] `2 is set

curry' (uncurry m) is Relation-like Function-like set

(curry' (uncurry m)) . k is set

proj2 (uncurry m) is set

A is Relation-like Function-like set

proj1 A is set

proj2 A is set

C is Relation-like n -defined Function-like non empty total set

A is set

C . A is set

X . A is set

m . A is Relation-like Function-like set

(n --> X) . A is set

B is Relation-like Function-like set

[:X,(X . A):] is Relation-like set

bool [:X,(X . A):] is non empty set

proj1 B is set

(uncurry m) . (A,k) is set

B . k is set

C is Relation-like Function-like set

proj1 C is set

proj2 C is set

n is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

X is set

{X} is non empty trivial finite 1 -element countable set

n |-> {X} is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set

Seg n is finite n -element countable V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of bool NAT

(Seg n) --> {X} is Relation-like non-empty Seg n -defined {{X}} -valued Function-like constant total quasi_total finite countable Element of bool [:(Seg n),{{X}}:]

{{X}} is non empty trivial finite V44() 1 -element countable set

[:(Seg n),{{X}}:] is Relation-like finite countable set

bool [:(Seg n),{{X}}:] is non empty finite V44() countable set

product (n |-> {X}) is functional with_common_domain product-like set

n |-> X is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set

(Seg n) --> X is Relation-like Seg n -defined {X} -valued Function-like constant total quasi_total finite countable Element of bool [:(Seg n),{X}:]

[:(Seg n),{X}:] is Relation-like finite countable set

bool [:(Seg n),{X}:] is non empty finite V44() countable set

{(n |-> X)} is functional non empty trivial finite V44() 1 -element with_common_domain countable set

X is set

dom (n |-> {X}) is finite countable V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of bool NAT

m is Relation-like Function-like set

proj1 m is set

k is set

m . k is set

(n |-> {X}) . k is set

k is set

m is Relation-like Function-like set

m . k is set

(n |-> {X}) . k is set

proj1 m is set

n is non empty set

FinTrees n is functional non empty constituted-DTrees DTree-set of n

X is Relation-like n -valued Function-like DecoratedTree-like Element of FinTrees n

proj1 X is non empty finite countable Tree-like set

n is Relation-like Function-like finite countable DecoratedTree-like set

proj1 n is non empty finite countable Tree-like set

X is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of proj1 n

n | X is Relation-like Function-like DecoratedTree-like set

proj1 (n | X) is non empty Tree-like set

(proj1 n) | X is non empty finite countable Tree-like set

n is non empty finite countable Tree-like set

X is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n

n | X is non empty finite countable Tree-like set

{ b

m is Relation-like Function-like set

proj1 m is set

proj2 m is set

k is set

m . k is set

C is set

m . C is set

A is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n | X

X ^ A is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT

B is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n | X

m . B is set

X ^ B is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT

k is set

C is set

m . C is set

A is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n | X

X ^ A is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT

m . A is set

B is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n

k is set

C is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n

C is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set

X ^ C is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set

A is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n

B is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n

A is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n | X

m . A is set

n is Relation-like Function-like finite countable DecoratedTree-like set

proj1 n is non empty finite countable Tree-like set

X is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of proj1 n

X is Relation-like Function-like finite countable DecoratedTree-like set

n with-replacement (X,X) is Relation-like Function-like DecoratedTree-like set

proj1 (n with-replacement (X,X)) is non empty Tree-like set

proj1 X is non empty finite countable Tree-like set

(proj1 n) with-replacement (X,(proj1 X)) is non empty finite countable Tree-like set

n is non empty finite countable Tree-like set

X is non empty finite countable Tree-like set

X is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n

n with-replacement (X,X) is non empty finite countable Tree-like set

{ b

{ (X ^ b

{ b

{ b

{ H

{ H

B is set

C is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n

{X} is functional non empty trivial finite V44() 1 -element with_common_domain countable set

C is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n

C is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n

{ b

X ^ {} is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set

B is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of X

C is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of X

( { b

{X} \/ { H

{ b

{ b

n is non empty finite countable Tree-like set

X is non empty finite countable Tree-like set

X is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n

n with-replacement (X,X) is non empty finite countable Tree-like set

m is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT

{ b

k is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n

{ (X ^ b

{ b

n is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Tree-yielding set

dom n is finite countable V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of bool NAT

tree n is non empty Tree-like set

X is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

X + 1 is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

<*X*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element countable FinSequence-like FinSubsequence-like FinSequence of NAT

(tree n) | <*X*> is non empty Tree-like set

n . (X + 1) is set

len n is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

n is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like DTree-yielding set

dom n is finite countable V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of bool NAT

doms n is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Tree-yielding set

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

X is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

X + 1 is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

<*X*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element countable FinSequence-like FinSubsequence-like FinSequence of NAT

len n is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

Seg (len n) is finite len n -element countable V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of bool NAT

len (doms n) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

Seg (len (doms n)) is finite len (doms n) -element countable V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of bool NAT

dom (doms n) is finite countable V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of bool NAT

(doms n) . (X + 1) is set

<*X*> ^ {} is Relation-like NAT -defined Function-like non empty finite countable FinSequence-like FinSubsequence-like set

n is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Tree-yielding set

len n is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

X is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Tree-yielding set

len X is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

dom n is finite countable V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of bool NAT

tree X is non empty Tree-like set

tree n is non empty Tree-like set

X is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

X + 1 is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

X . (X + 1) is set

<*X*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element countable FinSequence-like FinSubsequence-like FinSequence of NAT

m is non empty Tree-like set

(tree n) with-replacement (<*X*>,m) is non empty Tree-like set

C is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT

A is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

B is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set

A + 1 is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

X . (A + 1) is set

<*A*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element countable FinSequence-like FinSubsequence-like FinSequence of NAT

<*A*> ^ B is Relation-like NAT -defined Function-like non empty finite countable FinSequence-like FinSubsequence-like set

A is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

B is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set

A + 1 is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

X . (A + 1) is set

<*A*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element countable FinSequence-like FinSubsequence-like FinSequence of NAT

<*A*> ^ B is Relation-like NAT -defined Function-like non empty finite countable FinSequence-like FinSubsequence-like set

C is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT

t is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT

<*X*> ^ t is Relation-like NAT -defined NAT -valued Function-like non empty finite countable FinSequence-like FinSubsequence-like FinSequence of NAT

n . (A + 1) is set

C . 1 is set

C is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set

<*X*> ^ C is Relation-like NAT -defined Function-like non empty finite countable FinSequence-like FinSubsequence-like set

C is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT

<*X*> ^ C is Relation-like NAT -defined NAT -valued Function-like non empty finite countable FinSequence-like FinSubsequence-like FinSequence of NAT

A is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

B is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set

A + 1 is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

n . (A + 1) is set

<*A*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element countable FinSequence-like FinSubsequence-like FinSequence of NAT

<*A*> ^ B is Relation-like NAT -defined Function-like non empty finite countable FinSequence-like FinSubsequence-like set

A is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

B is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set

A + 1 is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

n . (A + 1) is set

<*A*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element countable FinSequence-like FinSubsequence-like FinSequence of NAT

<*A*> ^ B is Relation-like NAT -defined Function-like non empty finite countable FinSequence-like FinSubsequence-like set

dom X is finite countable V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of bool NAT

X . (A + 1) is set

X . (A + 1) is set

A is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT

<*X*> ^ A is Relation-like NAT -defined NAT -valued Function-like non empty finite countable FinSequence-like FinSubsequence-like FinSequence of NAT

A is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT

<*X*> ^ A is Relation-like NAT -defined NAT -valued Function-like non empty finite countable FinSequence-like FinSubsequence-like FinSequence of NAT

n . (X + 1) is set

<*X*> ^ {} is Relation-like NAT -defined Function-like non empty finite countable FinSequence-like FinSubsequence-like set

n is Relation-like Function-like finite countable DecoratedTree-like set

proj1 n is non empty finite countable Tree-like set

X is Relation-like Function-like finite countable DecoratedTree-like set

X is set

m is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

<*m*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element countable FinSequence-like FinSubsequence-like FinSequence of NAT

n with-replacement (<*m*>,X) is Relation-like Function-like DecoratedTree-like set

m + 1 is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

k is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like DTree-yielding set

X -tree k is Relation-like Function-like DecoratedTree-like set

len k is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

dom k is finite countable V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of bool NAT

A is Relation-like Function-like DecoratedTree-like set

proj1 A is non empty Tree-like set

C is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

C + 1 is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

k . (C + 1) is set

<*C*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element countable FinSequence-like FinSubsequence-like FinSequence of NAT

B is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of proj1 A

<*C*> ^ B is Relation-like NAT -defined NAT -valued Function-like non empty finite countable FinSequence-like FinSubsequence-like FinSequence of NAT

proj1 (X -tree k) is non empty Tree-like set

C is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like DTree-yielding set

doms C is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Tree-yielding set

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

dom (doms C) is finite countable V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of bool NAT

n is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set

len n is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

dom n is finite countable V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of bool NAT

Seg (len k) is finite len k -element countable V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of bool NAT

q is set

qq is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

n . qq is set

k . qq is set

IFEQ (qq,(m + 1),X,(k . qq)) is set

n . q is set

q is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like DTree-yielding set

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

proj1 (X -tree q) is non empty Tree-like set

qq is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like DTree-yielding set

doms qq is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Tree-yielding set

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

len (doms C) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

len (doms qq) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

dqq is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

q . dqq is set

k . dqq is set

IFEQ (dqq,(m + 1),X,(k . dqq)) is set

(doms C) . dqq is set

i is Relation-like Function-like DecoratedTree-like set

proj1 i is non empty Tree-like set

(doms qq) . dqq is set

len q is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

q . (m + 1) is set

<*m*> . 1 is set

k . (m + 1) is set

IFEQ ((m + 1),(m + 1),X,(k . (m + 1))) is set

(doms qq) . (m + 1) is set

proj1 X is non empty finite countable Tree-like set

(proj1 n) with-replacement (<*m*>,(proj1 X)) is non empty Tree-like set

f is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT

(X -tree q) . f is set

n . f is set

i is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of proj1 n

dqq is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Tree-yielding set

len dqq is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

doms q is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Tree-yielding set

len (doms q) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

r is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

r is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set

r + 1 is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

dqq . (r + 1) is set

<*r*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element countable FinSequence-like FinSubsequence-like FinSequence of NAT

<*r*> ^ r is Relation-like NAT -defined Function-like non empty finite countable FinSequence-like FinSubsequence-like set

r is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

r is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set

r + 1 is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

(doms q) . (r + 1) is set

<*r*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element countable FinSequence-like FinSubsequence-like FinSequence of NAT

<*r*> ^ r is Relation-like NAT -defined Function-like non empty finite countable FinSequence-like FinSubsequence-like set

(X -tree q) | <*r*> is Relation-like Function-like DecoratedTree-like set

q . (r + 1) is set

k . (r + 1) is set

IFEQ ((r + 1),(m + 1),X,(k . (r + 1))) is set

doms k is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Tree-yielding set

dom (doms k) is finite countable V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of bool NAT

(proj1 (X -tree k)) | <*r*> is non empty Tree-like set

(doms k) . (r + 1) is set

pw1 is Relation-like Function-like DecoratedTree-like set

proj1 pw1 is non empty Tree-like set

c

doms c

tree (doms c

dom (doms q) is finite countable V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of bool NAT

(proj1 (X -tree q)) | <*r*> is non empty Tree-like set

ww is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT

(X -tree q) | ww is Relation-like Function-like DecoratedTree-like set

c

((X -tree q) | ww) . c

(X -tree k) | ww is Relation-like Function-like DecoratedTree-like set

((X -tree k) | ww) . c

dqq is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Tree-yielding set

len dqq is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

i is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of proj1 n

r is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of proj1 X

i ^ r is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT

r is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of proj1 X

<*m*> ^ r is Relation-like NAT -defined NAT -valued Function-like non empty finite countable FinSequence-like FinSubsequence-like FinSequence of NAT

(X -tree q) | <*m*> is Relation-like Function-like DecoratedTree-like set

r is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT

<*m*> ^ r is Relation-like NAT -defined NAT -valued Function-like non empty finite countable FinSequence-like FinSubsequence-like FinSequence of NAT

X . r is set

(proj1 (X -tree q)) | <*m*> is non empty Tree-like set

i is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of proj1 n

i is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

q . i is set

k . i is set

IFEQ (i,(m + 1),X,(k . i)) is set

n is non empty finite countable Tree-like set

card n is V6() V7() V8() V12() non empty ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V77() V78() V79() V80() V81() Element of NAT

X is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n

n | X is non empty finite countable Tree-like set

card (n | X) is V6() V7() V8() V12() non empty ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V77() V78() V79() V80() V81() Element of NAT

X is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of NAT *

{ (X ^ b

k is Relation-like Function-like set

proj1 k is set

proj2 k is set

C is set

k . C is set

A is set

k . A is set

B is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n | X

X ^ B is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT

C is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n | X

k . C is set

X ^ C is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT

C is set

A is set

k . A is set

B is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of NAT *

k . B is set

X ^ B is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT

C is set

A is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of NAT *

X ^ A is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT

B is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n | X

k . B is set

k is finite countable set

card k is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

C is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of NAT *

X ^ C is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT

C is set

A is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of NAT *

X ^ A is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT

n is non empty finite countable Tree-like set

card n is V6() V7() V8() V12() non empty ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V77() V78() V79() V80() V81() Element of NAT

X is non empty finite countable Tree-like set

card X is V6() V7() V8() V12() non empty ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V77() V78() V79() V80() V81() Element of NAT

(card n) + (card X) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

X is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n

n with-replacement (X,X) is non empty finite countable Tree-like set

card (n with-replacement (X,X)) is V6() V7() V8() V12() non empty ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V77() V78() V79() V80() V81() Element of NAT

n | X is non empty finite countable Tree-like set

card (n | X) is V6() V7() V8() V12() non empty ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V77() V78() V79() V80() V81() Element of NAT

(card (n with-replacement (X,X))) + (card (n | X)) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

{ b

{ b

{ (X ^ b

bool n is non empty finite V44() countable set

A is Relation-like Function-like set

proj1 A is set

proj2 A is set

B is set

A . B is set

C is set

A . C is set

t is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of X

X ^ t is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT

n is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of X

A . n is set

X ^ n is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT

B is set

C is set

A . C is set

t is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of NAT *

A . t is set

X ^ t is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT

B is set

C is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of X

X ^ C is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT

A . C is set

C is set

t is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n

A is finite countable set

B is finite countable set

A \/ B is finite countable set

A /\ { (X ^ b

C is set

t is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n

n is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of X

X ^ n is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT

A /\ B is finite countable set

C is set

t is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n

n is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n

A \/ { (X ^ b

C is finite countable set

card C is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

card B is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

card A is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

(card A) + (card C) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

((card A) + (card C)) + (card B) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

(card A) + (card B) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

((card A) + (card B)) + (card C) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

n is Relation-like Function-like finite countable DecoratedTree-like set

proj1 n is non empty finite countable Tree-like set

X is Relation-like Function-like finite countable DecoratedTree-like set

card n is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

card X is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

(card n) + (card X) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

X is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of proj1 n

n with-replacement (X,X) is Relation-like Function-like finite countable DecoratedTree-like set

card (n with-replacement (X,X)) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

n | X is Relation-like Function-like finite countable DecoratedTree-like set

card (n | X) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

(card (n with-replacement (X,X))) + (card (n | X)) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

card (proj1 n) is V6() V7() V8() V12() non empty ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V77() V78() V79() V80() V81() Element of NAT

proj1 X is non empty finite countable Tree-like set

card (proj1 X) is V6() V7() V8() V12() non empty ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V77() V78() V79() V80() V81() Element of NAT

proj1 (n with-replacement (X,X)) is non empty finite countable Tree-like set

card (proj1 (n with-replacement (X,X))) is V6() V7() V8() V12() non empty ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V77() V78() V79() V80() V81() Element of NAT

proj1 (n | X) is non empty finite countable Tree-like set

card (proj1 (n | X)) is V6() V7() V8() V12() non empty ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V77() V78() V79() V80() V81() Element of NAT

(proj1 n) with-replacement (X,(proj1 X)) is non empty finite countable Tree-like set

(proj1 n) | X is non empty finite countable Tree-like set

n is set

root-tree n is Relation-like Function-like DecoratedTree-like set

[{},n] is V22() set

{{},n} is non empty finite countable set

{{{},n},{{}}} is non empty finite V44() countable set

{[{},n]} is Relation-like Function-like constant non empty trivial finite 1 -element countable set

n is set

root-tree n is Relation-like Function-like finite countable DecoratedTree-like set

card (root-tree n) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

[{},n] is V22() set

{{},n} is non empty finite countable set

{{{},n},{{}}} is non empty finite V44() countable set

{[{},n]} is Relation-like Function-like constant non empty trivial finite 1 -element countable set

n is non empty finite countable set

card n is V6() V7() V8() V12() non empty ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V77() V78() V79() V80() V81() Element of NAT

(card n) - 1 is ext-real V39() V53() set

(card n) -' 1 is ext-real non negative V39() V53() set

n is Relation-like Function-like set

proj1 n is set

X is Relation-like Function-like set

proj1 X is set

card n is V6() V7() V8() cardinal set

card (proj1 n) is V6() V7() V8() cardinal set

card X is V6() V7() V8() cardinal set

card (proj1 X) is V6() V7() V8() cardinal set

n is Relation-like Function-like finite countable set

proj1 n is finite countable set

X is Relation-like Function-like finite countable set

proj1 X is finite countable set

n +* X is Relation-like Function-like finite countable set

card (n +* X) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

card n is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

card X is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

(card n) + (card X) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

proj1 (n +* X) is finite countable set

card (proj1 (n +* X)) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

(proj1 n) \/ (proj1 X) is finite countable set

card ((proj1 n) \/ (proj1 X)) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

card (proj1 n) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

card (proj1 X) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

(card (proj1 n)) + (card (proj1 X)) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

(card (proj1 n)) + (card X) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

n is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() set

{ b

X is set

m is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

n + 1 is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

n + {} is ext-real V39() V53() set

X is non empty finite countable V66() V67() V68() V69() V70() V71() V77() V78() V79() V80() V81() Element of bool NAT

max X is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() set

k is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

k + 1 is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

k + {} is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

(max X) + 1 is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT

(max X) + {} is ext-real V39() V53() set