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

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

union { (b

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

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

D . k is set

{ F

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

[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

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

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

c

[c

{c

{c

{{c

c

[c

{c

{{c

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