theorem Th4: :: JORDAN1D:4

for a, b, i, n being Nat
for D being non empty Subset of (TOP-REAL 2) st 2 <= n & n < len (Gauge (D,i)) & 1 <= a & a <= len (Gauge (D,i)) & 1 <= b & b <= len (Gauge (D,(i + 1))) holds
((Gauge (D,i)) * (a,n)) `2 = ((Gauge (D,(i + 1))) * (b,((2 * n) -' 2))) `2