let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for n being 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 Nat st front_right_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 -' 1),j2] in Indices (Gauge (C,n))
let n be 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 Nat st front_right_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 -' 1),j2] 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 i1, j2 being Nat st front_right_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 -' 1),j2] in Indices (Gauge (C,n)) )
assume that
A2: f is_sequence_on Gauge (C,n) and
A3: len f > 1 ; :: thesis: for i1, j2 being Nat st front_right_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 -' 1),j2] in Indices (Gauge (C,n))
A4: ( 1 <= (len f) -' 1 & ((len f) -' 1) + 1 = len f ) by A3, NAT_D:49, XREAL_1:235;
let i1, j2 be Nat; :: thesis: ( front_right_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 -' 1),j2] in Indices (Gauge (C,n)) )
assume that
A5: ( front_right_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)) ) and
A6: [i1,j2] in Indices (Gauge (C,n)) and
A7: f /. (len f) = (Gauge (C,n)) * (i1,j2) ; :: thesis: [(i1 -' 1),j2] in Indices (Gauge (C,n))
A8: j2 <= width (Gauge (C,n)) by A6, MATRIX_0:32;
A9: 1 <= i1 by A6, MATRIX_0:32;

A10: now :: thesis: not i1 -' 1 < 1

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),(j2 -' 1)) meets C by A2, A5, A6, A7, A4, GOBRD13:41;
then cell ((Gauge (C,n)),0,(j2 -' 1)) meets C by XREAL_1:232;
hence contradiction by A1, A8, JORDAN8:18, NAT_D:44; :: thesis: verum

end;

i1 <= len (Gauge (C,n)) by A6, MATRIX_0:32;
then A11: i1 -' 1 <= len (Gauge (C,n)) by NAT_D:44;
1 <= j2 by A6, MATRIX_0:32;
hence [(i1 -' 1),j2] in Indices (Gauge (C,n)) by A8, A11, A10, MATRIX_0:30; :: thesis: verum