REAL is non empty V38() V174() V175() V176() V180() set
NAT is V174() V175() V176() V177() V178() V179() V180() Element of K19(REAL)
K19(REAL) is non empty set
COMPLEX is non empty V38() V174() V180() set
omega is V174() V175() V176() V177() V178() V179() V180() set
K19(omega) is non empty set
K19(NAT) is non empty set
1 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
K20(1,1) is non empty set
K19(K20(1,1)) is non empty set
K20(K20(1,1),1) is non empty set
K19(K20(K20(1,1),1)) is non empty set
K20(K20(1,1),REAL) is non empty set
K19(K20(K20(1,1),REAL)) is non empty set
K20(REAL,REAL) is non empty set
K20(K20(REAL,REAL),REAL) is non empty set
K19(K20(K20(REAL,REAL),REAL)) is non empty set
2 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
K20(2,2) is non empty set
K20(K20(2,2),REAL) is non empty set
K19(K20(K20(2,2),REAL)) is non empty set
RAT is non empty V38() V174() V175() V176() V177() V180() set
INT is non empty V38() V174() V175() V176() V177() V178() V180() set
K19(K20(REAL,REAL)) is non empty set
K404() is non empty V123() L10()
the carrier of K404() is non empty set
K409() is non empty V123() V145() V146() V147() V149() V196() V197() V198() V199() V200() V201() L10()
K410() is non empty V123() V147() V149() V199() V200() V201() M15(K409())
K411() is non empty V123() V145() V147() V149() V199() V200() V201() V202() M18(K409(),K410())
K413() is non empty V123() V145() V147() V149() L10()
K414() is non empty V123() V145() V147() V149() V202() M15(K413())
TOP-REAL 2 is non empty V55() TopSpace-like V121() V186() V187() V204() V205() V206() V207() V208() V209() V210() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL 2) is non empty V12() set
the carrier of (TOP-REAL 2) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (TOP-REAL 2)
K20( the carrier of (TOP-REAL 2),REAL) is non empty set
K19(K20( the carrier of (TOP-REAL 2),REAL)) is non empty set
K19( the carrier of (TOP-REAL 2)) is non empty set
K20(COMPLEX,COMPLEX) is non empty set
K19(K20(COMPLEX,COMPLEX)) is non empty set
K20(COMPLEX,REAL) is non empty set
K19(K20(COMPLEX,REAL)) is non empty set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is non empty set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is non empty set
K20(RAT,RAT) is non empty set
K19(K20(RAT,RAT)) is non empty set
K20(K20(RAT,RAT),RAT) is non empty set
K19(K20(K20(RAT,RAT),RAT)) is non empty set
K20(INT,INT) is non empty set
K19(K20(INT,INT)) is non empty set
K20(K20(INT,INT),INT) is non empty set
K19(K20(K20(INT,INT),INT)) is non empty set
K20(NAT,NAT) is set
K20(K20(NAT,NAT),NAT) is set
K19(K20(K20(NAT,NAT),NAT)) is non empty set
{} is Function-like functional empty V12() FinSequence-membered V174() V175() V176() V177() V178() V179() V180() set
the Function-like functional empty V12() FinSequence-membered V174() V175() V176() V177() V178() V179() V180() set is Function-like functional empty V12() FinSequence-membered V174() V175() V176() V177() V178() V179() V180() set
3 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
0 is Function-like functional empty V12() ordinal natural V28() real ext-real non positive non negative integer FinSequence-membered V108() V174() V175() V176() V177() V178() V179() V180() Element of NAT
Seg 1 is non empty V38() V45(1) V174() V175() V176() V177() V178() V179() Element of K19(NAT)
{1} is non empty V12() V174() V175() V176() V177() V178() V179() set
Seg 2 is non empty V38() V45(2) V174() V175() V176() V177() V178() V179() Element of K19(NAT)
{1,2} is non empty V174() V175() V176() V177() V178() V179() set
4 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
proj1 is Relation-like the carrier of (TOP-REAL 2) -defined REAL -valued Function-like V18( the carrier of (TOP-REAL 2), REAL ) V229( TOP-REAL 2) Element of K19(K20( the carrier of (TOP-REAL 2),REAL))
proj2 is Relation-like the carrier of (TOP-REAL 2) -defined REAL -valued Function-like V18( the carrier of (TOP-REAL 2), REAL ) V229( TOP-REAL 2) Element of K19(K20( the carrier of (TOP-REAL 2),REAL))
Euclid 2 is non empty strict Reflexive discerning symmetric triangle MetrStruct
REAL 2 is functional non empty FinSequence-membered FinSequenceSet of REAL
2 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
Pitag_dist 2 is Relation-like K20((REAL 2),(REAL 2)) -defined REAL -valued Function-like V18(K20((REAL 2),(REAL 2)), REAL ) Element of K19(K20(K20((REAL 2),(REAL 2)),REAL))
K20((REAL 2),(REAL 2)) is non empty set
K20(K20((REAL 2),(REAL 2)),REAL) is non empty set
K19(K20(K20((REAL 2),(REAL 2)),REAL)) is non empty set
MetrStruct(# (REAL 2),(Pitag_dist 2) #) is strict MetrStruct
the carrier of (Euclid 2) is non empty set
0.REAL 2 is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
2 |-> 0 is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like Element of 2 -tuples_on REAL
g is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() V38() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
L~ g is non empty boundary compact bounded non horizontal non vertical Element of K19( the carrier of (TOP-REAL 2))
A is Element of K19( the carrier of (TOP-REAL 2))
A is Element of the carrier of (Euclid 2)
K19( the carrier of (Euclid 2)) is non empty set
x is bounded Element of K19( the carrier of (Euclid 2))
x is V28() real ext-real Element of REAL
b is Element of the carrier of (Euclid 2)
dist (A,b) is V28() real ext-real Element of REAL
(dist (A,b)) + x is V28() real ext-real Element of REAL
((dist (A,b)) + x) + 1 is V28() real ext-real Element of REAL
Ball (A,(((dist (A,b)) + x) + 1)) is Element of K19( the carrier of (Euclid 2))
(Ball (A,(((dist (A,b)) + x) + 1))) ` is Element of K19( the carrier of (Euclid 2))
the carrier of (Euclid 2) \ (Ball (A,(((dist (A,b)) + x) + 1))) is set
{ b1 where b1 is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2) : not ((dist (A,b)) + x) + 1 <= |.b1.| } is set
(REAL 2) \ { b1 where b1 is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2) : not ((dist (A,b)) + x) + 1 <= |.b1.| } is functional FinSequence-membered Element of K19((REAL 2))
K19((REAL 2)) is non empty set
((dist (A,b)) + x) + 0 is V28() real ext-real Element of REAL
abs (((dist (A,b)) + x) + 1) is V28() real ext-real Element of REAL
|[0,(((dist (A,b)) + x) + 1)]| is Relation-like NAT -defined Function-like non empty V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
O is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
|.O.| is V28() real ext-real non negative Element of REAL
K391(O) is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of REAL
K397(K391(O)) is V28() real ext-real Element of REAL
sqrt K397(K391(O)) is V28() real ext-real Element of REAL
i is set
p2 is Element of the carrier of (Euclid 2)
dist (A,p2) is V28() real ext-real Element of REAL
x is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
|.x.| is V28() real ext-real non negative Element of REAL
K391(x) is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of REAL
K397(K391(x)) is V28() real ext-real Element of REAL
sqrt K397(K391(x)) is V28() real ext-real Element of REAL
p is set
q is Element of the carrier of (Euclid 2)
dist (b,q) is V28() real ext-real Element of REAL
(dist (A,b)) + (dist (b,q)) is V28() real ext-real Element of REAL
dist (A,q) is V28() real ext-real Element of REAL
O is non empty Element of K19( the carrier of (TOP-REAL 2))
(L~ g) ` is non empty Element of K19( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ (L~ g) is set
p is set
q is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
|.q.| is V28() real ext-real non negative Element of REAL
K391(q) is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of REAL
K397(K391(q)) is V28() real ext-real Element of REAL
sqrt K397(K391(q)) is V28() real ext-real Element of REAL
t is Element of the carrier of (Euclid 2)
dist (t,A) is V28() real ext-real Element of REAL
p is Element of K19( the carrier of (TOP-REAL 2))
q is Element of K19( the carrier of (Euclid 2))
{ b1 where b1 is Element of K19( the carrier of (TOP-REAL 2)) : b1 is_outside_component_of L~ g } is set
q is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
|.q.| is V28() real ext-real non negative Element of REAL
K391(q) is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of REAL
K397(K391(q)) is V28() real ext-real Element of REAL
sqrt K397(K391(q)) is V28() real ext-real Element of REAL
UBD (L~ g) is non empty connected Element of K19( the carrier of (TOP-REAL 2))
union { b1 where b1 is Element of K19( the carrier of (TOP-REAL 2)) : b1 is_outside_component_of L~ g } is set
g is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
TOP-REAL g is non empty TopSpace-like V121() V186() V187() V204() V205() V206() V207() V208() V209() V210() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL g) is non empty set
A is Relation-like NAT -defined the carrier of (TOP-REAL g) -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL g)
L~ A is Element of K19( the carrier of (TOP-REAL g))
K19( the carrier of (TOP-REAL g)) is non empty set
len A is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
1 + 1 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
g is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
g + 1 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
A is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
A + 1 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
A is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like V38() 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 A is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
width A is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
cell (A,g,A) is Element of K19( the carrier of (TOP-REAL 2))
A * (g,1) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
(A * (g,1)) `1 is V28() real ext-real Element of REAL
K526((A * (g,1)),1) is V28() real ext-real Element of REAL
A * ((g + 1),1) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
(A * ((g + 1),1)) `1 is V28() real ext-real Element of REAL
K526((A * ((g + 1),1)),1) is V28() real ext-real Element of REAL
[.((A * (g,1)) `1),((A * ((g + 1),1)) `1).] is compact V174() V175() V176() real-bounded Element of K19(REAL)
A * (1,A) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
(A * (1,A)) `2 is V28() real ext-real Element of REAL
K526((A * (1,A)),2) is V28() real ext-real Element of REAL
A * (1,(A + 1)) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
(A * (1,(A + 1))) `2 is V28() real ext-real Element of REAL
K526((A * (1,(A + 1))),2) is V28() real ext-real Element of REAL
[.((A * (1,A)) `2),((A * (1,(A + 1))) `2).] is compact V174() V175() V176() real-bounded Element of K19(REAL)
(1,2) --> ([.((A * (g,1)) `1),((A * ((g + 1),1)) `1).],[.((A * (1,A)) `2),((A * (1,(A + 1))) `2).]) is Relation-like {1,2} -defined K19(REAL) -valued Function-like V18({1,2},K19(REAL)) Element of K19(K20({1,2},K19(REAL)))
K20({1,2},K19(REAL)) is non empty set
K19(K20({1,2},K19(REAL))) is non empty set
product ((1,2) --> ([.((A * (g,1)) `1),((A * ((g + 1),1)) `1).],[.((A * (1,A)) `2),((A * (1,(A + 1))) `2).])) is set
{ b1 where b1 is V28() real ext-real Element of REAL : ( (A * (1,A)) `2 <= b1 & b1 <= (A * (1,(A + 1))) `2 ) } is set
dom ((1,2) --> ([.((A * (g,1)) `1),((A * ((g + 1),1)) `1).],[.((A * (1,A)) `2),((A * (1,(A + 1))) `2).])) is V174() V175() V176() V177() V178() V179() Element of K19({1,2})
K19({1,2}) is non empty set
{ |[b1,b2]| where b1, b2 is V28() real ext-real Element of REAL : ( (A * (g,1)) `1 <= b1 & b1 <= (A * ((g + 1),1)) `1 & (A * (1,A)) `2 <= b2 & b2 <= (A * (1,(A + 1))) `2 ) } is set
{ b1 where b1 is V28() real ext-real Element of REAL : ( (A * (g,1)) `1 <= b1 & b1 <= (A * ((g + 1),1)) `1 ) } is set
x is set
b is V28() real ext-real Element of REAL
c is V28() real ext-real Element of REAL
|[b,c]| is Relation-like NAT -defined Function-like non empty V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
<*b,c*> is Relation-like NAT -defined Function-like non empty V38() V45(2) FinSequence-like FinSubsequence-like set
c is set
<*b,c*> . c is set
((1,2) --> ([.((A * (g,1)) `1),((A * ((g + 1),1)) `1).],[.((A * (1,A)) `2),((A * (1,(A + 1))) `2).])) . c is set
|[b,c]| `2 is V28() real ext-real Element of REAL
K526(|[b,c]|,2) is V28() real ext-real Element of REAL
<*b,c*> . 2 is set
|[b,c]| `1 is V28() real ext-real Element of REAL
K526(|[b,c]|,1) is V28() real ext-real Element of REAL
<*b,c*> . 1 is set
dom <*b,c*> is V174() V175() V176() V177() V178() V179() Element of K19(NAT)
x is set
b is Relation-like Function-like set
dom b is set
b . 2 is set
((1,2) --> ([.((A * (g,1)) `1),((A * ((g + 1),1)) `1).],[.((A * (1,A)) `2),((A * (1,(A + 1))) `2).])) . 2 is set
c is V28() real ext-real Element of REAL
b . 1 is set
((1,2) --> ([.((A * (g,1)) `1),((A * ((g + 1),1)) `1).],[.((A * (1,A)) `2),((A * (1,(A + 1))) `2).])) . 1 is set
c is V28() real ext-real Element of REAL
<*c,c*> is Relation-like NAT -defined Function-like non empty V38() V45(2) FinSequence-like FinSubsequence-like set
O is set
b . O is set
<*c,c*> . O is set
dom <*c,c*> is V174() V175() V176() V177() V178() V179() Element of K19(NAT)
|[c,c]| is Relation-like NAT -defined Function-like non empty V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
g is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
A is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
A is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like V38() 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 A is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
width A is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
cell (A,g,A) is Element of K19( the carrier of (TOP-REAL 2))
A * (g,1) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
(A * (g,1)) `1 is V28() real ext-real Element of REAL
K526((A * (g,1)),1) is V28() real ext-real Element of REAL
g + 1 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
A * ((g + 1),1) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
(A * ((g + 1),1)) `1 is V28() real ext-real Element of REAL
K526((A * ((g + 1),1)),1) is V28() real ext-real Element of REAL
[.((A * (g,1)) `1),((A * ((g + 1),1)) `1).] is compact V174() V175() V176() real-bounded Element of K19(REAL)
A * (1,A) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
(A * (1,A)) `2 is V28() real ext-real Element of REAL
K526((A * (1,A)),2) is V28() real ext-real Element of REAL
A + 1 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
A * (1,(A + 1)) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
(A * (1,(A + 1))) `2 is V28() real ext-real Element of REAL
K526((A * (1,(A + 1))),2) is V28() real ext-real Element of REAL
[.((A * (1,A)) `2),((A * (1,(A + 1))) `2).] is compact V174() V175() V176() real-bounded Element of K19(REAL)
(1,2) --> ([.((A * (g,1)) `1),((A * ((g + 1),1)) `1).],[.((A * (1,A)) `2),((A * (1,(A + 1))) `2).]) is Relation-like {1,2} -defined K19(REAL) -valued Function-like V18({1,2},K19(REAL)) Element of K19(K20({1,2},K19(REAL)))
K20({1,2},K19(REAL)) is non empty set
K19(K20({1,2},K19(REAL))) is non empty set
product ((1,2) --> ([.((A * (g,1)) `1),((A * ((g + 1),1)) `1).],[.((A * (1,A)) `2),((A * (1,(A + 1))) `2).])) is set
g is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
A is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
[g,A] is non empty set
{g,A} is non empty V174() V175() V176() V177() V178() V179() set
{g} is non empty V12() V174() V175() V176() V177() V178() V179() set
{{g,A},{g}} is non empty set
A is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
g + A is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
[(g + A),A] is non empty set
{(g + A),A} is non empty V174() V175() V176() V177() V178() V179() set
{(g + A)} is non empty V12() V174() V175() V176() V177() V178() V179() set
{{(g + A),A},{(g + A)}} is non empty set
x is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like V38() 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 x is set
x * (g,A) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
x * ((g + A),A) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
dist ((x * (g,A)),(x * ((g + A),A))) is V28() real ext-real Element of REAL
(x * ((g + A),A)) `1 is V28() real ext-real Element of REAL
K526((x * ((g + A),A)),1) is V28() real ext-real Element of REAL
(x * (g,A)) `1 is V28() real ext-real Element of REAL
K526((x * (g,A)),1) is V28() real ext-real Element of REAL
((x * ((g + A),A)) `1) - ((x * (g,A)) `1) is V28() real ext-real Element of REAL
len x is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
width x is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
((x * (g,A)) `1) - ((x * (g,A)) `1) is V28() real ext-real Element of REAL
(x * (g,A)) `2 is V28() real ext-real Element of REAL
K526((x * (g,A)),2) is V28() real ext-real Element of REAL
x * (1,A) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
(x * (1,A)) `2 is V28() real ext-real Element of REAL
K526((x * (1,A)),2) is V28() real ext-real Element of REAL
(x * ((g + A),A)) `2 is V28() real ext-real Element of REAL
K526((x * ((g + A),A)),2) is V28() real ext-real Element of REAL
((x * (g,A)) `1) - ((x * ((g + A),A)) `1) is V28() real ext-real Element of REAL
(((x * (g,A)) `1) - ((x * ((g + A),A)) `1)) ^2 is V28() real ext-real Element of REAL
K104((((x * (g,A)) `1) - ((x * ((g + A),A)) `1)),(((x * (g,A)) `1) - ((x * ((g + A),A)) `1))) is V28() real ext-real set
((x * (g,A)) `2) - ((x * ((g + A),A)) `2) is V28() real ext-real Element of REAL
(((x * (g,A)) `2) - ((x * ((g + A),A)) `2)) ^2 is V28() real ext-real Element of REAL
K104((((x * (g,A)) `2) - ((x * ((g + A),A)) `2)),(((x * (g,A)) `2) - ((x * ((g + A),A)) `2))) is V28() real ext-real set
((((x * (g,A)) `1) - ((x * ((g + A),A)) `1)) ^2) + ((((x * (g,A)) `2) - ((x * ((g + A),A)) `2)) ^2) is V28() real ext-real Element of REAL
sqrt (((((x * (g,A)) `1) - ((x * ((g + A),A)) `1)) ^2) + ((((x * (g,A)) `2) - ((x * ((g + A),A)) `2)) ^2)) is V28() real ext-real Element of REAL
abs (((x * (g,A)) `1) - ((x * ((g + A),A)) `1)) is V28() real ext-real Element of REAL
- (((x * (g,A)) `1) - ((x * ((g + A),A)) `1)) is V28() real ext-real Element of REAL
abs (- (((x * (g,A)) `1) - ((x * ((g + A),A)) `1))) is V28() real ext-real Element of REAL
g is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
A is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
[g,A] is non empty set
{g,A} is non empty V174() V175() V176() V177() V178() V179() set
{g} is non empty V12() V174() V175() V176() V177() V178() V179() set
{{g,A},{g}} is non empty set
A is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
A + A is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
[g,(A + A)] is non empty set
{g,(A + A)} is non empty V174() V175() V176() V177() V178() V179() set
{{g,(A + A)},{g}} is non empty set
x is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like V38() 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 x is set
x * (g,A) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
x * (g,(A + A)) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
dist ((x * (g,A)),(x * (g,(A + A)))) is V28() real ext-real Element of REAL
(x * (g,(A + A))) `2 is V28() real ext-real Element of REAL
K526((x * (g,(A + A))),2) is V28() real ext-real Element of REAL
(x * (g,A)) `2 is V28() real ext-real Element of REAL
K526((x * (g,A)),2) is V28() real ext-real Element of REAL
((x * (g,(A + A))) `2) - ((x * (g,A)) `2) is V28() real ext-real Element of REAL
width x is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
len x is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
((x * (g,A)) `2) - ((x * (g,A)) `2) is V28() real ext-real Element of REAL
(x * (g,A)) `1 is V28() real ext-real Element of REAL
K526((x * (g,A)),1) is V28() real ext-real Element of REAL
x * (g,1) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
(x * (g,1)) `1 is V28() real ext-real Element of REAL
K526((x * (g,1)),1) is V28() real ext-real Element of REAL
(x * (g,(A + A))) `1 is V28() real ext-real Element of REAL
K526((x * (g,(A + A))),1) is V28() real ext-real Element of REAL
((x * (g,A)) `1) - ((x * (g,(A + A))) `1) is V28() real ext-real Element of REAL
(((x * (g,A)) `1) - ((x * (g,(A + A))) `1)) ^2 is V28() real ext-real Element of REAL
K104((((x * (g,A)) `1) - ((x * (g,(A + A))) `1)),(((x * (g,A)) `1) - ((x * (g,(A + A))) `1))) is V28() real ext-real set
((x * (g,A)) `2) - ((x * (g,(A + A))) `2) is V28() real ext-real Element of REAL
(((x * (g,A)) `2) - ((x * (g,(A + A))) `2)) ^2 is V28() real ext-real Element of REAL
K104((((x * (g,A)) `2) - ((x * (g,(A + A))) `2)),(((x * (g,A)) `2) - ((x * (g,(A + A))) `2))) is V28() real ext-real set
((((x * (g,A)) `1) - ((x * (g,(A + A))) `1)) ^2) + ((((x * (g,A)) `2) - ((x * (g,(A + A))) `2)) ^2) is V28() real ext-real Element of REAL
sqrt (((((x * (g,A)) `1) - ((x * (g,(A + A))) `1)) ^2) + ((((x * (g,A)) `2) - ((x * (g,(A + A))) `2)) ^2)) is V28() real ext-real Element of REAL
abs (((x * (g,A)) `2) - ((x * (g,(A + A))) `2)) is V28() real ext-real Element of REAL
- (((x * (g,A)) `2) - ((x * (g,(A + A))) `2)) is V28() real ext-real Element of REAL
abs (- (((x * (g,A)) `2) - ((x * (g,(A + A))) `2))) is V28() real ext-real Element of REAL
g is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
A is non empty compact bounded non horizontal non vertical Element of K19( the carrier of (TOP-REAL 2))
Gauge (A,g) is Relation-like NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like V38() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of (TOP-REAL 2) *
len (Gauge (A,g)) is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
(len (Gauge (A,g))) -' 1 is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
4 - 1 is V28() real ext-real integer Element of REAL
(len (Gauge (A,g))) - 1 is V28() real ext-real integer Element of REAL
g is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
A is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
A -' g is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
2 |^ (A -' g) is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
A is non empty compact bounded non horizontal non vertical Element of K19( the carrier of (TOP-REAL 2))
Gauge (A,g) is Relation-like NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like V38() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of (TOP-REAL 2) *
len (Gauge (A,g)) is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
(len (Gauge (A,g))) - 1 is V28() real ext-real integer Element of REAL
Gauge (A,A) is Relation-like NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like V38() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of (TOP-REAL 2) *
len (Gauge (A,A)) is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
(len (Gauge (A,A))) - 1 is V28() real ext-real integer Element of REAL
Indices (Gauge (A,A)) is set
2 |^ g is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
(2 |^ (A -' g)) * (2 |^ g) is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
2 |^ A is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
(2 |^ A) / (2 |^ g) is V28() real ext-real non negative Element of REAL
((2 |^ A) / (2 |^ g)) * (2 |^ g) is V28() real ext-real non negative Element of REAL
x is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
x is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
(Gauge (A,g)) * (x,x) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
x -' 2 is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
(2 |^ (A -' g)) * (x -' 2) is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
2 + ((2 |^ (A -' g)) * (x -' 2)) is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
x -' 2 is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
(2 |^ (A -' g)) * (x -' 2) is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
2 + ((2 |^ (A -' g)) * (x -' 2)) is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
x - 2 is V28() real ext-real integer Element of REAL
N-bound A is V28() real ext-real Element of REAL
E-bound A is V28() real ext-real Element of REAL
S-bound A is V28() real ext-real Element of REAL
W-bound A is V28() real ext-real Element of REAL
(N-bound A) - (S-bound A) is V28() real ext-real Element of REAL
((N-bound A) - (S-bound A)) / (2 |^ A) is V28() real ext-real Element of REAL
(2 + ((2 |^ (A -' g)) * (x -' 2))) - 2 is V28() real ext-real integer Element of REAL
(((N-bound A) - (S-bound A)) / (2 |^ A)) * ((2 + ((2 |^ (A -' g)) * (x -' 2))) - 2) is V28() real ext-real Element of REAL
((2 |^ A) / (2 |^ g)) * (x -' 2) is V28() real ext-real non negative Element of REAL
(((N-bound A) - (S-bound A)) / (2 |^ A)) * (((2 |^ A) / (2 |^ g)) * (x -' 2)) is V28() real ext-real Element of REAL
(((N-bound A) - (S-bound A)) / (2 |^ A)) * ((2 |^ A) / (2 |^ g)) is V28() real ext-real Element of REAL
((((N-bound A) - (S-bound A)) / (2 |^ A)) * ((2 |^ A) / (2 |^ g))) * (x -' 2) is V28() real ext-real Element of REAL
(2 |^ A) / ((2 |^ A) / (2 |^ g)) is V28() real ext-real non negative Element of REAL
((N-bound A) - (S-bound A)) / ((2 |^ A) / ((2 |^ A) / (2 |^ g))) is V28() real ext-real Element of REAL
(((N-bound A) - (S-bound A)) / ((2 |^ A) / ((2 |^ A) / (2 |^ g)))) * (x -' 2) is V28() real ext-real Element of REAL
((N-bound A) - (S-bound A)) / (2 |^ g) is V28() real ext-real Element of REAL
(((N-bound A) - (S-bound A)) / (2 |^ g)) * (x -' 2) is V28() real ext-real Element of REAL
(((N-bound A) - (S-bound A)) / (2 |^ g)) * (x - 2) is V28() real ext-real Element of REAL
[(2 + ((2 |^ (A -' g)) * (x -' 2))),(2 + ((2 |^ (A -' g)) * (x -' 2)))] is non empty set
{(2 + ((2 |^ (A -' g)) * (x -' 2))),(2 + ((2 |^ (A -' g)) * (x -' 2)))} is non empty V174() V175() V176() V177() V178() V179() set
{(2 + ((2 |^ (A -' g)) * (x -' 2)))} is non empty V12() V174() V175() V176() V177() V178() V179() set
{{(2 + ((2 |^ (A -' g)) * (x -' 2))),(2 + ((2 |^ (A -' g)) * (x -' 2)))},{(2 + ((2 |^ (A -' g)) * (x -' 2)))}} is non empty set
(Gauge (A,A)) * ((2 + ((2 |^ (A -' g)) * (x -' 2))),(2 + ((2 |^ (A -' g)) * (x -' 2)))) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
2 + 0 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
(2 |^ g) + 2 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
((2 |^ g) + 2) - 2 is V28() real ext-real integer Element of REAL
((2 |^ g) + 2) -' 2 is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
(2 |^ g) + 0 is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
x - 2 is V28() real ext-real integer Element of REAL
(E-bound A) - (W-bound A) is V28() real ext-real Element of REAL
((E-bound A) - (W-bound A)) / (2 |^ A) is V28() real ext-real Element of REAL
(2 + ((2 |^ (A -' g)) * (x -' 2))) - 2 is V28() real ext-real integer Element of REAL
(((E-bound A) - (W-bound A)) / (2 |^ A)) * ((2 + ((2 |^ (A -' g)) * (x -' 2))) - 2) is V28() real ext-real Element of REAL
((2 |^ A) / (2 |^ g)) * (x -' 2) is V28() real ext-real non negative Element of REAL
(((E-bound A) - (W-bound A)) / (2 |^ A)) * (((2 |^ A) / (2 |^ g)) * (x -' 2)) is V28() real ext-real Element of REAL
(((E-bound A) - (W-bound A)) / (2 |^ A)) * ((2 |^ A) / (2 |^ g)) is V28() real ext-real Element of REAL
((((E-bound A) - (W-bound A)) / (2 |^ A)) * ((2 |^ A) / (2 |^ g))) * (x -' 2) is V28() real ext-real Element of REAL
((E-bound A) - (W-bound A)) / ((2 |^ A) / ((2 |^ A) / (2 |^ g))) is V28() real ext-real Element of REAL
(((E-bound A) - (W-bound A)) / ((2 |^ A) / ((2 |^ A) / (2 |^ g)))) * (x -' 2) is V28() real ext-real Element of REAL
((E-bound A) - (W-bound A)) / (2 |^ g) is V28() real ext-real Element of REAL
(((E-bound A) - (W-bound A)) / (2 |^ g)) * (x -' 2) is V28() real ext-real Element of REAL
(((E-bound A) - (W-bound A)) / (2 |^ g)) * (x - 2) is V28() real ext-real Element of REAL
(len (Gauge (A,A))) - 0 is V28() real ext-real non negative integer Element of REAL
(2 |^ g) + 3 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
((2 |^ g) + 3) - 1 is V28() real ext-real integer Element of REAL
(len (Gauge (A,g))) - 0 is V28() real ext-real non negative integer Element of REAL
(2 |^ A) + 3 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
((2 |^ A) + 3) - 1 is V28() real ext-real integer Element of REAL
(2 |^ A) + 2 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
width (Gauge (A,A)) is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
(W-bound A) + ((((E-bound A) - (W-bound A)) / (2 |^ A)) * ((2 + ((2 |^ (A -' g)) * (x -' 2))) - 2)) is V28() real ext-real Element of REAL
(S-bound A) + ((((N-bound A) - (S-bound A)) / (2 |^ A)) * ((2 + ((2 |^ (A -' g)) * (x -' 2))) - 2)) is V28() real ext-real Element of REAL
|[((W-bound A) + ((((E-bound A) - (W-bound A)) / (2 |^ A)) * ((2 + ((2 |^ (A -' g)) * (x -' 2))) - 2))),((S-bound A) + ((((N-bound A) - (S-bound A)) / (2 |^ A)) * ((2 + ((2 |^ (A -' g)) * (x -' 2))) - 2)))]| is Relation-like NAT -defined Function-like non empty V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
width (Gauge (A,g)) is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
[x,x] is non empty set
{x,x} is non empty V174() V175() V176() V177() V178() V179() set
{x} is non empty V12() V174() V175() V176() V177() V178() V179() set
{{x,x},{x}} is non empty set
Indices (Gauge (A,g)) is set
(W-bound A) + ((((E-bound A) - (W-bound A)) / (2 |^ g)) * (x - 2)) is V28() real ext-real Element of REAL
(S-bound A) + ((((N-bound A) - (S-bound A)) / (2 |^ g)) * (x - 2)) is V28() real ext-real Element of REAL
|[((W-bound A) + ((((E-bound A) - (W-bound A)) / (2 |^ g)) * (x - 2))),((S-bound A) + ((((N-bound A) - (S-bound A)) / (2 |^ g)) * (x - 2)))]| is Relation-like NAT -defined Function-like non empty V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
((Gauge (A,g)) * (x,x)) `2 is V28() real ext-real Element of REAL
K526(((Gauge (A,g)) * (x,x)),2) is V28() real ext-real Element of REAL
((Gauge (A,A)) * ((2 + ((2 |^ (A -' g)) * (x -' 2))),(2 + ((2 |^ (A -' g)) * (x -' 2))))) `2 is V28() real ext-real Element of REAL
K526(((Gauge (A,A)) * ((2 + ((2 |^ (A -' g)) * (x -' 2))),(2 + ((2 |^ (A -' g)) * (x -' 2))))),2) is V28() real ext-real Element of REAL
((Gauge (A,g)) * (x,x)) `1 is V28() real ext-real Element of REAL
K526(((Gauge (A,g)) * (x,x)),1) is V28() real ext-real Element of REAL
((Gauge (A,A)) * ((2 + ((2 |^ (A -' g)) * (x -' 2))),(2 + ((2 |^ (A -' g)) * (x -' 2))))) `1 is V28() real ext-real Element of REAL
K526(((Gauge (A,A)) * ((2 + ((2 |^ (A -' g)) * (x -' 2))),(2 + ((2 |^ (A -' g)) * (x -' 2))))),1) is V28() real ext-real Element of REAL
g is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
A is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
[g,A] is non empty set
{g,A} is non empty V174() V175() V176() V177() V178() V179() set
{g} is non empty V12() V174() V175() V176() V177() V178() V179() set
{{g,A},{g}} is non empty set
A + 1 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
[g,(A + 1)] is non empty set
{g,(A + 1)} is non empty V174() V175() V176() V177() V178() V179() set
{{g,(A + 1)},{g}} is non empty set
A is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
2 |^ A is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
x is non empty compact bounded non horizontal non vertical Element of K19( the carrier of (TOP-REAL 2))
Gauge (x,A) is Relation-like NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like V38() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of (TOP-REAL 2) *
Indices (Gauge (x,A)) is set
(Gauge (x,A)) * (g,A) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
(Gauge (x,A)) * (g,(A + 1)) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
dist (((Gauge (x,A)) * (g,A)),((Gauge (x,A)) * (g,(A + 1)))) is V28() real ext-real Element of REAL
N-bound x is V28() real ext-real Element of REAL
S-bound x is V28() real ext-real Element of REAL
(N-bound x) - (S-bound x) is V28() real ext-real Element of REAL
((N-bound x) - (S-bound x)) / (2 |^ A) is V28() real ext-real Element of REAL
E-bound x is V28() real ext-real Element of REAL
W-bound x is V28() real ext-real Element of REAL
(E-bound x) - (W-bound x) is V28() real ext-real Element of REAL
((E-bound x) - (W-bound x)) / (2 |^ A) is V28() real ext-real Element of REAL
g - 2 is V28() real ext-real integer Element of REAL
(((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2) is V28() real ext-real Element of REAL
(W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2)) is V28() real ext-real Element of REAL
(A + 1) - 2 is V28() real ext-real integer Element of REAL
(((N-bound x) - (S-bound x)) / (2 |^ A)) * ((A + 1) - 2) is V28() real ext-real Element of REAL
(S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * ((A + 1) - 2)) is V28() real ext-real Element of REAL
|[((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2))),((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * ((A + 1) - 2)))]| is Relation-like NAT -defined Function-like non empty V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
(S-bound x) - (S-bound x) is V28() real ext-real Element of REAL
p is Element of the carrier of (Euclid 2)
q is Element of the carrier of (Euclid 2)
dist (p,q) is V28() real ext-real Element of REAL
A - 2 is V28() real ext-real integer Element of REAL
(((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2) is V28() real ext-real Element of REAL
(S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2)) is V28() real ext-real Element of REAL
|[((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2))),((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2)))]| is Relation-like NAT -defined Function-like non empty V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
(Pitag_dist 2) . (p,q) is set
((Gauge (x,A)) * (g,A)) `1 is V28() real ext-real Element of REAL
K526(((Gauge (x,A)) * (g,A)),1) is V28() real ext-real Element of REAL
((Gauge (x,A)) * (g,(A + 1))) `1 is V28() real ext-real Element of REAL
K526(((Gauge (x,A)) * (g,(A + 1))),1) is V28() real ext-real Element of REAL
(((Gauge (x,A)) * (g,A)) `1) - (((Gauge (x,A)) * (g,(A + 1))) `1) is V28() real ext-real Element of REAL
((((Gauge (x,A)) * (g,A)) `1) - (((Gauge (x,A)) * (g,(A + 1))) `1)) ^2 is V28() real ext-real Element of REAL
K104(((((Gauge (x,A)) * (g,A)) `1) - (((Gauge (x,A)) * (g,(A + 1))) `1)),((((Gauge (x,A)) * (g,A)) `1) - (((Gauge (x,A)) * (g,(A + 1))) `1))) is V28() real ext-real set
((Gauge (x,A)) * (g,A)) `2 is V28() real ext-real Element of REAL
K526(((Gauge (x,A)) * (g,A)),2) is V28() real ext-real Element of REAL
((Gauge (x,A)) * (g,(A + 1))) `2 is V28() real ext-real Element of REAL
K526(((Gauge (x,A)) * (g,(A + 1))),2) is V28() real ext-real Element of REAL
(((Gauge (x,A)) * (g,A)) `2) - (((Gauge (x,A)) * (g,(A + 1))) `2) is V28() real ext-real Element of REAL
((((Gauge (x,A)) * (g,A)) `2) - (((Gauge (x,A)) * (g,(A + 1))) `2)) ^2 is V28() real ext-real Element of REAL
K104(((((Gauge (x,A)) * (g,A)) `2) - (((Gauge (x,A)) * (g,(A + 1))) `2)),((((Gauge (x,A)) * (g,A)) `2) - (((Gauge (x,A)) * (g,(A + 1))) `2))) is V28() real ext-real set
(((((Gauge (x,A)) * (g,A)) `1) - (((Gauge (x,A)) * (g,(A + 1))) `1)) ^2) + (((((Gauge (x,A)) * (g,A)) `2) - (((Gauge (x,A)) * (g,(A + 1))) `2)) ^2) is V28() real ext-real Element of REAL
sqrt ((((((Gauge (x,A)) * (g,A)) `1) - (((Gauge (x,A)) * (g,(A + 1))) `1)) ^2) + (((((Gauge (x,A)) * (g,A)) `2) - (((Gauge (x,A)) * (g,(A + 1))) `2)) ^2)) is V28() real ext-real Element of REAL
((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2))) - (((Gauge (x,A)) * (g,(A + 1))) `1) is V28() real ext-real Element of REAL
(((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2))) - (((Gauge (x,A)) * (g,(A + 1))) `1)) ^2 is V28() real ext-real Element of REAL
K104((((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2))) - (((Gauge (x,A)) * (g,(A + 1))) `1)),(((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2))) - (((Gauge (x,A)) * (g,(A + 1))) `1))) is V28() real ext-real set
((((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2))) - (((Gauge (x,A)) * (g,(A + 1))) `1)) ^2) + (((((Gauge (x,A)) * (g,A)) `2) - (((Gauge (x,A)) * (g,(A + 1))) `2)) ^2) is V28() real ext-real Element of REAL
sqrt (((((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2))) - (((Gauge (x,A)) * (g,(A + 1))) `1)) ^2) + (((((Gauge (x,A)) * (g,A)) `2) - (((Gauge (x,A)) * (g,(A + 1))) `2)) ^2)) is V28() real ext-real Element of REAL
((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2))) - ((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2))) is V28() real ext-real Element of REAL
(((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2))) - ((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2)))) ^2 is V28() real ext-real Element of REAL
K104((((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2))) - ((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2)))),(((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2))) - ((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2))))) is V28() real ext-real set
((((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2))) - ((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2)))) ^2) + (((((Gauge (x,A)) * (g,A)) `2) - (((Gauge (x,A)) * (g,(A + 1))) `2)) ^2) is V28() real ext-real Element of REAL
sqrt (((((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2))) - ((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2)))) ^2) + (((((Gauge (x,A)) * (g,A)) `2) - (((Gauge (x,A)) * (g,(A + 1))) `2)) ^2)) is V28() real ext-real Element of REAL
abs ((((Gauge (x,A)) * (g,A)) `2) - (((Gauge (x,A)) * (g,(A + 1))) `2)) is V28() real ext-real Element of REAL
((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2))) - (((Gauge (x,A)) * (g,(A + 1))) `2) is V28() real ext-real Element of REAL
abs (((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2))) - (((Gauge (x,A)) * (g,(A + 1))) `2)) is V28() real ext-real Element of REAL
((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2))) - ((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * ((A + 1) - 2))) is V28() real ext-real Element of REAL
abs (((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2))) - ((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * ((A + 1) - 2)))) is V28() real ext-real Element of REAL
- (((N-bound x) - (S-bound x)) / (2 |^ A)) is V28() real ext-real Element of REAL
abs (- (((N-bound x) - (S-bound x)) / (2 |^ A))) is V28() real ext-real Element of REAL
abs (((N-bound x) - (S-bound x)) / (2 |^ A)) is V28() real ext-real Element of REAL
abs ((N-bound x) - (S-bound x)) is V28() real ext-real Element of REAL
abs (2 |^ A) is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
(abs ((N-bound x) - (S-bound x))) / (abs (2 |^ A)) is V28() real ext-real Element of REAL
((N-bound x) - (S-bound x)) / (abs (2 |^ A)) is V28() real ext-real Element of REAL
g is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
g + 1 is non empty ordinal natural V28() real ext-real positive non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
A is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
[g,A] is non empty set
{g,A} is non empty V174() V175() V176() V177() V178() V179() set
{g} is non empty V12() V174() V175() V176() V177() V178() V179() set
{{g,A},{g}} is non empty set
[(g + 1),A] is non empty set
{(g + 1),A} is non empty V174() V175() V176() V177() V178() V179() set
{(g + 1)} is non empty V12() V174() V175() V176() V177() V178() V179() set
{{(g + 1),A},{(g + 1)}} is non empty set
A is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
2 |^ A is ordinal natural V28() real ext-real non negative integer V108() V174() V175() V176() V177() V178() V179() Element of NAT
x is non empty compact bounded non horizontal non vertical Element of K19( the carrier of (TOP-REAL 2))
Gauge (x,A) is Relation-like NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like V38() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of (TOP-REAL 2) *
Indices (Gauge (x,A)) is set
(Gauge (x,A)) * (g,A) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
(Gauge (x,A)) * ((g + 1),A) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
dist (((Gauge (x,A)) * (g,A)),((Gauge (x,A)) * ((g + 1),A))) is V28() real ext-real Element of REAL
E-bound x is V28() real ext-real Element of REAL
W-bound x is V28() real ext-real Element of REAL
(E-bound x) - (W-bound x) is V28() real ext-real Element of REAL
((E-bound x) - (W-bound x)) / (2 |^ A) is V28() real ext-real Element of REAL
N-bound x is V28() real ext-real Element of REAL
S-bound x is V28() real ext-real Element of REAL
(g + 1) - 2 is V28() real ext-real integer Element of REAL
(((E-bound x) - (W-bound x)) / (2 |^ A)) * ((g + 1) - 2) is V28() real ext-real Element of REAL
(W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * ((g + 1) - 2)) is V28() real ext-real Element of REAL
(N-bound x) - (S-bound x) is V28() real ext-real Element of REAL
((N-bound x) - (S-bound x)) / (2 |^ A) is V28() real ext-real Element of REAL
A - 2 is V28() real ext-real integer Element of REAL
(((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2) is V28() real ext-real Element of REAL
(S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2)) is V28() real ext-real Element of REAL
|[((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * ((g + 1) - 2))),((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2)))]| is Relation-like NAT -defined Function-like non empty V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
(W-bound x) - (W-bound x) is V28() real ext-real Element of REAL
p is Element of the carrier of (Euclid 2)
q is Element of the carrier of (Euclid 2)
dist (p,q) is V28() real ext-real Element of REAL
g - 2 is V28() real ext-real integer Element of REAL
(((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2) is V28() real ext-real Element of REAL
(W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2)) is V28() real ext-real Element of REAL
|[((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A)) * (g - 2))),((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2)))]| is Relation-like NAT -defined Function-like non empty V38() V45(2) FinSequence-like FinSubsequence-like V166() Element of the carrier of (TOP-REAL 2)
(Pitag_dist 2) . (p,q) is set
((Gauge (x,A)) * (g,A)) `1 is V28() real ext-real Element of REAL
K526(((Gauge (x,A)) * (g,A)),1) is V28() real ext-real Element of REAL
((Gauge (x,A)) * ((g + 1),A)) `1 is V28() real ext-real Element of REAL
K526(((Gauge (x,A)) * ((g + 1),A)),1) is V28() real ext-real Element of REAL
(((Gauge (x,A)) * (g,A)) `1) - (((Gauge (x,A)) * ((g + 1),A)) `1) is V28() real ext-real Element of REAL
((((Gauge (x,A)) * (g,A)) `1) - (((Gauge (x,A)) * ((g + 1),A)) `1)) ^2 is V28() real ext-real Element of REAL
K104(((((Gauge (x,A)) * (g,A)) `1) - (((Gauge (x,A)) * ((g + 1),A)) `1)),((((Gauge (x,A)) * (g,A)) `1) - (((Gauge (x,A)) * ((g + 1),A)) `1))) is V28() real ext-real set
((Gauge (x,A)) * (g,A)) `2 is V28() real ext-real Element of REAL
K526(((Gauge (x,A)) * (g,A)),2) is V28() real ext-real Element of REAL
((Gauge (x,A)) * ((g + 1),A)) `2 is V28() real ext-real Element of REAL
K526(((Gauge (x,A)) * ((g + 1),A)),2) is V28() real ext-real Element of REAL
(((Gauge (x,A)) * (g,A)) `2) - (((Gauge (x,A)) * ((g + 1),A)) `2) is V28() real ext-real Element of REAL
((((Gauge (x,A)) * (g,A)) `2) - (((Gauge (x,A)) * ((g + 1),A)) `2)) ^2 is V28() real ext-real Element of REAL
K104(((((Gauge (x,A)) * (g,A)) `2) - (((Gauge (x,A)) * ((g + 1),A)) `2)),((((Gauge (x,A)) * (g,A)) `2) - (((Gauge (x,A)) * ((g + 1),A)) `2))) is V28() real ext-real set
(((((Gauge (x,A)) * (g,A)) `1) - (((Gauge (x,A)) * ((g + 1),A)) `1)) ^2) + (((((Gauge (x,A)) * (g,A)) `2) - (((Gauge (x,A)) * ((g + 1),A)) `2)) ^2) is V28() real ext-real Element of REAL
sqrt ((((((Gauge (x,A)) * (g,A)) `1) - (((Gauge (x,A)) * ((g + 1),A)) `1)) ^2) + (((((Gauge (x,A)) * (g,A)) `2) - (((Gauge (x,A)) * ((g + 1),A)) `2)) ^2)) is V28() real ext-real Element of REAL
((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2))) - (((Gauge (x,A)) * ((g + 1),A)) `2) is V28() real ext-real Element of REAL
(((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2))) - (((Gauge (x,A)) * ((g + 1),A)) `2)) ^2 is V28() real ext-real Element of REAL
K104((((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2))) - (((Gauge (x,A)) * ((g + 1),A)) `2)),(((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2))) - (((Gauge (x,A)) * ((g + 1),A)) `2))) is V28() real ext-real set
(((((Gauge (x,A)) * (g,A)) `1) - (((Gauge (x,A)) * ((g + 1),A)) `1)) ^2) + ((((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2))) - (((Gauge (x,A)) * ((g + 1),A)) `2)) ^2) is V28() real ext-real Element of REAL
sqrt ((((((Gauge (x,A)) * (g,A)) `1) - (((Gauge (x,A)) * ((g + 1),A)) `1)) ^2) + ((((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2))) - (((Gauge (x,A)) * ((g + 1),A)) `2)) ^2)) is V28() real ext-real Element of REAL
((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2))) - ((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2))) is V28() real ext-real Element of REAL
(((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2))) - ((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2)))) ^2 is V28() real ext-real Element of REAL
K104((((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2))) - ((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2)))),(((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2))) - ((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2))))) is V28() real ext-real set
(((((Gauge (x,A)) * (g,A)) `1) - (((Gauge (x,A)) * ((g + 1),A)) `1)) ^2) + ((((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2))) - ((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2)))) ^2) is V28() real ext-real Element of REAL
sqrt ((((((Gauge (x,A)) * (g,A)) `1) - (((Gauge (x,A)) * ((g + 1),A)) `1)) ^2) + ((((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2))) - ((S-bound x) + ((((N-bound x) - (S-bound x)) / (2 |^ A)) * (A - 2)))) ^2)) is V28() real ext-real Element of REAL
abs ((((Gauge (x,A)) * (g,A)) `1) - (((Gauge (x,A)) * ((g + 1),A)) `1)) is V28() real ext-real Element of REAL
((W-bound x) + ((((E-bound x) - (W-bound x)) / (2 |^ A))