:: CARD_4 semantic presentation

REAL is V43() V44() V45() V49() set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal V43() V44() V45() V46() V47() V48() V49() non finite cardinal limit_cardinal countable denumerable Element of bool REAL
bool REAL is non empty set
COMPLEX is V43() V49() set
omega is non empty non trivial epsilon-transitive epsilon-connected ordinal V43() V44() V45() V46() V47() V48() V49() non finite cardinal limit_cardinal countable denumerable set
bool omega is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V39() V43() V44() V45() V46() V47() V48() V49() finite finite-yielding V54() cardinal {} -element Cardinal-yielding countable FinSequence-like FinSubsequence-like FinSequence-membered set
the Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V39() V43() V44() V45() V46() V47() V48() V49() finite finite-yielding V54() cardinal {} -element Cardinal-yielding countable FinSequence-like FinSubsequence-like FinSequence-membered set is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V39() V43() V44() V45() V46() V47() V48() V49() finite finite-yielding V54() cardinal {} -element Cardinal-yielding countable FinSequence-like FinSubsequence-like FinSequence-membered set
1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
2 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() V49() finite finite-yielding V54() cardinal {} -element Cardinal-yielding countable FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT
card omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set
Seg 1 is non empty trivial V43() V44() V45() V46() V47() V48() finite 1 -element countable Element of bool NAT
D is set
D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() finite cardinal countable set
X is ext-real V39() V40() Element of REAL
X |^ D is ext-real V39() V40() Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() finite cardinal countable set
X |^ k is ext-real V39() V40() Element of REAL
k + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
X |^ (k + 1) is ext-real V39() V40() Element of REAL
(X |^ k) * X is V39() set
X |^ 0 is ext-real V39() V40() Element of REAL
D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() finite cardinal countable set
2 |^ D is ext-real V39() V40() Element of REAL
X is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() finite cardinal countable set
2 * X is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
(2 * X) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
(2 |^ D) * ((2 * X) + 1) is V39() set
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() finite cardinal countable set
2 |^ k is ext-real V39() V40() Element of REAL
N is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() finite cardinal countable set
2 * N is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
(2 * N) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
(2 |^ k) * ((2 * N) + 1) is V39() set
K is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() finite cardinal countable set
k + K is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() finite cardinal countable set
L is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() finite cardinal countable set
L + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
M is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
M + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
2 |^ (M + 1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
(2 |^ k) * (2 |^ (M + 1)) is V39() set
(2 |^ (M + 1)) * ((2 * X) + 1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
(2 |^ k) * ((2 |^ (M + 1)) * ((2 * X) + 1)) is V39() set
2 |^ M is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
2 |^ 1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
(2 |^ M) * (2 |^ 1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
((2 |^ M) * (2 |^ 1)) * ((2 * X) + 1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
2 * (2 |^ M) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
(2 * (2 |^ M)) * ((2 * X) + 1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
(2 |^ M) * ((2 * X) + 1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
2 * ((2 |^ M) * ((2 * X) + 1)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() finite cardinal countable set
2 |^ D is ext-real V39() V40() Element of REAL
X is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() finite cardinal countable set
2 * X is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
(2 * X) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
(2 |^ D) * ((2 * X) + 1) is V39() set
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() finite cardinal countable set
2 |^ k is ext-real V39() V40() Element of REAL
N is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() finite cardinal countable set
2 * N is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
(2 * N) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
(2 |^ k) * ((2 * N) + 1) is V39() set
[:NAT,NAT:] is Relation-like REAL -defined REAL -valued non empty non trivial non finite Element of bool [:REAL,REAL:]
[:REAL,REAL:] is Relation-like set
bool [:REAL,REAL:] is non empty set
D is set
D `1 is set
D `2 is set
X is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
[X,k] is V22() Element of [:NAT,NAT:]
[:NAT,NAT:] is Relation-like non empty non trivial non finite set
{X,k} is non empty V43() V44() V45() V46() V47() V48() finite V54() countable set
{X} is non empty trivial V43() V44() V45() V46() V47() V48() finite V54() 1 -element countable set
{{X,k},{X}} is non empty finite V54() countable set
card NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set
card [:NAT,NAT:] is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set
{0} is functional non empty trivial V43() V44() V45() V46() V47() V48() finite V54() 1 -element with_common_domain countable Element of bool NAT
[:NAT,{0}:] is Relation-like REAL -defined NAT -valued non empty non trivial non finite Element of bool [:REAL,NAT:]
[:REAL,NAT:] is Relation-like set
bool [:REAL,NAT:] is non empty set
card [:NAT,{0}:] is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal 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
D is Relation-like [:NAT,NAT:] -defined NAT -valued Function-like V25([:NAT,NAT:], NAT ) Element of bool [:[:NAT,NAT:],NAT:]
X is set
dom D is Relation-like set
D . X is set
k is set
D . k is set
dom D is Relation-like NAT -defined NAT -valued Element of bool [:NAT,NAT:]
bool [:NAT,NAT:] is non empty non trivial non finite set
N is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
K is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
[N,K] is V22() Element of [:NAT,NAT:]
[:NAT,NAT:] is Relation-like non empty non trivial non finite set
{N,K} is non empty V43() V44() V45() V46() V47() V48() finite V54() countable set
{N} is non empty trivial V43() V44() V45() V46() V47() V48() finite V54() 1 -element countable set
{{N,K},{N}} is non empty finite V54() countable set
L is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
M is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
[L,M] is V22() Element of [:NAT,NAT:]
{L,M} is non empty V43() V44() V45() V46() V47() V48() finite V54() countable set
{L} is non empty trivial V43() V44() V45() V46() V47() V48() finite V54() 1 -element countable set
{{L,M},{L}} is non empty finite V54() countable set
2 |^ N is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
2 * K is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
(2 * K) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
(2 |^ N) * ((2 * K) + 1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
D . (N,K) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
[N,K] is V22() set
D . [N,K] is set
D . (L,M) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
[L,M] is V22() set
D . [L,M] is set
2 |^ L is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
2 * M is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
(2 * M) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
(2 |^ L) * ((2 * M) + 1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
dom D is Relation-like NAT -defined NAT -valued Element of bool [:NAT,NAT:]
bool [:NAT,NAT:] is non empty non trivial non finite set
rng D is V43() V44() V45() V46() V47() V48() countable Element of bool NAT
omega *` omega is epsilon-transitive epsilon-connected ordinal cardinal set
D is set
X is set
[:D,X:] is Relation-like set
card D is epsilon-transitive epsilon-connected ordinal cardinal set
card X is epsilon-transitive epsilon-connected ordinal cardinal set
[:(card D),(card X):] is Relation-like set
[:omega,omega:] is Relation-like non empty non trivial non finite set
card [:(card D),(card X):] is epsilon-transitive epsilon-connected ordinal cardinal set
card [:omega,omega:] is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set
card [:D,X:] is epsilon-transitive epsilon-connected ordinal cardinal set
D is non empty set
1 -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
card (1 -tuples_on D) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
card D is non empty epsilon-transitive epsilon-connected ordinal cardinal set
X is Relation-like Function-like set
dom X is set
rng X is set
k is set
X . k is set
N is set
X . N is set
<*k*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element countable FinSequence-like FinSubsequence-like set
<*N*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element countable FinSequence-like FinSubsequence-like set
<*k*> . 1 is set
k is set
N is set
X . N is set
K is Element of D
<*K*> is Relation-like NAT -defined D -valued Function-like constant non empty trivial finite 1 -element countable FinSequence-like FinSubsequence-like FinSequence of D
{ <*b<sub>1</sub>*> where b<sub>1</sub> is Element of D : verum } is set
k is set
N is Relation-like NAT -defined D -valued Function-like constant non empty trivial finite 1 -element countable FinSequence-like FinSubsequence-like Element of 1 -tuples_on D
K is Element of D
<*K*> is Relation-like NAT -defined D -valued Function-like constant non empty trivial finite 1 -element countable FinSequence-like FinSubsequence-like FinSequence of D
X . K is set
D is non empty set
X is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
X -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
k -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
[:(X -tuples_on D),(k -tuples_on D):] is Relation-like non empty set
X + k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
(X + k) -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
card [:(X -tuples_on D),(k -tuples_on D):] is non empty epsilon-transitive epsilon-connected ordinal cardinal set
card ((X + k) -tuples_on D) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
L is set
L `1 is set
L `2 is set
M is Relation-like NAT -defined D -valued Function-like finite X -element countable FinSequence-like FinSubsequence-like Element of X -tuples_on D
N is Relation-like NAT -defined D -valued Function-like finite k -element countable FinSequence-like FinSubsequence-like Element of k -tuples_on D
M ^ N is Relation-like NAT -defined D -valued Function-like finite X + k -element countable FinSequence-like FinSubsequence-like FinSequence of D
X + k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
K is set
[(L `1),(L `2)] is V22() set
{(L `1),(L `2)} is non empty finite countable set
{(L `1)} is non empty trivial finite 1 -element countable set
{{(L `1),(L `2)},{(L `1)}} is non empty finite V54() countable set
L is Relation-like Function-like set
dom L is set
rng L is set
M is set
L . M is set
N is set
L . N is set
K is Relation-like NAT -defined D -valued Function-like finite X -element countable FinSequence-like FinSubsequence-like Element of X -tuples_on D
M is Relation-like NAT -defined D -valued Function-like finite k -element countable FinSequence-like FinSubsequence-like Element of k -tuples_on D
[K,M] is V22() Element of [:(X -tuples_on D),(k -tuples_on D):]
{K,M} is functional non empty finite V54() countable set
{K} is functional non empty trivial finite V54() 1 -element with_common_domain countable set
{{K,M},{K}} is non empty finite V54() countable set
K ^ M is Relation-like NAT -defined D -valued Function-like finite X + k -element countable FinSequence-like FinSubsequence-like FinSequence of D
X + k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
M is Relation-like NAT -defined D -valued Function-like finite X -element countable FinSequence-like FinSubsequence-like Element of X -tuples_on D
K is Relation-like NAT -defined D -valued Function-like finite k -element countable FinSequence-like FinSubsequence-like Element of k -tuples_on D
[M,K] is V22() Element of [:(X -tuples_on D),(k -tuples_on D):]
{M,K} is functional non empty finite V54() countable set
{M} is functional non empty trivial finite V54() 1 -element with_common_domain countable set
{{M,K},{M}} is non empty finite V54() countable set
M ^ K is Relation-like NAT -defined D -valued Function-like finite X + k -element countable FinSequence-like FinSubsequence-like FinSequence of D
len K is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
len M is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
p is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
K ^ p is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
q is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
M ^ q is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
(len K) + 0 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
len (K ^ p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
len q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
(len (K ^ p)) + (len q) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
len p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
(len K) + (len p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
((len K) + (len p)) + (len q) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
(len p) + (len q) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
(len K) + ((len p) + (len q)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
M is set
N is set
L . N is set
K is Relation-like NAT -defined D -valued Function-like finite X -element countable FinSequence-like FinSubsequence-like Element of X -tuples_on D
M is Relation-like NAT -defined D -valued Function-like finite k -element countable FinSequence-like FinSubsequence-like Element of k -tuples_on D
[K,M] is V22() Element of [:(X -tuples_on D),(k -tuples_on D):]
{K,M} is functional non empty finite V54() countable set
{K} is functional non empty trivial finite V54() 1 -element with_common_domain countable set
{{K,M},{K}} is non empty finite V54() countable set
K ^ M is Relation-like NAT -defined D -valued Function-like finite X + k -element countable FinSequence-like FinSubsequence-like FinSequence of D
X + k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
M is set
N is Relation-like NAT -defined D -valued Function-like finite X + k -element countable FinSequence-like FinSubsequence-like Element of (X + k) -tuples_on D
K is Relation-like NAT -defined D -valued Function-like finite X -element countable FinSequence-like FinSubsequence-like Element of X -tuples_on D
M is Relation-like NAT -defined D -valued Function-like finite k -element countable FinSequence-like FinSubsequence-like Element of k -tuples_on D
K ^ M is Relation-like NAT -defined D -valued Function-like finite X + k -element countable FinSequence-like FinSubsequence-like FinSequence of D
X + k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
[K,M] is V22() Element of [:(X -tuples_on D),(k -tuples_on D):]
{K,M} is functional non empty finite V54() countable set
{K} is functional non empty trivial finite V54() 1 -element with_common_domain countable set
{{K,M},{K}} is non empty finite V54() countable set
L . [K,M] is set
M is Relation-like NAT -defined D -valued Function-like finite X -element countable FinSequence-like FinSubsequence-like Element of X -tuples_on D
K is Relation-like NAT -defined D -valued Function-like finite k -element countable FinSequence-like FinSubsequence-like Element of k -tuples_on D
[M,K] is V22() Element of [:(X -tuples_on D),(k -tuples_on D):]
{M,K} is functional non empty finite V54() countable set
{M} is functional non empty trivial finite V54() 1 -element with_common_domain countable set
{{M,K},{M}} is non empty finite V54() countable set
M ^ K is Relation-like NAT -defined D -valued Function-like finite X + k -element countable FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
X is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
X -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
card D is non empty epsilon-transitive epsilon-connected ordinal cardinal set
1 -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
card (1 -tuples_on D) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() finite cardinal countable set
k -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
k + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
(k + 1) -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
[:(k -tuples_on D),(1 -tuples_on D):] is Relation-like non empty set
card [:(k -tuples_on D),(1 -tuples_on D):] is non empty epsilon-transitive epsilon-connected ordinal cardinal set
card ((k + 1) -tuples_on D) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
[:NAT,D:] is Relation-like non empty non trivial non finite set
bool [:NAT,D:] is non empty non trivial non finite set
<*> D is Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V39() V43() V44() V45() V46() V47() V48() V49() finite finite-yielding V54() cardinal {} -element Cardinal-yielding countable FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
{(<*> D)} is functional non empty trivial V43() V44() V45() V46() V47() V48() finite V54() 1 -element with_common_domain countable Element of bool (bool [:NAT,D:])
bool (bool [:NAT,D:]) is non empty non trivial non finite set
0 -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
D is Relation-like Function-like set
dom D is set
Union D is set
rng D is set
union (rng D) is set
card (dom D) is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
D . X is set
card (D . X) is epsilon-transitive epsilon-connected ordinal cardinal set
card (Union D) is epsilon-transitive epsilon-connected ordinal cardinal set
D is set
union D is set
card D is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
card X is epsilon-transitive epsilon-connected ordinal cardinal set
card (union D) is epsilon-transitive epsilon-connected ordinal cardinal set
D is non empty set
D * is functional non empty FinSequence-membered FinSequenceSet of D
X is set
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
k -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
N is set
X is Relation-like Function-like set
dom X is set
{ (b<sub>1</sub> -tuples_on D) where b<sub>1</sub> is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT : verum } is set
union { (b<sub>1</sub> -tuples_on D) where b<sub>1</sub> is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT : verum } is set
Union X is set
rng X is set
union (rng X) is set
k is set
N is set
K is set
X . K is set
L is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
M is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
M -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
k is set
N is set
K is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
K -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
X . K is set
L is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
L -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
k is set
X . k is set
N is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
N -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
D is non empty set
D * is functional non empty FinSequence-membered FinSequenceSet of D
card (D *) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
len {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() V49() finite finite-yielding V54() cardinal {} -element Cardinal-yielding countable FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT
X is set
k is Relation-like NAT -defined D -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of D *
N is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
len N is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
K is set
X is Relation-like Function-like set
dom X is set
X .: (D *) is set
the Element of D is Element of D
N is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() finite cardinal countable set
N + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
K is set
X . K is set
L is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
len L is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
M is Relation-like NAT -defined D -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of D
<* the Element of D*> is Relation-like NAT -defined D -valued Function-like constant non empty trivial finite 1 -element countable FinSequence-like FinSubsequence-like FinSequence of D
M ^ <* the Element of D*> is Relation-like NAT -defined D -valued Function-like non empty finite countable FinSequence-like FinSubsequence-like FinSequence of D
len (M ^ <* the Element of D*>) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
len <* the Element of D*> is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
N + (len <* the Element of D*>) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
X . (M ^ <* the Element of D*>) is set
N is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
len N is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
X . {} is set
k is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
len k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
k is set
N is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
{ F<sub>1</sub>(b<sub>1</sub>) where b<sub>1</sub> is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT : P<sub>1</sub>[b<sub>1</sub>] } is set
D is Relation-like Function-like set
dom D is set
rng D is set
X is set
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
F<sub>1</sub>(k) is set
D . k is set
{ F<sub>1</sub>(b<sub>1</sub>,b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT : P<sub>1</sub>[b<sub>1</sub>,b<sub>2</sub>] } is set
D is Relation-like Function-like set
dom D is set
rng D is set
X is Relation-like Function-like set
dom X is set
rng X is set
k is set
N is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
K is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
F<sub>1</sub>(N,K) is set
[N,K] is V22() Element of [:NAT,NAT:]
[:NAT,NAT:] is Relation-like non empty non trivial non finite set
{N,K} is non empty V43() V44() V45() V46() V47() V48() finite V54() countable set
{N} is non empty trivial V43() V44() V45() V46() V47() V48() finite V54() 1 -element countable set
{{N,K},{N}} is non empty finite V54() countable set
L is set
D . L is set
[N,K] `1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
[N,K] `2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
X . L is set
{ F<sub>1</sub>(b<sub>1</sub>,b<sub>2</sub>,b<sub>3</sub>) where b<sub>1</sub>, b<sub>2</sub>, b<sub>3</sub> is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT : P<sub>1</sub>[b<sub>1</sub>,b<sub>2</sub>,b<sub>3</sub>] } is set
[:[:NAT,NAT:],NAT:] is Relation-like [:REAL,REAL:] -defined REAL -valued non empty non trivial non finite Element of bool [:[:REAL,REAL:],REAL:]
[:[:REAL,REAL:],REAL:] is Relation-like set
bool [:[:REAL,REAL:],REAL:] is non empty set
[:NAT,NAT,NAT:] is non empty Element of bool [:REAL,REAL,REAL:]
[:REAL,REAL,REAL:] is set
bool [:REAL,REAL,REAL:] is non empty set
D is Relation-like Function-like set
dom D is set
rng D is set
X is Relation-like Function-like set
dom X is set
rng X is set
N is set
K is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
L is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
M is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
F<sub>1</sub>(K,L,M) is set
k is non empty set
N is Element of k
K is Element of k
M is Element of k
[N,K,M] is V22() V23() Element of [:k,k,k:]
[:k,k,k:] is non empty set
[N,K] is V22() set
{N,K} is non empty finite countable set
{N} is non empty trivial finite 1 -element countable set
{{N,K},{N}} is non empty finite V54() countable set
[[N,K],M] is V22() set
{[N,K],M} is non empty finite countable set
{[N,K]} is Relation-like Function-like constant non empty trivial finite 1 -element countable set
{{[N,K],M},{[N,K]}} is non empty finite V54() countable set
[N,K,M] `3_3 is Element of k
[N,K,M] `1_3 is Element of k
[N,K,M] `1 is set
([N,K,M] `1) `1 is set
M is set
D . M is set
[N,K,M] `2_3 is Element of k
([N,K,M] `1) `2 is set
X . M is set
D is epsilon-transitive epsilon-connected ordinal cardinal set
D *` D is epsilon-transitive epsilon-connected ordinal cardinal set
[:D,D:] is Relation-like set
PFuncs ([:D,D:],D) is set
X is set
k is set
N is Relation-like Function-like set
dom N is set
rng N is set
[:(rng N),(rng N):] is Relation-like set
k is set
union k is set
K is set
L is set
M is Relation-like Function-like set
N is set
K is set
L is set
[K,L] is V22() set
{K,L} is non empty finite countable set
{K} is non empty trivial finite 1 -element countable set
{{K,L},{K}} is non empty finite V54() countable set
M is set
[K,M] is V22() set
{K,M} is non empty finite countable set
{{K,M},{K}} is non empty finite V54() countable set
N is set
K is set
M is Relation-like Function-like set
M is Relation-like Function-like set
K is set
p is set
[K,p] is V22() set
{K,p} is non empty finite countable set
{K} is non empty trivial finite 1 -element countable set
{{K,p},{K}} is non empty finite V54() countable set
q is set
[K,q] is V22() set
{K,q} is non empty finite countable set
{{K,q},{K}} is non empty finite V54() countable set
c₁₅ is set
c₁₆ is set
[c₁₅,c₁₆] is V22() set
{c₁₅,c₁₆} is non empty finite countable set
{c₁₅} is non empty trivial finite 1 -element countable set
{{c₁₅,c₁₆},{c₁₅}} is non empty finite V54() countable set
c₁₇ is set
[c₁₅,c₁₇] is V22() set
{c₁₅,c₁₇} is non empty finite countable set
{{c₁₅,c₁₇},{c₁₅}} is non empty finite V54() countable set
N is Relation-like Function-like set
K is set
dom N is set
L is set
N . K is set
N . L is set
[K,(N . K)] is V22() set
{K,(N . K)} is non empty finite countable set
{K} is non empty trivial finite 1 -element countable set
{{K,(N . K)},{K}} is non empty finite V54() countable set
M is set
[L,(N . L)] is V22() set
{L,(N . L)} is non empty finite countable set
{L} is non empty trivial finite 1 -element countable set
{{L,(N . L)},{L}} is non empty finite V54() countable set
N is set
K is Relation-like Function-like set
dom K is set
rng K is set
[:(rng K),(rng K):] is Relation-like set
M is Relation-like Function-like set
dom M is set
rng M is set
[:(rng M),(rng M):] is Relation-like set
M . K is set
M . L is set
K . K is set
K . L is set
dom N is set
rng N is set
[:(rng N),(rng N):] is Relation-like set
K is set
N . K is set
[K,(N . K)] is V22() set
{K,(N . K)} is non empty finite countable set
{K} is non empty trivial finite 1 -element countable set
{{K,(N . K)},{K}} is non empty finite V54() countable set
L is set
M is Relation-like Function-like set
dom M is set
rng M is set
[:(rng M),(rng M):] is Relation-like set
K is set
L is set
[K,L] is V22() set
{K,L} is non empty finite countable set
{K} is non empty trivial finite 1 -element countable set
{{K,L},{K}} is non empty finite V54() countable set
[K,L] `1 is set
M is set
N . M is set
[K,L] `2 is set
N is set
N . N is set
[N,([K,L] `2)] is V22() set
{N,([K,L] `2)} is non empty finite countable set
{N} is non empty trivial finite 1 -element countable set
{{N,([K,L] `2)},{N}} is non empty finite V54() countable set
K is set
M is Relation-like Function-like set
dom M is set
rng M is set
[:(rng M),(rng M):] is Relation-like set
[M,([K,L] `1)] is V22() set
{M,([K,L] `1)} is non empty finite countable set
{M} is non empty trivial finite 1 -element countable set
{{M,([K,L] `1)},{M}} is non empty finite V54() countable set
M is set
K is Relation-like Function-like set
dom K is set
rng K is set
[:(rng K),(rng K):] is Relation-like set
K . M is set
K . N is set
M . M is set
M . N is set
K is set
L is set
N . L is set
[L,K] is V22() set
{L,K} is non empty finite countable set
{L} is non empty trivial finite 1 -element countable set
{{L,K},{L}} is non empty finite V54() countable set
M is set
N is Relation-like Function-like set
dom N is set
rng N is set
N . L is set
K is set
N . K is set
[K,(N . K)] is V22() set
{K,(N . K)} is non empty finite countable set
{K} is non empty trivial finite 1 -element countable set
{{K,(N . K)},{K}} is non empty finite V54() countable set
L is set
M is Relation-like Function-like set
dom M is set
rng M is set
[:omega,omega:] is Relation-like non empty non trivial non finite set
k is Relation-like Function-like set
dom k is set
rng k is set
N is set
K is Relation-like Function-like set
dom K is set
rng K is set
[:(rng K),(rng K):] is Relation-like set
card (rng K) is epsilon-transitive epsilon-connected ordinal cardinal set
card D is epsilon-transitive epsilon-connected ordinal cardinal set
N is Relation-like Function-like set
dom N is set
rng N is set
omega \ (rng K) is V43() V44() V45() V46() V47() V48() countable Element of bool omega
(omega \ (rng K)) /\ (rng K) is V43() V44() V45() V46() V47() V48() countable Element of bool omega
(rng K) /\ (omega \ (rng K)) is V43() V44() V45() V46() V47() V48() countable Element of bool omega
[:((omega \ (rng K)) /\ (rng K)),((rng K) /\ (omega \ (rng K))):] is Relation-like omega -defined omega -valued Element of bool [:omega,omega:]
bool [:omega,omega:] is non empty non trivial non finite set
[:(omega \ (rng K)),(rng K):] is Relation-like set
[:(rng K),(omega \ (rng K)):] is Relation-like set
[:(omega \ (rng K)),(rng K):] /\ [:(rng K),(omega \ (rng K)):] is Relation-like set
(omega \ (rng K)) /\ (omega \ (rng K)) is V43() V44() V45() V46() V47() V48() countable Element of bool omega
[:((omega \ (rng K)) /\ (omega \ (rng K))),((omega \ (rng K)) /\ (rng K)):] is Relation-like omega -defined omega -valued Element of bool [:omega,omega:]
[:(omega \ (rng K)),(omega \ (rng K)):] is Relation-like omega -defined omega -valued Element of bool [:omega,omega:]
[:(omega \ (rng K)),(omega \ (rng K)):] /\ [:(omega \ (rng K)),(rng K):] is Relation-like omega -defined omega -valued Element of bool [:omega,omega:]
(rng K) /\ (rng K) is set
[:((rng K) /\ (rng K)),((omega \ (rng K)) /\ (rng K)):] is Relation-like set
[:(rng K),(omega \ (rng K)):] /\ [:(rng K),(rng K):] is Relation-like set
[:((omega \ (rng K)) /\ (rng K)),((rng K) /\ (rng K)):] is Relation-like set
{} \/ {} is Relation-like NAT -defined V43() V44() V45() V46() V47() V48() finite V54() countable set
[:(omega \ (rng K)),(rng K):] /\ [:(rng K),(rng K):] is Relation-like set
[:((omega \ (rng K)) /\ (rng K)),((omega \ (rng K)) /\ (rng K)):] is Relation-like omega -defined omega -valued Element of bool [:omega,omega:]
[:(omega \ (rng K)),(omega \ (rng K)):] /\ [:(rng K),(rng K):] is Relation-like omega -defined omega -valued Element of bool [:omega,omega:]
[:(omega \ (rng K)),(omega \ (rng K)):] \/ [:(omega \ (rng K)),(rng K):] is Relation-like set
([:(omega \ (rng K)),(omega \ (rng K)):] \/ [:(omega \ (rng K)),(rng K):]) /\ [:(rng K),(rng K):] is Relation-like set
omega +` (card (rng K)) is epsilon-transitive epsilon-connected ordinal cardinal set
omega +` omega is epsilon-transitive epsilon-connected ordinal cardinal set
card (card (rng K)) is epsilon-transitive epsilon-connected ordinal cardinal set
omega *` (card (rng K)) is epsilon-transitive epsilon-connected ordinal cardinal set
omega +` (omega *` (card (rng K))) is epsilon-transitive epsilon-connected ordinal cardinal set
card (omega \ (rng K)) is epsilon-transitive epsilon-connected ordinal cardinal set
[:((omega \ (rng K)) /\ (rng K)),((omega \ (rng K)) /\ (omega \ (rng K))):] is Relation-like omega -defined omega -valued Element of bool [:omega,omega:]
[:(omega \ (rng K)),(omega \ (rng K)):] /\ [:(rng K),(omega \ (rng K)):] is Relation-like omega -defined omega -valued Element of bool [:omega,omega:]
([:(omega \ (rng K)),(omega \ (rng K)):] \/ [:(omega \ (rng K)),(rng K):]) /\ [:(rng K),(omega \ (rng K)):] is Relation-like set
([:(omega \ (rng K)),(omega \ (rng K)):] \/ [:(omega \ (rng K)),(rng K):]) \/ [:(rng K),(omega \ (rng K)):] is Relation-like set
card (([:(omega \ (rng K)),(omega \ (rng K)):] \/ [:(omega \ (rng K)),(rng K):]) \/ [:(rng K),(omega \ (rng K)):]) is epsilon-transitive epsilon-connected ordinal cardinal set
card ([:(omega \ (rng K)),(omega \ (rng K)):] \/ [:(omega \ (rng K)),(rng K):]) is epsilon-transitive epsilon-connected ordinal cardinal set
card [:(rng K),(omega \ (rng K)):] is epsilon-transitive epsilon-connected ordinal cardinal set
(card ([:(omega \ (rng K)),(omega \ (rng K)):] \/ [:(omega \ (rng K)),(rng K):])) +` (card [:(rng K),(omega \ (rng K)):]) is epsilon-transitive epsilon-connected ordinal cardinal set
card [:(omega \ (rng K)),(omega \ (rng K)):] is epsilon-transitive epsilon-connected ordinal cardinal set
card [:(omega \ (rng K)),(rng K):] is epsilon-transitive epsilon-connected ordinal cardinal set
(card [:(omega \ (rng K)),(omega \ (rng K)):]) +` (card [:(omega \ (rng K)),(rng K):]) is epsilon-transitive epsilon-connected ordinal cardinal set
((card [:(omega \ (rng K)),(omega \ (rng K)):]) +` (card [:(omega \ (rng K)),(rng K):])) +` (card [:(rng K),(omega \ (rng K)):]) is epsilon-transitive epsilon-connected ordinal cardinal set
[:omega,(card (rng K)):] is Relation-like set
card [:omega,(card (rng K)):] is epsilon-transitive epsilon-connected ordinal cardinal set
(card [:(omega \ (rng K)),(omega \ (rng K)):]) +` (card [:omega,(card (rng K)):]) is epsilon-transitive epsilon-connected ordinal cardinal set
((card [:(omega \ (rng K)),(omega \ (rng K)):]) +` (card [:omega,(card (rng K)):])) +` (card [:(rng K),(omega \ (rng K)):]) is epsilon-transitive epsilon-connected ordinal cardinal set
card [:omega,omega:] is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set
(card [:omega,omega:]) +` (card [:omega,(card (rng K)):]) is epsilon-transitive epsilon-connected ordinal cardinal set
((card [:omega,omega:]) +` (card [:omega,(card (rng K)):])) +` (card [:(rng K),(omega \ (rng K)):]) is epsilon-transitive epsilon-connected ordinal cardinal set
omega +` (card [:omega,(card (rng K)):]) is epsilon-transitive epsilon-connected ordinal cardinal set
[:(card (rng K)),omega:] is Relation-like set
card [:(card (rng K)),omega:] is epsilon-transitive epsilon-connected ordinal cardinal set
(omega +` (card [:omega,(card (rng K)):])) +` (card [:(card (rng K)),omega:]) is epsilon-transitive epsilon-connected ordinal cardinal set
(omega +` (omega *` (card (rng K)))) +` (card [:(card (rng K)),omega:]) is epsilon-transitive epsilon-connected ordinal cardinal set
(card (rng K)) *` omega is epsilon-transitive epsilon-connected ordinal cardinal set
(omega +` (omega *` (card (rng K)))) +` ((card (rng K)) *` omega) is epsilon-transitive epsilon-connected ordinal cardinal set
N is Relation-like Function-like set
dom N is set
rng N is set
N +* K is Relation-like Function-like set
dom (N +* K) is set
(dom N) \/ (dom K) is set
(omega \ (rng K)) \/ (rng K) is set
[:(omega \ (rng K)),((omega \ (rng K)) \/ (rng K)):] is Relation-like set
[:(omega \ (rng K)),((omega \ (rng K)) \/ (rng K)):] \/ [:(rng K),(omega \ (rng K)):] is Relation-like set
([:(omega \ (rng K)),((omega \ (rng K)) \/ (rng K)):] \/ [:(rng K),(omega \ (rng K)):]) \/ [:(rng K),(rng K):] is Relation-like set
[:(rng K),(omega \ (rng K)):] \/ [:(rng K),(rng K):] is Relation-like set
[:(omega \ (rng K)),((omega \ (rng K)) \/ (rng K)):] \/ ([:(rng K),(omega \ (rng K)):] \/ [:(rng K),(rng K):]) is Relation-like set
[:(rng K),((omega \ (rng K)) \/ (rng K)):] is Relation-like set
[:(omega \ (rng K)),((omega \ (rng K)) \/ (rng K)):] \/ [:(rng K),((omega \ (rng K)) \/ (rng K)):] is Relation-like set
[:((omega \ (rng K)) \/ (rng K)),((omega \ (rng K)) \/ (rng K)):] is Relation-like set
omega \/ (rng K) is non empty set
[:(omega \/ (rng K)),((omega \ (rng K)) \/ (rng K)):] is Relation-like set
[:(omega \/ (rng K)),(omega \/ (rng K)):] is Relation-like non empty set
(dom N) /\ (dom K) is set
rng (N +* K) is set
(rng N) \/ (rng K) is set
(rng K) /\ (rng N) is set
K is set
(N +* K) . K is set
M is set
(N +* K) . M is set
K . K is set
K . M is set
N . K is set
N . M is set
the epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() finite cardinal countable Element of omega \ (rng K) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() finite cardinal countable Element of omega \ (rng K)
M is Relation-like Function-like set
dom M is set
rng M is set
(card (rng K)) *` (card (rng K)) is epsilon-transitive epsilon-connected ordinal cardinal set
[:(card (rng K)),(card (rng K)):] is Relation-like set
card [:(card (rng K)),(card (rng K)):] is epsilon-transitive epsilon-connected ordinal cardinal set
card [:(rng K),(rng K):] is epsilon-transitive epsilon-connected ordinal cardinal set
D +` (card (rng K)) is epsilon-transitive epsilon-connected ordinal cardinal set
D \ (rng K) is Element of bool D
bool D is non empty set
card (D \ (rng K)) is epsilon-transitive epsilon-connected ordinal cardinal set
N is Relation-like Function-like set
dom N is set
rng N is set
card (rng N) is epsilon-transitive epsilon-connected ordinal cardinal set
(rng K) /\ (rng N) is set
(rng K) /\ (D \ (rng K)) is Element of bool D
(rng K) \/ (rng N) is set
((rng K) \/ (rng N)) \ (rng K) is Element of bool ((rng K) \/ (rng N))
bool ((rng K) \/ (rng N)) is non empty set
(rng N) \ (rng K) is Element of bool (rng N)
bool (rng N) is non empty set
[:(rng N),(rng N):] is Relation-like set
[:(((rng K) \/ (rng N)) \ (rng K)),((rng K) \/ (rng N)):] is Relation-like set
[:((rng K) \/ (rng N)),(((rng K) \/ (rng N)) \ (rng K)):] is Relation-like set
[:(((rng K) \/ (rng N)) \ (rng K)),((rng K) \/ (rng N)):] \/ [:((rng K) \/ (rng N)),(((rng K) \/ (rng N)) \ (rng K)):] is Relation-like set
[:((rng K) \/ (rng N)),((rng K) \/ (rng N)):] is Relation-like set
[:((rng K) \/ (rng N)),((rng K) \/ (rng N)):] \ [:(rng K),(rng K):] is Relation-like (rng K) \/ (rng N) -defined (rng K) \/ (rng N) -valued Element of bool [:((rng K) \/ (rng N)),((rng K) \/ (rng N)):]
bool [:((rng K) \/ (rng N)),((rng K) \/ (rng N)):] is non empty set
(card (rng K)) +` (card (rng K)) is epsilon-transitive epsilon-connected ordinal cardinal set
card ((rng K) \/ (rng N)) is epsilon-transitive epsilon-connected ordinal cardinal set
card [:((rng K) \/ (rng N)),((rng K) \/ (rng N)):] is epsilon-transitive epsilon-connected ordinal cardinal set
card ([:((rng K) \/ (rng N)),((rng K) \/ (rng N)):] \ [:(rng K),(rng K):]) is epsilon-transitive epsilon-connected ordinal cardinal set
card [:(rng N),(rng N):] is epsilon-transitive epsilon-connected ordinal cardinal set
M is Relation-like Function-like set
dom M is set
rng M is set
M +* K is Relation-like Function-like set
dom (M +* K) is set
(dom M) \/ (dom K) is set
[:((rng K) \/ (rng N)),((rng K) \/ (rng N)):] \/ [:(rng K),(rng K):] is Relation-like set
M is set
(M +* K) . M is set
K is set
(M +* K) . K is set
K . M is set
K . K is set
M . M is set
M . K is set
(rng K) /\ (rng M) is set
the Element of rng N is Element of rng N
rng (M +* K) is set
(rng M) \/ (rng K) is set
K is Relation-like Function-like set
dom K is set
rng K is set
D is epsilon-transitive epsilon-connected ordinal cardinal set
X is epsilon-transitive epsilon-connected ordinal cardinal set
D *` X is epsilon-transitive epsilon-connected ordinal cardinal set
X *` D is epsilon-transitive epsilon-connected ordinal cardinal set
1 *` D is epsilon-transitive epsilon-connected ordinal cardinal set
D *` D is epsilon-transitive epsilon-connected ordinal cardinal set
D is epsilon-transitive epsilon-connected ordinal cardinal set
X is epsilon-transitive epsilon-connected ordinal cardinal set
D *` X is epsilon-transitive epsilon-connected ordinal cardinal set
X *` D is epsilon-transitive epsilon-connected ordinal cardinal set
D *` 0 is epsilon-transitive epsilon-connected ordinal cardinal set
D is set
[:D,D:] is Relation-like set
card [:D,D:] is epsilon-transitive epsilon-connected ordinal cardinal set
card D is epsilon-transitive epsilon-connected ordinal cardinal set
(card D) *` (card D) is epsilon-transitive epsilon-connected ordinal cardinal set
[:(card D),(card D):] is Relation-like set
card [:(card D),(card D):] is epsilon-transitive epsilon-connected ordinal cardinal set
D is set
card D is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
[:D,X:] is Relation-like set
card [:D,X:] is epsilon-transitive epsilon-connected ordinal cardinal set
card X is epsilon-transitive epsilon-connected ordinal cardinal set
(card D) *` (card X) is epsilon-transitive epsilon-connected ordinal cardinal set
[:(card D),(card X):] is Relation-like set
card [:(card D),(card X):] is epsilon-transitive epsilon-connected ordinal cardinal set
D is epsilon-transitive epsilon-connected ordinal cardinal set
X is epsilon-transitive epsilon-connected ordinal cardinal set
k is epsilon-transitive epsilon-connected ordinal cardinal set
D *` k is epsilon-transitive epsilon-connected ordinal cardinal set
k *` D is epsilon-transitive epsilon-connected ordinal cardinal set
N is epsilon-transitive epsilon-connected ordinal cardinal set
X *` N is epsilon-transitive epsilon-connected ordinal cardinal set
K is epsilon-transitive epsilon-connected ordinal cardinal set
L is epsilon-transitive epsilon-connected ordinal cardinal set
M is epsilon-transitive epsilon-connected ordinal cardinal set
K *` M is epsilon-transitive epsilon-connected ordinal cardinal set
N is epsilon-transitive epsilon-connected ordinal cardinal set
L *` N is epsilon-transitive epsilon-connected ordinal cardinal set
K is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() finite cardinal countable set
card K is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of omega
M is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() finite cardinal countable set
card M is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of omega
K is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() finite cardinal countable set
card K is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of omega
(card K) * (card M) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
(card K) * (card K) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
M is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() finite cardinal countable set
card M is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of omega
M *` K is epsilon-transitive epsilon-connected ordinal cardinal set
(card M) * (card K) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
card ((card M) * (card K)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of omega
K *` M is epsilon-transitive epsilon-connected ordinal cardinal set
card ((card K) * (card M)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of omega
K is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() finite cardinal countable set
card K is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of omega
M is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() finite cardinal countable set
card M is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of omega
K *` M is epsilon-transitive epsilon-connected ordinal cardinal set
(card K) * (card M) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
card ((card K) * (card M)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of omega
D is set
card D is epsilon-transitive epsilon-connected ordinal cardinal set
omega *` (card D) is epsilon-transitive epsilon-connected ordinal cardinal set
D is set
card D is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
card X is epsilon-transitive epsilon-connected ordinal cardinal set
(card X) *` (card D) is epsilon-transitive epsilon-connected ordinal cardinal set
D is non empty set
card D is non empty epsilon-transitive epsilon-connected ordinal cardinal set
X is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
X -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
card (X -tuples_on D) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() finite cardinal countable set
k -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
card (k -tuples_on D) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
k + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
(k + 1) -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
card ((k + 1) -tuples_on D) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
0 -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
[:NAT,D:] is Relation-like non empty non trivial non finite set
bool [:NAT,D:] is non empty non trivial non finite set
<*> D is Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V39() V43() V44() V45() V46() V47() V48() V49() finite finite-yielding V54() cardinal {} -element Cardinal-yielding countable FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
{(<*> D)} is functional non empty trivial V43() V44() V45() V46() V47() V48() finite V54() 1 -element with_common_domain countable Element of bool (bool [:NAT,D:])
bool (bool [:NAT,D:]) is non empty non trivial non finite set
card (0 -tuples_on D) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
1 -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
[:(k -tuples_on D),(1 -tuples_on D):] is Relation-like non empty set
card [:(k -tuples_on D),(1 -tuples_on D):] is non empty epsilon-transitive epsilon-connected ordinal cardinal set
card (1 -tuples_on D) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
[:(card (k -tuples_on D)),(card (1 -tuples_on D)):] is Relation-like non empty set
card [:(card (k -tuples_on D)),(card (1 -tuples_on D)):] is non empty epsilon-transitive epsilon-connected ordinal cardinal set
[:(card (k -tuples_on D)),(card D):] is Relation-like non empty set
card [:(card (k -tuples_on D)),(card D):] is non empty epsilon-transitive epsilon-connected ordinal cardinal set
(card (k -tuples_on D)) *` (card D) is epsilon-transitive epsilon-connected ordinal cardinal set
0 -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
card (0 -tuples_on D) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
D is non empty set
card D is non empty epsilon-transitive epsilon-connected ordinal cardinal set
D * is functional non empty FinSequence-membered FinSequenceSet of D
card (D *) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
{ (b<sub>1</sub> -tuples_on D) where b<sub>1</sub> is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT : verum } is set
union { (b<sub>1</sub> -tuples_on D) where b<sub>1</sub> is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT : verum } is set
X is set
card X is epsilon-transitive epsilon-connected ordinal cardinal set
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT
k -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
0 -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
[:NAT,D:] is Relation-like non empty non trivial non finite set
bool [:NAT,D:] is non empty non trivial non finite set
<*> D is Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V39() V43() V44() V45() V46() V47() V48() V49() finite finite-yielding V54() cardinal {} -element Cardinal-yielding countable FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
{(<*> D)} is functional non empty trivial V43() V44() V45() V46() V47() V48() finite V54() 1 -element with_common_domain countable Element of bool (bool [:NAT,D:])
bool (bool [:NAT,D:]) is non empty non trivial non finite set
card (0 -tuples_on D) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
1 -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
card (1 -tuples_on D) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
{ H<sub>1</sub>(b<sub>1</sub>) where b<sub>1</sub> is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT : S<sub>1</sub>[b<sub>1</sub>] } is set
card { (b<sub>1</sub> -tuples_on D) where b<sub>1</sub> is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT : verum } is epsilon-transitive epsilon-connected ordinal cardinal set
card (union { (b<sub>1</sub> -tuples_on D) where b<sub>1</sub> is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V39() V40() V41() V43() V44() V45() V46() V47() V48() finite cardinal countable Element of NAT : verum } ) is epsilon-transitive epsilon-connected ordinal cardinal set
omega *` (card D) is epsilon-transitive epsilon-connected ordinal cardinal set