:: 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() () 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
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
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
(D,j,f,i) is Element of D
(D,i,i,f) is Element of D
(D,M,f,i) is Element of D
f is set
i is set
[f,i] is set
{f,i} is non empty finite countable set
{f} is non empty trivial finite 1 -element countable set
{{f,i},{f}} is non empty finite V40() countable set
f 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
[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
f 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
[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
Seg (len M) is finite len M -element countable Element of bool NAT
Seg (len j) is finite len j -element countable Element of bool 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 *
(i) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
(D,i) is Relation-like NAT -defined D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () FinSequence of D *
len (D,i) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
((D,i)) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
len i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
dom (D,i) is finite countable Element of bool NAT
Seg ((D,i)) is finite ((D,i)) -element countable Element of bool NAT
[:(dom (D,i)),(Seg ((D,i))):] is Relation-like finite countable set
Seg (i) is finite (i) -element countable Element of bool NAT
dom i is finite countable Element of bool NAT
[:(Seg (i)),(dom i):] is Relation-like finite countable set
j is set
M is set
[j,M] is set
{j,M} is non empty finite countable set
{j} is non empty trivial finite 1 -element countable set
{{j,M},{j}} is non empty finite V40() countable set
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
[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
((D,i)) is 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
(i) is set
[:(dom i),(Seg (i)):] is Relation-like finite countable set
i 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
[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
(i) is set
[:(dom i),(Seg (i)):] is Relation-like finite countable 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
((D,i)) is set
Seg (len i) is finite len i -element countable Element of bool NAT
D is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
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)
(i,j) is Relation-like NAT -defined i * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () FinSequence of i *
len j is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
rng (i,j) is finite countable set
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
f is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() 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 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
(j) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
((i,j)) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
len (i,j) 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
len (i,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 (i,j) is finite countable Element of bool NAT
Seg (j) is finite (j) -element countable Element of bool NAT
i is set
(i,j) . i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set
len (i,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
i is non empty set
i * is functional non empty FinSequence-membered FinSequenceSet of i
D is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
j is Relation-like NAT -defined i * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () (i,D,D)
(i,j) is Relation-like NAT -defined i * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () FinSequence of i *
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
Seg (i) is finite (i) -element countable Element of bool NAT
j is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() 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
dom M is finite countable Element of bool NAT
f is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
M . f is set
(D,i,j,f) is Element of D
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
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
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
f . i is set
(D,i,j,i) is Element of D
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
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
dom M is finite countable Element of bool NAT
f is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
M . f is set
(D,i,f,j) is Element of D
Seg (len i) is finite len i -element countable Element of bool NAT
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
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
dom M is finite countable Element of bool NAT
Seg (len i) is finite len i -element countable Element of bool NAT
i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
M . i is set
f . i is set
(D,i,i,j) is Element of D
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 *
j is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
(D,i,j) is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() FinSequence of D
(i) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
(i) -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₁ = (i) } is set
len (D,i,j) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
(D,i,j) 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
(len i) -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₁ = len i } is set
len (D,i,j) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
D is non empty doubleLoopStr
the carrier of D is non empty set
i -tuples_on the carrier of D is functional non empty FinSequence-membered FinSequenceSet of the carrier of D
the carrier of D * is functional non empty FinSequence-membered FinSequenceSet of the carrier of D
{ b₁ where b₁ is Relation-like NAT -defined the carrier of D -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() Element of the carrier of D * : len b₁ = i } is set
i -tuples_on (i -tuples_on the carrier of D) is functional non empty FinSequence-membered FinSequenceSet of i -tuples_on the carrier of D
(i -tuples_on the carrier of D) * is functional non empty FinSequence-membered FinSequenceSet of i -tuples_on the carrier of D
{ b₁ where b₁ is Relation-like NAT -defined i -tuples_on the carrier of D -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() Element of (i -tuples_on the carrier of D) * : len b₁ = i } is set
0. D is V58(D) Element of the carrier of D
the ZeroF of D is Element of the carrier of D
i |-> (0. D) is Relation-like NAT -defined the carrier of D -valued Function-like finite i -element FinSequence-like FinSubsequence-like countable V172() Element of i -tuples_on the carrier of D
Seg i is finite i -element countable Element of bool NAT
K100((Seg i),(0. D)) is Relation-like NAT -defined Function-like V18( Seg i,{(0. D)}) finite FinSequence-like FinSubsequence-like countable V172() Element of bool [:(Seg i),{(0. D)}:]
{(0. D)} is non empty trivial finite 1 -element countable set
[:(Seg i),{(0. D)}:] is Relation-like finite countable set
bool [:(Seg i),{(0. D)}:] is finite V40() countable set
i |-> (i |-> (0. D)) is Relation-like NAT -defined i -tuples_on the carrier of D -valued Function-like finite i -element FinSequence-like FinSubsequence-like countable V172() Element of i -tuples_on (i -tuples_on the carrier of D)
K100((Seg i),(i |-> (0. D))) is Relation-like NAT -defined Function-like V18( Seg i,{(i |-> (0. D))}) finite FinSequence-like FinSubsequence-like countable V172() Element of bool [:(Seg i),{(i |-> (0. D))}:]
{(i |-> (0. D))} is functional non empty trivial finite V40() 1 -element with_common_domain countable set
[:(Seg i),{(i |-> (0. D))}:] is Relation-like finite countable set
bool [:(Seg i),{(i |-> (0. D))}:] is finite V40() countable set
1. D is Element of the carrier of D
the OneF of D is Element of the carrier of D
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
[:(Seg 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
M is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,j,j)
(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 the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,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
i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
[i,i] is set
{i,i} is non empty finite V40() countable set
{i} is non empty trivial finite V40() 1 -element countable set
{{i,i},{i}} is non empty finite V40() countable set
( the carrier of D,f,i,i) is Element of the carrier of D
j 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
[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
( the carrier of D,f,j,f) is Element of the carrier of D
j is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,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
M is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,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 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
( the carrier of D,j,f,i) is Element of the carrier of D
( the carrier of D,M,f,i) is Element of the carrier of D
len M is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
len j is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
j is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,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
M is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
f is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,M,M)
(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
[:(Seg i),(Seg i):] is Relation-like finite countable set
i is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
j 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
[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
( the carrier of D,i,j,f) is Element of the carrier of D
( the carrier of D,j,j,f) is Element of the carrier of D
- ( the carrier of D,j,j,f) is Element of the carrier of D
M is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
f is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
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
( the carrier of D,M,i,j) is Element of the carrier of D
( the carrier of D,j,i,j) is Element of the carrier of D
- ( the carrier of D,j,i,j) is Element of the carrier of D
( the carrier of D,f,i,j) is Element of the carrier of D
(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 i),(Seg i):] is Relation-like finite countable set
M is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
f is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
i is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,f,f)
(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
[:(Seg i),(Seg i):] is Relation-like finite countable set
j is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
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
( the carrier of D,j,f,i) is Element of the carrier of D
( the carrier of D,j,f,i) is Element of the carrier of D
( the carrier of D,M,f,i) is Element of the carrier of D
( the carrier of D,j,f,i) + ( the carrier of D,M,f,i) is Element of the carrier of D
the addF of D is Relation-like Function-like V18([: the carrier of D, the carrier of D:], the carrier of D) Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is Relation-like set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is Relation-like set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is set
the addF of D . (( the carrier of D,j,f,i),( the carrier of D,M,f,i)) is Element of the carrier of D
[( the carrier of D,j,f,i),( the carrier of D,M,f,i)] is set
{( the carrier of D,j,f,i),( the carrier of D,M,f,i)} is non empty finite countable set
{( the carrier of D,j,f,i)} is non empty trivial finite 1 -element countable set
{{( the carrier of D,j,f,i),( the carrier of D,M,f,i)},{( the carrier of D,j,f,i)}} is non empty finite V40() countable set
the addF of D . [( the carrier of D,j,f,i),( the carrier of D,M,f,i)] is set
f is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
i is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
j 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
[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
( the carrier of D,f,j,f) is Element of the carrier of D
( the carrier of D,j,j,f) is Element of the carrier of D
( the carrier of D,M,j,f) is Element of the carrier of D
( the carrier of D,j,j,f) + ( the carrier of D,M,j,f) is Element of the carrier of D
the addF of D is Relation-like Function-like V18([: the carrier of D, the carrier of D:], the carrier of D) Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is Relation-like set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is Relation-like set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is set
the addF of D . (( the carrier of D,j,j,f),( the carrier of D,M,j,f)) is Element of the carrier of D
[( the carrier of D,j,j,f),( the carrier of D,M,j,f)] is set
{( the carrier of D,j,j,f),( the carrier of D,M,j,f)} is non empty finite countable set
{( the carrier of D,j,j,f)} is non empty trivial finite 1 -element countable set
{{( the carrier of D,j,j,f),( the carrier of D,M,j,f)},{( the carrier of D,j,j,f)}} is non empty finite V40() countable set
the addF of D . [( the carrier of D,j,j,f),( the carrier of D,M,j,f)] is set
( the carrier of D,i,j,f) is Element of the carrier of D
(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
[:(Seg i),(Seg i):] is Relation-like finite countable set
D is non empty doubleLoopStr
i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
(D,i) is set
the carrier of D is non empty set
i -tuples_on the carrier of D is functional non empty FinSequence-membered FinSequenceSet of the carrier of D
the carrier of D * is functional non empty FinSequence-membered FinSequenceSet of the carrier of D
{ b₁ where b₁ is Relation-like NAT -defined the carrier of D -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() Element of the carrier of D * : len b₁ = i } is set
i -tuples_on (i -tuples_on the carrier of D) is functional non empty FinSequence-membered FinSequenceSet of i -tuples_on the carrier of D
(i -tuples_on the carrier of D) * is functional non empty FinSequence-membered FinSequenceSet of i -tuples_on the carrier of D
{ b₁ where b₁ is Relation-like NAT -defined i -tuples_on the carrier of D -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() Element of (i -tuples_on the carrier of D) * : len b₁ = i } is 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
[D,i] is set
{D,i} is non empty finite V40() countable set
{D} is non empty trivial finite V40() 1 -element countable set
{{D,i},{D}} is non empty finite V40() countable set
j is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
M is non empty doubleLoopStr
(M,j) is Relation-like NAT -defined the carrier of M * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of M,j,j)
the carrier of M is non empty set
the carrier of M * is functional non empty FinSequence-membered FinSequenceSet of the carrier of M
j -tuples_on the carrier of M is functional non empty FinSequence-membered FinSequenceSet of the carrier of M
{ b₁ where b₁ is Relation-like NAT -defined the carrier of M -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() Element of the carrier of M * : len b₁ = j } is set
0. M is V58(M) Element of the carrier of M
the ZeroF of M is Element of the carrier of M
j |-> (0. M) is Relation-like NAT -defined the carrier of M -valued Function-like finite j -element FinSequence-like FinSubsequence-like countable V172() Element of j -tuples_on the carrier of M
Seg j is finite j -element countable Element of bool NAT
K100((Seg j),(0. M)) is Relation-like NAT -defined Function-like V18( Seg j,{(0. M)}) finite FinSequence-like FinSubsequence-like countable V172() Element of bool [:(Seg j),{(0. M)}:]
{(0. M)} is non empty trivial finite 1 -element countable set
[:(Seg j),{(0. M)}:] is Relation-like finite countable set
bool [:(Seg j),{(0. M)}:] is finite V40() countable set
j |-> (j |-> (0. M)) is Relation-like NAT -defined j -tuples_on the carrier of M -valued Function-like finite j -element FinSequence-like FinSubsequence-like countable V172() Element of j -tuples_on (j -tuples_on the carrier of M)
j -tuples_on (j -tuples_on the carrier of M) is functional non empty FinSequence-membered FinSequenceSet of j -tuples_on the carrier of M
(j -tuples_on the carrier of M) * is functional non empty FinSequence-membered FinSequenceSet of j -tuples_on the carrier of M
{ b₁ where b₁ is Relation-like NAT -defined j -tuples_on the carrier of M -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() Element of (j -tuples_on the carrier of M) * : len b₁ = j } is set
K100((Seg j),(j |-> (0. M))) is Relation-like NAT -defined Function-like V18( Seg j,{(j |-> (0. M))}) finite FinSequence-like FinSubsequence-like countable V172() Element of bool [:(Seg j),{(j |-> (0. M))}:]
{(j |-> (0. M))} is functional non empty trivial finite V40() 1 -element with_common_domain countable set
[:(Seg j),{(j |-> (0. M))}:] is Relation-like finite countable set
bool [:(Seg j),{(j |-> (0. M))}:] is finite V40() countable set
((M,j)) is set
dom (M,j) is finite countable Element of bool NAT
((M,j)) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
Seg ((M,j)) is finite ((M,j)) -element countable Element of bool NAT
[:(dom (M,j)),(Seg ((M,j))):] is Relation-like finite countable set
( the carrier of M,(M,j),D,i) is Element of the carrier of M
[:(Seg j),(Seg j):] is Relation-like finite countable set
f is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
f |-> (0. M) is Relation-like NAT -defined the carrier of M -valued Function-like finite f -element FinSequence-like FinSubsequence-like countable V172() Element of f -tuples_on the carrier of M
f -tuples_on the carrier of M is functional non empty FinSequence-membered FinSequenceSet of the carrier of M
{ b₁ where b₁ is Relation-like NAT -defined the carrier of M -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() Element of the carrier of M * : len b₁ = f } is set
Seg f is finite f -element countable Element of bool NAT
K100((Seg f),(0. M)) is Relation-like NAT -defined Function-like V18( Seg f,{(0. M)}) finite FinSequence-like FinSubsequence-like countable V172() Element of bool [:(Seg f),{(0. M)}:]
[:(Seg f),{(0. M)}:] is Relation-like finite countable set
bool [:(Seg f),{(0. M)}:] is finite V40() countable set
(f |-> (0. M)) . i is set
(M,j) . D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set
D is set
i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
j is non empty doubleLoopStr
(j,i) is non empty set
the carrier of j is non empty set
i -tuples_on the carrier of j is functional non empty FinSequence-membered FinSequenceSet of the carrier of j
the carrier of j * is functional non empty FinSequence-membered FinSequenceSet of the carrier of j
{ b₁ where b₁ is Relation-like NAT -defined the carrier of j -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() Element of the carrier of j * : len b₁ = i } is set
i -tuples_on (i -tuples_on the carrier of j) is functional non empty FinSequence-membered FinSequenceSet of i -tuples_on the carrier of j
(i -tuples_on the carrier of j) * is functional non empty FinSequence-membered FinSequenceSet of i -tuples_on the carrier of j
{ b₁ where b₁ is Relation-like NAT -defined i -tuples_on the carrier of j -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() Element of (i -tuples_on the carrier of j) * : len b₁ = i } is set
M is Relation-like NAT -defined i -tuples_on the carrier of j -valued Function-like finite i -element FinSequence-like FinSubsequence-like countable V172() Element of i -tuples_on (i -tuples_on the carrier of j)
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
i is Relation-like NAT -defined the carrier of j -valued Function-like finite i -element FinSequence-like FinSubsequence-like countable V172() Element of i -tuples_on the carrier of j
j is Relation-like NAT -defined the carrier of j -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() FinSequence of the carrier of j
len j is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
f is Relation-like NAT -defined the carrier of j * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () FinSequence of the carrier of j *
rng f is finite countable set
i is Relation-like NAT -defined the carrier of j -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() FinSequence of the carrier of j
len i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
j is Relation-like NAT -defined the carrier of j -valued Function-like finite i -element FinSequence-like FinSubsequence-like countable V172() Element of i -tuples_on the carrier of j
len j is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
M is Relation-like NAT -defined the carrier of j * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of j,i,i)
len M is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
i -tuples_on ( the carrier of j *) is functional non empty FinSequence-membered FinSequenceSet of the carrier of j *
( the carrier of j *) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of j *
{ b₁ where b₁ is Relation-like NAT -defined the carrier of j * -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() Element of ( the carrier of j *) * : len b₁ = i } is set
f is Relation-like NAT -defined the carrier of j * -valued Function-like V27() finite i -element FinSequence-like FinSubsequence-like countable V171() V172() Element of i -tuples_on ( the carrier of j *)
rng f is finite countable set
i is set
j is Relation-like NAT -defined the carrier of j -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() FinSequence of the carrier of j
len j is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
D is non empty ZeroStr
the carrier of D is non empty set
the carrier of D * is functional non empty FinSequence-membered FinSequenceSet of the carrier of D
i is non empty doubleLoopStr
the carrier of i is non empty set
the carrier of i * is functional non empty FinSequence-membered FinSequenceSet of the carrier of i
D is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
(i,D) is Relation-like NAT -defined the carrier of i * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of i,D,D)
j is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
((i,D)) is set
dom (i,D) is finite countable Element of bool NAT
((i,D)) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
Seg ((i,D)) is finite ((i,D)) -element countable Element of bool NAT
[:(dom (i,D)),(Seg ((i,D))):] is Relation-like finite countable set
0. i is V58(i) Element of the carrier of i
the ZeroF of i is Element of the carrier of i
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
( the carrier of i,(i,D),j,M) is Element of the carrier of i
D is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
i is non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr
the carrier of i is non empty set
the carrier of i * is functional non empty FinSequence-membered FinSequenceSet of the carrier of i
j is Relation-like NAT -defined the carrier of i * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of i,D,D)
M is Relation-like NAT -defined the carrier of i * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of i,D,D)
(i,D,j,M) is Relation-like NAT -defined the carrier of i * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of i,D,D)
(i,D,M,j) is Relation-like NAT -defined the carrier of i * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of 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
((i,D,j,M)) is set
dom (i,D,j,M) is finite countable Element of bool NAT
((i,D,j,M)) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
Seg ((i,D,j,M)) is finite ((i,D,j,M)) -element countable Element of bool NAT
[:(dom (i,D,j,M)),(Seg ((i,D,j,M))):] is Relation-like finite countable set
(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
( the carrier of i,(i,D,j,M),f,i) is Element of the carrier of i
( the carrier of i,j,f,i) is Element of the carrier of i
( the carrier of i,M,f,i) is Element of the carrier of i
( the carrier of i,j,f,i) + ( the carrier of i,M,f,i) is Element of the carrier of i
the addF of i is Relation-like Function-like V18([: the carrier of i, the carrier of i:], the carrier of i) Element of bool [:[: the carrier of i, the carrier of i:], the carrier of i:]
[: the carrier of i, the carrier of i:] is Relation-like set
[:[: the carrier of i, the carrier of i:], the carrier of i:] is Relation-like set
bool [:[: the carrier of i, the carrier of i:], the carrier of i:] is set
the addF of i . (( the carrier of i,j,f,i),( the carrier of i,M,f,i)) is Element of the carrier of i
[( the carrier of i,j,f,i),( the carrier of i,M,f,i)] is set
{( the carrier of i,j,f,i),( the carrier of i,M,f,i)} is non empty finite countable set
{( the carrier of i,j,f,i)} is non empty trivial finite 1 -element countable set
{{( the carrier of i,j,f,i),( the carrier of i,M,f,i)},{( the carrier of i,j,f,i)}} is non empty finite V40() countable set
the addF of i . [( the carrier of i,j,f,i),( the carrier of i,M,f,i)] is set
( the carrier of i,(i,D,M,j),f,i) is Element of the carrier of i
D is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
i is non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr
the carrier of i is non empty set
the carrier of i * is functional non empty FinSequence-membered FinSequenceSet of the carrier of i
j is Relation-like NAT -defined the carrier of i * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of i,D,D)
M is Relation-like NAT -defined the carrier of i * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of i,D,D)
(i,D,j,M) is Relation-like NAT -defined the carrier of i * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of i,D,D)
f is Relation-like NAT -defined the carrier of i * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of i,D,D)
(i,D,(i,D,j,M),f) is Relation-like NAT -defined the carrier of i * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of i,D,D)
(i,D,M,f) is Relation-like NAT -defined the carrier of i * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of i,D,D)
(i,D,j,(i,D,M,f)) is Relation-like NAT -defined the carrier of i * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of 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
((i,D,(i,D,j,M),f)) is set
dom (i,D,(i,D,j,M),f) is finite countable Element of bool NAT
((i,D,(i,D,j,M),f)) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
Seg ((i,D,(i,D,j,M),f)) is finite ((i,D,(i,D,j,M),f)) -element countable Element of bool NAT
[:(dom (i,D,(i,D,j,M),f)),(Seg ((i,D,(i,D,j,M),f))):] is Relation-like finite countable set
((i,D,j,M)) is set
dom (i,D,j,M) is finite countable Element of bool NAT
((i,D,j,M)) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
Seg ((i,D,j,M)) is finite ((i,D,j,M)) -element countable Element of bool NAT
[:(dom (i,D,j,M)),(Seg ((i,D,j,M))):] is Relation-like finite countable set
(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
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
( the carrier of i,(i,D,(i,D,j,M),f),i,j) is Element of the carrier of i
( the carrier of i,(i,D,j,M),i,j) is Element of the carrier of i
( the carrier of i,f,i,j) is Element of the carrier of i
( the carrier of i,(i,D,j,M),i,j) + ( the carrier of i,f,i,j) is Element of the carrier of i
the addF of i is Relation-like Function-like V18([: the carrier of i, the carrier of i:], the carrier of i) Element of bool [:[: the carrier of i, the carrier of i:], the carrier of i:]
[: the carrier of i, the carrier of i:] is Relation-like set
[:[: the carrier of i, the carrier of i:], the carrier of i:] is Relation-like set
bool [:[: the carrier of i, the carrier of i:], the carrier of i:] is set
the addF of i . (( the carrier of i,(i,D,j,M),i,j),( the carrier of i,f,i,j)) is Element of the carrier of i
[( the carrier of i,(i,D,j,M),i,j),( the carrier of i,f,i,j)] is set
{( the carrier of i,(i,D,j,M),i,j),( the carrier of i,f,i,j)} is non empty finite countable set
{( the carrier of i,(i,D,j,M),i,j)} is non empty trivial finite 1 -element countable set
{{( the carrier of i,(i,D,j,M),i,j),( the carrier of i,f,i,j)},{( the carrier of i,(i,D,j,M),i,j)}} is non empty finite V40() countable set
the addF of i . [( the carrier of i,(i,D,j,M),i,j),( the carrier of i,f,i,j)] is set
( the carrier of i,j,i,j) is Element of the carrier of i
( the carrier of i,M,i,j) is Element of the carrier of i
( the carrier of i,j,i,j) + ( the carrier of i,M,i,j) is Element of the carrier of i
the addF of i . (( the carrier of i,j,i,j),( the carrier of i,M,i,j)) is Element of the carrier of i
[( the carrier of i,j,i,j),( the carrier of i,M,i,j)] is set
{( the carrier of i,j,i,j),( the carrier of i,M,i,j)} is non empty finite countable set
{( the carrier of i,j,i,j)} is non empty trivial finite 1 -element countable set
{{( the carrier of i,j,i,j),( the carrier of i,M,i,j)},{( the carrier of i,j,i,j)}} is non empty finite V40() countable set
the addF of i . [( the carrier of i,j,i,j),( the carrier of i,M,i,j)] is set
(( the carrier of i,j,i,j) + ( the carrier of i,M,i,j)) + ( the carrier of i,f,i,j) is Element of the carrier of i
the addF of i . ((( the carrier of i,j,i,j) + ( the carrier of i,M,i,j)),( the carrier of i,f,i,j)) is Element of the carrier of i
[(( the carrier of i,j,i,j) + ( the carrier of i,M,i,j)),( the carrier of i,f,i,j)] is set
{(( the carrier of i,j,i,j) + ( the carrier of i,M,i,j)),( the carrier of i,f,i,j)} is non empty finite countable set
{(( the carrier of i,j,i,j) + ( the carrier of i,M,i,j))} is non empty trivial finite 1 -element countable set
{{(( the carrier of i,j,i,j) + ( the carrier of i,M,i,j)),( the carrier of i,f,i,j)},{(( the carrier of i,j,i,j) + ( the carrier of i,M,i,j))}} is non empty finite V40() countable set
the addF of i . [(( the carrier of i,j,i,j) + ( the carrier of i,M,i,j)),( the carrier of i,f,i,j)] is set
( the carrier of i,M,i,j) + ( the carrier of i,f,i,j) is Element of the carrier of i
the addF of i . (( the carrier of i,M,i,j),( the carrier of i,f,i,j)) is Element of the carrier of i
[( the carrier of i,M,i,j),( the carrier of i,f,i,j)] is set
{( the carrier of i,M,i,j),( the carrier of i,f,i,j)} is non empty finite countable set
{( the carrier of i,M,i,j)} is non empty trivial finite 1 -element countable set
{{( the carrier of i,M,i,j),( the carrier of i,f,i,j)},{( the carrier of i,M,i,j)}} is non empty finite V40() countable set
the addF of i . [( the carrier of i,M,i,j),( the carrier of i,f,i,j)] is set
( the carrier of i,j,i,j) + (( the carrier of i,M,i,j) + ( the carrier of i,f,i,j)) is Element of the carrier of i
the addF of i . (( the carrier of i,j,i,j),(( the carrier of i,M,i,j) + ( the carrier of i,f,i,j))) is Element of the carrier of i
[( the carrier of i,j,i,j),(( the carrier of i,M,i,j) + ( the carrier of i,f,i,j))] is set
{( the carrier of i,j,i,j),(( the carrier of i,M,i,j) + ( the carrier of i,f,i,j))} is non empty finite countable set
{{( the carrier of i,j,i,j),(( the carrier of i,M,i,j) + ( the carrier of i,f,i,j))},{( the carrier of i,j,i,j)}} is non empty finite V40() countable set
the addF of i . [( the carrier of i,j,i,j),(( the carrier of i,M,i,j) + ( the carrier of i,f,i,j))] is set
( the carrier of i,(i,D,M,f),i,j) is Element of the carrier of i
( the carrier of i,j,i,j) + ( the carrier of i,(i,D,M,f),i,j) is Element of the carrier of i
the addF of i . (( the carrier of i,j,i,j),( the carrier of i,(i,D,M,f),i,j)) is Element of the carrier of i
[( the carrier of i,j,i,j),( the carrier of i,(i,D,M,f),i,j)] is set
{( the carrier of i,j,i,j),( the carrier of i,(i,D,M,f),i,j)} is non empty finite countable set
{{( the carrier of i,j,i,j),( the carrier of i,(i,D,M,f),i,j)},{( the carrier of i,j,i,j)}} is non empty finite V40() countable set
the addF of i . [( the carrier of i,j,i,j),( the carrier of i,(i,D,M,f),i,j)] is set
( the carrier of i,(i,D,j,(i,D,M,f)),i,j) is Element of the carrier of i
D is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
i is non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr
the carrier of i is non empty set
the carrier of i * is functional non empty FinSequence-membered FinSequenceSet of the carrier of i
(i,D) is Relation-like NAT -defined the carrier of i * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of i,D,D)
D -tuples_on the carrier of i is functional non empty FinSequence-membered FinSequenceSet of the carrier of i
{ b₁ where b₁ is Relation-like NAT -defined the carrier of i -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() Element of the carrier of i * : len b₁ = D } is set
0. i is V58(i) Element of the carrier of i
the ZeroF of i is Element of the carrier of i
D |-> (0. i) is Relation-like NAT -defined the carrier of i -valued Function-like finite D -element FinSequence-like FinSubsequence-like countable V172() Element of D -tuples_on the carrier of i
Seg D is finite D -element countable Element of bool NAT
K100((Seg D),(0. i)) is Relation-like NAT -defined Function-like V18( Seg D,{(0. i)}) finite FinSequence-like FinSubsequence-like countable V172() Element of bool [:(Seg D),{(0. i)}:]
{(0. i)} is non empty trivial finite 1 -element countable set
[:(Seg D),{(0. i)}:] is Relation-like finite countable set
bool [:(Seg D),{(0. i)}:] is finite V40() countable set
D |-> (D |-> (0. i)) is Relation-like NAT -defined D -tuples_on the carrier of i -valued Function-like finite D -element FinSequence-like FinSubsequence-like countable V172() Element of D -tuples_on (D -tuples_on the carrier of i)
D -tuples_on (D -tuples_on the carrier of i) is functional non empty FinSequence-membered FinSequenceSet of D -tuples_on the carrier of i
(D -tuples_on the carrier of i) * is functional non empty FinSequence-membered FinSequenceSet of D -tuples_on the carrier of i
{ b₁ where b₁ is Relation-like NAT -defined D -tuples_on the carrier of i -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() Element of (D -tuples_on the carrier of i) * : len b₁ = D } is set
K100((Seg D),(D |-> (0. i))) is Relation-like NAT -defined Function-like V18( Seg D,{(D |-> (0. i))}) finite FinSequence-like FinSubsequence-like countable V172() Element of bool [:(Seg D),{(D |-> (0. i))}:]
{(D |-> (0. i))} is functional non empty trivial finite V40() 1 -element with_common_domain countable set
[:(Seg D),{(D |-> (0. i))}:] is Relation-like finite countable set
bool [:(Seg D),{(D |-> (0. i))}:] is finite V40() countable set
j is Relation-like NAT -defined the carrier of i * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of i,D,D)
(i,D,j,(i,D)) is Relation-like NAT -defined the carrier of i * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of 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
((i,D,j,(i,D))) is set
dom (i,D,j,(i,D)) is finite countable Element of bool NAT
((i,D,j,(i,D))) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
Seg ((i,D,j,(i,D))) is finite ((i,D,j,(i,D))) -element countable Element of bool NAT
[:(dom (i,D,j,(i,D))),(Seg ((i,D,j,(i,D)))):] is Relation-like finite countable set
((i,D)) is set
dom (i,D) is finite countable Element of bool NAT
((i,D)) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
Seg ((i,D)) is finite ((i,D)) -element countable Element of bool NAT
[:(dom (i,D)),(Seg ((i,D))):] 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
( the carrier of i,(i,D,j,(i,D)),M,f) is Element of the carrier of i
( the carrier of i,j,M,f) is Element of the carrier of i
( the carrier of i,(i,D),M,f) is Element of the carrier of i
( the carrier of i,j,M,f) + ( the carrier of i,(i,D),M,f) is Element of the carrier of i
the addF of i is Relation-like Function-like V18([: the carrier of i, the carrier of i:], the carrier of i) Element of bool [:[: the carrier of i, the carrier of i:], the carrier of i:]
[: the carrier of i, the carrier of i:] is Relation-like set
[:[: the carrier of i, the carrier of i:], the carrier of i:] is Relation-like set
bool [:[: the carrier of i, the carrier of i:], the carrier of i:] is set
the addF of i . (( the carrier of i,j,M,f),( the carrier of i,(i,D),M,f)) is Element of the carrier of i
[( the carrier of i,j,M,f),( the carrier of i,(i,D),M,f)] is set
{( the carrier of i,j,M,f),( the carrier of i,(i,D),M,f)} is non empty finite countable set
{( the carrier of i,j,M,f)} is non empty trivial finite 1 -element countable set
{{( the carrier of i,j,M,f),( the carrier of i,(i,D),M,f)},{( the carrier of i,j,M,f)}} is non empty finite V40() countable set
the addF of i . [( the carrier of i,j,M,f),( the carrier of i,(i,D),M,f)] is set
( the carrier of i,j,M,f) + (0. i) is Element of the carrier of i
the addF of i . (( the carrier of i,j,M,f),(0. i)) is Element of the carrier of i
[( the carrier of i,j,M,f),(0. i)] is set
{( the carrier of i,j,M,f),(0. i)} is non empty finite countable set
{{( the carrier of i,j,M,f),(0. i)},{( the carrier of i,j,M,f)}} is non empty finite V40() countable set
the addF of i . [( the carrier of i,j,M,f),(0. i)] is set
D is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
i is non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr
the carrier of i is non empty set
the carrier of i * is functional non empty FinSequence-membered FinSequenceSet of the carrier of i
(i,D) is Relation-like NAT -defined the carrier of i * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of i,D,D)
D -tuples_on the carrier of i is functional non empty FinSequence-membered FinSequenceSet of the carrier of i
{ b₁ where b₁ is Relation-like NAT -defined the carrier of i -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() Element of the carrier of i * : len b₁ = D } is set
0. i is V58(i) Element of the carrier of i
the ZeroF of i is Element of the carrier of i
D |-> (0. i) is Relation-like NAT -defined the carrier of i -valued Function-like finite D -element FinSequence-like FinSubsequence-like countable V172() Element of D -tuples_on the carrier of i
Seg D is finite D -element countable Element of bool NAT
K100((Seg D),(0. i)) is Relation-like NAT -defined Function-like V18( Seg D,{(0. i)}) finite FinSequence-like FinSubsequence-like countable V172() Element of bool [:(Seg D),{(0. i)}:]
{(0. i)} is non empty trivial finite 1 -element countable set
[:(Seg D),{(0. i)}:] is Relation-like finite countable set
bool [:(Seg D),{(0. i)}:] is finite V40() countable set
D |-> (D |-> (0. i)) is Relation-like NAT -defined D -tuples_on the carrier of i -valued Function-like finite D -element FinSequence-like FinSubsequence-like countable V172() Element of D -tuples_on (D -tuples_on the carrier of i)
D -tuples_on (D -tuples_on the carrier of i) is functional non empty FinSequence-membered FinSequenceSet of D -tuples_on the carrier of i
(D -tuples_on the carrier of i) * is functional non empty FinSequence-membered FinSequenceSet of D -tuples_on the carrier of i
{ b₁ where b₁ is Relation-like NAT -defined D -tuples_on the carrier of i -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() Element of (D -tuples_on the carrier of i) * : len b₁ = D } is set
K100((Seg D),(D |-> (0. i))) is Relation-like NAT -defined Function-like V18( Seg D,{(D |-> (0. i))}) finite FinSequence-like FinSubsequence-like countable V172() Element of bool [:(Seg D),{(D |-> (0. i))}:]
{(D |-> (0. i))} is functional non empty trivial finite V40() 1 -element with_common_domain countable set
[:(Seg D),{(D |-> (0. i))}:] is Relation-like finite countable set
bool [:(Seg D),{(D |-> (0. i))}:] is finite V40() countable set
j is Relation-like NAT -defined the carrier of i * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of i,D,D)
(i,D,j) is Relation-like NAT -defined the carrier of i * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of i,D,D)
(i,D,j,(i,D,j)) is Relation-like NAT -defined the carrier of i * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of 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
((i,D,j,(i,D,j))) is set
dom (i,D,j,(i,D,j)) is finite countable Element of bool NAT
((i,D,j,(i,D,j))) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
Seg ((i,D,j,(i,D,j))) is finite ((i,D,j,(i,D,j))) -element countable Element of bool NAT
[:(dom (i,D,j,(i,D,j))),(Seg ((i,D,j,(i,D,j)))):] is Relation-like finite countable set
((i,D)) is set
dom (i,D) is finite countable Element of bool NAT
((i,D)) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
Seg ((i,D)) is finite ((i,D)) -element countable Element of bool NAT
[:(dom (i,D)),(Seg ((i,D))):] 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
( the carrier of i,(i,D,j,(i,D,j)),M,f) is Element of the carrier of i
( the carrier of i,j,M,f) is Element of the carrier of i
( the carrier of i,(i,D,j),M,f) is Element of the carrier of i
( the carrier of i,j,M,f) + ( the carrier of i,(i,D,j),M,f) is Element of the carrier of i
the addF of i is Relation-like Function-like V18([: the carrier of i, the carrier of i:], the carrier of i) Element of bool [:[: the carrier of i, the carrier of i:], the carrier of i:]
[: the carrier of i, the carrier of i:] is Relation-like set
[:[: the carrier of i, the carrier of i:], the carrier of i:] is Relation-like set
bool [:[: the carrier of i, the carrier of i:], the carrier of i:] is set
the addF of i . (( the carrier of i,j,M,f),( the carrier of i,(i,D,j),M,f)) is Element of the carrier of i
[( the carrier of i,j,M,f),( the carrier of i,(i,D,j),M,f)] is set
{( the carrier of i,j,M,f),( the carrier of i,(i,D,j),M,f)} is non empty finite countable set
{( the carrier of i,j,M,f)} is non empty trivial finite 1 -element countable set
{{( the carrier of i,j,M,f),( the carrier of i,(i,D,j),M,f)},{( the carrier of i,j,M,f)}} is non empty finite V40() countable set
the addF of i . [( the carrier of i,j,M,f),( the carrier of i,(i,D,j),M,f)] is set
- ( the carrier of i,j,M,f) is Element of the carrier of i
( the carrier of i,j,M,f) + (- ( the carrier of i,j,M,f)) is Element of the carrier of i
the addF of i . (( the carrier of i,j,M,f),(- ( the carrier of i,j,M,f))) is Element of the carrier of i
[( the carrier of i,j,M,f),(- ( the carrier of i,j,M,f))] is set
{( the carrier of i,j,M,f),(- ( the carrier of i,j,M,f))} is non empty finite countable set
{{( the carrier of i,j,M,f),(- ( the carrier of i,j,M,f))},{( the carrier of i,j,M,f)}} is non empty finite V40() countable set
the addF of i . [( the carrier of i,j,M,f),(- ( the carrier of i,j,M,f))] is set
( the carrier of i,(i,D),M,f) is Element of the carrier of i
D is non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr
i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
(D,i) is non empty set
the carrier of D is non empty set
i -tuples_on the carrier of D is functional non empty FinSequence-membered FinSequenceSet of the carrier of D
the carrier of D * is functional non empty FinSequence-membered FinSequenceSet of the carrier of D
{ b₁ where b₁ is Relation-like NAT -defined the carrier of D -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() Element of the carrier of D * : len b₁ = i } is set
i -tuples_on (i -tuples_on the carrier of D) is functional non empty FinSequence-membered FinSequenceSet of i -tuples_on the carrier of D
(i -tuples_on the carrier of D) * is functional non empty FinSequence-membered FinSequenceSet of i -tuples_on the carrier of D
{ b₁ where b₁ is Relation-like NAT -defined i -tuples_on the carrier of D -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() Element of (i -tuples_on the carrier of D) * : len b₁ = i } is set
(D,i) is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
0. D is V58(D) Element of the carrier of D
the ZeroF of D is Element of the carrier of D
i |-> (0. D) is Relation-like NAT -defined the carrier of D -valued Function-like finite i -element FinSequence-like FinSubsequence-like countable V172() Element of i -tuples_on the carrier of D
Seg i is finite i -element countable Element of bool NAT
K100((Seg i),(0. D)) is Relation-like NAT -defined Function-like V18( Seg i,{(0. D)}) finite FinSequence-like FinSubsequence-like countable V172() Element of bool [:(Seg i),{(0. D)}:]
{(0. D)} is non empty trivial finite 1 -element countable set
[:(Seg i),{(0. D)}:] is Relation-like finite countable set
bool [:(Seg i),{(0. D)}:] is finite V40() countable set
i |-> (i |-> (0. D)) is Relation-like NAT -defined i -tuples_on the carrier of D -valued Function-like finite i -element FinSequence-like FinSubsequence-like countable V172() Element of i -tuples_on (i -tuples_on the carrier of D)
K100((Seg i),(i |-> (0. D))) is Relation-like NAT -defined Function-like V18( Seg i,{(i |-> (0. D))}) finite FinSequence-like FinSubsequence-like countable V172() Element of bool [:(Seg i),{(i |-> (0. D))}:]
{(i |-> (0. D))} is functional non empty trivial finite V40() 1 -element with_common_domain countable set
[:(Seg i),{(i |-> (0. D))}:] is Relation-like finite countable set
bool [:(Seg i),{(i |-> (0. D))}:] is finite V40() countable set
M is Element of (D,i)
f is Element of (D,i)
j is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
i is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
(D,i,j,i) is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
f is Element of (D,i)
[:(D,i),(D,i):] is Relation-like set
[:[:(D,i),(D,i):],(D,i):] is Relation-like set
bool [:[:(D,i),(D,i):],(D,i):] is set
M is Relation-like Function-like V18([:(D,i),(D,i):],(D,i)) Element of bool [:[:(D,i),(D,i):],(D,i):]
j is Element of (D,i)
addLoopStr(# (D,i),M,j #) is strict addLoopStr
i is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
j is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
M . (i,j) is set
[i,j] is set
{i,j} is functional non empty finite V40() countable set
{i} is functional non empty trivial finite V40() 1 -element with_common_domain countable set
{{i,j},{i}} is non empty finite V40() countable set
M . [i,j] is set
(D,i,i,j) is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
f is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
i is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
(D,i,f,i) is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
i is Element of (D,i)
j is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
(D,i,j) is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
f is Element of (D,i)
the carrier of addLoopStr(# (D,i),M,j #) is set
i is Element of the carrier of addLoopStr(# (D,i),M,j #)
j is Element of the carrier of addLoopStr(# (D,i),M,j #)
i + j is Element of the carrier of addLoopStr(# (D,i),M,j #)
the addF of addLoopStr(# (D,i),M,j #) is Relation-like Function-like V18([: the carrier of addLoopStr(# (D,i),M,j #), the carrier of addLoopStr(# (D,i),M,j #):], the carrier of addLoopStr(# (D,i),M,j #)) Element of bool [:[: the carrier of addLoopStr(# (D,i),M,j #), the carrier of addLoopStr(# (D,i),M,j #):], the carrier of addLoopStr(# (D,i),M,j #):]
[: the carrier of addLoopStr(# (D,i),M,j #), the carrier of addLoopStr(# (D,i),M,j #):] is Relation-like set
[:[: the carrier of addLoopStr(# (D,i),M,j #), the carrier of addLoopStr(# (D,i),M,j #):], the carrier of addLoopStr(# (D,i),M,j #):] is Relation-like set
bool [:[: the carrier of addLoopStr(# (D,i),M,j #), the carrier of addLoopStr(# (D,i),M,j #):], the carrier of addLoopStr(# (D,i),M,j #):] is set
the addF of addLoopStr(# (D,i),M,j #) . (i,j) is Element of the carrier of addLoopStr(# (D,i),M,j #)
[i,j] is set
{i,j} is non empty finite countable set
{i} is non empty trivial finite 1 -element countable set
{{i,j},{i}} is non empty finite V40() countable set
the addF of addLoopStr(# (D,i),M,j #) . [i,j] is set
j + i is Element of the carrier of addLoopStr(# (D,i),M,j #)
the addF of addLoopStr(# (D,i),M,j #) . (j,i) is Element of the carrier of addLoopStr(# (D,i),M,j #)
[j,i] is set
{j,i} is non empty finite countable set
{j} is non empty trivial finite 1 -element countable set
{{j,i},{j}} is non empty finite V40() countable set
the addF of addLoopStr(# (D,i),M,j #) . [j,i] is set
f is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
i is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
(D,i,f,i) is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
(D,i,i,f) is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
the carrier of addLoopStr(# (D,i),M,j #) is set
i is Element of the carrier of addLoopStr(# (D,i),M,j #)
j is Element of the carrier of addLoopStr(# (D,i),M,j #)
f is Element of the carrier of addLoopStr(# (D,i),M,j #)
i + j is Element of the carrier of addLoopStr(# (D,i),M,j #)
the addF of addLoopStr(# (D,i),M,j #) is Relation-like Function-like V18([: the carrier of addLoopStr(# (D,i),M,j #), the carrier of addLoopStr(# (D,i),M,j #):], the carrier of addLoopStr(# (D,i),M,j #)) Element of bool [:[: the carrier of addLoopStr(# (D,i),M,j #), the carrier of addLoopStr(# (D,i),M,j #):], the carrier of addLoopStr(# (D,i),M,j #):]
[: the carrier of addLoopStr(# (D,i),M,j #), the carrier of addLoopStr(# (D,i),M,j #):] is Relation-like set
[:[: the carrier of addLoopStr(# (D,i),M,j #), the carrier of addLoopStr(# (D,i),M,j #):], the carrier of addLoopStr(# (D,i),M,j #):] is Relation-like set
bool [:[: the carrier of addLoopStr(# (D,i),M,j #), the carrier of addLoopStr(# (D,i),M,j #):], the carrier of addLoopStr(# (D,i),M,j #):] is set
the addF of addLoopStr(# (D,i),M,j #) . (i,j) is Element of the carrier of addLoopStr(# (D,i),M,j #)
[i,j] is set
{i,j} is non empty finite countable set
{i} is non empty trivial finite 1 -element countable set
{{i,j},{i}} is non empty finite V40() countable set
the addF of addLoopStr(# (D,i),M,j #) . [i,j] is set
(i + j) + f is Element of the carrier of addLoopStr(# (D,i),M,j #)
the addF of addLoopStr(# (D,i),M,j #) . ((i + j),f) is Element of the carrier of addLoopStr(# (D,i),M,j #)
[(i + j),f] is set
{(i + j),f} is non empty finite countable set
{(i + j)} is non empty trivial finite 1 -element countable set
{{(i + j),f},{(i + j)}} is non empty finite V40() countable set
the addF of addLoopStr(# (D,i),M,j #) . [(i + j),f] is set
i is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
i is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
(D,i,i,i) is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
j is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
M . ((D,i,i,i),j) is set
[(D,i,i,i),j] is set
{(D,i,i,i),j} is functional non empty finite V40() countable set
{(D,i,i,i)} is functional non empty trivial finite V40() 1 -element with_common_domain countable set
{{(D,i,i,i),j},{(D,i,i,i)}} is non empty finite V40() countable set
M . [(D,i,i,i),j] is set
(D,i,(D,i,i,i),j) is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
(D,i,i,j) is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
(D,i,i,(D,i,i,j)) is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
M . (i,(D,i,i,j)) is set
[i,(D,i,i,j)] is set
{i,(D,i,i,j)} is functional non empty finite V40() countable set
{i} is functional non empty trivial finite V40() 1 -element with_common_domain countable set
{{i,(D,i,i,j)},{i}} is non empty finite V40() countable set
M . [i,(D,i,i,j)] is set
j + f is Element of the carrier of addLoopStr(# (D,i),M,j #)
the addF of addLoopStr(# (D,i),M,j #) . (j,f) is Element of the carrier of addLoopStr(# (D,i),M,j #)
[j,f] is set
{j,f} is non empty finite countable set
{j} is non empty trivial finite 1 -element countable set
{{j,f},{j}} is non empty finite V40() countable set
the addF of addLoopStr(# (D,i),M,j #) . [j,f] is set
i + (j + f) is Element of the carrier of addLoopStr(# (D,i),M,j #)
the addF of addLoopStr(# (D,i),M,j #) . (i,(j + f)) is Element of the carrier of addLoopStr(# (D,i),M,j #)
[i,(j + f)] is set
{i,(j + f)} is non empty finite countable set
{{i,(j + f)},{i}} is non empty finite V40() countable set
the addF of addLoopStr(# (D,i),M,j #) . [i,(j + f)] is set
i is Element of the carrier of addLoopStr(# (D,i),M,j #)
0. addLoopStr(# (D,i),M,j #) is V58( addLoopStr(# (D,i),M,j #)) Element of the carrier of addLoopStr(# (D,i),M,j #)
the ZeroF of addLoopStr(# (D,i),M,j #) is Element of the carrier of addLoopStr(# (D,i),M,j #)
i + (0. addLoopStr(# (D,i),M,j #)) is Element of the carrier of addLoopStr(# (D,i),M,j #)
the addF of addLoopStr(# (D,i),M,j #) . (i,(0. addLoopStr(# (D,i),M,j #))) is Element of the carrier of addLoopStr(# (D,i),M,j #)
[i,(0. addLoopStr(# (D,i),M,j #))] is set
{i,(0. addLoopStr(# (D,i),M,j #))} is non empty finite countable set
{i} is non empty trivial finite 1 -element countable set
{{i,(0. addLoopStr(# (D,i),M,j #))},{i}} is non empty finite V40() countable set
the addF of addLoopStr(# (D,i),M,j #) . [i,(0. addLoopStr(# (D,i),M,j #))] is set
j is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
(D,i,j,(D,i)) is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
i is Element of the carrier of addLoopStr(# (D,i),M,j #)
j is Element of (D,i)
f is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
(D,i,f) is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
f is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
(D,i,f) is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
i is Element of the carrier of addLoopStr(# (D,i),M,j #)
i + i is Element of the carrier of addLoopStr(# (D,i),M,j #)
the addF of addLoopStr(# (D,i),M,j #) . (i,i) is Element of the carrier of addLoopStr(# (D,i),M,j #)
[i,i] is set
{i,i} is non empty finite countable set
{i} is non empty trivial finite 1 -element countable set
{{i,i},{i}} is non empty finite V40() countable set
the addF of addLoopStr(# (D,i),M,j #) . [i,i] is set
(D,i,f,(D,i,f)) is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
i is non empty strict right_complementable Abelian add-associative right_zeroed addLoopStr
the carrier of i is non empty set
the addF of i is Relation-like Function-like V18([: the carrier of i, the carrier of i:], the carrier of i) Element of bool [:[: the carrier of i, the carrier of i:], the carrier of i:]
[: the carrier of i, the carrier of i:] is Relation-like set
[:[: the carrier of i, the carrier of i:], the carrier of i:] is Relation-like set
bool [:[: the carrier of i, the carrier of i:], the carrier of i:] is set
0. i is V58(i) Element of the carrier of i
the ZeroF of i is Element of the carrier of i
j is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
f is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
the addF of i . (j,f) is set
[j,f] is set
{j,f} is functional non empty finite V40() countable set
{j} is functional non empty trivial finite V40() 1 -element with_common_domain countable set
{{j,f},{j}} is non empty finite V40() countable set
the addF of i . [j,f] is set
(D,i,j,f) is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
j is non empty strict right_complementable Abelian add-associative right_zeroed addLoopStr
the carrier of j is non empty set
the addF of j is Relation-like Function-like V18([: the carrier of j, the carrier of j:], the carrier of j) Element of bool [:[: the carrier of j, the carrier of j:], the carrier of j:]
[: the carrier of j, the carrier of j:] is Relation-like set
[:[: the carrier of j, the carrier of j:], the carrier of j:] is Relation-like set
bool [:[: the carrier of j, the carrier of j:], the carrier of j:] is set
0. j is V58(j) Element of the carrier of j
the ZeroF of j is Element of the carrier of j
M is non empty strict right_complementable Abelian add-associative right_zeroed addLoopStr
the carrier of M is non empty set
the addF of M is Relation-like Function-like V18([: the carrier of M, the carrier of M:], the carrier of M) Element of bool [:[: the carrier of M, the carrier of M:], the carrier of M:]
[: the carrier of M, the carrier of M:] is Relation-like set
[:[: the carrier of M, the carrier of M:], the carrier of M:] is Relation-like set
bool [:[: the carrier of M, the carrier of M:], the carrier of M:] is set
0. M is V58(M) Element of the carrier of M
the ZeroF of M is Element of the carrier of M
f is Element of the carrier of j
i is Element of the carrier of j
the addF of j . (f,i) is Element of the carrier of j
[f,i] is set
{f,i} is non empty finite countable set
{f} is non empty trivial finite 1 -element countable set
{{f,i},{f}} is non empty finite V40() countable set
the addF of j . [f,i] is set
j is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
f is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
(D,i,j,f) is Relation-like NAT -defined the carrier of D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of D,i,i)
the addF of M . (f,i) is set
the addF of M . [f,i] is 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 doubleLoopStr
the carrier of j is non empty set
the carrier of j * is functional non empty FinSequence-membered FinSequenceSet of the carrier of j
M is Relation-like NAT -defined the carrier of j * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of j, {} ,D)
f is Relation-like NAT -defined the carrier of j * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () ( the carrier of j, {} ,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
D is 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
[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
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 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
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 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
f is non empty set
f * is functional non empty FinSequence-membered FinSequenceSet of f
i is Relation-like NAT -defined f * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () (f,D,i)
(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
len i 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 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
len D is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
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
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 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
f is non empty set
f * is functional non empty FinSequence-membered FinSequenceSet of f
i is Relation-like NAT -defined f * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () (f,D,i)
(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
len i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
D is Relation-like Function-like set
rngs D is Relation-like Function-like set
Union (rngs D) 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() FinSequence of i *
j . D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set
dom j is finite countable Element of bool NAT
<*> 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
dom j is finite countable Element of bool NAT
rng j is finite countable set
dom j is finite countable Element of bool 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 *
(i) is set
rngs i is Relation-like Function-like set
Union (rngs i) is set
rng i is finite countable set
{ (rng b₁) where b₁ is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() Element of D * : b₁ in rng i } is set
union { (rng b₁) where b₁ is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() Element of D * : b₁ in rng i } is set
rng (rngs i) is set
union (rng (rngs i)) is set
M is set
f is set
dom (rngs i) is set
i is set
(rngs i) . i is set
dom i is finite countable Element of bool NAT
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 finite FinSequence-like FinSubsequence-like countable V172() set
f is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() FinSequence of D
rng f is finite countable set
f is set
i is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() Element of D *
rng i is finite countable set
j is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
i . j is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set
(rngs i) . j 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 *
(i) is set
rngs i is Relation-like Function-like set
Union (rngs i) is set
rng i is finite countable set
{ H₁(b₁) where b₁ is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() Element of D * : b₁ in rng i } is set
M is set
f is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() Element of D *
rng f is finite countable set
union { H₁(b₁) where b₁ is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() Element of D * : b₁ in rng i } 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 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 V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () FinSequence of i *
dom M is finite countable Element of bool NAT
M . D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set
(M) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
len M is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
rng M is finite countable 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 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
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 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
[D,i] is set
{D,i} is non empty finite V40() countable set
{D} is non empty trivial finite V40() 1 -element countable set
{{D,i},{D}} is non empty finite V40() 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 finite FinSequence-like FinSubsequence-like countable V172() FinSequence of j
dom M is finite countable Element of bool NAT
f is Relation-like NAT -defined j * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () FinSequence of j *
dom f is finite countable Element of bool NAT
f . D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set
(f) is set
(f) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
Seg (f) is finite (f) -element countable Element of bool NAT
[:(dom f),(Seg (f)):] is Relation-like finite countable set
len 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 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 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
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
[D,i] is set
{D,i} is non empty finite V40() countable set
{D} is non empty trivial finite V40() 1 -element countable set
{{D,i},{D}} is non empty finite V40() 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 finite FinSequence-like FinSubsequence-like countable V172() FinSequence of j
len M is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
dom M is finite countable Element of bool NAT
f is Relation-like NAT -defined j * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() () FinSequence of j *
(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
f . D 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 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 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
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 finite countable set
rngs i is Relation-like Function-like set
Union (rngs i) is set
(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
{ (D,i,b₁,b₂) where b₁, b₂ is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT : [b₁,b₂] in (i) } is set
rng i is finite countable set
{ (rng b₁) where b₁ is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() Element of D * : b₁ in rng i } is set
union { (rng b₁) where b₁ is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() Element of D * : b₁ in rng i } is set
f is set
i is set
j is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() Element of D *
rng j is finite countable 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 set
i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() set
i . i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set
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
[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 . i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set
(D,i,i,j) is Element of D
c₁₂ is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() FinSequence of D
c₁₂ . j is set
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
(D,i,i,j) is Element of D
[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 . i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set
f is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() FinSequence of D
f . j is set
dom f is finite countable Element of bool NAT
rng f is 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 finite countable set
rngs i is Relation-like Function-like set
Union (rngs i) is set
card (i) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
len i is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
(i) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
(len i) * (i) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
j is set
dom (rngs i) is set
dom i is finite countable Element of bool NAT
M is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
i . M is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() set
f is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like countable V172() FinSequence of D
rng f is finite countable set
card (rng f) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
dom f is finite countable Element of bool NAT
card (dom f) 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 (len f) is finite len f -element countable Element of bool NAT
card (Seg (len f)) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
card (len f) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
card (i) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
(rngs i) . j is set
card ((rngs i) . j) is V29() V30() V31() cardinal set
card (dom (rngs i)) is V29() V30() V31() cardinal set
card (dom i) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
card (len i) is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
card (Union (rngs i)) is V29() V30() V31() cardinal set
(card (len i)) *` (card (i)) is V29() V30() V31() cardinal set
card ((len i) * (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 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 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 ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT
(D,M,i,j) is Element of D
(M) is finite countable set
rngs M is Relation-like Function-like set
Union (rngs M) is 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
(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
{ (D,M,b₁,b₂) where b₁, b₂ is ext-real V29() V30() V31() V35() finite cardinal V48() countable V134() Element of NAT : [b₁,b₂] in (M) } is set