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

now

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

end;

hence [(i2 -' 1),j1] in Indices (Gauge C,n) by A9, A10, MATRIX_1:37; :: thesis: verum