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, j2 being Element of NAT st front_left_cell f,((len f) -' 1),(Gauge C,n) meets C & [i1,(j2 + 1)] in Indices (Gauge C,n) & f /. ((len f) -' 1) = (Gauge C,n) * i1,(j2 + 1) & [i1,j2] in Indices (Gauge C,n) & f /. (len f) = (Gauge C,n) * i1,j2 holds
[i1,(j2 -' 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, j2 being Element of NAT st front_left_cell f,((len f) -' 1),(Gauge C,n) meets C & [i1,(j2 + 1)] in Indices (Gauge C,n) & f /. ((len f) -' 1) = (Gauge C,n) * i1,(j2 + 1) & [i1,j2] in Indices (Gauge C,n) & f /. (len f) = (Gauge C,n) * i1,j2 holds
[i1,(j2 -' 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, j2 being Element of NAT st front_left_cell f,((len f) -' 1),(Gauge C,n) meets C & [i1,(j2 + 1)] in Indices (Gauge C,n) & f /. ((len f) -' 1) = (Gauge C,n) * i1,(j2 + 1) & [i1,j2] in Indices (Gauge C,n) & f /. (len f) = (Gauge C,n) * i1,j2 holds
[i1,(j2 -' 1)] in Indices (Gauge C,n) )
assume that
A1: f is_sequence_on Gauge C,n and
A2: len f > 1 ; :: thesis: for i1, j2 being Element of NAT st front_left_cell f,((len f) -' 1),(Gauge C,n) meets C & [i1,(j2 + 1)] in Indices (Gauge C,n) & f /. ((len f) -' 1) = (Gauge C,n) * i1,(j2 + 1) & [i1,j2] in Indices (Gauge C,n) & f /. (len f) = (Gauge C,n) * i1,j2 holds
[i1,(j2 -' 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, j2 be Element of NAT ; :: thesis: ( front_left_cell f,((len f) -' 1),(Gauge C,n) meets C & [i1,(j2 + 1)] in Indices (Gauge C,n) & f /. ((len f) -' 1) = (Gauge C,n) * i1,(j2 + 1) & [i1,j2] in Indices (Gauge C,n) & f /. (len f) = (Gauge C,n) * i1,j2 implies [i1,(j2 -' 1)] in Indices (Gauge C,n) )
assume that
A4: front_left_cell f,((len f) -' 1),(Gauge C,n) meets C and
A5: [i1,(j2 + 1)] in Indices (Gauge C,n) and
A6: f /. ((len f) -' 1) = (Gauge C,n) * i1,(j2 + 1) and
A7: [i1,j2] in Indices (Gauge C,n) and
A8: f /. (len f) = (Gauge C,n) * i1,j2 ; :: thesis: [i1,(j2 -' 1)] in Indices (Gauge C,n)
A9: 1 <= j2 by A7, MATRIX_1:39;
A10: i1 <= len (Gauge C,n) by A5, MATRIX_1:39;

A11: now

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

end;

j2 <= width (Gauge C,n) by A7, MATRIX_1:39;
then A12: j2 -' 1 <= width (Gauge C,n) by NAT_D:44;
( 1 <= i1 & i1 <= len (Gauge C,n) ) by A7, MATRIX_1:39;
hence [i1,(j2 -' 1)] in Indices (Gauge C,n) by A12, A11, MATRIX_1:37; :: thesis: verum