:: 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₁ where b₁ is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() Element of D * : len b₁ = f } is set
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₁ where b₁ is Relation-like NAT -defined D * -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() Element of (D *) * : len b₁ = M } is set
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₁ where b₁ is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() Element of D * : len b₁ = j } is set
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₁ where b₁ is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() Element of D * : len b₁ = j } is set
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₁ where b₁ is Relation-like NAT -defined j -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() Element of j * : len b₁ = i } is set
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₁ where b₁ is Relation-like NAT -defined i -tuples_on j -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() Element of (i -tuples_on j) * : len b₁ = D } is set
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₁ where b₁ is Relation-like NAT -defined j -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() Element of j * : len b₁ = f } is set
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₁ where b₁ is Relation-like NAT -defined j * -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() Element of (j *) * : len b₁ = i } is set
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₁() is non empty set
F₁() * is functional non empty FinSequence-membered FinSequenceSet of F₁()
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
Seg F₃() is finite F₃() -element countable Element of bool NAT
Seg F₂() is finite F₂() -element countable Element of bool 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
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,j) is Element of 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₄(j,i) is Element of F₁()
i is Relation-like NAT -defined F₁() * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() FinSequence of 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₄(M,j) is Element of F₁()
i is Relation-like NAT -defined F₁() -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() FinSequence of 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₁() * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () FinSequence of F₁() *
rng j is finite countable set
M is Relation-like NAT -defined F₁() -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() FinSequence of 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₁() * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () (F₁(),F₂(),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₁(),M,f,i) is Element of F₁()
F₄(f,i) is Element of 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₁() -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() FinSequence of 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₂() 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
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
[:(Seg F₂()),(Seg F₃()):] is Relation-like finite countable set
F₁() is non empty set
F₁() * is functional non empty FinSequence-membered FinSequenceSet of 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₂()),(Seg F₃()):],F₁():] is Relation-like set
bool [:[:(Seg F₂()),(Seg F₃()):],F₁():] is set
D is Relation-like Function-like V18([:(Seg F₂()),(Seg F₃()):],F₁()) finite countable V172() Element of bool [:[:(Seg F₂()),(Seg F₃()):],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₁() * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() FinSequence of 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₁() -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() FinSequence of 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₁() * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () FinSequence of F₁() *
rng M is finite countable set
f is Relation-like NAT -defined F₁() -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() FinSequence of 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₁() * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () (F₁(),F₂(),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,j) is Element of 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₁() -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() FinSequence of 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() ()