:: CARD_4 semantic presentation

REAL is V43() V44() V45() V49() set

bool REAL is non empty set
COMPLEX is V43() V49() set

bool omega is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set

Seg 1 is non empty trivial V43() V44() V45() V46() V47() V48() finite 1 -element countable Element of bool NAT
D is set

X is ext-real V39() V40() Element of REAL
X |^ D is ext-real V39() V40() Element of REAL

X |^ k is ext-real V39() V40() Element of REAL

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

2 |^ D is ext-real V39() V40() Element of REAL

(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

2 |^ k is ext-real V39() V40() Element of REAL

(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

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

2 |^ D is ext-real V39() V40() Element of REAL

(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

2 |^ k is ext-real V39() V40() Element of REAL

(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

bool is non empty set
D is set
D `1 is set
D `2 is set

[X,k] is V22() Element of
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

bool is non empty set

is Relation-like non empty non trivial non finite set
bool is non empty non trivial non finite set

X is set

D . X is set
k is set
D . k is set

bool is non empty non trivial non finite set

[N,K] is V22() Element of
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,M] is V22() Element of
{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 * 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 * 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

bool is non empty non trivial non finite set
rng D is V43() V44() V45() V46() V47() V48() countable Element of bool NAT

D is set
X is set
[:D,X:] is Relation-like set

[:(card D),(card X):] is Relation-like set
is Relation-like non empty non trivial non finite set

D is non empty set

dom X is set
rng X is set
k is set
X . k is set
N is set
X . N is set

<*k*> . 1 is set
k is set
N is set
X . N is set
K is Element of D

{ <*b1*> where b1 is Element of D : verum } is set
k is set

K is Element of D

X . K is set
D is non empty set

[:(),():] is Relation-like non empty set

(X + k) -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D

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

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

dom L is set
rng L is set
M is set
L . M is set
N is set
L . N is set

[K,M] is V22() Element of [:(),():]
{K,M} is functional non empty finite V54() countable set

{{K,M},{K}} is non empty finite V54() countable set

[M,K] is V22() Element of [:(),():]
{M,K} is functional non empty finite V54() countable set

{{M,K},{M}} is non empty finite V54() countable set

(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 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,M] is V22() Element of [:(),():]
{K,M} is functional non empty finite V54() countable set

{{K,M},{K}} is non empty finite V54() countable set

M is set

[K,M] is V22() Element of [:(),():]
{K,M} is functional non empty finite V54() countable set

{{K,M},{K}} is non empty finite V54() countable set
L . [K,M] is set

[M,K] is V22() Element of [:(),():]
{M,K} is functional non empty finite V54() countable set

{{M,K},{M}} is non empty finite V54() countable set

D is non empty set

(k + 1) -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
[:(),():] is Relation-like non empty 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 functional non empty trivial V43() V44() V45() V46() V47() V48() finite V54() 1 -element with_common_domain countable Element of bool ()
bool () is non empty non trivial non finite set

dom D is set
Union D is set
rng D is set
union (rng D) is set

X is set
D . X is set

D is set
union D is set

X is set

D is non empty set

X is set

N is set

dom X is set
{ (b1 -tuples_on D) where b1 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 { (b1 -tuples_on D) where b1 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

k is set
N is set

X . K is set

k is set
X . k is set

D is non empty set

X is set

K is set

dom X is set
X .: (D *) is set
the Element of D is Element of D

K is set
X . K is set

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

X . {} is set

k is set

{ F1(b1) where b1 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 : P1[b1] } is set

dom D is set
rng D is set
X is set

F1(k) is set
D . k is set
{ F1(b1,b2) where b1, b2 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 : P1[b1,b2] } is set

dom D is set
rng D is set

dom X is set
rng X is set
k is set

F1(N,K) is set
[N,K] is V22() Element of
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

X . L is set
{ F1(b1,b2,b3) where b1, b2, b3 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 : P1[b1,b2,b3] } is set

bool is non empty set
is non empty Element of bool

bool is non empty set

dom D is set
rng D is set

dom X is set
rng X is set
N is set

F1(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],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,D:] is Relation-like set
PFuncs ([:D,D:],D) is set
X is set
k is 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

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

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
c15 is set
c16 is set
[c15,c16] is V22() set
{c15,c16} is non empty finite countable set
{c15} is non empty trivial finite 1 -element countable set
{{c15,c16},{c15}} is non empty finite V54() countable set
c17 is set
[c15,c17] is V22() set
{c15,c17} is non empty finite countable set
{{c15,c17},{c15}} is non empty finite V54() countable 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

dom K is set
rng K is set
[:(rng K),(rng K):] is Relation-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

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

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

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

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

dom M is set
rng M is set
is Relation-like non empty non trivial non finite set

dom k is set
rng k is set
N is set

dom K is set
rng K is set
[:(rng K),(rng K):] is Relation-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
bool 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 \ (rng K)),(omega \ (rng K)):] is Relation-like omega -defined omega -valued Element of bool
[:(omega \ (rng K)),(omega \ (rng K)):] /\ [:(omega \ (rng K)),(rng K):] is Relation-like omega -defined omega -valued Element of bool
(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

[:(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 \ (rng K)),(omega \ (rng K)):] /\ [:(rng K),(rng K):] is Relation-like omega -defined omega -valued Element of bool
[:(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 \ (rng K)) /\ (rng K)),((omega \ (rng K)) /\ (omega \ (rng K))):] is Relation-like omega -defined omega -valued Element of bool
[:(omega \ (rng K)),(omega \ (rng K)):] /\ [:(rng K),(omega \ (rng K)):] is Relation-like omega -defined omega -valued Element of bool
([:(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 ([:(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)):]) +` (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 \ (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,(card (rng K)):])) +` (card [:(rng K),(omega \ (rng K)):]) is epsilon-transitive epsilon-connected ordinal cardinal set

[:(card (rng K)),omega:] is Relation-like 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

(omega +` (omega *` (card (rng K)))) +` ((card (rng K)) *` omega) is epsilon-transitive epsilon-connected ordinal cardinal set

dom N is set
rng N is 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

dom M is set
rng M is set

[:(card (rng K)),(card (rng K)):] is Relation-like set

D \ (rng K) is Element of bool D
bool D is non empty set

dom N is set
rng N is 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) \/ (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

dom M is set
rng M is 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

dom K is set
rng K is set

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

[:(card D),(card D):] is Relation-like set

D is set

X is set
[:D,X:] is Relation-like set

[:(card D),(card X):] is Relation-like set

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

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

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

D is set

X is set

D is non empty 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