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

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

bool [:1,1:] is non empty finite V44() 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

bool is non empty set

bool 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

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set
is Relation-like non empty non trivial non finite set
is Relation-like non empty non trivial non finite set
bool 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

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

F1() is non empty finite countable set
{ F2(b1) where b1 is Element of F1() : P1[b1] } is set
{ F2(b1) where b1 is Element of F1() : b1 in F1() } is set
X is set
X is Element of F1()
F2(X) is 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

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

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

F1() is set
n is set
F2(n) is set
F3(n) is set

X is Element of F1()
n . X is set
F2(X) is set
F3(X) is set
n is set

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

bool is non empty set

m is set
X . m is set
n is set
bool n is non empty set
X is Element of bool n

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

n is set
bool n is non empty set
X is Element of bool n

X is set

proj2 (n | X) is set
proj2 n is set
n is non empty set

proj2 X is non empty set
union () 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

bool [:n,:] is non empty set

Funcs ({},{}) is set
proj1 (uncurry ()) is set
proj1 () is set
[:(proj1 ()),{}:] is Relation-like set
n is non empty set
X is set

{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

proj1 () 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

(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

bool [:n,:] is non empty set

proj2 m is non empty set
proj2 X is non empty set
union () is set
Funcs (X,(union ())) is set
k is set
C is 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

proj2 A is set
proj1 A is set
Funcs (n,(Funcs (X,(union ())))) is set
Funcs (n,(union ())) is set
Funcs (X,(Funcs (n,(union ())))) is set
[:X,(Funcs (n,(union ()))):] is Relation-like set
bool [:X,(Funcs (n,(union ()))):] is non empty set
F1() is non empty set
[:NAT,F1():] is Relation-like non empty non trivial non finite set
bool [:NAT,F1():] is non empty non trivial non finite set
F2() is Element of F1()

n . {} is Element of F1()

X . {} is Element of F1()
F1() is non empty set
bool F1() is non empty set
F2() is Element of bool F1()
F3() is Relation-like F2() -defined Function-like total set
F4() is Relation-like F2() -defined Function-like total set

X is set
proj1 n is set
n . X is set
F5(X) is set

X is set

F3() . X is set
F4() . X is set
[:(F3() . X),(F4() . X):] is Relation-like set
bool [:(F3() . X),(F4() . X):] is non empty set
F5(X) is set
X is Relation-like F2() -defined Function-like total Function-yielding V89() ManySortedFunction of F3(),F4()
m is Element of F1()

F5(m) is set
n is set

proj1 X is set

proj1 X is 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

proj1 C is set
proj1 (m +* X) is set
proj1 m is set
() \/ () is set
n is non empty set
X is non empty set

{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

k is Element of X

proj1 m is non empty set

proj1 () 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

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

(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' ()) . k is set
proj2 () is set

proj1 A is set
proj2 A is set

A is set
C . A is set
X . A is set

(n --> X) . A is set

[:X,(X . A):] is Relation-like set
bool [:X,(X . A):] is non empty set
proj1 B is set
() . (A,k) is set
B . k is 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

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

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

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

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

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

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

m . k is set
(n |-> {X}) . k is set
proj1 m is set
n is non empty set

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

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

proj1 m is set
proj2 m is set
k is set
m . k is set
C is set
m . C is set

m . B is set

k is set
C is set
m . C is set

m . A is set

k is set

m . A is set

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

() with-replacement (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

n with-replacement (X,X) is non empty finite countable Tree-like set
{ } is set
{ } is set
{ } \/ { } is set
{ } is set
{ H1(b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of X : S2[b1] } is set
{ H1(b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of X : S1[b1] } is set
B is set

{ } \/ {X} is non empty set

( { } \/ {X}) \/ { H1(b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of X : S1[b1] } is non empty set
{X} \/ { H1(b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of X : S1[b1] } is non empty set
{ } \/ ({X} \/ { H1(b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of X : S1[b1] } ) is non empty set
{ } \/ { H1(b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of X : S1[b1] } is set
n is non empty finite countable Tree-like set
X is non empty finite countable Tree-like set

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

{ } is set

{ } is set
{ } \/ { } is 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

(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

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

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

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

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

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

m is non empty Tree-like set
(tree n) with-replacement (<*X*>,m) is non empty Tree-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

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

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

n . (A + 1) is set
C . 1 is 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

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

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

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

n . (X + 1) is 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 + 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

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

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

proj1 (X -tree k) is non empty Tree-like 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

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

proj1 (X -tree q) is non empty Tree-like 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

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

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

(X -tree q) . f is set
n . f is 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

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

q . (r + 1) is set
k . (r + 1) is set
IFEQ ((r + 1),(m + 1),X,(k . (r + 1))) is 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

proj1 pw1 is non empty Tree-like set

tree (doms c22) is non empty Tree-like set
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

((X -tree q) | ww) . c19 is set

((X -tree k) | ww) . c19 is 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

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

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

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

{ } is set

proj1 k is set
proj2 k is set
C is set
k . C is set
A is set
k . A is set

k . C is set

C is set
A is set
k . A is set

k . B is set

C is set

k . B is 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 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 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

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
{ } is set
{ } is set
{ } is set
bool n is non empty finite V44() countable set

proj1 A is set
proj2 A is set
B is set
A . B is set
C is set
A . C is set

A . n is set

B is set
C is set
A . C is set

A . t is set

B is set

A . C is set
C is set

A /\ { } is finite countable set
C is set

C is set

A \/ { } is 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

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

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

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 () 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 () 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
() with-replacement (X,()) is non empty finite countable Tree-like set
() | X is non empty finite countable Tree-like set
n is set

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

n is set

card () 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 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

proj1 n is set

proj1 X is set
card n is V6() V7() V8() cardinal set
card () is V6() V7() V8() cardinal set
card X is V6() V7() V8() cardinal set
card () is V6() V7() V8() cardinal 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
() \/ () is finite countable set
card (() \/ ()) 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 () 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 () 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 ()) + (card ()) 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 ()) + (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
{ b1 where b1 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 : not b1 <= n } is 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
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