REAL is set
NAT is non empty V14() V15() V16() Element of K19(REAL)
K19(REAL) is set
NAT is non empty V14() V15() V16() set
K19(NAT) is set
K19(NAT) is set
COMPLEX is set
RAT is set
INT is set
1 is non empty V14() V15() V16() V20() V35() V36() ext-real positive Element of NAT
K20(1,1) is set
K19(K20(1,1)) is set
K20(K20(1,1),1) is set
K19(K20(K20(1,1),1)) is set
K20(K20(1,1),REAL) is set
K19(K20(K20(1,1),REAL)) is set
K20(REAL,REAL) is set
K20(K20(REAL,REAL),REAL) is set
K19(K20(K20(REAL,REAL),REAL)) is set
2 is non empty V14() V15() V16() V20() V35() V36() ext-real positive Element of NAT
K20(2,2) is set
K20(K20(2,2),REAL) is set
K19(K20(K20(2,2),REAL)) is set
K19(K20(REAL,REAL)) is set
TOP-REAL 2 is non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict RLTopStruct
the carrier of (TOP-REAL 2) is non empty set
the carrier of (TOP-REAL 2) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (TOP-REAL 2)
K19( the carrier of (TOP-REAL 2)) is set
K20(COMPLEX,COMPLEX) is set
K19(K20(COMPLEX,COMPLEX)) is set
K20(COMPLEX,REAL) is set
K19(K20(COMPLEX,REAL)) is set
{} is functional empty V14() V15() V16() V18() V19() V20() FinSequence-membered V35() V36() ext-real set
3 is non empty V14() V15() V16() V20() V35() V36() ext-real positive Element of NAT
0 is functional empty V14() V15() V16() V18() V19() V20() FinSequence-membered V35() V36() ext-real Element of NAT
k is non empty set
D is functional non empty FinSequence-membered FinSequenceSet of the carrier of (TOP-REAL 2)
K20(k,D) is set
K19(K20(k,D)) is set
f1 is V1() V4(k) V5(D) Function-like V43(k,D) Element of K19(K20(k,D))
f2 is Element of k
f1 . f2 is FinSequence-like set
f1 . f2 is FinSequence-like Element of D
k is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
rng k is set
D is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of (TOP-REAL 2) *
Values D is set
f1 is set
dom k is Element of K19(NAT)
f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k /. f2 is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
Indices D is set
{ (D * (b1,b2)) where b1, b2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT : [b1,b2] in Indices D } is set
G is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[G,i1] is set
{G,i1} is non empty set
{G} is non empty set
{{G,i1},{G}} is non empty set
D * (G,i1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[k,D] is set
{k,D} is non empty set
{k} is non empty set
{{k,D},{k}} is non empty set
f1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Values f2 is set
G is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Values G is set
Indices f2 is set
width G is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 * (k,D) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
G * (1,f1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
f2 * (1,D) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
width f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
len f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
(f2 * (k,D)) `1 is V35() V36() ext-real Element of REAL
(f2 * (1,D)) `1 is V35() V36() ext-real Element of REAL
[1,D] is set
{1,D} is non empty set
{1} is non empty set
{{1,D},{1}} is non empty set
{ (f2 * (b1,b2)) where b1, b2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT : [b1,b2] in Indices f2 } is set
Indices G is set
{ (G * (b1,b2)) where b1, b2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT : [b1,b2] in Indices G } is set
j1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
G * (j1,i2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
[j1,i2] is set
{j1,i2} is non empty set
{j1} is non empty set
{{j1,i2},{j1}} is non empty set
len G is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
G * (1,i2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (1,i2)) `1 is V35() V36() ext-real Element of REAL
G * (1,1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (1,1)) `1 is V35() V36() ext-real Element of REAL
(G * (1,f1)) `1 is V35() V36() ext-real Element of REAL
k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[k,D] is set
{k,D} is non empty set
{k} is non empty set
{{k,D},{k}} is non empty set
f1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Values f2 is set
G is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Values G is set
Indices f2 is set
width G is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 * (k,D) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
len G is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
G * ((len G),f1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
len f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 * ((len f2),D) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
width f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
(f2 * ((len f2),D)) `1 is V35() V36() ext-real Element of REAL
(f2 * (k,D)) `1 is V35() V36() ext-real Element of REAL
[(len f2),D] is set
{(len f2),D} is non empty set
{(len f2)} is non empty set
{{(len f2),D},{(len f2)}} is non empty set
{ (f2 * (b1,b2)) where b1, b2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT : [b1,b2] in Indices f2 } is set
Indices G is set
{ (G * (b1,b2)) where b1, b2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT : [b1,b2] in Indices G } is set
j1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
G * (j1,i2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
[j1,i2] is set
{j1,i2} is non empty set
{j1} is non empty set
{{j1,i2},{j1}} is non empty set
G * ((len G),i2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * ((len G),i2)) `1 is V35() V36() ext-real Element of REAL
G * ((len G),1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * ((len G),1)) `1 is V35() V36() ext-real Element of REAL
(G * ((len G),f1)) `1 is V35() V36() ext-real Element of REAL
k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[k,D] is set
{k,D} is non empty set
{k} is non empty set
{{k,D},{k}} is non empty set
f1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Values f2 is set
G is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Values G is set
Indices f2 is set
len G is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 * (k,D) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
G * (f1,1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
f2 * (k,1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
len f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
width f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
(f2 * (k,D)) `2 is V35() V36() ext-real Element of REAL
(f2 * (k,1)) `2 is V35() V36() ext-real Element of REAL
[k,1] is set
{k,1} is non empty set
{{k,1},{k}} is non empty set
{ (f2 * (b1,b2)) where b1, b2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT : [b1,b2] in Indices f2 } is set
Indices G is set
{ (G * (b1,b2)) where b1, b2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT : [b1,b2] in Indices G } is set
j1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
G * (j1,i2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
[j1,i2] is set
{j1,i2} is non empty set
{j1} is non empty set
{{j1,i2},{j1}} is non empty set
width G is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
G * (j1,1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (j1,1)) `2 is V35() V36() ext-real Element of REAL
G * (1,1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (1,1)) `2 is V35() V36() ext-real Element of REAL
(G * (f1,1)) `2 is V35() V36() ext-real Element of REAL
k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[k,D] is set
{k,D} is non empty set
{k} is non empty set
{{k,D},{k}} is non empty set
f1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Values f2 is set
G is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Values G is set
Indices f2 is set
len G is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 * (k,D) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
width G is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
G * (f1,(width G)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
width f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 * (k,(width f2)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
len f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
(f2 * (k,(width f2))) `2 is V35() V36() ext-real Element of REAL
(f2 * (k,D)) `2 is V35() V36() ext-real Element of REAL
[k,(width f2)] is set
{k,(width f2)} is non empty set
{{k,(width f2)},{k}} is non empty set
{ (f2 * (b1,b2)) where b1, b2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT : [b1,b2] in Indices f2 } is set
Indices G is set
{ (G * (b1,b2)) where b1, b2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT : [b1,b2] in Indices G } is set
j1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
G * (j1,i2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
[j1,i2] is set
{j1,i2} is non empty set
{j1} is non empty set
{{j1,i2},{j1}} is non empty set
G * (j1,(width G)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (j1,(width G))) `2 is V35() V36() ext-real Element of REAL
G * (1,(width G)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (1,(width G))) `2 is V35() V36() ext-real Element of REAL
(G * (f1,(width G))) `2 is V35() V36() ext-real Element of REAL
k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
G is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Values G is set
i1 is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Values i1 is set
len G is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
width G is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
len i1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
width i1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
G * (k,D) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
i1 * (f1,f2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
i1 * ((f1 + 1),f2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * ((f1 + 1),f2)) `1 is V35() V36() ext-real Element of REAL
G * ((k + 1),D) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * ((k + 1),D)) `1 is V35() V36() ext-real Element of REAL
[(k + 1),D] is set
{(k + 1),D} is non empty set
{(k + 1)} is non empty set
{{(k + 1),D},{(k + 1)}} is non empty set
Indices G is set
{ (G * (b1,b2)) where b1, b2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT : [b1,b2] in Indices G } is set
Indices i1 is set
{ (i1 * (b1,b2)) where b1, b2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT : [b1,b2] in Indices i1 } is set
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i1 * (i2,j2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
[i2,j2] is set
{i2,j2} is non empty set
{i2} is non empty set
{{i2,j2},{i2}} is non empty set
(i1 * (i2,j2)) `1 is V35() V36() ext-real Element of REAL
i1 * (i2,1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * (i2,1)) `1 is V35() V36() ext-real Element of REAL
i1 * (i2,f2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * (i2,f2)) `1 is V35() V36() ext-real Element of REAL
(i1 * (f1,f2)) `1 is V35() V36() ext-real Element of REAL
k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
D is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f1 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
G is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
G * ((k -' 1),D) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
i1 is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Values i1 is set
len G is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
width G is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
len i1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
width i1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
G * (k,D) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
i1 * (f1,f2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * ((k -' 1),D)) `1 is V35() V36() ext-real Element of REAL
i1 * ((f1 -' 1),f2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * ((f1 -' 1),f2)) `1 is V35() V36() ext-real Element of REAL
Indices i1 is set
{ (i1 * (b1,b2)) where b1, b2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT : [b1,b2] in Indices i1 } is set
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i1 * (i2,j2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
[i2,j2] is set
{i2,j2} is non empty set
{i2} is non empty set
{{i2,j2},{i2}} is non empty set
(i1 * (i2,j2)) `1 is V35() V36() ext-real Element of REAL
i1 * (i2,1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * (i2,1)) `1 is V35() V36() ext-real Element of REAL
i1 * (i2,f2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * (i2,f2)) `1 is V35() V36() ext-real Element of REAL
(i1 * (f1,f2)) `1 is V35() V36() ext-real Element of REAL
k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
G is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
G * (k,(D + 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
i1 is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Values i1 is set
len G is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
width G is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
len i1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
width i1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
G * (k,D) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
i1 * (f1,f2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
i1 * (f1,(f2 + 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * (f1,(f2 + 1))) `2 is V35() V36() ext-real Element of REAL
(G * (k,(D + 1))) `2 is V35() V36() ext-real Element of REAL
Indices i1 is set
{ (i1 * (b1,b2)) where b1, b2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT : [b1,b2] in Indices i1 } is set
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i1 * (i2,j2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
[i2,j2] is set
{i2,j2} is non empty set
{i2} is non empty set
{{i2,j2},{i2}} is non empty set
(i1 * (i2,j2)) `2 is V35() V36() ext-real Element of REAL
i1 * (1,j2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * (1,j2)) `2 is V35() V36() ext-real Element of REAL
i1 * (f1,j2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * (f1,j2)) `2 is V35() V36() ext-real Element of REAL
(i1 * (f1,f2)) `2 is V35() V36() ext-real Element of REAL
k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
f1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
G is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Values G is set
i1 is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Values i1 is set
len G is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
width G is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
len i1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
width i1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
G * (k,D) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
i1 * (f1,f2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
G * (k,(D -' 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (k,(D -' 1))) `2 is V35() V36() ext-real Element of REAL
i1 * (f1,(f2 -' 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * (f1,(f2 -' 1))) `2 is V35() V36() ext-real Element of REAL
[k,(D -' 1)] is set
{k,(D -' 1)} is non empty set
{k} is non empty set
{{k,(D -' 1)},{k}} is non empty set
Indices G is set
{ (G * (b1,b2)) where b1, b2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT : [b1,b2] in Indices G } is set
Indices i1 is set
{ (i1 * (b1,b2)) where b1, b2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT : [b1,b2] in Indices i1 } is set
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i1 * (i2,j2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
[i2,j2] is set
{i2,j2} is non empty set
{i2} is non empty set
{{i2,j2},{i2}} is non empty set
(i1 * (i2,j2)) `2 is V35() V36() ext-real Element of REAL
i1 * (1,j2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * (1,j2)) `2 is V35() V36() ext-real Element of REAL
i1 * (f1,j2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * (f1,j2)) `2 is V35() V36() ext-real Element of REAL
(i1 * (f1,f2)) `2 is V35() V36() ext-real Element of REAL
k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[k,D] is set
{k,D} is non empty set
{k} is non empty set
{{k,D},{k}} is non empty set
f1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[f1,f2] is set
{f1,f2} is non empty set
{f1} is non empty set
{{f1,f2},{f1}} is non empty set
G is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Values G is set
i1 is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Values i1 is set
Indices G is set
Indices i1 is set
G * (k,D) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
i1 * (f1,f2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
cell (i1,f1,f2) is Element of K19( the carrier of (TOP-REAL 2))
cell (G,k,D) is Element of K19( the carrier of (TOP-REAL 2))
width G is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j1 is set
width i1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
len i1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
(i1 * (f1,f2)) `1 is V35() V36() ext-real Element of REAL
i1 * (f1,1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * (f1,1)) `1 is V35() V36() ext-real Element of REAL
(i1 * (f1,f2)) `2 is V35() V36() ext-real Element of REAL
i1 * (1,f2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * (1,f2)) `2 is V35() V36() ext-real Element of REAL
len G is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
(G * (k,D)) `1 is V35() V36() ext-real Element of REAL
G * (k,1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (k,1)) `1 is V35() V36() ext-real Element of REAL
(G * (k,D)) `2 is V35() V36() ext-real Element of REAL
G * (1,D) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (1,D)) `2 is V35() V36() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V35() V36() ext-real Element of REAL : ( (i1 * (f1,f2)) `1 <= b1 & (i1 * (f1,f2)) `2 <= b2 ) } is set
f2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i1 * (1,(f2 + 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * (1,(f2 + 1))) `2 is V35() V36() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V35() V36() ext-real Element of REAL : ( (i1 * (f1,f2)) `1 <= b1 & (i1 * (f1,f2)) `2 <= b2 & b2 <= (i1 * (1,(f2 + 1))) `2 ) } is set
i2 is V35() V36() ext-real Element of REAL
j2 is V35() V36() ext-real Element of REAL
|[i2,j2]| is V1() V4( NAT ) Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like V46() V47() V48() Element of the carrier of (TOP-REAL 2)
{ |[b1,b2]| where b1, b2 is V35() V36() ext-real Element of REAL : ( (G * (k,D)) `1 <= b1 & (G * (k,D)) `2 <= b2 ) } is set
i1 * (f1,(f2 + 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * (f1,(f2 + 1))) `2 is V35() V36() ext-real Element of REAL
D + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
G * (k,(D + 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (k,(D + 1))) `2 is V35() V36() ext-real Element of REAL
G * (1,(D + 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (1,(D + 1))) `2 is V35() V36() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V35() V36() ext-real Element of REAL : ( (G * (k,D)) `1 <= b1 & (G * (k,D)) `2 <= b2 & b2 <= (G * (1,(D + 1))) `2 ) } is set
f1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i1 * ((f1 + 1),1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * ((f1 + 1),1)) `1 is V35() V36() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V35() V36() ext-real Element of REAL : ( (i1 * (f1,f2)) `1 <= b1 & b1 <= (i1 * ((f1 + 1),1)) `1 & (i1 * (f1,f2)) `2 <= b2 ) } is set
i2 is V35() V36() ext-real Element of REAL
j2 is V35() V36() ext-real Element of REAL
|[i2,j2]| is V1() V4( NAT ) Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like V46() V47() V48() Element of the carrier of (TOP-REAL 2)
{ |[b1,b2]| where b1, b2 is V35() V36() ext-real Element of REAL : ( (G * (k,D)) `1 <= b1 & (G * (k,D)) `2 <= b2 ) } is set
i1 * ((f1 + 1),f2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * ((f1 + 1),f2)) `1 is V35() V36() ext-real Element of REAL
k + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
G * ((k + 1),D) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * ((k + 1),D)) `1 is V35() V36() ext-real Element of REAL
G * ((k + 1),1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * ((k + 1),1)) `1 is V35() V36() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V35() V36() ext-real Element of REAL : ( (G * (k,D)) `1 <= b1 & b1 <= (G * ((k + 1),1)) `1 & (G * (k,D)) `2 <= b2 ) } is set
f2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i1 * (f1,(f2 + 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * (f1,(f2 + 1))) `2 is V35() V36() ext-real Element of REAL
i1 * (1,(f2 + 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * (1,(f2 + 1))) `2 is V35() V36() ext-real Element of REAL
f1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i1 * ((f1 + 1),f2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * ((f1 + 1),f2)) `1 is V35() V36() ext-real Element of REAL
i1 * ((f1 + 1),1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * ((f1 + 1),1)) `1 is V35() V36() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V35() V36() ext-real Element of REAL : ( (i1 * (f1,f2)) `1 <= b1 & b1 <= (i1 * ((f1 + 1),f2)) `1 & (i1 * (f1,f2)) `2 <= b2 & b2 <= (i1 * (f1,(f2 + 1))) `2 ) } is set
i2 is V35() V36() ext-real Element of REAL
j2 is V35() V36() ext-real Element of REAL
|[i2,j2]| is V1() V4( NAT ) Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like V46() V47() V48() Element of the carrier of (TOP-REAL 2)
{ |[b1,b2]| where b1, b2 is V35() V36() ext-real Element of REAL : ( (G * (k,D)) `1 <= b1 & (G * (k,D)) `2 <= b2 ) } is set
D + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
G * (k,(D + 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (k,(D + 1))) `2 is V35() V36() ext-real Element of REAL
G * (1,(D + 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (1,(D + 1))) `2 is V35() V36() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V35() V36() ext-real Element of REAL : ( (G * (k,D)) `1 <= b1 & (G * (k,D)) `2 <= b2 & b2 <= (G * (1,(D + 1))) `2 ) } is set
k + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
G * ((k + 1),D) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * ((k + 1),D)) `1 is V35() V36() ext-real Element of REAL
G * ((k + 1),1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * ((k + 1),1)) `1 is V35() V36() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V35() V36() ext-real Element of REAL : ( (G * (k,D)) `1 <= b1 & b1 <= (G * ((k + 1),1)) `1 & (G * (k,D)) `2 <= b2 ) } is set
k + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
G * ((k + 1),D) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * ((k + 1),D)) `1 is V35() V36() ext-real Element of REAL
G * ((k + 1),1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * ((k + 1),1)) `1 is V35() V36() ext-real Element of REAL
D + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
G * (k,(D + 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (k,(D + 1))) `2 is V35() V36() ext-real Element of REAL
G * (1,(D + 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (1,(D + 1))) `2 is V35() V36() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V35() V36() ext-real Element of REAL : ( (G * (k,1)) `1 <= b1 & b1 <= (G * ((k + 1),1)) `1 & (G * (1,D)) `2 <= b2 & b2 <= (G * (1,(D + 1))) `2 ) } is set
k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
D is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[k,D] is set
{k,D} is non empty set
{k} is non empty set
{{k,D},{k}} is non empty set
f1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f1 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[f1,f2] is set
{f1,f2} is non empty set
{f1} is non empty set
{{f1,f2},{f1}} is non empty set
G is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Values G is set
i1 is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Values i1 is set
Indices G is set
Indices i1 is set
G * (k,D) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
i1 * (f1,f2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
cell (i1,(f1 -' 1),f2) is Element of K19( the carrier of (TOP-REAL 2))
cell (G,(k -' 1),D) is Element of K19( the carrier of (TOP-REAL 2))
len i1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
width G is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
width i1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
(i1 * (f1,f2)) `1 is V35() V36() ext-real Element of REAL
i1 * (f1,1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * (f1,1)) `1 is V35() V36() ext-real Element of REAL
(i1 * (f1,f2)) `2 is V35() V36() ext-real Element of REAL
i1 * (1,f2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * (1,f2)) `2 is V35() V36() ext-real Element of REAL
j1 is set
len G is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i1 * (1,1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * (1,1)) `1 is V35() V36() ext-real Element of REAL
i1 * (1,(width i1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * (1,(width i1))) `2 is V35() V36() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V35() V36() ext-real Element of REAL : ( b1 <= (i1 * (1,1)) `1 & (i1 * (1,(width i1))) `2 <= b2 ) } is set
i2 is V35() V36() ext-real Element of REAL
j2 is V35() V36() ext-real Element of REAL
|[i2,j2]| is V1() V4( NAT ) Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like V46() V47() V48() Element of the carrier of (TOP-REAL 2)
i1 * (k,f2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * (k,f2)) `1 is V35() V36() ext-real Element of REAL
G * (1,1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (1,1)) `1 is V35() V36() ext-real Element of REAL
G * (1,(width G)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (1,(width G))) `2 is V35() V36() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V35() V36() ext-real Element of REAL : ( b1 <= (G * (1,1)) `1 & (G * (1,(width G))) `2 <= b2 ) } is set
i1 * (1,1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * (1,1)) `1 is V35() V36() ext-real Element of REAL
f2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i1 * (1,(f2 + 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * (1,(f2 + 1))) `2 is V35() V36() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V35() V36() ext-real Element of REAL : ( b1 <= (i1 * (1,1)) `1 & (i1 * (1,f2)) `2 <= b2 & b2 <= (i1 * (1,(f2 + 1))) `2 ) } is set
i2 is V35() V36() ext-real Element of REAL
j2 is V35() V36() ext-real Element of REAL
|[i2,j2]| is V1() V4( NAT ) Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like V46() V47() V48() Element of the carrier of (TOP-REAL 2)
i1 * (k,f2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * (k,f2)) `1 is V35() V36() ext-real Element of REAL
G * (1,1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (1,1)) `1 is V35() V36() ext-real Element of REAL
G * (1,(width G)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (1,(width G))) `2 is V35() V36() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V35() V36() ext-real Element of REAL : ( b1 <= (G * (1,1)) `1 & (G * (1,(width G))) `2 <= b2 ) } is set
D + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
G * (k,(D + 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
G * (1,(D + 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (1,(D + 1))) `2 is V35() V36() ext-real Element of REAL
G * (1,D) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (1,D)) `2 is V35() V36() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V35() V36() ext-real Element of REAL : ( b1 <= (G * (1,1)) `1 & (G * (1,D)) `2 <= b2 & b2 <= (G * (1,(D + 1))) `2 ) } is set
(f1 -' 1) + 1 is V14() V15() V16() V20() V35() V36() ext-real positive Element of NAT
i1 * ((f1 -' 1),1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * ((f1 -' 1),1)) `1 is V35() V36() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V35() V36() ext-real Element of REAL : ( (i1 * ((f1 -' 1),1)) `1 <= b1 & b1 <= (i1 * (f1,1)) `1 & (i1 * (1,f2)) `2 <= b2 ) } is set
i2 is V35() V36() ext-real Element of REAL
j2 is V35() V36() ext-real Element of REAL
|[i2,j2]| is V1() V4( NAT ) Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like V46() V47() V48() Element of the carrier of (TOP-REAL 2)
G * (1,1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (1,1)) `1 is V35() V36() ext-real Element of REAL
G * (1,D) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (1,D)) `2 is V35() V36() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V35() V36() ext-real Element of REAL : ( b1 <= (G * (1,1)) `1 & (G * (1,D)) `2 <= b2 ) } is set
i1 * ((f1 -' 1),1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * ((f1 -' 1),1)) `1 is V35() V36() ext-real Element of REAL
f2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i1 * (1,(f2 + 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * (1,(f2 + 1))) `2 is V35() V36() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V35() V36() ext-real Element of REAL : ( (i1 * ((f1 -' 1),1)) `1 <= b1 & b1 <= (i1 * (f1,1)) `1 & (i1 * (1,f2)) `2 <= b2 & b2 <= (i1 * (1,(f2 + 1))) `2 ) } is set
i2 is V35() V36() ext-real Element of REAL
j2 is V35() V36() ext-real Element of REAL
|[i2,j2]| is V1() V4( NAT ) Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like V46() V47() V48() Element of the carrier of (TOP-REAL 2)
G * (1,1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (1,1)) `1 is V35() V36() ext-real Element of REAL
G * (1,D) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (1,D)) `2 is V35() V36() ext-real Element of REAL
G * (1,(width G)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (1,(width G))) `2 is V35() V36() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V35() V36() ext-real Element of REAL : ( b1 <= (G * (1,1)) `1 & (G * (1,(width G))) `2 <= b2 ) } is set
i1 * (f1,(f2 + 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * (f1,(f2 + 1))) `2 is V35() V36() ext-real Element of REAL
D + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
G * (k,(D + 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (k,(D + 1))) `2 is V35() V36() ext-real Element of REAL
G * (1,(D + 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (1,(D + 1))) `2 is V35() V36() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V35() V36() ext-real Element of REAL : ( b1 <= (G * (1,1)) `1 & (G * (1,D)) `2 <= b2 & b2 <= (G * (1,(D + 1))) `2 ) } is set
(f1 -' 1) + 1 is V14() V15() V16() V20() V35() V36() ext-real positive Element of NAT
i1 * ((f1 -' 1),1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * ((f1 -' 1),1)) `1 is V35() V36() ext-real Element of REAL
i1 * ((f1 -' 1),f2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * ((f1 -' 1),f2)) `1 is V35() V36() ext-real Element of REAL
(k -' 1) + 1 is V14() V15() V16() V20() V35() V36() ext-real positive Element of NAT
G * ((k -' 1),D) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
G * ((k -' 1),1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * ((k -' 1),1)) `1 is V35() V36() ext-real Element of REAL
(G * ((k -' 1),D)) `1 is V35() V36() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V35() V36() ext-real Element of REAL : ( (i1 * ((f1 -' 1),1)) `1 <= b1 & b1 <= (i1 * (f1,1)) `1 & (i1 * (1,f2)) `2 <= b2 ) } is set
i2 is V35() V36() ext-real Element of REAL
j2 is V35() V36() ext-real Element of REAL
|[i2,j2]| is V1() V4( NAT ) Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like V46() V47() V48() Element of the carrier of (TOP-REAL 2)
G * (1,D) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (1,D)) `2 is V35() V36() ext-real Element of REAL
G * (k,1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (k,1)) `1 is V35() V36() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V35() V36() ext-real Element of REAL : ( (G * ((k -' 1),1)) `1 <= b1 & b1 <= (G * (k,1)) `1 & (G * (1,D)) `2 <= b2 ) } is set
f2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i1 * (1,(f2 + 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * (1,(f2 + 1))) `2 is V35() V36() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V35() V36() ext-real Element of REAL : ( (i1 * ((f1 -' 1),1)) `1 <= b1 & b1 <= (i1 * (f1,1)) `1 & (i1 * (1,f2)) `2 <= b2 & b2 <= (i1 * (1,(f2 + 1))) `2 ) } is set
i2 is V35() V36() ext-real Element of REAL
j2 is V35() V36() ext-real Element of REAL
|[i2,j2]| is V1() V4( NAT ) Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like V46() V47() V48() Element of the carrier of (TOP-REAL 2)
G * (1,D) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (1,D)) `2 is V35() V36() ext-real Element of REAL
G * (k,1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (k,1)) `1 is V35() V36() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V35() V36() ext-real Element of REAL : ( (G * ((k -' 1),1)) `1 <= b1 & b1 <= (G * (k,1)) `1 & (G * (1,D)) `2 <= b2 ) } is set
i1 * (f1,(f2 + 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * (f1,(f2 + 1))) `2 is V35() V36() ext-real Element of REAL
D + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
G * (k,(D + 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (k,(D + 1))) `2 is V35() V36() ext-real Element of REAL
G * (1,(D + 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (1,(D + 1))) `2 is V35() V36() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V35() V36() ext-real Element of REAL : ( (G * ((k -' 1),1)) `1 <= b1 & b1 <= (G * (k,1)) `1 & (G * (1,D)) `2 <= b2 & b2 <= (G * (1,(D + 1))) `2 ) } is set
k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[k,D] is set
{k,D} is non empty set
{k} is non empty set
{{k,D},{k}} is non empty set
D -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
f1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[f1,f2] is set
{f1,f2} is non empty set
{f1} is non empty set
{{f1,f2},{f1}} is non empty set
f2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
G is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Values G is set
i1 is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Values i1 is set
Indices G is set
Indices i1 is set
G * (k,D) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
i1 * (f1,f2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
cell (i1,f1,(f2 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
cell (G,k,(D -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
width G is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
width i1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
len i1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
(i1 * (f1,f2)) `1 is V35() V36() ext-real Element of REAL
i1 * (f1,1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * (f1,1)) `1 is V35() V36() ext-real Element of REAL
len G is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
(G * (k,D)) `2 is V35() V36() ext-real Element of REAL
G * (1,D) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (1,D)) `2 is V35() V36() ext-real Element of REAL
j1 is set
(i1 * (f1,f2)) `2 is V35() V36() ext-real Element of REAL
i1 * (1,f2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * (1,f2)) `2 is V35() V36() ext-real Element of REAL
i1 * ((len i1),1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * ((len i1),1)) `1 is V35() V36() ext-real Element of REAL
i1 * (1,1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * (1,1)) `2 is V35() V36() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V35() V36() ext-real Element of REAL : ( (i1 * ((len i1),1)) `1 <= b1 & b2 <= (i1 * (1,1)) `2 ) } is set
i2 is V35() V36() ext-real Element of REAL
j2 is V35() V36() ext-real Element of REAL
|[i2,j2]| is V1() V4( NAT ) Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like V46() V47() V48() Element of the carrier of (TOP-REAL 2)
G * (1,1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (1,1)) `2 is V35() V36() ext-real Element of REAL
G * ((len G),1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * ((len G),1)) `1 is V35() V36() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V35() V36() ext-real Element of REAL : ( (G * ((len G),1)) `1 <= b1 & b2 <= (G * (1,1)) `2 ) } is set
f1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i1 * ((f1 + 1),1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * ((f1 + 1),1)) `1 is V35() V36() ext-real Element of REAL
i1 * (1,1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * (1,1)) `2 is V35() V36() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V35() V36() ext-real Element of REAL : ( (i1 * (f1,1)) `1 <= b1 & b1 <= (i1 * ((f1 + 1),1)) `1 & b2 <= (i1 * (1,1)) `2 ) } is set
i2 is V35() V36() ext-real Element of REAL
j2 is V35() V36() ext-real Element of REAL
|[i2,j2]| is V1() V4( NAT ) Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like V46() V47() V48() Element of the carrier of (TOP-REAL 2)
i1 * (f1,D) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * (f1,D)) `2 is V35() V36() ext-real Element of REAL
G * (1,1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (1,1)) `2 is V35() V36() ext-real Element of REAL
G * ((len G),1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * ((len G),1)) `1 is V35() V36() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V35() V36() ext-real Element of REAL : ( (G * ((len G),1)) `1 <= b1 & b2 <= (G * (1,1)) `2 ) } is set
k + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
G * ((k + 1),1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * ((k + 1),1)) `1 is V35() V36() ext-real Element of REAL
G * (k,1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (k,1)) `1 is V35() V36() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V35() V36() ext-real Element of REAL : ( (G * (k,1)) `1 <= b1 & b1 <= (G * ((k + 1),1)) `1 & b2 <= (G * (1,1)) `2 ) } is set
(f2 -' 1) + 1 is V14() V15() V16() V20() V35() V36() ext-real positive Element of NAT
i1 * (1,(f2 -' 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * (1,(f2 -' 1))) `2 is V35() V36() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V35() V36() ext-real Element of REAL : ( (i1 * (f1,1)) `1 <= b1 & (i1 * (1,(f2 -' 1))) `2 <= b2 & b2 <= (i1 * (1,f2)) `2 ) } is set
G * (k,1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (k,1)) `1 is V35() V36() ext-real Element of REAL
G * (1,1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (1,1)) `2 is V35() V36() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V35() V36() ext-real Element of REAL : ( (G * (k,1)) `1 <= b1 & b2 <= (G * (1,1)) `2 ) } is set
i2 is V35() V36() ext-real Element of REAL
j2 is V35() V36() ext-real Element of REAL
|[i2,j2]| is V1() V4( NAT ) Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like V46() V47() V48() Element of the carrier of (TOP-REAL 2)
f1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i1 * ((f1 + 1),1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * ((f1 + 1),1)) `1 is V35() V36() ext-real Element of REAL
i1 * (1,(f2 -' 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * (1,(f2 -' 1))) `2 is V35() V36() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V35() V36() ext-real Element of REAL : ( (i1 * (f1,1)) `1 <= b1 & b1 <= (i1 * ((f1 + 1),1)) `1 & (i1 * (1,(f2 -' 1))) `2 <= b2 & b2 <= (i1 * (1,f2)) `2 ) } is set
i2 is V35() V36() ext-real Element of REAL
j2 is V35() V36() ext-real Element of REAL
|[i2,j2]| is V1() V4( NAT ) Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like V46() V47() V48() Element of the carrier of (TOP-REAL 2)
G * (1,1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (1,1)) `2 is V35() V36() ext-real Element of REAL
G * (k,1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (k,1)) `1 is V35() V36() ext-real Element of REAL
G * ((len G),1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * ((len G),1)) `1 is V35() V36() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V35() V36() ext-real Element of REAL : ( (G * ((len G),1)) `1 <= b1 & b2 <= (G * (1,1)) `2 ) } is set
i1 * ((f1 + 1),f2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * ((f1 + 1),f2)) `1 is V35() V36() ext-real Element of REAL
k + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
G * ((k + 1),D) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * ((k + 1),D)) `1 is V35() V36() ext-real Element of REAL
G * ((k + 1),1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * ((k + 1),1)) `1 is V35() V36() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V35() V36() ext-real Element of REAL : ( (G * (k,1)) `1 <= b1 & b1 <= (G * ((k + 1),1)) `1 & b2 <= (G * (1,1)) `2 ) } is set
(f2 -' 1) + 1 is V14() V15() V16() V20() V35() V36() ext-real positive Element of NAT
i1 * (1,(f2 -' 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * (1,(f2 -' 1))) `2 is V35() V36() ext-real Element of REAL
i1 * (f1,(f2 -' 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * (f1,(f2 -' 1))) `2 is V35() V36() ext-real Element of REAL
(D -' 1) + 1 is V14() V15() V16() V20() V35() V36() ext-real positive Element of NAT
G * (1,(D -' 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (1,(D -' 1))) `2 is V35() V36() ext-real Element of REAL
G * (k,(D -' 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (k,(D -' 1))) `2 is V35() V36() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V35() V36() ext-real Element of REAL : ( (i1 * (f1,1)) `1 <= b1 & (i1 * (1,(f2 -' 1))) `2 <= b2 & b2 <= (i1 * (1,f2)) `2 ) } is set
i2 is V35() V36() ext-real Element of REAL
j2 is V35() V36() ext-real Element of REAL
|[i2,j2]| is V1() V4( NAT ) Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like V46() V47() V48() Element of the carrier of (TOP-REAL 2)
G * (k,1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (k,1)) `1 is V35() V36() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V35() V36() ext-real Element of REAL : ( (G * (k,1)) `1 <= b1 & (G * (1,(D -' 1))) `2 <= b2 & b2 <= (G * (1,D)) `2 ) } is set
f1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i1 * ((f1 + 1),1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * ((f1 + 1),1)) `1 is V35() V36() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V35() V36() ext-real Element of REAL : ( (i1 * (f1,1)) `1 <= b1 & b1 <= (i1 * ((f1 + 1),1)) `1 & (i1 * (1,(f2 -' 1))) `2 <= b2 & b2 <= (i1 * (1,f2)) `2 ) } is set
i2 is V35() V36() ext-real Element of REAL
j2 is V35() V36() ext-real Element of REAL
|[i2,j2]| is V1() V4( NAT ) Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like V46() V47() V48() Element of the carrier of (TOP-REAL 2)
G * (k,1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * (k,1)) `1 is V35() V36() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V35() V36() ext-real Element of REAL : ( (G * (k,1)) `1 <= b1 & (G * (1,(D -' 1))) `2 <= b2 & b2 <= (G * (1,D)) `2 ) } is set
i1 * ((f1 + 1),f2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(i1 * ((f1 + 1),f2)) `1 is V35() V36() ext-real Element of REAL
k + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
G * ((k + 1),D) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * ((k + 1),D)) `1 is V35() V36() ext-real Element of REAL
G * ((k + 1),1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(G * ((k + 1),1)) `1 is V35() V36() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V35() V36() ext-real Element of REAL : ( (G * (k,1)) `1 <= b1 & b1 <= (G * ((k + 1),1)) `1 & (G * (1,(D -' 1))) `2 <= b2 & b2 <= (G * (1,D)) `2 ) } is set
k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f1 is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like non empty V24() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
GoB f1 is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
len (GoB f1) is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
width (GoB f1) is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
dom f1 is Element of K19(NAT)
(GoB f1) * (k,D) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
((GoB f1) * (k,D)) `1 is V35() V36() ext-real Element of REAL
X_axis f1 is V1() V4( NAT ) V5( REAL ) Function-like non empty V24() FinSequence-like FinSubsequence-like V46() V47() V48() FinSequence of REAL
Incr (X_axis f1) is V1() V4( NAT ) V5( REAL ) Function-like one-to-one non empty V24() FinSequence-like FinSubsequence-like V46() V47() V48() V50() V52() FinSequence of REAL
Y_axis f1 is V1() V4( NAT ) V5( REAL ) Function-like non empty V24() FinSequence-like FinSubsequence-like V46() V47() V48() FinSequence of REAL
Incr (Y_axis f1) is V1() V4( NAT ) V5( REAL ) Function-like one-to-one non empty V24() FinSequence-like FinSubsequence-like V46() V47() V48() V50() V52() FinSequence of REAL
GoB ((Incr (X_axis f1)),(Incr (Y_axis f1))) is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
len (Incr (X_axis f1)) is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
dom (Incr (X_axis f1)) is Element of K19(NAT)
(Incr (X_axis f1)) . k is V35() V36() ext-real set
rng (Incr (X_axis f1)) is V57() V58() V59() set
rng (X_axis f1) is V57() V58() V59() set
dom (X_axis f1) is Element of K19(NAT)
f2 is V14() V15() V16() V20() V35() V36() ext-real set
(X_axis f1) . f2 is V35() V36() ext-real set
[k,D] is set
{k,D} is non empty set
{k} is non empty set
{{k,D},{k}} is non empty set
Indices (GoB f1) is set
(Incr (Y_axis f1)) . D is V35() V36() ext-real set
|[((Incr (X_axis f1)) . k),((Incr (Y_axis f1)) . D)]| is V1() V4( NAT ) Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like V46() V47() V48() Element of the carrier of (TOP-REAL 2)
G is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f1 /. G is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(f1 /. G) `1 is V35() V36() ext-real Element of REAL
len (X_axis f1) is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
len f1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f1 is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like non empty V24() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
GoB f1 is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
len (GoB f1) is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
width (GoB f1) is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
dom f1 is Element of K19(NAT)
(GoB f1) * (k,D) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
((GoB f1) * (k,D)) `2 is V35() V36() ext-real Element of REAL
X_axis f1 is V1() V4( NAT ) V5( REAL ) Function-like non empty V24() FinSequence-like FinSubsequence-like V46() V47() V48() FinSequence of REAL
Incr (X_axis f1) is V1() V4( NAT ) V5( REAL ) Function-like one-to-one non empty V24() FinSequence-like FinSubsequence-like V46() V47() V48() V50() V52() FinSequence of REAL
Y_axis f1 is V1() V4( NAT ) V5( REAL ) Function-like non empty V24() FinSequence-like FinSubsequence-like V46() V47() V48() FinSequence of REAL
Incr (Y_axis f1) is V1() V4( NAT ) V5( REAL ) Function-like one-to-one non empty V24() FinSequence-like FinSubsequence-like V46() V47() V48() V50() V52() FinSequence of REAL
GoB ((Incr (X_axis f1)),(Incr (Y_axis f1))) is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
len (Incr (Y_axis f1)) is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
dom (Incr (Y_axis f1)) is Element of K19(NAT)
(Incr (Y_axis f1)) . D is V35() V36() ext-real set
rng (Incr (Y_axis f1)) is V57() V58() V59() set
rng (Y_axis f1) is V57() V58() V59() set
dom (Y_axis f1) is Element of K19(NAT)
f2 is V14() V15() V16() V20() V35() V36() ext-real set
(Y_axis f1) . f2 is V35() V36() ext-real set
[k,D] is set
{k,D} is non empty set
{k} is non empty set
{{k,D},{k}} is non empty set
Indices (GoB f1) is set
(Incr (X_axis f1)) . k is V35() V36() ext-real set
|[((Incr (X_axis f1)) . k),((Incr (Y_axis f1)) . D)]| is V1() V4( NAT ) Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like V46() V47() V48() Element of the carrier of (TOP-REAL 2)
G is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f1 /. G is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(f1 /. G) `2 is V35() V36() ext-real Element of REAL
len (Y_axis f1) is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
len f1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Values k is set
D is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like non empty V24() FinSequence-like FinSubsequence-like V166( the carrier of (TOP-REAL 2)) V167() V168() s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
GoB D is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Values (GoB D) is set
f1 is set
Indices (GoB D) is set
{ ((GoB D) * (b1,b2)) where b1, b2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT : [b1,b2] in Indices (GoB D) } is set
G is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
(GoB D) * (G,i1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
[G,i1] is set
{G,i1} is non empty set
{G} is non empty set
{{G,i1},{G}} is non empty set
width (GoB D) is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
len (GoB D) is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
dom D is Element of K19(NAT)
j1 is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
j1 `1 is V35() V36() ext-real Element of REAL
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D /. i2 is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(D /. i2) `1 is V35() V36() ext-real Element of REAL
j1 `2 is V35() V36() ext-real Element of REAL
j2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D /. j2 is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(D /. j2) `2 is V35() V36() ext-real Element of REAL
Indices k is set
j1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[j1,i2] is set
{j1,i2} is non empty set
{j1} is non empty set
{{j1,i2},{j1}} is non empty set
k * (j1,i2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
len k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
l is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[j2,l] is set
{j2,l} is non empty set
{j2} is non empty set
{{j2,l},{j2}} is non empty set
k * (j2,l) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
width k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
|[(j1 `1),(j1 `2)]| is V1() V4( NAT ) Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like V46() V47() V48() Element of the carrier of (TOP-REAL 2)
[j2,i2] is set
{j2,i2} is non empty set
{{j2,i2},{j2}} is non empty set
k * (j2,i2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(k * (j2,i2)) `2 is V35() V36() ext-real Element of REAL
k * (1,i2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(k * (1,i2)) `2 is V35() V36() ext-real Element of REAL
(k * (j1,i2)) `2 is V35() V36() ext-real Element of REAL
(k * (j2,i2)) `1 is V35() V36() ext-real Element of REAL
k * (j2,1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(k * (j2,1)) `1 is V35() V36() ext-real Element of REAL
(k * (j2,l)) `1 is V35() V36() ext-real Element of REAL
{ (k * (b1,b2)) where b1, b2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT : [b1,b2] in Indices k } is set
f1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Indices D is set
k /. f1 is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
k /. (f1 + 1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
G is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[f2,G] is set
{f2,G} is non empty set
{f2} is non empty set
{{f2,G},{f2}} is non empty set
D * (f2,G) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
i1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i1,j1] is set
{i1,j1} is non empty set
{i1} is non empty set
{{i1,j1},{i1}} is non empty set
D * (i1,j1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
G + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
cell (D,f2,G) is Element of K19( the carrier of (TOP-REAL 2))
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i2,j2] is set
{i2,j2} is non empty set
{i2} is non empty set
{{i2,j2},{i2}} is non empty set
j1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[j1,i2] is set
{j1,i2} is non empty set
{j1} is non empty set
{{j1,i2},{j1}} is non empty set
D * (i2,j2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
D * (j1,i2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
j2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
cell (D,i2,j2) is Element of K19( the carrier of (TOP-REAL 2))
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,i2,(j2 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
j1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
cell (D,j1,i2) is Element of K19( the carrier of (TOP-REAL 2))
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,(i2 -' 1),i2) is Element of K19( the carrier of (TOP-REAL 2))
G -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,f2,(G -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i2,j2] is set
{i2,j2} is non empty set
{i2} is non empty set
{{i2,j2},{i2}} is non empty set
j1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[j1,i2] is set
{j1,i2} is non empty set
{j1} is non empty set
{{j1,i2},{j1}} is non empty set
D * (i2,j2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
D * (j1,i2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
j2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
cell (D,i2,j2) is Element of K19( the carrier of (TOP-REAL 2))
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,i2,(j2 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
j1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
cell (D,j1,i2) is Element of K19( the carrier of (TOP-REAL 2))
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,(i2 -' 1),i2) is Element of K19( the carrier of (TOP-REAL 2))
cell (D,i1,j1) is Element of K19( the carrier of (TOP-REAL 2))
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i2,j2] is set
{i2,j2} is non empty set
{i2} is non empty set
{{i2,j2},{i2}} is non empty set
j1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[j1,i2] is set
{j1,i2} is non empty set
{j1} is non empty set
{{j1,i2},{j1}} is non empty set
D * (i2,j2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
D * (j1,i2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
j2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
cell (D,i2,j2) is Element of K19( the carrier of (TOP-REAL 2))
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,i2,(j2 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
j1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
cell (D,j1,i2) is Element of K19( the carrier of (TOP-REAL 2))
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,(i2 -' 1),i2) is Element of K19( the carrier of (TOP-REAL 2))
f2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,(f2 -' 1),j1) is Element of K19( the carrier of (TOP-REAL 2))
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i2,j2] is set
{i2,j2} is non empty set
{i2} is non empty set
{{i2,j2},{i2}} is non empty set
j1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[j1,i2] is set
{j1,i2} is non empty set
{j1} is non empty set
{{j1,i2},{j1}} is non empty set
D * (i2,j2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
D * (j1,i2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
j2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
cell (D,i2,j2) is Element of K19( the carrier of (TOP-REAL 2))
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,i2,(j2 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
j1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
cell (D,j1,i2) is Element of K19( the carrier of (TOP-REAL 2))
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,(i2 -' 1),i2) is Element of K19( the carrier of (TOP-REAL 2))
i2 is Element of K19( the carrier of (TOP-REAL 2))
j2 is Element of K19( the carrier of (TOP-REAL 2))
cell (D,f2,G) is Element of K19( the carrier of (TOP-REAL 2))
G -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,f2,(G -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
cell (D,i1,j1) is Element of K19( the carrier of (TOP-REAL 2))
f2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,(f2 -' 1),j1) is Element of K19( the carrier of (TOP-REAL 2))
f2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,(f2 -' 1),G) is Element of K19( the carrier of (TOP-REAL 2))
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i2,j2] is set
{i2,j2} is non empty set
{i2} is non empty set
{{i2,j2},{i2}} is non empty set
j1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[j1,i2] is set
{j1,i2} is non empty set
{j1} is non empty set
{{j1,i2},{j1}} is non empty set
D * (i2,j2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
D * (j1,i2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
j2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,(i2 -' 1),j2) is Element of K19( the carrier of (TOP-REAL 2))
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
cell (D,i2,j2) is Element of K19( the carrier of (TOP-REAL 2))
j1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,j1,(i2 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
cell (D,i2,i2) is Element of K19( the carrier of (TOP-REAL 2))
cell (D,f2,G) is Element of K19( the carrier of (TOP-REAL 2))
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i2,j2] is set
{i2,j2} is non empty set
{i2} is non empty set
{{i2,j2},{i2}} is non empty set
j1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[j1,i2] is set
{j1,i2} is non empty set
{j1} is non empty set
{{j1,i2},{j1}} is non empty set
D * (i2,j2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
D * (j1,i2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
j2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,(i2 -' 1),j2) is Element of K19( the carrier of (TOP-REAL 2))
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
cell (D,i2,j2) is Element of K19( the carrier of (TOP-REAL 2))
j1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,j1,(i2 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
cell (D,i2,i2) is Element of K19( the carrier of (TOP-REAL 2))
j1 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,i1,(j1 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i2,j2] is set
{i2,j2} is non empty set
{i2} is non empty set
{{i2,j2},{i2}} is non empty set
j1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[j1,i2] is set
{j1,i2} is non empty set
{j1} is non empty set
{{j1,i2},{j1}} is non empty set
D * (i2,j2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
D * (j1,i2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
j2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,(i2 -' 1),j2) is Element of K19( the carrier of (TOP-REAL 2))
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
cell (D,i2,j2) is Element of K19( the carrier of (TOP-REAL 2))
j1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,j1,(i2 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
cell (D,i2,i2) is Element of K19( the carrier of (TOP-REAL 2))
cell (D,f2,j1) is Element of K19( the carrier of (TOP-REAL 2))
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i2,j2] is set
{i2,j2} is non empty set
{i2} is non empty set
{{i2,j2},{i2}} is non empty set
j1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[j1,i2] is set
{j1,i2} is non empty set
{j1} is non empty set
{{j1,i2},{j1}} is non empty set
D * (i2,j2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
D * (j1,i2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
j2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,(i2 -' 1),j2) is Element of K19( the carrier of (TOP-REAL 2))
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
cell (D,i2,j2) is Element of K19( the carrier of (TOP-REAL 2))
j1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,j1,(i2 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
cell (D,i2,i2) is Element of K19( the carrier of (TOP-REAL 2))
i2 is Element of K19( the carrier of (TOP-REAL 2))
j2 is Element of K19( the carrier of (TOP-REAL 2))
f2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,(f2 -' 1),G) is Element of K19( the carrier of (TOP-REAL 2))
cell (D,f2,G) is Element of K19( the carrier of (TOP-REAL 2))
j1 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,i1,(j1 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
cell (D,f2,j1) is Element of K19( the carrier of (TOP-REAL 2))
k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
f1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[D,f1] is set
{D,f1} is non empty set
{D} is non empty set
{{D,f1},{D}} is non empty set
f1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[D,(f1 + 1)] is set
{D,(f1 + 1)} is non empty set
{{D,(f1 + 1)},{D}} is non empty set
f2 is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 /. k is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
f2 /. (k + 1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
G is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Indices G is set
G * (D,f1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
G * (D,(f1 + 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(f2,G,k) is Element of K19( the carrier of (TOP-REAL 2))
cell (G,(D -' 1),f1) is Element of K19( the carrier of (TOP-REAL 2))
(f1 + 1) + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[D,f1] is set
{D,f1} is non empty set
{D} is non empty set
{{D,f1},{D}} is non empty set
f1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[D,(f1 + 1)] is set
{D,(f1 + 1)} is non empty set
{{D,(f1 + 1)},{D}} is non empty set
f2 is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 /. k is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
f2 /. (k + 1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
G is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Indices G is set
G * (D,f1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
G * (D,(f1 + 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(f2,G,k) is Element of K19( the carrier of (TOP-REAL 2))
cell (G,D,f1) is Element of K19( the carrier of (TOP-REAL 2))
(f1 + 1) + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[D,f1] is set
{D,f1} is non empty set
{D} is non empty set
{{D,f1},{D}} is non empty set
[(D + 1),f1] is set
{(D + 1),f1} is non empty set
{(D + 1)} is non empty set
{{(D + 1),f1},{(D + 1)}} is non empty set
f2 is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 /. k is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
f2 /. (k + 1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
G is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Indices G is set
G * (D,f1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
G * ((D + 1),f1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(f2,G,k) is Element of K19( the carrier of (TOP-REAL 2))
cell (G,D,f1) is Element of K19( the carrier of (TOP-REAL 2))
(D + 1) + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[D,f1] is set
{D,f1} is non empty set
{D} is non empty set
{{D,f1},{D}} is non empty set
[(D + 1),f1] is set
{(D + 1),f1} is non empty set
{(D + 1)} is non empty set
{{(D + 1),f1},{(D + 1)}} is non empty set
f1 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
f2 is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 /. k is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
f2 /. (k + 1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
G is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Indices G is set
G * (D,f1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
G * ((D + 1),f1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(f2,G,k) is Element of K19( the carrier of (TOP-REAL 2))
cell (G,D,(f1 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
(D + 1) + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[D,f1] is set
{D,f1} is non empty set
{D} is non empty set
{{D,f1},{D}} is non empty set
[(D + 1),f1] is set
{(D + 1),f1} is non empty set
{(D + 1)} is non empty set
{{(D + 1),f1},{(D + 1)}} is non empty set
f1 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
f2 is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 /. k is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
f2 /. (k + 1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
G is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Indices G is set
G * ((D + 1),f1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
G * (D,f1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(f2,G,k) is Element of K19( the carrier of (TOP-REAL 2))
cell (G,D,(f1 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
(D + 1) + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[D,f1] is set
{D,f1} is non empty set
{D} is non empty set
{{D,f1},{D}} is non empty set
[(D + 1),f1] is set
{(D + 1),f1} is non empty set
{(D + 1)} is non empty set
{{(D + 1),f1},{(D + 1)}} is non empty set
f2 is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 /. k is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
f2 /. (k + 1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
G is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Indices G is set
G * ((D + 1),f1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
G * (D,f1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(f2,G,k) is Element of K19( the carrier of (TOP-REAL 2))
cell (G,D,f1) is Element of K19( the carrier of (TOP-REAL 2))
(D + 1) + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[D,(f1 + 1)] is set
{D,(f1 + 1)} is non empty set
{D} is non empty set
{{D,(f1 + 1)},{D}} is non empty set
[D,f1] is set
{D,f1} is non empty set
{{D,f1},{D}} is non empty set
f2 is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 /. k is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
f2 /. (k + 1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
G is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Indices G is set
G * (D,(f1 + 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
G * (D,f1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(f2,G,k) is Element of K19( the carrier of (TOP-REAL 2))
cell (G,D,f1) is Element of K19( the carrier of (TOP-REAL 2))
(f1 + 1) + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
f1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[D,(f1 + 1)] is set
{D,(f1 + 1)} is non empty set
{D} is non empty set
{{D,(f1 + 1)},{D}} is non empty set
[D,f1] is set
{D,f1} is non empty set
{{D,f1},{D}} is non empty set
f2 is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 /. k is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
f2 /. (k + 1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
G is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Indices G is set
G * (D,(f1 + 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
G * (D,f1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(f2,G,k) is Element of K19( the carrier of (TOP-REAL 2))
cell (G,(D -' 1),f1) is Element of K19( the carrier of (TOP-REAL 2))
(f1 + 1) + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len D is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
LSeg (D,k) is Element of K19( the carrier of (TOP-REAL 2))
f1 is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
(D,f1,k) is Element of K19( the carrier of (TOP-REAL 2))
(D,f1,k) is Element of K19( the carrier of (TOP-REAL 2))
(D,f1,k) /\ (D,f1,k) is Element of K19( the carrier of (TOP-REAL 2))
dom D is Element of K19(NAT)
Indices f1 is set
D /. (k + 1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
G is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[f2,G] is set
{f2,G} is non empty set
{f2} is non empty set
{{f2,G},{f2}} is non empty set
f1 * (f2,G) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
len f1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
width f1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D /. k is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
i1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i1,j1] is set
{i1,j1} is non empty set
{i1} is non empty set
{{i1,j1},{i1}} is non empty set
f1 * (i1,j1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
0 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 is V14() V15() V16() V20() V35() V36() ext-real set
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i1 - f2 is V35() V36() ext-real set
abs (i1 - f2) is V35() V36() ext-real Element of REAL
j1 - G is V35() V36() ext-real set
abs (j1 - G) is V35() V36() ext-real Element of REAL
(abs (i1 - f2)) + (abs (j1 - G)) is V35() V36() ext-real Element of REAL
- (i1 - f2) is V35() V36() ext-real set
f2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
- (j1 - G) is V35() V36() ext-real set
G + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
G + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
G + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j1 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
j2 is V14() V15() V16() V20() V35() V36() ext-real set
j2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i1 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (f1,i1,j1) is Element of K19( the carrier of (TOP-REAL 2))
j1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
cell (f1,j1,j1) is Element of K19( the carrier of (TOP-REAL 2))
f1 * (i1,(j1 + 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
LSeg ((f1 * (i1,j1)),(f1 * (i1,(j1 + 1)))) is Element of K19( the carrier of (TOP-REAL 2))
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
cell (f1,i1,i2) is Element of K19( the carrier of (TOP-REAL 2))
cell (f1,i1,j1) is Element of K19( the carrier of (TOP-REAL 2))
f1 * ((i1 + 1),j1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
LSeg ((f1 * (i1,j1)),(f1 * ((i1 + 1),j1))) is Element of K19( the carrier of (TOP-REAL 2))
cell (f1,f2,j1) is Element of K19( the carrier of (TOP-REAL 2))
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
cell (f1,f2,i2) is Element of K19( the carrier of (TOP-REAL 2))
f1 * ((f2 + 1),j1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
f1 * (f2,j1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
LSeg ((f1 * ((f2 + 1),j1)),(f1 * (f2,j1))) is Element of K19( the carrier of (TOP-REAL 2))
j1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
cell (f1,j1,G) is Element of K19( the carrier of (TOP-REAL 2))
cell (f1,i1,G) is Element of K19( the carrier of (TOP-REAL 2))
f1 * (i1,(G + 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
f1 * (i1,G) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
LSeg ((f1 * (i1,(G + 1))),(f1 * (i1,G))) is Element of K19( the carrier of (TOP-REAL 2))
k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len D is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f1 is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
(D,f1,k) is Element of K19( the carrier of (TOP-REAL 2))
Indices f1 is set
D /. k is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
D /. (k + 1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
G is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[f2,G] is set
{f2,G} is non empty set
{f2} is non empty set
{{f2,G},{f2}} is non empty set
f1 * (f2,G) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
i1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i1,j1] is set
{i1,j1} is non empty set
{i1} is non empty set
{{i1,j1},{i1}} is non empty set
f1 * (i1,j1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
G + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
cell (f1,f2,G) is Element of K19( the carrier of (TOP-REAL 2))
G -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (f1,f2,(G -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
cell (f1,i1,j1) is Element of K19( the carrier of (TOP-REAL 2))
f2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (f1,(f2 -' 1),j1) is Element of K19( the carrier of (TOP-REAL 2))
k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f1 is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f1 | D is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
f2 is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
(f1,f2,k) is Element of K19( the carrier of (TOP-REAL 2))
((f1 | D),f2,k) is Element of K19( the carrier of (TOP-REAL 2))
(f1,f2,k) is Element of K19( the carrier of (TOP-REAL 2))
((f1 | D),f2,k) is Element of K19( the carrier of (TOP-REAL 2))
len (f1 | D) is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
dom (f1 | D) is Element of K19(NAT)
(f1 | D) /. k is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
f1 /. k is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(f1 | D) /. (k + 1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
f1 /. (k + 1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
Indices f2 is set
j2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[j2,j1] is set
{j2,j1} is non empty set
{j2} is non empty set
{{j2,j1},{j2}} is non empty set
f2 * (j2,j1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i2,j2] is set
{i2,j2} is non empty set
{i2} is non empty set
{{i2,j2},{i2}} is non empty set
f2 * (i2,j2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
j1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (f2,(j2 -' 1),j1) is Element of K19( the carrier of (TOP-REAL 2))
cell (f2,j2,j1) is Element of K19( the carrier of (TOP-REAL 2))
cell (f2,j2,j1) is Element of K19( the carrier of (TOP-REAL 2))
j1 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (f2,j2,(j1 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
j2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (f2,i2,(j2 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
cell (f2,i2,j2) is Element of K19( the carrier of (TOP-REAL 2))
cell (f2,j2,j2) is Element of K19( the carrier of (TOP-REAL 2))
j2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (f2,(j2 -' 1),j2) is Element of K19( the carrier of (TOP-REAL 2))
k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k + D is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f1 is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
f1 /^ D is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len (f1 /^ D) is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
len f1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
(f1,f2,(k + D)) is Element of K19( the carrier of (TOP-REAL 2))
((f1 /^ D),f2,k) is Element of K19( the carrier of (TOP-REAL 2))
(f1,f2,(k + D)) is Element of K19( the carrier of (TOP-REAL 2))
((f1 /^ D),f2,k) is Element of K19( the carrier of (TOP-REAL 2))
(len f1) - D is V35() V36() ext-real Element of REAL
(k + 1) + D is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
(len (f1 /^ D)) + D is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
dom (f1 /^ D) is Element of K19(NAT)
(f1 /^ D) /. k is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
f1 /. (k + D) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(k + D) + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
(f1 /^ D) /. (k + 1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
f1 /. ((k + 1) + D) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
Indices f2 is set
j1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[j1,i2] is set
{j1,i2} is non empty set
{j1} is non empty set
{{j1,i2},{j1}} is non empty set
f2 * (j1,i2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
j2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
l is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[j2,l] is set
{j2,l} is non empty set
{j2} is non empty set
{{j2,l},{j2}} is non empty set
f2 * (j2,l) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
l + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j1 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (f2,(j1 -' 1),i2) is Element of K19( the carrier of (TOP-REAL 2))
cell (f2,j1,i2) is Element of K19( the carrier of (TOP-REAL 2))
cell (f2,j1,i2) is Element of K19( the carrier of (TOP-REAL 2))
i2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (f2,j1,(i2 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
l -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (f2,j2,(l -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
cell (f2,j2,l) is Element of K19( the carrier of (TOP-REAL 2))
cell (f2,j1,l) is Element of K19( the carrier of (TOP-REAL 2))
j1 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (f2,(j1 -' 1),l) is Element of K19( the carrier of (TOP-REAL 2))
k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
f1 is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like non empty V24() FinSequence-like FinSubsequence-like V166( the carrier of (TOP-REAL 2)) V167() V168() s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
len f1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
(f1,D,k) is Element of K19( the carrier of (TOP-REAL 2))
left_cell (f1,k) is Element of K19( the carrier of (TOP-REAL 2))
(f1,D,k) is Element of K19( the carrier of (TOP-REAL 2))
right_cell (f1,k) is Element of K19( the carrier of (TOP-REAL 2))
Indices D is set
f1 /. k is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
f1 /. (k + 1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
G is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[f2,G] is set
{f2,G} is non empty set
{f2} is non empty set
{{f2,G},{f2}} is non empty set
D * (f2,G) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
i1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i1,j1] is set
{i1,j1} is non empty set
{i1} is non empty set
{{i1,j1},{i1}} is non empty set
D * (i1,j1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
G + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
width D is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
len D is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D * (i1,G) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(D * (i1,G)) `2 is V35() V36() ext-real Element of REAL
D * (1,G) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(D * (1,G)) `2 is V35() V36() ext-real Element of REAL
(D * (i1,j1)) `1 is V35() V36() ext-real Element of REAL
D * (i1,1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(D * (i1,1)) `1 is V35() V36() ext-real Element of REAL
GoB f1 is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Values (GoB f1) is set
Values D is set
Indices (GoB f1) is set
j2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[j2,j1] is set
{j2,j1} is non empty set
{j2} is non empty set
{{j2,j1},{j2}} is non empty set
(GoB f1) * (j2,j1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i2,j2] is set
{i2,j2} is non empty set
{i2} is non empty set
{{i2,j2},{i2}} is non empty set
(GoB f1) * (i2,j2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
j1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
(D * (f2,G)) `1 is V35() V36() ext-real Element of REAL
D * (f2,1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(D * (f2,1)) `1 is V35() V36() ext-real Element of REAL
(D * (f2,G)) `2 is V35() V36() ext-real Element of REAL
len (GoB f1) is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
width (GoB f1) is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
(GoB f1) * (j2,j2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
((GoB f1) * (j2,j2)) `2 is V35() V36() ext-real Element of REAL
(GoB f1) * (1,j2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
((GoB f1) * (1,j2)) `2 is V35() V36() ext-real Element of REAL
((GoB f1) * (i2,j2)) `1 is V35() V36() ext-real Element of REAL
(GoB f1) * (i2,1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
((GoB f1) * (i2,1)) `1 is V35() V36() ext-real Element of REAL
((GoB f1) * (i2,j2)) `2 is V35() V36() ext-real Element of REAL
(GoB f1) * (i2,j1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
((GoB f1) * (i2,j1)) `1 is V35() V36() ext-real Element of REAL
(D * (i1,j1)) `2 is V35() V36() ext-real Element of REAL
D * (1,j1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(D * (1,j1)) `2 is V35() V36() ext-real Element of REAL
dom f1 is Element of K19(NAT)
l is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i9 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i9,(j1 + 1)] is set
{i9,(j1 + 1)} is non empty set
{i9} is non empty set
{{i9,(j1 + 1)},{i9}} is non empty set
f1 /. l is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(GoB f1) * (i9,(j1 + 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(GoB f1) * (j2,(j1 + 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
((GoB f1) * (j2,(j1 + 1))) `2 is V35() V36() ext-real Element of REAL
(GoB f1) * (1,(j1 + 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
((GoB f1) * (1,(j1 + 1))) `2 is V35() V36() ext-real Element of REAL
((GoB f1) * (i9,(j1 + 1))) `2 is V35() V36() ext-real Element of REAL
i19 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j19 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i19,j19] is set
{i19,j19} is non empty set
{i19} is non empty set
{{i19,j19},{i19}} is non empty set
D * (i19,j19) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
D * (i19,G) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(D * (i19,G)) `2 is V35() V36() ext-real Element of REAL
(D * (i19,j19)) `2 is V35() V36() ext-real Element of REAL
D * (i19,j1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(D * (i19,j1)) `2 is V35() V36() ext-real Element of REAL
((GoB f1) * (j2,j1)) `2 is V35() V36() ext-real Element of REAL
cell ((GoB f1),j2,j1) is Element of K19( the carrier of (TOP-REAL 2))
j2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell ((GoB f1),(j2 -' 1),j1) is Element of K19( the carrier of (TOP-REAL 2))
cell (D,f2,G) is Element of K19( the carrier of (TOP-REAL 2))
f2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,(f2 -' 1),G) is Element of K19( the carrier of (TOP-REAL 2))
dom f1 is Element of K19(NAT)
l is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i9 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[(j2 + 1),i9] is set
{(j2 + 1),i9} is non empty set
{(j2 + 1)} is non empty set
{{(j2 + 1),i9},{(j2 + 1)}} is non empty set
f1 /. l is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(GoB f1) * ((j2 + 1),i9) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(GoB f1) * ((j2 + 1),j1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
((GoB f1) * ((j2 + 1),j1)) `1 is V35() V36() ext-real Element of REAL
(GoB f1) * ((j2 + 1),1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
((GoB f1) * ((j2 + 1),1)) `1 is V35() V36() ext-real Element of REAL
((GoB f1) * ((j2 + 1),i9)) `1 is V35() V36() ext-real Element of REAL
(GoB f1) * ((j2 + 1),j2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
((GoB f1) * ((j2 + 1),j2)) `1 is V35() V36() ext-real Element of REAL
i19 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j19 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i19,j19] is set
{i19,j19} is non empty set
{i19} is non empty set
{{i19,j19},{i19}} is non empty set
D * (i19,j19) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(D * (i19,j19)) `1 is V35() V36() ext-real Element of REAL
D * (i19,1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(D * (i19,1)) `1 is V35() V36() ext-real Element of REAL
D * (i19,G) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(D * (i19,G)) `1 is V35() V36() ext-real Element of REAL
D * (i1,j19) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(D * (i1,j19)) `1 is V35() V36() ext-real Element of REAL
((GoB f1) * (j2,j1)) `1 is V35() V36() ext-real Element of REAL
j1 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell ((GoB f1),j2,(j1 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
cell ((GoB f1),j2,j1) is Element of K19( the carrier of (TOP-REAL 2))
G -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,f2,(G -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
cell (D,f2,G) is Element of K19( the carrier of (TOP-REAL 2))
dom f1 is Element of K19(NAT)
l is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i9 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[(i2 + 1),i9] is set
{(i2 + 1),i9} is non empty set
{(i2 + 1)} is non empty set
{{(i2 + 1),i9},{(i2 + 1)}} is non empty set
f1 /. l is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(GoB f1) * ((i2 + 1),i9) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(GoB f1) * ((i2 + 1),j1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
((GoB f1) * ((i2 + 1),j1)) `1 is V35() V36() ext-real Element of REAL
(GoB f1) * ((i2 + 1),1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
((GoB f1) * ((i2 + 1),1)) `1 is V35() V36() ext-real Element of REAL
((GoB f1) * ((i2 + 1),i9)) `1 is V35() V36() ext-real Element of REAL
(GoB f1) * ((i2 + 1),j2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
((GoB f1) * ((i2 + 1),j2)) `1 is V35() V36() ext-real Element of REAL
i19 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j19 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i19,j19] is set
{i19,j19} is non empty set
{i19} is non empty set
{{i19,j19},{i19}} is non empty set
D * (i19,j19) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(D * (i19,j19)) `1 is V35() V36() ext-real Element of REAL
D * (i19,1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(D * (i19,1)) `1 is V35() V36() ext-real Element of REAL
D * (i19,G) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(D * (i19,G)) `1 is V35() V36() ext-real Element of REAL
D * (i1,j19) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(D * (i1,j19)) `1 is V35() V36() ext-real Element of REAL
((GoB f1) * (j2,j1)) `1 is V35() V36() ext-real Element of REAL
cell ((GoB f1),i2,j2) is Element of K19( the carrier of (TOP-REAL 2))
j2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell ((GoB f1),i2,(j2 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
cell (D,i1,j1) is Element of K19( the carrier of (TOP-REAL 2))
j1 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,i1,(j1 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
(D * (i1,j1)) `2 is V35() V36() ext-real Element of REAL
D * (1,j1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(D * (1,j1)) `2 is V35() V36() ext-real Element of REAL
dom f1 is Element of K19(NAT)
l is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i9 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i9,(j2 + 1)] is set
{i9,(j2 + 1)} is non empty set
{i9} is non empty set
{{i9,(j2 + 1)},{i9}} is non empty set
f1 /. l is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(GoB f1) * (i9,(j2 + 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(GoB f1) * (j2,(j2 + 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
((GoB f1) * (j2,(j2 + 1))) `2 is V35() V36() ext-real Element of REAL
(GoB f1) * (1,(j2 + 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
((GoB f1) * (1,(j2 + 1))) `2 is V35() V36() ext-real Element of REAL
((GoB f1) * (i9,(j2 + 1))) `2 is V35() V36() ext-real Element of REAL
i19 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j19 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i19,j19] is set
{i19,j19} is non empty set
{i19} is non empty set
{{i19,j19},{i19}} is non empty set
D * (i19,j19) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
D * (i19,G) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(D * (i19,G)) `2 is V35() V36() ext-real Element of REAL
(D * (i19,j19)) `2 is V35() V36() ext-real Element of REAL
(GoB f1) * (i2,(j2 + 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
((GoB f1) * (i2,(j2 + 1))) `2 is V35() V36() ext-real Element of REAL
D * (i19,j1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(D * (i19,j1)) `2 is V35() V36() ext-real Element of REAL
((GoB f1) * (j2,j1)) `2 is V35() V36() ext-real Element of REAL
j2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell ((GoB f1),(j2 -' 1),j2) is Element of K19( the carrier of (TOP-REAL 2))
cell ((GoB f1),j2,j2) is Element of K19( the carrier of (TOP-REAL 2))
f2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,(f2 -' 1),j1) is Element of K19( the carrier of (TOP-REAL 2))
cell (D,f2,j1) is Element of K19( the carrier of (TOP-REAL 2))
f1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Indices D is set
k /. f1 is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
k /. (f1 + 1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
G is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[f2,G] is set
{f2,G} is non empty set
{f2} is non empty set
{{f2,G},{f2}} is non empty set
D * (f2,G) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
i1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i1,j1] is set
{i1,j1} is non empty set
{i1} is non empty set
{{i1,j1},{i1}} is non empty set
D * (i1,j1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
G + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
cell (D,i1,j1) is Element of K19( the carrier of (TOP-REAL 2))
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i2,j2] is set
{i2,j2} is non empty set
{i2} is non empty set
{{i2,j2},{i2}} is non empty set
j1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[j1,i2] is set
{j1,i2} is non empty set
{j1} is non empty set
{{j1,i2},{j1}} is non empty set
D * (i2,j2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
D * (j1,i2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
j2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
cell (D,j1,i2) is Element of K19( the carrier of (TOP-REAL 2))
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,j1,(i2 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
j1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j1 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,(j1 -' 1),i2) is Element of K19( the carrier of (TOP-REAL 2))
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
cell (D,(j1 -' 1),(i2 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
j1 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,i1,(j1 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i2,j2] is set
{i2,j2} is non empty set
{i2} is non empty set
{{i2,j2},{i2}} is non empty set
j1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[j1,i2] is set
{j1,i2} is non empty set
{j1} is non empty set
{{j1,i2},{j1}} is non empty set
D * (i2,j2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
D * (j1,i2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
j2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
cell (D,j1,i2) is Element of K19( the carrier of (TOP-REAL 2))
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,j1,(i2 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
j1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j1 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,(j1 -' 1),i2) is Element of K19( the carrier of (TOP-REAL 2))
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
cell (D,(j1 -' 1),(i2 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
i1 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,(i1 -' 1),j1) is Element of K19( the carrier of (TOP-REAL 2))
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i2,j2] is set
{i2,j2} is non empty set
{i2} is non empty set
{{i2,j2},{i2}} is non empty set
j1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[j1,i2] is set
{j1,i2} is non empty set
{j1} is non empty set
{{j1,i2},{j1}} is non empty set
D * (i2,j2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
D * (j1,i2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
j2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
cell (D,j1,i2) is Element of K19( the carrier of (TOP-REAL 2))
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,j1,(i2 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
j1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j1 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,(j1 -' 1),i2) is Element of K19( the carrier of (TOP-REAL 2))
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
cell (D,(j1 -' 1),(i2 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
i1 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
j1 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,(i1 -' 1),(j1 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i2,j2] is set
{i2,j2} is non empty set
{i2} is non empty set
{{i2,j2},{i2}} is non empty set
j1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[j1,i2] is set
{j1,i2} is non empty set
{j1} is non empty set
{{j1,i2},{j1}} is non empty set
D * (i2,j2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
D * (j1,i2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
j2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
cell (D,j1,i2) is Element of K19( the carrier of (TOP-REAL 2))
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,j1,(i2 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
j1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j1 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,(j1 -' 1),i2) is Element of K19( the carrier of (TOP-REAL 2))
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
cell (D,(j1 -' 1),(i2 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
i2 is Element of K19( the carrier of (TOP-REAL 2))
j2 is Element of K19( the carrier of (TOP-REAL 2))
cell (D,i1,j1) is Element of K19( the carrier of (TOP-REAL 2))
j1 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,i1,(j1 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
i1 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,(i1 -' 1),j1) is Element of K19( the carrier of (TOP-REAL 2))
i1 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
j1 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,(i1 -' 1),(j1 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
i1 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,(i1 -' 1),j1) is Element of K19( the carrier of (TOP-REAL 2))
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i2,j2] is set
{i2,j2} is non empty set
{i2} is non empty set
{{i2,j2},{i2}} is non empty set
j1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[j1,i2] is set
{j1,i2} is non empty set
{j1} is non empty set
{{j1,i2},{j1}} is non empty set
D * (i2,j2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
D * (j1,i2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
j2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j1 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,(j1 -' 1),i2) is Element of K19( the carrier of (TOP-REAL 2))
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
cell (D,j1,i2) is Element of K19( the carrier of (TOP-REAL 2))
j1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,(j1 -' 1),(i2 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
cell (D,j1,(i2 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
cell (D,i1,j1) is Element of K19( the carrier of (TOP-REAL 2))
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i2,j2] is set
{i2,j2} is non empty set
{i2} is non empty set
{{i2,j2},{i2}} is non empty set
j1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[j1,i2] is set
{j1,i2} is non empty set
{j1} is non empty set
{{j1,i2},{j1}} is non empty set
D * (i2,j2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
D * (j1,i2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
j2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j1 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,(j1 -' 1),i2) is Element of K19( the carrier of (TOP-REAL 2))
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
cell (D,j1,i2) is Element of K19( the carrier of (TOP-REAL 2))
j1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,(j1 -' 1),(i2 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
cell (D,j1,(i2 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
i1 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
j1 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,(i1 -' 1),(j1 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i2,j2] is set
{i2,j2} is non empty set
{i2} is non empty set
{{i2,j2},{i2}} is non empty set
j1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[j1,i2] is set
{j1,i2} is non empty set
{j1} is non empty set
{{j1,i2},{j1}} is non empty set
D * (i2,j2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
D * (j1,i2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
j2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j1 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,(j1 -' 1),i2) is Element of K19( the carrier of (TOP-REAL 2))
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
cell (D,j1,i2) is Element of K19( the carrier of (TOP-REAL 2))
j1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,(j1 -' 1),(i2 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
cell (D,j1,(i2 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
j1 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,i1,(j1 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i2,j2] is set
{i2,j2} is non empty set
{i2} is non empty set
{{i2,j2},{i2}} is non empty set
j1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[j1,i2] is set
{j1,i2} is non empty set
{j1} is non empty set
{{j1,i2},{j1}} is non empty set
D * (i2,j2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
D * (j1,i2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
j2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j1 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,(j1 -' 1),i2) is Element of K19( the carrier of (TOP-REAL 2))
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
cell (D,j1,i2) is Element of K19( the carrier of (TOP-REAL 2))
j1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,(j1 -' 1),(i2 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
cell (D,j1,(i2 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
i2 is Element of K19( the carrier of (TOP-REAL 2))
j2 is Element of K19( the carrier of (TOP-REAL 2))
i1 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,(i1 -' 1),j1) is Element of K19( the carrier of (TOP-REAL 2))
cell (D,i1,j1) is Element of K19( the carrier of (TOP-REAL 2))
i1 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
j1 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,(i1 -' 1),(j1 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
j1 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (D,i1,(j1 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
f1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[D,f1] is set
{D,f1} is non empty set
{D} is non empty set
{{D,f1},{D}} is non empty set
f1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[D,(f1 + 1)] is set
{D,(f1 + 1)} is non empty set
{{D,(f1 + 1)},{D}} is non empty set
f2 is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 /. k is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
f2 /. (k + 1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
G is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Indices G is set
G * (D,f1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
G * (D,(f1 + 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(f2,G,k) is Element of K19( the carrier of (TOP-REAL 2))
cell (G,(D -' 1),(f1 + 1)) is Element of K19( the carrier of (TOP-REAL 2))
(f1 + 1) + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[D,f1] is set
{D,f1} is non empty set
{D} is non empty set
{{D,f1},{D}} is non empty set
f1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[D,(f1 + 1)] is set
{D,(f1 + 1)} is non empty set
{{D,(f1 + 1)},{D}} is non empty set
f2 is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 /. k is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
f2 /. (k + 1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
G is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Indices G is set
G * (D,f1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
G * (D,(f1 + 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(f2,G,k) is Element of K19( the carrier of (TOP-REAL 2))
cell (G,D,(f1 + 1)) is Element of K19( the carrier of (TOP-REAL 2))
(f1 + 1) + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[D,f1] is set
{D,f1} is non empty set
{D} is non empty set
{{D,f1},{D}} is non empty set
[(D + 1),f1] is set
{(D + 1),f1} is non empty set
{(D + 1)} is non empty set
{{(D + 1),f1},{(D + 1)}} is non empty set
f2 is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 /. k is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
f2 /. (k + 1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
G is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Indices G is set
G * (D,f1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
G * ((D + 1),f1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(f2,G,k) is Element of K19( the carrier of (TOP-REAL 2))
cell (G,(D + 1),f1) is Element of K19( the carrier of (TOP-REAL 2))
(D + 1) + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[D,f1] is set
{D,f1} is non empty set
{D} is non empty set
{{D,f1},{D}} is non empty set
[(D + 1),f1] is set
{(D + 1),f1} is non empty set
{(D + 1)} is non empty set
{{(D + 1),f1},{(D + 1)}} is non empty set
f1 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
f2 is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 /. k is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
f2 /. (k + 1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
G is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Indices G is set
G * (D,f1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
G * ((D + 1),f1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(f2,G,k) is Element of K19( the carrier of (TOP-REAL 2))
cell (G,(D + 1),(f1 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
(D + 1) + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
f1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[D,f1] is set
{D,f1} is non empty set
{D} is non empty set
{{D,f1},{D}} is non empty set
[(D + 1),f1] is set
{(D + 1),f1} is non empty set
{(D + 1)} is non empty set
{{(D + 1),f1},{(D + 1)}} is non empty set
f1 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
f2 is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 /. k is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
f2 /. (k + 1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
G is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Indices G is set
G * ((D + 1),f1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
G * (D,f1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(f2,G,k) is Element of K19( the carrier of (TOP-REAL 2))
cell (G,(D -' 1),(f1 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
(D + 1) + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
f1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[D,f1] is set
{D,f1} is non empty set
{D} is non empty set
{{D,f1},{D}} is non empty set
[(D + 1),f1] is set
{(D + 1),f1} is non empty set
{(D + 1)} is non empty set
{{(D + 1),f1},{(D + 1)}} is non empty set
f2 is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 /. k is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
f2 /. (k + 1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
G is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Indices G is set
G * ((D + 1),f1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
G * (D,f1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(f2,G,k) is Element of K19( the carrier of (TOP-REAL 2))
cell (G,(D -' 1),f1) is Element of K19( the carrier of (TOP-REAL 2))
(D + 1) + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[D,(f1 + 1)] is set
{D,(f1 + 1)} is non empty set
{D} is non empty set
{{D,(f1 + 1)},{D}} is non empty set
[D,f1] is set
{D,f1} is non empty set
{{D,f1},{D}} is non empty set
f1 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
f2 is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 /. k is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
f2 /. (k + 1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
G is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Indices G is set
G * (D,(f1 + 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
G * (D,f1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(f2,G,k) is Element of K19( the carrier of (TOP-REAL 2))
cell (G,D,(f1 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
(f1 + 1) + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
f1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[D,(f1 + 1)] is set
{D,(f1 + 1)} is non empty set
{D} is non empty set
{{D,(f1 + 1)},{D}} is non empty set
[D,f1] is set
{D,f1} is non empty set
{{D,f1},{D}} is non empty set
f1 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
f2 is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 /. k is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
f2 /. (k + 1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
G is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Indices G is set
G * (D,(f1 + 1)) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
G * (D,f1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(f2,G,k) is Element of K19( the carrier of (TOP-REAL 2))
cell (G,(D -' 1),(f1 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
(f1 + 1) + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f1 is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f1 | D is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
f2 is V1() non empty-yielding V4( NAT ) V5( the carrier of (TOP-REAL 2) * ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
(f1,f2,k) is Element of K19( the carrier of (TOP-REAL 2))
((f1 | D),f2,k) is Element of K19( the carrier of (TOP-REAL 2))
(f1,f2,k) is Element of K19( the carrier of (TOP-REAL 2))
((f1 | D),f2,k) is Element of K19( the carrier of (TOP-REAL 2))
len (f1 | D) is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
dom (f1 | D) is Element of K19(NAT)
(f1 | D) /. k is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
f1 /. k is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
(f1 | D) /. (k + 1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
f1 /. (k + 1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
Indices f2 is set
j2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[j2,j1] is set
{j2,j1} is non empty set
{j2} is non empty set
{{j2,j1},{j2}} is non empty set
f2 * (j2,j1) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i2,j2] is set
{i2,j2} is non empty set
{i2} is non empty set
{{i2,j2},{i2}} is non empty set
f2 * (i2,j2) is V31(2) FinSequence-like V48() Element of the carrier of (TOP-REAL 2)
j1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (f2,(i2 -' 1),j2) is Element of K19( the carrier of (TOP-REAL 2))
cell (f2,i2,j2) is Element of K19( the carrier of (TOP-REAL 2))
cell (f2,i2,j2) is Element of K19( the carrier of (TOP-REAL 2))
j2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (f2,i2,(j2 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
i2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
j2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (f2,(i2 -' 1),(j2 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
cell (f2,(i2 -' 1),j2) is Element of K19( the carrier of (TOP-REAL 2))
j2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (f2,i2,(j2 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
i2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
cell (f2,(i2 -' 1),(j2 -' 1)) is Element of K19( the carrier of (TOP-REAL 2))
k is set
k * is functional non empty FinSequence-membered FinSequenceSet of k
k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k + 2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f1 is set
f1 * is functional non empty FinSequence-membered FinSequenceSet of f1
f2 is V1() V4( NAT ) V5(f1) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of f1
f2 | D is V1() V4( NAT ) V5(f1) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of f1
G is V1() V4( NAT ) V5(f1 * ) Function-like V24() FinSequence-like FinSubsequence-like tabular FinSequence of f1 *
len f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
len f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i1,j1] is set
{i1,j1} is non empty set
{i1} is non empty set
{{i1,j1},{i1}} is non empty set
Indices G is set
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i2,j2] is set
{i2,j2} is non empty set
{i2} is non empty set
{{i2,j2},{i2}} is non empty set
f2 /. k is Element of f1
G * (i1,j1) is Element of f1
k + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 /. (k + 1) is Element of f1
G * (i2,j2) is Element of f1
j1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[(i2 + 1),j2] is set
{(i2 + 1),j2} is non empty set
{(i2 + 1)} is non empty set
{{(i2 + 1),j2},{(i2 + 1)}} is non empty set
f2 /. (k + 2) is Element of f1
G * ((i2 + 1),j2) is Element of f1
i1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
[i2,(j2 -' 1)] is set
{i2,(j2 -' 1)} is non empty set
{{i2,(j2 -' 1)},{i2}} is non empty set
G * (i2,(j2 -' 1)) is Element of f1
j2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i2,(j2 + 1)] is set
{i2,(j2 + 1)} is non empty set
{{i2,(j2 + 1)},{i2}} is non empty set
G * (i2,(j2 + 1)) is Element of f1
i2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
[(i2 -' 1),j2] is set
{(i2 -' 1),j2} is non empty set
{(i2 -' 1)} is non empty set
{{(i2 -' 1),j2},{(i2 -' 1)}} is non empty set
G * ((i2 -' 1),j2) is Element of f1
len (f2 | D) is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
dom (f2 | D) is Element of K19(NAT)
(f2 | D) /. (k + 1) is Element of f1
(f2 | D) /. (k + 2) is Element of f1
(f2 | D) /. k is Element of f1
len f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k + 2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f1 is set
f1 * is functional non empty FinSequence-membered FinSequenceSet of f1
f2 is V1() V4( NAT ) V5(f1) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of f1
f2 | D is V1() V4( NAT ) V5(f1) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of f1
G is V1() V4( NAT ) V5(f1 * ) Function-like V24() FinSequence-like FinSubsequence-like tabular FinSequence of f1 *
len f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
len f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i1,j1] is set
{i1,j1} is non empty set
{i1} is non empty set
{{i1,j1},{i1}} is non empty set
Indices G is set
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i2,j2] is set
{i2,j2} is non empty set
{i2} is non empty set
{{i2,j2},{i2}} is non empty set
f2 /. k is Element of f1
G * (i1,j1) is Element of f1
k + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 /. (k + 1) is Element of f1
G * (i2,j2) is Element of f1
j1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
[(i2 -' 1),j2] is set
{(i2 -' 1),j2} is non empty set
{(i2 -' 1)} is non empty set
{{(i2 -' 1),j2},{(i2 -' 1)}} is non empty set
f2 /. (k + 2) is Element of f1
G * ((i2 -' 1),j2) is Element of f1
i1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i2,(j2 + 1)] is set
{i2,(j2 + 1)} is non empty set
{{i2,(j2 + 1)},{i2}} is non empty set
G * (i2,(j2 + 1)) is Element of f1
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
[i2,(j2 -' 1)] is set
{i2,(j2 -' 1)} is non empty set
{{i2,(j2 -' 1)},{i2}} is non empty set
G * (i2,(j2 -' 1)) is Element of f1
[(i2 + 1),j2] is set
{(i2 + 1),j2} is non empty set
{(i2 + 1)} is non empty set
{{(i2 + 1),j2},{(i2 + 1)}} is non empty set
G * ((i2 + 1),j2) is Element of f1
len (f2 | D) is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
dom (f2 | D) is Element of K19(NAT)
(f2 | D) /. (k + 1) is Element of f1
(f2 | D) /. (k + 2) is Element of f1
(f2 | D) /. k is Element of f1
len f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k + 2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
D is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f1 is set
f1 * is functional non empty FinSequence-membered FinSequenceSet of f1
f2 is V1() V4( NAT ) V5(f1) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of f1
f2 | D is V1() V4( NAT ) V5(f1) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of f1
G is V1() V4( NAT ) V5(f1 * ) Function-like V24() FinSequence-like FinSubsequence-like tabular FinSequence of f1 *
len f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
len f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i1,j1] is set
{i1,j1} is non empty set
{i1} is non empty set
{{i1,j1},{i1}} is non empty set
Indices G is set
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i2,j2] is set
{i2,j2} is non empty set
{i2} is non empty set
{{i2,j2},{i2}} is non empty set
f2 /. k is Element of f1
G * (i1,j1) is Element of f1
k + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 /. (k + 1) is Element of f1
G * (i2,j2) is Element of f1
j1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i2,(j2 + 1)] is set
{i2,(j2 + 1)} is non empty set
{{i2,(j2 + 1)},{i2}} is non empty set
f2 /. (k + 2) is Element of f1
G * (i2,(j2 + 1)) is Element of f1
i1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[(i2 + 1),j2] is set
{(i2 + 1),j2} is non empty set
{(i2 + 1)} is non empty set
{{(i2 + 1),j2},{(i2 + 1)}} is non empty set
G * ((i2 + 1),j2) is Element of f1
i2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
[(i2 -' 1),j2] is set
{(i2 -' 1),j2} is non empty set
{(i2 -' 1)} is non empty set
{{(i2 -' 1),j2},{(i2 -' 1)}} is non empty set
G * ((i2 -' 1),j2) is Element of f1
j2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
[i2,(j2 -' 1)] is set
{i2,(j2 -' 1)} is non empty set
{{i2,(j2 -' 1)},{i2}} is non empty set
G * (i2,(j2 -' 1)) is Element of f1
len (f2 | D) is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
dom (f2 | D) is Element of K19(NAT)
(f2 | D) /. (k + 1) is Element of f1
(f2 | D) /. (k + 2) is Element of f1
(f2 | D) /. k is Element of f1
len f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
D is set
D * is functional non empty FinSequence-membered FinSequenceSet of D
f1 is V1() V4( NAT ) V5(D) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of D
len f1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f1 | k is V1() V4( NAT ) V5(D) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of D
f1 | (k + 1) is V1() V4( NAT ) V5(D) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of D
f2 is V1() V4( NAT ) V5(D) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of D
len f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 | k is V1() V4( NAT ) V5(D) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of D
f2 | (k + 1) is V1() V4( NAT ) V5(D) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of D
G is V1() V4( NAT ) V5(D * ) Function-like V24() FinSequence-like FinSubsequence-like tabular FinSequence of D *
len (f1 | k) is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
dom (f1 | k) is Element of K19(NAT)
f2 /. k is Element of D
(f2 | k) /. k is Element of D
f2 /. (k -' 1) is Element of D
(f2 | k) /. (k -' 1) is Element of D
f1 /. k is Element of D
(f1 | k) /. k is Element of D
f1 /. (k -' 1) is Element of D
(f1 | k) /. (k -' 1) is Element of D
(k -' 1) + 1 is V14() V15() V16() V20() V35() V36() ext-real positive Element of NAT
1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
(k -' 1) + (1 + 1) is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
Indices G is set
i1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i1,j1] is set
{i1,j1} is non empty set
{i1} is non empty set
{{i1,j1},{i1}} is non empty set
G * (i1,j1) is Element of D
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i2,j2] is set
{i2,j2} is non empty set
{i2} is non empty set
{{i2,j2},{i2}} is non empty set
G * (i2,j2) is Element of D
j1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f1 /. (k + 1) is Element of D
G * ((i2 + 1),j2) is Element of D
f2 /. (k + 1) is Element of D
f1 /. (k + 1) is Element of D
j2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
G * (i2,(j2 -' 1)) is Element of D
f2 /. (k + 1) is Element of D
f1 /. (k + 1) is Element of D
G * (i2,(j2 + 1)) is Element of D
f2 /. (k + 1) is Element of D
f1 /. (k + 1) is Element of D
i2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
G * ((i2 -' 1),j2) is Element of D
f2 /. (k + 1) is Element of D
f1 /. (k + 1) is Element of D
f2 /. (k + 1) is Element of D
f1 /. (k + 1) is Element of D
f2 /. (k + 1) is Element of D
<*(f2 /. (k + 1))*> is V1() V4( NAT ) Function-like non empty V24() V31(1) FinSequence-like FinSubsequence-like set
(f2 | k) ^ <*(f2 /. (k + 1))*> is V1() V4( NAT ) Function-like non empty V24() FinSequence-like FinSubsequence-like set
k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
D is set
D * is functional non empty FinSequence-membered FinSequenceSet of D
f1 is V1() V4( NAT ) V5(D) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of D
len f1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f1 | k is V1() V4( NAT ) V5(D) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of D
f1 | (k + 1) is V1() V4( NAT ) V5(D) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of D
f2 is V1() V4( NAT ) V5(D) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of D
len f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 | k is V1() V4( NAT ) V5(D) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of D
f2 | (k + 1) is V1() V4( NAT ) V5(D) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of D
G is V1() V4( NAT ) V5(D * ) Function-like V24() FinSequence-like FinSubsequence-like tabular FinSequence of D *
len (f1 | k) is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
dom (f1 | k) is Element of K19(NAT)
f2 /. k is Element of D
(f2 | k) /. k is Element of D
f2 /. (k -' 1) is Element of D
(f2 | k) /. (k -' 1) is Element of D
f1 /. k is Element of D
(f1 | k) /. k is Element of D
f1 /. (k -' 1) is Element of D
(f1 | k) /. (k -' 1) is Element of D
(k -' 1) + 1 is V14() V15() V16() V20() V35() V36() ext-real positive Element of NAT
1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
(k -' 1) + (1 + 1) is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
Indices G is set
i1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i1,j1] is set
{i1,j1} is non empty set
{i1} is non empty set
{{i1,j1},{i1}} is non empty set
G * (i1,j1) is Element of D
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i2,j2] is set
{i2,j2} is non empty set
{i2} is non empty set
{{i2,j2},{i2}} is non empty set
G * (i2,j2) is Element of D
j1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f1 /. (k + 1) is Element of D
i2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
G * ((i2 -' 1),j2) is Element of D
f2 /. (k + 1) is Element of D
f1 /. (k + 1) is Element of D
G * (i2,(j2 + 1)) is Element of D
f2 /. (k + 1) is Element of D
f1 /. (k + 1) is Element of D
j2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
G * (i2,(j2 -' 1)) is Element of D
f2 /. (k + 1) is Element of D
f1 /. (k + 1) is Element of D
G * ((i2 + 1),j2) is Element of D
f2 /. (k + 1) is Element of D
f1 /. (k + 1) is Element of D
f2 /. (k + 1) is Element of D
f1 /. (k + 1) is Element of D
f2 /. (k + 1) is Element of D
<*(f2 /. (k + 1))*> is V1() V4( NAT ) Function-like non empty V24() V31(1) FinSequence-like FinSubsequence-like set
(f2 | k) ^ <*(f2 /. (k + 1))*> is V1() V4( NAT ) Function-like non empty V24() FinSequence-like FinSubsequence-like set
k is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
k -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
D is set
D * is functional non empty FinSequence-membered FinSequenceSet of D
f1 is V1() V4( NAT ) V5(D) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of D
len f1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f1 | k is V1() V4( NAT ) V5(D) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of D
f1 | (k + 1) is V1() V4( NAT ) V5(D) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of D
f2 is V1() V4( NAT ) V5(D) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of D
len f2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f2 | k is V1() V4( NAT ) V5(D) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of D
f2 | (k + 1) is V1() V4( NAT ) V5(D) Function-like V24() FinSequence-like FinSubsequence-like FinSequence of D
G is V1() V4( NAT ) V5(D * ) Function-like V24() FinSequence-like FinSubsequence-like tabular FinSequence of D *
len (f1 | k) is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
dom (f1 | k) is Element of K19(NAT)
f2 /. k is Element of D
(f2 | k) /. k is Element of D
f2 /. (k -' 1) is Element of D
(f2 | k) /. (k -' 1) is Element of D
f1 /. k is Element of D
(f1 | k) /. k is Element of D
f1 /. (k -' 1) is Element of D
(f1 | k) /. (k -' 1) is Element of D
(k -' 1) + 1 is V14() V15() V16() V20() V35() V36() ext-real positive Element of NAT
1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
(k -' 1) + (1 + 1) is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
Indices G is set
i1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i1,j1] is set
{i1,j1} is non empty set
{i1} is non empty set
{{i1,j1},{i1}} is non empty set
G * (i1,j1) is Element of D
i2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
[i2,j2] is set
{i2,j2} is non empty set
{i2} is non empty set
{{i2,j2},{i2}} is non empty set
G * (i2,j2) is Element of D
j1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i1 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
i2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
j2 + 1 is V14() V15() V16() V20() V35() V36() ext-real Element of NAT
f1 /. (k + 1) is Element of D
G * (i2,(j2 + 1)) is Element of D
f2 /. (k + 1) is Element of D
f1 /. (k + 1) is Element of D
G * ((i2 + 1),j2) is Element of D
f2 /. (k + 1) is Element of D
f1 /. (k + 1) is Element of D
i2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
G * ((i2 -' 1),j2) is Element of D
f2 /. (k + 1) is Element of D
f1 /. (k + 1) is Element of D
j2 -' 1 is V14() V15() V16() V20() V35() V36() ext-real non negative Element of NAT
G * (i2,(j2 -' 1)) is Element of D
f2 /. (k + 1) is Element of D
f1 /. (k + 1) is Element of D
f2 /. (k + 1) is Element of D
f1 /. (k + 1) is Element of D
f2 /. (k + 1) is Element of D
<*(f2 /. (k + 1))*> is V1() V4( NAT ) Function-like non empty V24() V31(1) FinSequence-like FinSubsequence-like set
(f2 | k) ^ <*(f2 /. (k + 1))*> is V1() V4( NAT ) Function-like non empty V24() FinSequence-like FinSubsequence-like set