let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for n being Element of NAT
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge C,n & len f > 1 holds
for i1, j1 being Element of NAT st left_cell f,((len f) -' 1),(Gauge C,n) meets C & [i1,j1] in Indices (Gauge C,n) & f /. ((len f) -' 1) = (Gauge C,n) * i1,j1 & [i1,(j1 + 1)] in Indices (Gauge C,n) & f /. (len f) = (Gauge C,n) * i1,(j1 + 1) holds
[(i1 -' 1),(j1 + 1)] in Indices (Gauge C,n)
let n be Element of NAT ; :: thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge C,n & len f > 1 holds
for i1, j1 being Element of NAT st left_cell f,((len f) -' 1),(Gauge C,n) meets C & [i1,j1] in Indices (Gauge C,n) & f /. ((len f) -' 1) = (Gauge C,n) * i1,j1 & [i1,(j1 + 1)] in Indices (Gauge C,n) & f /. (len f) = (Gauge C,n) * i1,(j1 + 1) holds
[(i1 -' 1),(j1 + 1)] in Indices (Gauge C,n)
set G = Gauge C,n;
let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is_sequence_on Gauge C,n & len f > 1 implies for i1, j1 being Element of NAT st left_cell f,((len f) -' 1),(Gauge C,n) meets C & [i1,j1] in Indices (Gauge C,n) & f /. ((len f) -' 1) = (Gauge C,n) * i1,j1 & [i1,(j1 + 1)] in Indices (Gauge C,n) & f /. (len f) = (Gauge C,n) * i1,(j1 + 1) holds
[(i1 -' 1),(j1 + 1)] in Indices (Gauge C,n) )
assume that
A1: f is_sequence_on Gauge C,n and
A2: len f > 1 ; :: thesis: for i1, j1 being Element of NAT st left_cell f,((len f) -' 1),(Gauge C,n) meets C & [i1,j1] in Indices (Gauge C,n) & f /. ((len f) -' 1) = (Gauge C,n) * i1,j1 & [i1,(j1 + 1)] in Indices (Gauge C,n) & f /. (len f) = (Gauge C,n) * i1,(j1 + 1) holds
[(i1 -' 1),(j1 + 1)] in Indices (Gauge C,n)
A3: ( 1 <= (len f) -' 1 & ((len f) -' 1) + 1 = len f ) by A2, NAT_D:49, XREAL_1:237;
let i1, j1 be Element of NAT ; :: thesis: ( left_cell f,((len f) -' 1),(Gauge C,n) meets C & [i1,j1] in Indices (Gauge C,n) & f /. ((len f) -' 1) = (Gauge C,n) * i1,j1 & [i1,(j1 + 1)] in Indices (Gauge C,n) & f /. (len f) = (Gauge C,n) * i1,(j1 + 1) implies [(i1 -' 1),(j1 + 1)] in Indices (Gauge C,n) )
assume that
A4: left_cell f,((len f) -' 1),(Gauge C,n) meets C and
A5: [i1,j1] in Indices (Gauge C,n) and
A6: f /. ((len f) -' 1) = (Gauge C,n) * i1,j1 and
A7: [i1,(j1 + 1)] in Indices (Gauge C,n) and
A8: f /. (len f) = (Gauge C,n) * i1,(j1 + 1) ; :: thesis: [(i1 -' 1),(j1 + 1)] in Indices (Gauge C,n)
A9: 1 <= i1 by A7, MATRIX_1:39;
A10: ( len (Gauge C,n) = width (Gauge C,n) & j1 <= width (Gauge C,n) ) by A5, JORDAN8:def 1, MATRIX_1:39;

A11: now

assume i1 -' 1 < 1 ; :: thesis: contradiction
then i1 <= 1 by NAT_1:14, NAT_D:36;
then i1 = 1 by A9, XXREAL_0:1;
then cell (Gauge C,n),(1 -' 1),j1 meets C by A1, A4, A5, A6, A7, A8, A3, GOBRD13:22;
then cell (Gauge C,n),0 ,j1 meets C by XREAL_1:234;
hence contradiction by A10, JORDAN8:21; :: thesis: verum

end;

A12: i1 -' 1 <= i1 by NAT_D:35;
i1 <= len (Gauge C,n) by A5, MATRIX_1:39;
then A13: i1 -' 1 <= len (Gauge C,n) by A12, XXREAL_0:2;
( 1 <= j1 + 1 & j1 + 1 <= width (Gauge C,n) ) by A7, MATRIX_1:39;
hence [(i1 -' 1),(j1 + 1)] in Indices (Gauge C,n) by A13, A11, MATRIX_1:37; :: thesis: verum