:: MATRIX_1 semantic presentation

REAL is set
NAT is non empty non trivial V29() V30() V31() non finite cardinal limit_cardinal countable denumerable Element of bool REAL

NAT is non empty non trivial V29() V30() V31() non finite cardinal limit_cardinal countable denumerable set
bool NAT is non trivial non finite set
bool NAT is non trivial non finite set

RAT is set
INT is set

2 is non empty ext-real positive V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
1 is non empty ext-real positive V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
3 is non empty ext-real positive V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

Seg 1 is non empty trivial finite 1 -element countable Element of bool NAT

i is set
D is non empty set
i is Element of D

j is non empty ext-real positive V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
M is set
len <*i*> is non empty ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

D is set
i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
j is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set

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

bool [:(Seg j),{D}:] is finite V40() countable set

K100((Seg i),(j |-> D)) is Relation-like NAT -defined Function-like V18( Seg i,{(j |-> D)}) finite FinSequence-like FinSubsequence-like countable V172() Element of bool [:(Seg i),{(j |-> D)}:]

[:(Seg i),{(j |-> D)}:] is Relation-like finite countable set
bool [:(Seg i),{(j |-> D)}:] is finite V40() countable set
f is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
rng (i |-> (j |-> D)) is finite countable set
i is set
len (j |-> D) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

len D is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

i is set

len j is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
D is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set

len i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

len j is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

f is set
rng <*i,j*> is non empty finite countable set
{i,j} is functional non empty finite V40() countable set

len j is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
M is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
M is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
i is set

D is non empty set
i is Element of D

j is Element of D

len <*i*> is non empty ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
len <*j*> is non empty ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
D is non empty set
i is Element of D
j is Element of D

M is Element of D
f is Element of D

len <*i,j*> is non empty ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
len <*M,f*> is non empty ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
D is set

i is set
D is non empty set

the Element of D is Element of D

rng <*<* the Element of D*>*> is non empty trivial finite 1 -element countable set
{<* the Element of D*>} is functional non empty trivial finite V40() 1 -element with_common_domain countable set

D is non empty set

M is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
f is set

len i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

len j is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
f is set
j is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
M is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
f is set

len i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

len j is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
f is set
M is set

len i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

D is non empty set

i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
j is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
the Element of D is Element of D
f is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

{ } is set

K100((Seg f), the Element of D) is Relation-like NAT -defined Function-like V18( Seg f,{ the Element of D}) finite FinSequence-like FinSubsequence-like countable V172() Element of bool [:(Seg f),{ the Element of D}:]
{ the Element of D} is non empty trivial finite 1 -element countable set
[:(Seg f),{ the Element of D}:] is Relation-like finite countable set
bool [:(Seg f),{ the Element of D}:] is finite V40() countable set
M is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

{ } is set

bool [:(Seg M),{j}:] is finite V40() countable set

i is set

len i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

{ } is set

K100((Seg j), the Element of D) is Relation-like NAT -defined Function-like V18( Seg j,{ the Element of D}) finite FinSequence-like FinSubsequence-like countable V172() Element of bool [:(Seg j),{ the Element of D}:]
[:(Seg j),{ the Element of D}:] is Relation-like finite countable set
bool [:(Seg j),{ the Element of D}:] is finite V40() countable set
{(j |-> the Element of D)} is functional non empty trivial finite V40() 1 -element with_common_domain countable set
i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

len i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

len i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

{ } is set

K100((Seg j), the Element of D) is Relation-like NAT -defined Function-like V18( Seg j,{ the Element of D}) finite FinSequence-like FinSubsequence-like countable V172() Element of bool [:(Seg j),{ the Element of D}:]
[:(Seg j),{ the Element of D}:] is Relation-like finite countable set
bool [:(Seg j),{ the Element of D}:] is finite V40() countable set
{(j |-> the Element of D)} is functional non empty trivial finite V40() 1 -element with_common_domain countable set
D is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
j is non empty set

{ } is set
M is Element of j

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

bool [:(Seg i),{M}:] is finite V40() countable set

{ } is set

K100((Seg D),(i |-> M)) is Relation-like NAT -defined Function-like V18( Seg D,{(i |-> M)}) finite FinSequence-like FinSubsequence-like countable V172() Element of bool [:(Seg D),{(i |-> M)}:]

[:(Seg D),{(i |-> M)}:] is Relation-like finite countable set
bool [:(Seg D),{(i |-> M)}:] is finite V40() countable set
f is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

{ } is set

bool [:(Seg f),{M}:] is finite V40() countable set
i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

{ } is set

bool [:(Seg i),{j}:] is finite V40() countable set

len i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

len i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
D is non empty set

len i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

len M is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

len f is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

D is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
i is non empty set

len j is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

len M is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

len f is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

len i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
{j,M} is functional non empty finite V40() countable set
D is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
i is non empty set

len M is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

len f is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

D is non empty set

D is non empty set

i is Element of D

len <*i*> is non empty ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
D is non empty set

D is non empty set

i is Element of D
j is Element of D

len <*i,j*> is non empty ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
D is non empty set

i is Element of D

j is Element of D

len <*i*> is non empty ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
len <*j*> is non empty ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
D is non empty set

i is Element of D
j is Element of D

M is Element of D
f is Element of D

len <*i,j*> is non empty ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
len <*M,f*> is non empty ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

len D is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

the Element of rng D is Element of rng D
j is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
M is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

len f is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
j is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

len M is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
f is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set

len i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

len j is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

len f is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
D is non empty set

len i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
(i) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
j is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set

len M is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

len f is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

len M is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

(D) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
Seg (D) is finite (D) -element countable Element of bool NAT
[:(dom D),(Seg (D)):] is Relation-like finite countable set
D is set

j is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
M is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
[j,M] is set
{j,M} is non empty finite V40() countable set
{j} is non empty trivial finite V40() 1 -element countable set
{{j,M},{j}} is non empty finite V40() countable set

(i) is set

(i) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
Seg (i) is finite (i) -element countable Element of bool NAT
[:(dom i),(Seg (i)):] is Relation-like finite countable set

len i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

len i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
j is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set

len f is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

len i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
f . M is set

f is Element of D

f is Element of D
j . M is set

i is Element of D
f . M is set
D is non empty set

len i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
(i) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
(i) is set

Seg (i) is finite (i) -element countable Element of bool NAT
[:(dom i),(Seg (i)):] is Relation-like finite countable set

len j is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
(j) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

M is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set

len f is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

len i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
j is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
f . j is set
i . j is set

[M,j] is set
{M,j} is non empty finite V40() countable set
{M} is non empty trivial finite V40() 1 -element countable set
{{M,j},{M}} is non empty finite V40() countable set
(j) is set
Seg (j) is finite (j) -element countable Element of bool NAT
[:(dom j),(Seg (j)):] is Relation-like finite countable set
(D,j,M,j) is Element of D
i is Element of D
(D,i,M,j) is Element of D
f is Element of D
F1() is non empty set
F1() * is functional non empty FinSequence-membered FinSequenceSet of F1()
F2() is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
F3() is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
Seg F3() is finite F3() -element countable Element of bool NAT
Seg F2() is finite F2() -element countable Element of bool NAT
D is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set

len i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

j is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
i . j is set
F4(D,j) is Element of F1()

len D is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

i is set
j is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
D . j is set

len M is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

f is set

i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
M . i is set

F4(j,i) is Element of F1()

j is set

M is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set

len f is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

i is set

j is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
f . j is set

F4(M,j) is Element of F1()

len i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
M is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set

len M is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

f is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set

len i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
M is Relation-like NAT -defined F1() * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () (F1(),F2(),F3())
(M) is set

(M) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
Seg (M) is finite (M) -element countable Element of bool NAT
[:(dom M),(Seg (M)):] is Relation-like finite countable set
f is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
[f,i] is set
{f,i} is non empty finite V40() countable set
{f} is non empty trivial finite V40() 1 -element countable set
{{f,i},{f}} is non empty finite V40() countable set
(F1(),M,f,i) is Element of F1()
F4(f,i) is Element of F1()

j . i is set

len f is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
F2() is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
Seg F2() is finite F2() -element countable Element of bool NAT
F3() is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
Seg F3() is finite F3() -element countable Element of bool NAT
[:(Seg F2()),(Seg F3()):] is Relation-like finite countable set
F1() is non empty set
F1() * is functional non empty FinSequence-membered FinSequenceSet of F1()
D is set
i is set
M is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
j is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
[M,j] is set
{M,j} is non empty finite V40() countable set
{M} is non empty trivial finite V40() 1 -element countable set
{{M,j},{M}} is non empty finite V40() countable set
f is Element of F1()
[:[:(Seg F2()),(Seg F3()):],F1():] is Relation-like set
bool [:[:(Seg F2()),(Seg F3()):],F1():] is set
D is Relation-like Function-like V18([:(Seg F2()),(Seg F3()):],F1()) finite countable V172() Element of bool [:[:(Seg F2()),(Seg F3()):],F1():]
i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set

len j is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

M is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
j . M is set
D . (i,M) is set
[i,M] is set
{i,M} is non empty finite V40() countable set
{i} is non empty trivial finite V40() 1 -element countable set
{{i,M},{i}} is non empty finite V40() countable set
D . [i,M] is set

len i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

j is set
M is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
i . M is set

len f is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

i is set

j is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
f . j is set

[M,j] is set
{M,j} is non empty finite V40() countable set
{M} is non empty trivial finite V40() 1 -element countable set
{{M,j},{M}} is non empty finite V40() countable set
D . (M,j) is set
D . [M,j] is set

M is set

f is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set

len i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

j is set

f is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
i . f is set

[f,f] is set
{f,f} is non empty finite V40() countable set
{f} is non empty trivial finite V40() 1 -element countable set
{{f,f},{f}} is non empty finite V40() countable set
D . (f,f) is set
D . [f,f] is set

len j is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
f is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set

len f is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set

len j is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
f is Relation-like NAT -defined F1() * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () (F1(),F2(),F3())
(f) is set

(f) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
Seg (f) is finite (f) -element countable Element of bool NAT
[:(dom f),(Seg (f)):] is Relation-like finite countable set
i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
j is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
[i,j] is set
{i,j} is non empty finite V40() countable set
{i} is non empty trivial finite V40() 1 -element countable set
{{i,j},{i}} is non empty finite V40() countable set
(F1(),f,i,j) is Element of F1()

D . (i,j) is set
D . [i,j] is set

len f is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

i . j is set
D is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
i is non empty set

len j is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
(j) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
(j) is set

Seg (j) is finite (j) -element countable Element of bool NAT
[:(dom j),(Seg (j)):] is Relation-like finite countable set
D is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set

i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set

[:(Seg D),(Seg i):] is Relation-like finite countable set
j is non empty set

len M is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
(M) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
(M) is set

Seg (M) is finite (M) -element countable Element of bool NAT
[:(dom M),(Seg (M)):] is Relation-like finite countable set

D is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set

[:(Seg D),(Seg D):] is Relation-like finite countable set
i is non empty set

len j is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
(j) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
(j) is set

Seg (j) is finite (j) -element countable Element of bool NAT
[:(dom j),(Seg (j)):] is Relation-like finite countable set

D is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set

i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
j is non empty set

len M is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
(M) is set

(M) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
Seg (M) is finite (M) -element countable Element of bool NAT
[:(dom M),(Seg (M)):] is Relation-like finite countable set
[:(Seg D),(Seg (M)):] is Relation-like finite countable set
D is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
j is non empty set

(M) is set

(M) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
Seg (M) is finite (M) -element countable Element of bool NAT
[:(dom M),(Seg (M)):] is Relation-like finite countable set

(f) is set

(f) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
Seg (f) is finite (f) -element countable Element of bool NAT
[:(dom f),(Seg (f)):] is Relation-like finite countable set
len M is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
len f is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

D is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
j is non empty set

(M) is set

(M) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
Seg (M) is finite (M) -element countable Element of bool NAT
[:(dom M),(Seg (M)):] is Relation-like finite countable set

len M is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
len f is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
(f) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
(f) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
(f) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
(f) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
D is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
i is non empty set

(j) is set

(j) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
Seg (j) is finite (j) -element countable Element of bool NAT
[:(dom j),(Seg (j)):] is Relation-like finite countable set
M is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
f is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
[M,f] is set
{M,f} is non empty finite V40() countable set
{M} is non empty trivial finite V40() 1 -element countable set
{{M,f},{M}} is non empty finite V40() countable set
[f,M] is set
{f,M} is non empty finite V40() countable set
{f} is non empty trivial finite V40() 1 -element countable set
{{f,M},{f}} is non empty finite V40() countable set

[:(Seg D),(Seg D):] is Relation-like finite countable set
D is non empty set

(i) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
(i) is set

Seg (i) is finite (i) -element countable Element of bool NAT
[:(dom i),(Seg (i)):] is Relation-like finite countable set
len i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT

(j) is set

(j) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
Seg (j) is finite (j) -element countable Element of bool NAT
[:(dom j),(Seg (j)):] is Relation-like finite countable set

[:(Seg (i)),(dom i):] is Relation-like finite countable set

len M is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
(M) is set

(M) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
Seg (M) is finite (M) -element countable Element of bool NAT
[:(dom M),(Seg (M)):] is Relation-like finite countable set
f is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
[f,i] is set
{f,i} is non empty finite V40() countable set
{f} is non empty trivial finite V40() 1 -element countable set
{{f,i},{f}} is non empty finite V40() countable set
[i,f] is set
{i,f} is non empty finite V40() countable set
{i} is non empty trivial finite V40() 1 -element countable set
{{i,f},{i}} is non empty finite V40() countable set
f is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
j is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
[f,j] is set
{f,j} is non empty finite V40() countable set
{f} is non empty trivial finite V40() 1 -element countable set
{{f,j},{f}} is non empty finite V40() countable set
[j,f] is set
{j,f} is non empty finite V40() countable set
{j} is non empty trivial finite V40() 1 -element countable set
{{j,f},{j}} is non empty finite V40() countable set
f is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
[i,f] is set
{i,f} is non empty finite V40() countable set
{i} is non empty trivial finite V40() 1 -element countable set
{{i,f},{i}} is non empty finite V40() countable set
(D,M,f,i) is Element of D
(D,i,i,f) is Element of D
[f,i] is set
{f,i} is non empty finite V40() countable set
{f} is non empty trivial finite V40() 1 -element countable set
{{f,i},{f}} is non empty finite V40() countable set

len j is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
(j) is set

(j) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
Seg (j) is finite (j) -element countable Element of bool NAT
[:(dom j),(Seg (j)):] is Relation-like finite countable set

M is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
f is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
[M,f] is set
{M,f} is non empty finite V40() countable set
{M} is non empty trivial finite V40() 1 -element countable set
{{M,f},{M}} is non empty finite V40() countable set
[f,M] is set
{f,M} is non empty finite V40() countable set
{f} is non empty trivial finite V40() 1 -element countable set
{{f,M},{f}} is non empty finite V40() countable set
j is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
[j,i] is set
{j,i} is non empty finite V40() countable set
{j} is non empty trivial finite V40() 1 -element countable set
{{j,i},{j}} is non empty finite V40() countable set
[i,j] is set
{i,j} is non empty finite V40() countable set
{i} is non empty trivial finite V40() 1 -element countable set
{{i,j},{i}} is non empty finite V40() countable set
i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
f is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
[i,f] is set
{i,f} is non empty finite V40() countable set
{i} is non empty trivial finite V40() 1 -element countable set
{{i,f},{i}} is non empty finite V40() countable set
(D,j,f,i) is Element of D
(D,i,i,f) is Element of D