let i, j be Nat; :: thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st i <= j holds

for a, b being Nat st 2 <= a & a <= (len (Gauge (C,i))) - 1 & 2 <= b & b <= (len (Gauge (C,i))) - 1 holds

ex c, d being Nat st

( 2 <= c & c <= (len (Gauge (C,j))) - 1 & 2 <= d & d <= (len (Gauge (C,j))) - 1 & [c,d] in Indices (Gauge (C,j)) & (Gauge (C,i)) * (a,b) = (Gauge (C,j)) * (c,d) & c = 2 + ((2 |^ (j -' i)) * (a -' 2)) & d = 2 + ((2 |^ (j -' i)) * (b -' 2)) )

let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ( i <= j implies for a, b being Nat st 2 <= a & a <= (len (Gauge (C,i))) - 1 & 2 <= b & b <= (len (Gauge (C,i))) - 1 holds

ex c, d being Nat st

( 2 <= c & c <= (len (Gauge (C,j))) - 1 & 2 <= d & d <= (len (Gauge (C,j))) - 1 & [c,d] in Indices (Gauge (C,j)) & (Gauge (C,i)) * (a,b) = (Gauge (C,j)) * (c,d) & c = 2 + ((2 |^ (j -' i)) * (a -' 2)) & d = 2 + ((2 |^ (j -' i)) * (b -' 2)) ) )

A1: 0 <> 2 |^ i by NEWTON:83;

assume A2: i <= j ; :: thesis: for a, b being Nat st 2 <= a & a <= (len (Gauge (C,i))) - 1 & 2 <= b & b <= (len (Gauge (C,i))) - 1 holds

ex c, d being Nat st

( 2 <= c & c <= (len (Gauge (C,j))) - 1 & 2 <= d & d <= (len (Gauge (C,j))) - 1 & [c,d] in Indices (Gauge (C,j)) & (Gauge (C,i)) * (a,b) = (Gauge (C,j)) * (c,d) & c = 2 + ((2 |^ (j -' i)) * (a -' 2)) & d = 2 + ((2 |^ (j -' i)) * (b -' 2)) )

then A3: (2 |^ (j -' i)) * (2 |^ i) = ((2 |^ j) / (2 |^ i)) * (2 |^ i) by TOPREAL6:10

.= 2 |^ j by A1, XCMPLX_1:87 ;

let a, b be Nat; :: thesis: ( 2 <= a & a <= (len (Gauge (C,i))) - 1 & 2 <= b & b <= (len (Gauge (C,i))) - 1 implies ex c, d being Nat st

( 2 <= c & c <= (len (Gauge (C,j))) - 1 & 2 <= d & d <= (len (Gauge (C,j))) - 1 & [c,d] in Indices (Gauge (C,j)) & (Gauge (C,i)) * (a,b) = (Gauge (C,j)) * (c,d) & c = 2 + ((2 |^ (j -' i)) * (a -' 2)) & d = 2 + ((2 |^ (j -' i)) * (b -' 2)) ) )

assume that

A4: 2 <= a and

A5: a <= (len (Gauge (C,i))) - 1 and

A6: 2 <= b and

A7: b <= (len (Gauge (C,i))) - 1 ; :: thesis: ex c, d being Nat st

( 2 <= c & c <= (len (Gauge (C,j))) - 1 & 2 <= d & d <= (len (Gauge (C,j))) - 1 & [c,d] in Indices (Gauge (C,j)) & (Gauge (C,i)) * (a,b) = (Gauge (C,j)) * (c,d) & c = 2 + ((2 |^ (j -' i)) * (a -' 2)) & d = 2 + ((2 |^ (j -' i)) * (b -' 2)) )

A8: ( 1 <= a & 1 <= b ) by A4, A6, XXREAL_0:2;

set c = 2 + ((2 |^ (j -' i)) * (a -' 2));

set d = 2 + ((2 |^ (j -' i)) * (b -' 2));

A9: 0 <= b - 2 by A6, XREAL_1:48;

set n = N-bound C;

set e = E-bound C;

set s = S-bound C;

set w = W-bound C;

A10: 0 <> 2 |^ j by NEWTON:83;

A11: (((N-bound C) - (S-bound C)) / (2 |^ j)) * ((2 + ((2 |^ (j -' i)) * (b -' 2))) - 2) = (((N-bound C) - (S-bound C)) / (2 |^ j)) * (((2 |^ j) / (2 |^ i)) * (b -' 2)) by A2, TOPREAL6:10

.= ((((N-bound C) - (S-bound C)) / (2 |^ j)) * ((2 |^ j) / (2 |^ i))) * (b -' 2)

.= (((N-bound C) - (S-bound C)) / ((2 |^ j) / ((2 |^ j) / (2 |^ i)))) * (b -' 2) by XCMPLX_1:81

.= (((N-bound C) - (S-bound C)) / (2 |^ i)) * (b -' 2) by A10, XCMPLX_1:52

.= (((N-bound C) - (S-bound C)) / (2 |^ i)) * (b - 2) by A9, XREAL_0:def 2 ;

take 2 + ((2 |^ (j -' i)) * (a -' 2)) ; :: thesis: ex d being Nat st

( 2 <= 2 + ((2 |^ (j -' i)) * (a -' 2)) & 2 + ((2 |^ (j -' i)) * (a -' 2)) <= (len (Gauge (C,j))) - 1 & 2 <= d & d <= (len (Gauge (C,j))) - 1 & [(2 + ((2 |^ (j -' i)) * (a -' 2))),d] in Indices (Gauge (C,j)) & (Gauge (C,i)) * (a,b) = (Gauge (C,j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))),d) & 2 + ((2 |^ (j -' i)) * (a -' 2)) = 2 + ((2 |^ (j -' i)) * (a -' 2)) & d = 2 + ((2 |^ (j -' i)) * (b -' 2)) )

take 2 + ((2 |^ (j -' i)) * (b -' 2)) ; :: thesis: ( 2 <= 2 + ((2 |^ (j -' i)) * (a -' 2)) & 2 + ((2 |^ (j -' i)) * (a -' 2)) <= (len (Gauge (C,j))) - 1 & 2 <= 2 + ((2 |^ (j -' i)) * (b -' 2)) & 2 + ((2 |^ (j -' i)) * (b -' 2)) <= (len (Gauge (C,j))) - 1 & [(2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2)))] in Indices (Gauge (C,j)) & (Gauge (C,i)) * (a,b) = (Gauge (C,j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2)))) & 2 + ((2 |^ (j -' i)) * (a -' 2)) = 2 + ((2 |^ (j -' i)) * (a -' 2)) & 2 + ((2 |^ (j -' i)) * (b -' 2)) = 2 + ((2 |^ (j -' i)) * (b -' 2)) )

A12: 2 + 0 <= 2 + ((2 |^ (j -' i)) * (a -' 2)) by XREAL_1:6;

then A13: 1 <= 2 + ((2 |^ (j -' i)) * (a -' 2)) by XXREAL_0:2;

((2 |^ i) + 2) - 2 >= 0 ;

then A14: ((2 |^ i) + 2) -' 2 = (2 |^ i) + 0 by XREAL_0:def 2;

A15: 0 <= a - 2 by A4, XREAL_1:48;

A16: (((E-bound C) - (W-bound C)) / (2 |^ j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))) - 2) = (((E-bound C) - (W-bound C)) / (2 |^ j)) * (((2 |^ j) / (2 |^ i)) * (a -' 2)) by A2, TOPREAL6:10

.= ((((E-bound C) - (W-bound C)) / (2 |^ j)) * ((2 |^ j) / (2 |^ i))) * (a -' 2)

.= (((E-bound C) - (W-bound C)) / ((2 |^ j) / ((2 |^ j) / (2 |^ i)))) * (a -' 2) by XCMPLX_1:81

.= (((E-bound C) - (W-bound C)) / (2 |^ i)) * (a -' 2) by A10, XCMPLX_1:52

.= (((E-bound C) - (W-bound C)) / (2 |^ i)) * (a - 2) by A15, XREAL_0:def 2 ;

A17: (len (Gauge (C,j))) - 1 < (len (Gauge (C,j))) - 0 by XREAL_1:15;

A18: (len (Gauge (C,i))) - 1 = ((2 |^ i) + 3) - 1 by JORDAN8:def 1

.= (2 |^ i) + 2 ;

then a -' 2 <= ((2 |^ i) + 2) -' 2 by A5, NAT_D:42;

then A19: (2 |^ (j -' i)) * (a -' 2) <= 2 |^ j by A14, A3, XREAL_1:64;

b -' 2 <= ((2 |^ i) + 2) -' 2 by A7, A18, NAT_D:42;

then A20: (2 |^ (j -' i)) * (b -' 2) <= 2 |^ j by A14, A3, XREAL_1:64;

A21: (len (Gauge (C,i))) - 1 < (len (Gauge (C,i))) - 0 by XREAL_1:15;

then A22: a <= len (Gauge (C,i)) by A5, XXREAL_0:2;

(len (Gauge (C,j))) - 1 = ((2 |^ j) + 3) - 1 by JORDAN8:def 1

.= (2 |^ j) + 2 ;

hence A23: ( 2 <= 2 + ((2 |^ (j -' i)) * (a -' 2)) & 2 + ((2 |^ (j -' i)) * (a -' 2)) <= (len (Gauge (C,j))) - 1 & 2 <= 2 + ((2 |^ (j -' i)) * (b -' 2)) & 2 + ((2 |^ (j -' i)) * (b -' 2)) <= (len (Gauge (C,j))) - 1 ) by A19, A20, A12, XREAL_1:6; :: thesis: ( [(2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2)))] in Indices (Gauge (C,j)) & (Gauge (C,i)) * (a,b) = (Gauge (C,j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2)))) & 2 + ((2 |^ (j -' i)) * (a -' 2)) = 2 + ((2 |^ (j -' i)) * (a -' 2)) & 2 + ((2 |^ (j -' i)) * (b -' 2)) = 2 + ((2 |^ (j -' i)) * (b -' 2)) )

then A24: 1 <= 2 + ((2 |^ (j -' i)) * (b -' 2)) by XXREAL_0:2;

width (Gauge (C,j)) = len (Gauge (C,j)) by JORDAN8:def 1;

then A25: 2 + ((2 |^ (j -' i)) * (b -' 2)) <= width (Gauge (C,j)) by A23, A17, XXREAL_0:2;

2 + ((2 |^ (j -' i)) * (a -' 2)) <= len (Gauge (C,j)) by A23, A17, XXREAL_0:2;

hence [(2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2)))] in Indices (Gauge (C,j)) by A13, A24, A25, MATRIX_0:30; :: thesis: ( (Gauge (C,i)) * (a,b) = (Gauge (C,j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2)))) & 2 + ((2 |^ (j -' i)) * (a -' 2)) = 2 + ((2 |^ (j -' i)) * (a -' 2)) & 2 + ((2 |^ (j -' i)) * (b -' 2)) = 2 + ((2 |^ (j -' i)) * (b -' 2)) )

then A26: (Gauge (C,j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2)))) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))) - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ j)) * ((2 + ((2 |^ (j -' i)) * (b -' 2))) - 2)))]| by JORDAN8:def 1;

width (Gauge (C,i)) = len (Gauge (C,i)) by JORDAN8:def 1;

then b <= width (Gauge (C,i)) by A7, A21, XXREAL_0:2;

then [a,b] in Indices (Gauge (C,i)) by A22, A8, MATRIX_0:30;

then A27: (Gauge (C,i)) * (a,b) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ i)) * (a - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ i)) * (b - 2)))]| by JORDAN8:def 1;

then A28: ((Gauge (C,i)) * (a,b)) `2 = (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ i)) * (b - 2)) by EUCLID:52

.= ((Gauge (C,j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2))))) `2 by A26, A11, EUCLID:52 ;

((Gauge (C,i)) * (a,b)) `1 = (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ i)) * (a - 2)) by A27, EUCLID:52

.= ((Gauge (C,j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2))))) `1 by A26, A16, EUCLID:52 ;

hence (Gauge (C,i)) * (a,b) = (Gauge (C,j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2)))) by A28, TOPREAL3:6; :: thesis: ( 2 + ((2 |^ (j -' i)) * (a -' 2)) = 2 + ((2 |^ (j -' i)) * (a -' 2)) & 2 + ((2 |^ (j -' i)) * (b -' 2)) = 2 + ((2 |^ (j -' i)) * (b -' 2)) )

thus ( 2 + ((2 |^ (j -' i)) * (a -' 2)) = 2 + ((2 |^ (j -' i)) * (a -' 2)) & 2 + ((2 |^ (j -' i)) * (b -' 2)) = 2 + ((2 |^ (j -' i)) * (b -' 2)) ) ; :: thesis: verum

for a, b being Nat st 2 <= a & a <= (len (Gauge (C,i))) - 1 & 2 <= b & b <= (len (Gauge (C,i))) - 1 holds

ex c, d being Nat st

( 2 <= c & c <= (len (Gauge (C,j))) - 1 & 2 <= d & d <= (len (Gauge (C,j))) - 1 & [c,d] in Indices (Gauge (C,j)) & (Gauge (C,i)) * (a,b) = (Gauge (C,j)) * (c,d) & c = 2 + ((2 |^ (j -' i)) * (a -' 2)) & d = 2 + ((2 |^ (j -' i)) * (b -' 2)) )

let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ( i <= j implies for a, b being Nat st 2 <= a & a <= (len (Gauge (C,i))) - 1 & 2 <= b & b <= (len (Gauge (C,i))) - 1 holds

ex c, d being Nat st

( 2 <= c & c <= (len (Gauge (C,j))) - 1 & 2 <= d & d <= (len (Gauge (C,j))) - 1 & [c,d] in Indices (Gauge (C,j)) & (Gauge (C,i)) * (a,b) = (Gauge (C,j)) * (c,d) & c = 2 + ((2 |^ (j -' i)) * (a -' 2)) & d = 2 + ((2 |^ (j -' i)) * (b -' 2)) ) )

A1: 0 <> 2 |^ i by NEWTON:83;

assume A2: i <= j ; :: thesis: for a, b being Nat st 2 <= a & a <= (len (Gauge (C,i))) - 1 & 2 <= b & b <= (len (Gauge (C,i))) - 1 holds

ex c, d being Nat st

( 2 <= c & c <= (len (Gauge (C,j))) - 1 & 2 <= d & d <= (len (Gauge (C,j))) - 1 & [c,d] in Indices (Gauge (C,j)) & (Gauge (C,i)) * (a,b) = (Gauge (C,j)) * (c,d) & c = 2 + ((2 |^ (j -' i)) * (a -' 2)) & d = 2 + ((2 |^ (j -' i)) * (b -' 2)) )

then A3: (2 |^ (j -' i)) * (2 |^ i) = ((2 |^ j) / (2 |^ i)) * (2 |^ i) by TOPREAL6:10

.= 2 |^ j by A1, XCMPLX_1:87 ;

let a, b be Nat; :: thesis: ( 2 <= a & a <= (len (Gauge (C,i))) - 1 & 2 <= b & b <= (len (Gauge (C,i))) - 1 implies ex c, d being Nat st

( 2 <= c & c <= (len (Gauge (C,j))) - 1 & 2 <= d & d <= (len (Gauge (C,j))) - 1 & [c,d] in Indices (Gauge (C,j)) & (Gauge (C,i)) * (a,b) = (Gauge (C,j)) * (c,d) & c = 2 + ((2 |^ (j -' i)) * (a -' 2)) & d = 2 + ((2 |^ (j -' i)) * (b -' 2)) ) )

assume that

A4: 2 <= a and

A5: a <= (len (Gauge (C,i))) - 1 and

A6: 2 <= b and

A7: b <= (len (Gauge (C,i))) - 1 ; :: thesis: ex c, d being Nat st

( 2 <= c & c <= (len (Gauge (C,j))) - 1 & 2 <= d & d <= (len (Gauge (C,j))) - 1 & [c,d] in Indices (Gauge (C,j)) & (Gauge (C,i)) * (a,b) = (Gauge (C,j)) * (c,d) & c = 2 + ((2 |^ (j -' i)) * (a -' 2)) & d = 2 + ((2 |^ (j -' i)) * (b -' 2)) )

A8: ( 1 <= a & 1 <= b ) by A4, A6, XXREAL_0:2;

set c = 2 + ((2 |^ (j -' i)) * (a -' 2));

set d = 2 + ((2 |^ (j -' i)) * (b -' 2));

A9: 0 <= b - 2 by A6, XREAL_1:48;

set n = N-bound C;

set e = E-bound C;

set s = S-bound C;

set w = W-bound C;

A10: 0 <> 2 |^ j by NEWTON:83;

A11: (((N-bound C) - (S-bound C)) / (2 |^ j)) * ((2 + ((2 |^ (j -' i)) * (b -' 2))) - 2) = (((N-bound C) - (S-bound C)) / (2 |^ j)) * (((2 |^ j) / (2 |^ i)) * (b -' 2)) by A2, TOPREAL6:10

.= ((((N-bound C) - (S-bound C)) / (2 |^ j)) * ((2 |^ j) / (2 |^ i))) * (b -' 2)

.= (((N-bound C) - (S-bound C)) / ((2 |^ j) / ((2 |^ j) / (2 |^ i)))) * (b -' 2) by XCMPLX_1:81

.= (((N-bound C) - (S-bound C)) / (2 |^ i)) * (b -' 2) by A10, XCMPLX_1:52

.= (((N-bound C) - (S-bound C)) / (2 |^ i)) * (b - 2) by A9, XREAL_0:def 2 ;

take 2 + ((2 |^ (j -' i)) * (a -' 2)) ; :: thesis: ex d being Nat st

( 2 <= 2 + ((2 |^ (j -' i)) * (a -' 2)) & 2 + ((2 |^ (j -' i)) * (a -' 2)) <= (len (Gauge (C,j))) - 1 & 2 <= d & d <= (len (Gauge (C,j))) - 1 & [(2 + ((2 |^ (j -' i)) * (a -' 2))),d] in Indices (Gauge (C,j)) & (Gauge (C,i)) * (a,b) = (Gauge (C,j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))),d) & 2 + ((2 |^ (j -' i)) * (a -' 2)) = 2 + ((2 |^ (j -' i)) * (a -' 2)) & d = 2 + ((2 |^ (j -' i)) * (b -' 2)) )

take 2 + ((2 |^ (j -' i)) * (b -' 2)) ; :: thesis: ( 2 <= 2 + ((2 |^ (j -' i)) * (a -' 2)) & 2 + ((2 |^ (j -' i)) * (a -' 2)) <= (len (Gauge (C,j))) - 1 & 2 <= 2 + ((2 |^ (j -' i)) * (b -' 2)) & 2 + ((2 |^ (j -' i)) * (b -' 2)) <= (len (Gauge (C,j))) - 1 & [(2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2)))] in Indices (Gauge (C,j)) & (Gauge (C,i)) * (a,b) = (Gauge (C,j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2)))) & 2 + ((2 |^ (j -' i)) * (a -' 2)) = 2 + ((2 |^ (j -' i)) * (a -' 2)) & 2 + ((2 |^ (j -' i)) * (b -' 2)) = 2 + ((2 |^ (j -' i)) * (b -' 2)) )

A12: 2 + 0 <= 2 + ((2 |^ (j -' i)) * (a -' 2)) by XREAL_1:6;

then A13: 1 <= 2 + ((2 |^ (j -' i)) * (a -' 2)) by XXREAL_0:2;

((2 |^ i) + 2) - 2 >= 0 ;

then A14: ((2 |^ i) + 2) -' 2 = (2 |^ i) + 0 by XREAL_0:def 2;

A15: 0 <= a - 2 by A4, XREAL_1:48;

A16: (((E-bound C) - (W-bound C)) / (2 |^ j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))) - 2) = (((E-bound C) - (W-bound C)) / (2 |^ j)) * (((2 |^ j) / (2 |^ i)) * (a -' 2)) by A2, TOPREAL6:10

.= ((((E-bound C) - (W-bound C)) / (2 |^ j)) * ((2 |^ j) / (2 |^ i))) * (a -' 2)

.= (((E-bound C) - (W-bound C)) / ((2 |^ j) / ((2 |^ j) / (2 |^ i)))) * (a -' 2) by XCMPLX_1:81

.= (((E-bound C) - (W-bound C)) / (2 |^ i)) * (a -' 2) by A10, XCMPLX_1:52

.= (((E-bound C) - (W-bound C)) / (2 |^ i)) * (a - 2) by A15, XREAL_0:def 2 ;

A17: (len (Gauge (C,j))) - 1 < (len (Gauge (C,j))) - 0 by XREAL_1:15;

A18: (len (Gauge (C,i))) - 1 = ((2 |^ i) + 3) - 1 by JORDAN8:def 1

.= (2 |^ i) + 2 ;

then a -' 2 <= ((2 |^ i) + 2) -' 2 by A5, NAT_D:42;

then A19: (2 |^ (j -' i)) * (a -' 2) <= 2 |^ j by A14, A3, XREAL_1:64;

b -' 2 <= ((2 |^ i) + 2) -' 2 by A7, A18, NAT_D:42;

then A20: (2 |^ (j -' i)) * (b -' 2) <= 2 |^ j by A14, A3, XREAL_1:64;

A21: (len (Gauge (C,i))) - 1 < (len (Gauge (C,i))) - 0 by XREAL_1:15;

then A22: a <= len (Gauge (C,i)) by A5, XXREAL_0:2;

(len (Gauge (C,j))) - 1 = ((2 |^ j) + 3) - 1 by JORDAN8:def 1

.= (2 |^ j) + 2 ;

hence A23: ( 2 <= 2 + ((2 |^ (j -' i)) * (a -' 2)) & 2 + ((2 |^ (j -' i)) * (a -' 2)) <= (len (Gauge (C,j))) - 1 & 2 <= 2 + ((2 |^ (j -' i)) * (b -' 2)) & 2 + ((2 |^ (j -' i)) * (b -' 2)) <= (len (Gauge (C,j))) - 1 ) by A19, A20, A12, XREAL_1:6; :: thesis: ( [(2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2)))] in Indices (Gauge (C,j)) & (Gauge (C,i)) * (a,b) = (Gauge (C,j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2)))) & 2 + ((2 |^ (j -' i)) * (a -' 2)) = 2 + ((2 |^ (j -' i)) * (a -' 2)) & 2 + ((2 |^ (j -' i)) * (b -' 2)) = 2 + ((2 |^ (j -' i)) * (b -' 2)) )

then A24: 1 <= 2 + ((2 |^ (j -' i)) * (b -' 2)) by XXREAL_0:2;

width (Gauge (C,j)) = len (Gauge (C,j)) by JORDAN8:def 1;

then A25: 2 + ((2 |^ (j -' i)) * (b -' 2)) <= width (Gauge (C,j)) by A23, A17, XXREAL_0:2;

2 + ((2 |^ (j -' i)) * (a -' 2)) <= len (Gauge (C,j)) by A23, A17, XXREAL_0:2;

hence [(2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2)))] in Indices (Gauge (C,j)) by A13, A24, A25, MATRIX_0:30; :: thesis: ( (Gauge (C,i)) * (a,b) = (Gauge (C,j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2)))) & 2 + ((2 |^ (j -' i)) * (a -' 2)) = 2 + ((2 |^ (j -' i)) * (a -' 2)) & 2 + ((2 |^ (j -' i)) * (b -' 2)) = 2 + ((2 |^ (j -' i)) * (b -' 2)) )

then A26: (Gauge (C,j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2)))) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))) - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ j)) * ((2 + ((2 |^ (j -' i)) * (b -' 2))) - 2)))]| by JORDAN8:def 1;

width (Gauge (C,i)) = len (Gauge (C,i)) by JORDAN8:def 1;

then b <= width (Gauge (C,i)) by A7, A21, XXREAL_0:2;

then [a,b] in Indices (Gauge (C,i)) by A22, A8, MATRIX_0:30;

then A27: (Gauge (C,i)) * (a,b) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ i)) * (a - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ i)) * (b - 2)))]| by JORDAN8:def 1;

then A28: ((Gauge (C,i)) * (a,b)) `2 = (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ i)) * (b - 2)) by EUCLID:52

.= ((Gauge (C,j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2))))) `2 by A26, A11, EUCLID:52 ;

((Gauge (C,i)) * (a,b)) `1 = (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ i)) * (a - 2)) by A27, EUCLID:52

.= ((Gauge (C,j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2))))) `1 by A26, A16, EUCLID:52 ;

hence (Gauge (C,i)) * (a,b) = (Gauge (C,j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2)))) by A28, TOPREAL3:6; :: thesis: ( 2 + ((2 |^ (j -' i)) * (a -' 2)) = 2 + ((2 |^ (j -' i)) * (a -' 2)) & 2 + ((2 |^ (j -' i)) * (b -' 2)) = 2 + ((2 |^ (j -' i)) * (b -' 2)) )

thus ( 2 + ((2 |^ (j -' i)) * (a -' 2)) = 2 + ((2 |^ (j -' i)) * (a -' 2)) & 2 + ((2 |^ (j -' i)) * (b -' 2)) = 2 + ((2 |^ (j -' i)) * (b -' 2)) ) ; :: thesis: verum