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))
.= ((Gauge (C,j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2))))) `2 by A26, A11 ;
((Gauge (C,i)) * (a,b)) `1 = (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ i)) * (a - 2)) by A27
.= ((Gauge (C,j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2))))) `1 by A26, A16 ;
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