theorem Th3: :: JORDAN1D:3

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