let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis:
let n be Element of 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:237;
let j1, i2 be Element of NAT ; :: thesis:
assume that
A4: ( 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 ) and
A5: [i2,j1] in Indices (Gauge C,n) and
A6: f /. (len f) = (Gauge C,n) * i2,j1 ; :: thesis:
A7: i2 <= len (Gauge C,n) by A5, MATRIX_1:39;
A8: 1 <= j1 by A5, MATRIX_1:39;

end;