let n be Element of NAT ; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds E-bound (L~ (Cage C,n)) = (E-bound C) + (((E-bound C) - (W-bound C)) / (2 |^ n))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: E-bound (L~ (Cage C,n)) = (E-bound C) + (((E-bound C) - (W-bound C)) / (2 |^ n))
set a = N-bound C;
set s = S-bound C;
set w = W-bound C;
set e = E-bound C;
set f = Cage C,n;
set G = Gauge C,n;
consider p, q being Element of NAT such that
A1: ( 1 <= p & p < len (Cage C,n) & 1 <= q & q <= width (Gauge C,n) ) and
A2: (Cage C,n) /. p = (Gauge C,n) * (len (Gauge C,n)),q by Th78;
(Cage C,n) /. p in E-most (L~ (Cage C,n)) by A1, A2, Th82;
then A3: ((Cage C,n) /. p) `1 = (E-min (L~ (Cage C,n))) `1 by PSCOMP_1:108;
4 <= len (Gauge C,n) by JORDAN8:13;
then 1 <= len (Gauge C,n) by XXREAL_0:2;
then A4: [(len (Gauge C,n)),q] in Indices (Gauge C,n) by A1, MATRIX_1:37;
thus E-bound (L~ (Cage C,n)) = (E-min (L~ (Cage C,n))) `1 by EUCLID:56
.= |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * ((len (Gauge C,n)) - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (q - 2)))]| `1 by A2, A3, A4, JORDAN8:def 1
.= (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * ((len (Gauge C,n)) - 2)) by EUCLID:56
.= (E-bound C) + (((E-bound C) - (W-bound C)) / (2 |^ n)) by Lm10 ; :: thesis: verum