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

bool REAL is set

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

COMPLEX is set

RAT is set

INT is set

{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real V27() V29() V30() V31() V33() V34() V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V48() Cardinal-yielding countable V134() V171() V172() 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

0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real V27() V29() V30() V31() V33() V34() V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V48() Cardinal-yielding countable V134() V171() V172() Element of NAT

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

card {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real V27() V29() V30() V31() V33() V34() V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V48() Cardinal-yielding countable V134() V171() V172() set

D is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real V27() V29() V30() V31() V33() V34() V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V48() Cardinal-yielding countable V134() V171() V172() set

rng D is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty trivial ext-real V27() V29() V30() V31() V33() V34() V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V48() Cardinal-yielding countable V134() V171() V172() set

i is set

D is non empty set

i is Element of D

<*i*> is Relation-like NAT -defined D -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable V172() FinSequence of D

<*<*i*>*> is Relation-like NAT -defined Function-like constant non empty trivial V27() finite 1 -element FinSequence-like FinSubsequence-like countable V171() V172() set

rng <*<*i*>*> is non empty trivial finite 1 -element countable set

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

{<*i*>} is functional non empty trivial finite V40() 1 -element with_common_domain countable set

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

j |-> D is Relation-like NAT -defined Function-like finite j -element FinSequence-like FinSubsequence-like countable V172() set

Seg j is finite j -element countable Element of bool NAT

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

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

[:(Seg j),{D}:] is Relation-like finite countable set

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

i |-> (j |-> D) is Relation-like NAT -defined Function-like finite i -element FinSequence-like FinSubsequence-like countable V172() set

Seg i is finite i -element countable Element of bool NAT

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)}:]

{(j |-> D)} is functional non empty trivial finite V40() 1 -element with_common_domain countable set

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

D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set

<*D*> is Relation-like NAT -defined Function-like constant non empty trivial V27() finite 1 -element FinSequence-like FinSubsequence-like countable V171() V172() set

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

rng <*D*> is non empty trivial finite 1 -element countable set

i is set

{D} is functional non empty trivial finite V40() 1 -element with_common_domain countable set

j is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() 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

i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set

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

j is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set

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

<*i,j*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable V172() set

f is set

rng <*i,j*> is non empty finite countable set

{i,j} is functional non empty finite V40() countable set

i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set

j is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() 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

rng {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty trivial ext-real V27() V29() V30() V31() V33() V34() V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V48() Cardinal-yielding countable V134() V171() V172() set

D is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real V27() V29() V30() V31() V33() V34() V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V48() Cardinal-yielding countable V134() V171() V172() set

D is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real V27() V29() V30() V31() V33() V34() V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V48() Cardinal-yielding countable V134() V171() V172() set

<*{},{}*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable V172() set

D is non empty set

i is Element of D

<*i*> is Relation-like NAT -defined D -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable V172() FinSequence of D

j is Element of D

<*j*> is Relation-like NAT -defined D -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable V172() FinSequence of D

<*<*i*>,<*j*>*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable V172() set

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

<*i,j*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable V172() set

M is Element of D

f is Element of D

<*M,f*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable V172() set

<*<*i,j*>,<*M,f*>*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable V172() set

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

D * is functional non empty FinSequence-membered FinSequenceSet of D

<*> (D *) is Relation-like non-empty empty-yielding NAT -defined D * -valued Function-like one-to-one constant functional empty ext-real V27() V29() V30() V31() V33() V34() V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V48() Cardinal-yielding countable V134() V171() V172() FinSequence of D *

rng (<*> (D *)) is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty trivial ext-real V27() V29() V30() V31() V33() V34() V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V48() Cardinal-yielding countable V134() V171() V172() set

i is set

D is non empty set

D * is functional non empty FinSequence-membered FinSequenceSet of D

the Element of D is Element of D

<* the Element of D*> is Relation-like NAT -defined D -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable V172() FinSequence of D

<*<* the Element of D*>*> is Relation-like NAT -defined Function-like constant non empty trivial V27() finite 1 -element FinSequence-like FinSubsequence-like countable V171() V172() set

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

j is Relation-like NAT -defined D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() FinSequence of D *

f is Relation-like NAT -defined D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () FinSequence of D *

M is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set

i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set

rng f is finite countable set

i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set

D is non empty set

D * is functional non empty FinSequence-membered FinSequenceSet of D

i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set

rng i is finite countable set

j is Relation-like NAT -defined D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () FinSequence of D *

rng j is finite countable set

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

f is set

i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set

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

j is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() FinSequence of D

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

i is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() FinSequence of D

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

j is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set

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

f is set

M is set

i is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() FinSequence of D

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

f is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() FinSequence of D

D is non empty set

D * is functional non empty FinSequence-membered FinSequenceSet of D

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

f |-> the Element of D is Relation-like NAT -defined D -valued Function-like finite f -element FinSequence-like FinSubsequence-like countable V172() Element of f -tuples_on D

f -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D

{ b

Seg f is finite f -element countable Element of bool NAT

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

j is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() Element of D *

M |-> j is Relation-like NAT -defined D * -valued Function-like V27() finite M -element FinSequence-like FinSubsequence-like countable V171() V172() Element of M -tuples_on (D *)

M -tuples_on (D *) is functional non empty FinSequence-membered FinSequenceSet of D *

(D *) * is functional non empty FinSequence-membered FinSequenceSet of D *

{ b

Seg M is finite M -element countable Element of bool NAT

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

{j} is functional non empty trivial finite V40() 1 -element with_common_domain countable set

[:(Seg M),{j}:] is Relation-like finite countable set

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

f is Relation-like NAT -defined D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() FinSequence of D *

rng f is finite countable set

i is set

i is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() FinSequence of D

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

j |-> the Element of D is Relation-like NAT -defined D -valued Function-like finite j -element FinSequence-like FinSubsequence-like countable V172() Element of j -tuples_on D

j -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D

{ b

Seg j is finite j -element countable Element of bool NAT

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

i is Relation-like NAT -defined D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () FinSequence of D *

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

rng i is finite countable set

i is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() FinSequence of D

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

j |-> the Element of D is Relation-like NAT -defined D -valued Function-like finite j -element FinSequence-like FinSubsequence-like countable V172() Element of j -tuples_on D

j -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D

{ b

Seg j is finite j -element countable Element of bool NAT

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

i -tuples_on j is functional non empty FinSequence-membered FinSequenceSet of j

j * is functional non empty FinSequence-membered FinSequenceSet of j

{ b

M is Element of j

i |-> M is Relation-like NAT -defined j -valued Function-like finite i -element FinSequence-like FinSubsequence-like countable V172() Element of i -tuples_on j

Seg i is finite i -element countable Element of bool NAT

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

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

[:(Seg i),{M}:] is Relation-like finite countable set

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

D |-> (i |-> M) is Relation-like NAT -defined i -tuples_on j -valued Function-like finite D -element FinSequence-like FinSubsequence-like countable V172() Element of D -tuples_on (i -tuples_on j)

D -tuples_on (i -tuples_on j) is functional non empty FinSequence-membered FinSequenceSet of i -tuples_on j

(i -tuples_on j) * is functional non empty FinSequence-membered FinSequenceSet of i -tuples_on j

{ b

Seg D is finite D -element countable Element of bool NAT

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)}:]

{(i |-> M)} is functional non empty trivial finite V40() 1 -element with_common_domain countable set

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

f |-> M is Relation-like NAT -defined j -valued Function-like finite f -element FinSequence-like FinSubsequence-like countable V172() Element of f -tuples_on j

f -tuples_on j is functional non empty FinSequence-membered FinSequenceSet of j

{ b

Seg f is finite f -element countable Element of bool NAT

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

[:(Seg f),{M}:] is Relation-like finite countable 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

j is Relation-like NAT -defined j -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() Element of j *

i |-> j is Relation-like NAT -defined j * -valued Function-like V27() finite i -element FinSequence-like FinSubsequence-like countable V171() V172() Element of i -tuples_on (j *)

i -tuples_on (j *) is functional non empty FinSequence-membered FinSequenceSet of j *

(j *) * is functional non empty FinSequence-membered FinSequenceSet of j *

{ b

Seg i is finite i -element countable Element of bool NAT

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

{j} is functional non empty trivial finite V40() 1 -element with_common_domain countable set

[:(Seg i),{j}:] is Relation-like finite countable set

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

f is Relation-like NAT -defined j * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() FinSequence of j *

i is Relation-like NAT -defined j * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () FinSequence of j *

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

rng i is finite countable set

i is Relation-like NAT -defined j -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() FinSequence of j

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

D is non empty set

D * is functional non empty FinSequence-membered FinSequenceSet of D

i is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() FinSequence of D

<*i*> is Relation-like NAT -defined Function-like constant non empty trivial V27() finite 1 -element FinSequence-like FinSubsequence-like countable V171() V172() set

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

j is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() Element of D *

<*j*> is Relation-like NAT -defined D * -valued Function-like constant non empty trivial V27() finite 1 -element FinSequence-like FinSubsequence-like countable V171() V172() FinSequence of D *

M is Relation-like NAT -defined D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () FinSequence of D *

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

rng M is finite countable set

f is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() FinSequence of D

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

{i} 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 non empty set

i * is functional non empty FinSequence-membered FinSequenceSet of i

j is Relation-like NAT -defined i -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() FinSequence of i

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

M is Relation-like NAT -defined i -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() FinSequence of i

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

<*j,M*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable V172() set

f is Relation-like NAT -defined i -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() Element of i *

i is Relation-like NAT -defined i -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() Element of i *

<*f,i*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable V172() set

j is Relation-like NAT -defined i * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() FinSequence of i *

f is Relation-like NAT -defined i * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () FinSequence of i *

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

rng f is finite countable set

i is Relation-like NAT -defined i -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() FinSequence of i

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

i * is functional non empty FinSequence-membered FinSequenceSet of i

<*> (i *) is Relation-like non-empty empty-yielding NAT -defined i * -valued Function-like one-to-one constant functional empty ext-real V27() V29() V30() V31() V33() V34() V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V48() Cardinal-yielding countable V134() V171() V172() FinSequence of i *

j is Relation-like NAT -defined i * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() FinSequence of i *

M is Relation-like NAT -defined i * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () FinSequence of i *

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

rng M is finite countable set

f is Relation-like NAT -defined i -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() FinSequence of i

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

<*{}*> is Relation-like NAT -defined Function-like constant non empty trivial V27() finite 1 -element FinSequence-like FinSubsequence-like countable V171() V172() set

D is non empty set

D * is functional non empty FinSequence-membered FinSequenceSet of D

<*> D is Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional empty ext-real V27() V29() V30() V31() V33() V34() V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V48() Cardinal-yielding countable V134() V171() V172() FinSequence of D

len (<*> D) is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real V27() V29() V30() V31() V33() V34() V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V48() Cardinal-yielding countable V134() V171() V172() Element of NAT

D is non empty set

D * is functional non empty FinSequence-membered FinSequenceSet of D

i is Element of D

<*i*> is Relation-like NAT -defined D -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable V172() FinSequence of D

<*<*i*>*> is Relation-like NAT -defined Function-like constant non empty trivial V27() finite 1 -element FinSequence-like FinSubsequence-like countable V171() V172() set

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 functional non empty FinSequence-membered FinSequenceSet of D

<*> D is Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional empty ext-real V27() V29() V30() V31() V33() V34() V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V48() Cardinal-yielding countable V134() V171() V172() FinSequence of D

len (<*> D) is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real V27() V29() V30() V31() V33() V34() V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V48() Cardinal-yielding countable V134() V171() V172() Element of NAT

D is non empty set

D * is functional non empty FinSequence-membered FinSequenceSet of D

i is Element of D

j is Element of D

<*i,j*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable V172() set

<*<*i,j*>*> is Relation-like NAT -defined Function-like constant non empty trivial V27() finite 1 -element FinSequence-like FinSubsequence-like countable V171() V172() set

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

D * is functional non empty FinSequence-membered FinSequenceSet of D

i is Element of D

<*i*> is Relation-like NAT -defined D -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable V172() FinSequence of D

j is Element of D

<*j*> is Relation-like NAT -defined D -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable V172() FinSequence of D

<*<*i*>,<*j*>*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable V172() set

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

D * is functional non empty FinSequence-membered FinSequenceSet of D

i is Element of D

j is Element of D

<*i,j*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable V172() set

M is Element of D

f is Element of D

<*M,f*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable V172() set

<*<*i,j*>,<*M,f*>*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable V172() set

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 Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() () set

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

rng D is finite countable set

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

f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() 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() Element of NAT

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

M is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() 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

i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set

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

j is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set

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

f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set

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

D is non empty set

D * is functional non empty FinSequence-membered FinSequenceSet of D

i is Relation-like NAT -defined D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () FinSequence of D *

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

rng i is finite countable set

M is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set

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

f is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() FinSequence of D

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

rng i is finite countable set

M is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() FinSequence of D

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

D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() () set

dom D is finite countable Element of bool 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

D * is functional non empty FinSequence-membered FinSequenceSet of 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() 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 Relation-like NAT -defined D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () FinSequence of D *

(i) is set

dom i is finite countable Element of bool NAT

(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

i . j is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set

rng i is finite countable set

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

i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() 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

f is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() FinSequence of D

dom f is finite countable Element of bool NAT

f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set

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

i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set

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

f . M is set

rng f is finite countable set

f is Element of D

j is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() FinSequence of D

f is Element of D

j . M is set

f is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() FinSequence of D

i is Element of D

f . M is set

D is non empty set

D * is functional non empty FinSequence-membered FinSequenceSet of D

i is Relation-like NAT -defined D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () FinSequence of D *

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

dom i is finite countable Element of bool NAT

Seg (i) is finite (i) -element countable Element of bool NAT

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

j is Relation-like NAT -defined D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () FinSequence of D *

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

dom j is finite countable Element of bool NAT

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

i . M is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set

j . M is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set

rng i is finite countable set

f is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() FinSequence of D

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

rng j is finite countable set

i is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() FinSequence of D

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

rng f is finite countable set

dom f is finite countable Element of bool NAT

rng i is finite countable set

dom i is finite countable Element of bool 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

(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

F

F

F

F

Seg F

Seg F

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

i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set

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

dom i is finite countable Element of bool NAT

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

i . j is set

F

D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set

dom D is finite countable Element of bool NAT

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

rng D is finite countable set

i is set

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

D . j is set

M is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set

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

rng M is finite countable set

f is set

dom M is finite countable Element of bool NAT

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

M . i is set

Seg (len M) is finite len M -element countable Element of bool NAT

F

i is Relation-like NAT -defined F

rng i is finite countable set

j is set

dom i is finite countable Element of bool NAT

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

i . M is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set

f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set

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

rng f is finite countable set

i is set

dom f is finite countable Element of bool NAT

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

f . j is set

Seg (len f) is finite len f -element countable Element of bool NAT

F

i is Relation-like NAT -defined F

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

j is Relation-like NAT -defined F

rng j is finite countable set

M is Relation-like NAT -defined F

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

dom j is finite countable Element of bool NAT

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

j . f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set

i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set

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

M is Relation-like NAT -defined F

(M) is set

dom M is finite countable Element of bool NAT

(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

(F

F

M . f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set

j is Relation-like NAT -defined F

j . i is set

f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set

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

F

Seg F

F

Seg F

[:(Seg F

F

F

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 F

[:[:(Seg F

bool [:[:(Seg F

D is Relation-like Function-like V18([:(Seg F

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

j is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set

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

dom j is finite countable Element of bool 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

i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set

dom i is finite countable Element of bool NAT

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

rng i is finite countable set

j is set

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

i . M is set

f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set

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

rng f is finite countable set

i is set

dom f is finite countable Element of bool NAT

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

f . j is set

Seg (len f) is finite len f -element countable Element of bool 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

D . (M,j) is set

D . [M,j] is set

j is Relation-like NAT -defined F

rng j is finite countable set

M is set

dom j is finite countable Element of bool NAT

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

j . f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set

i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set

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

rng i is finite countable set

j is set

dom i is finite countable Element of bool NAT

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

i . f is set

Seg (len i) is finite len i -element countable Element of bool NAT

[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

j is Relation-like NAT -defined F

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

M is Relation-like NAT -defined F

rng M is finite countable set

f is Relation-like NAT -defined F

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

dom M is finite countable Element of bool NAT

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

M . i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set

j is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set

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

f is Relation-like NAT -defined F

(f) is set

dom f is finite countable Element of bool NAT

(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

(F

f . i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set

D . (i,j) is set

D . [i,j] is set

f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set

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

i is Relation-like NAT -defined F

i . j is set

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

i is non empty set

i * is functional non empty FinSequence-membered FinSequenceSet of i

j is Relation-like NAT -defined i * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () (i, {} ,D)

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

dom j is finite countable Element of bool NAT

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

Seg D is finite D -element countable Element of bool NAT

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

Seg i is finite i -element countable Element of bool NAT

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

j is non empty set

j * is functional non empty FinSequence-membered FinSequenceSet of j

M is Relation-like NAT -defined j * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () (j,D,i)

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

dom M is finite countable Element of bool NAT

Seg (M) is finite (M) -element countable Element of bool NAT

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

Seg (len M) is finite len M -element countable Element of bool NAT

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

Seg D is finite D -element countable Element of bool NAT

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

i is non empty set

i * is functional non empty FinSequence-membered FinSequenceSet of i

j is Relation-like NAT -defined i * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () (i,D,D)

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

dom j is finite countable Element of bool NAT

Seg (j) is finite (j) -element countable Element of bool NAT

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

Seg (len j) is finite len j -element countable Element of bool NAT

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

Seg D is finite D -element countable Element of bool NAT

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

j is non empty set

j * is functional non empty FinSequence-membered FinSequenceSet of j

M is Relation-like NAT -defined j * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () (j,D,i)

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

(M) is set

dom M is finite countable Element of bool NAT

(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

j * is functional non empty FinSequence-membered FinSequenceSet of j

M is Relation-like NAT -defined j * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () (j,D,i)

(M) is set

dom M is finite countable Element of bool NAT

(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 Relation-like NAT -defined j * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () (j,D,i)

(f) is set

dom f is finite countable Element of bool NAT

(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

Seg D is finite D -element countable Element of bool 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

j * is functional non empty FinSequence-membered FinSequenceSet of j

M is Relation-like NAT -defined j * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () (j,D,i)

(M) is set

dom M is finite countable Element of bool NAT

(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 Relation-like NAT -defined j * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () (j,D,i)

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

i * is functional non empty FinSequence-membered FinSequenceSet of i

j is Relation-like NAT -defined i * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () (i,D,D)

(j) is set

dom j is finite countable Element of bool NAT

(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 is finite D -element countable Element of bool NAT

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

D is non empty set

D * is functional non empty FinSequence-membered FinSequenceSet of D

i is Relation-like NAT -defined D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () FinSequence of D *

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

(i) is set

dom i is finite countable Element of bool 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

j is Relation-like NAT -defined D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () (D,(i), len i)

(j) is set

dom j is finite countable Element of bool NAT

(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 (len i) is finite len i -element countable Element of bool NAT

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

M is Relation-like NAT -defined D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () FinSequence of D *

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

(M) is set

dom M is finite countable Element of bool NAT

(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

j is Relation-like NAT -defined D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () FinSequence of D *

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

(j) is set

dom j is finite countable Element of bool NAT

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

j is Relation-like NAT -defined D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() ()