let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis:
let n be Nat; :: thesis:
set G = Gauge (C,n);
let f be FinSequence of (TOP-REAL 2); :: thesis:
assume that
A1: f is_sequence_on Gauge (C,n) and
A2: len f > 1 ; :: thesis:
A3: ( 1 <= (len f) -' 1 & ((len f) -' 1) + 1 = len f ) by A2, NAT_D:49, XREAL_1:235;
let i1, j2 be Nat; :: thesis:
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:
A9: 1 <= j2 by A7, MATRIX_0:32;
A10: i1 <= len (Gauge (C,n)) by A5, MATRIX_0:32;

end;