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, j1 being Nat st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds
[(i1 + 1),(j1 + 1)] 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, j1 being Nat st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds
[(i1 + 1),(j1 + 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, j1 being Nat st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds
[(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n)) )
assume that
A1: f is_sequence_on Gauge (C,n) and
A2: len f > 1 ; :: thesis: for i1, j1 being Nat st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds
[(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n))
A3: ( 1 <= (len f) -' 1 & ((len f) -' 1) + 1 = len f ) by A2, NAT_D:49, XREAL_1:235;
A4: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;
let i1, j1 be Nat; :: thesis: ( left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) implies [(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n)) )
assume that
A5: left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C and
A6: [i1,j1] in Indices (Gauge (C,n)) and
A7: f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) and
A8: [(i1 + 1),j1] in Indices (Gauge (C,n)) and
A9: f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) ; :: thesis: [(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n))
A10: j1 <= width (Gauge (C,n)) by A8, MATRIX_0:32;
A11: i1 <= len (Gauge (C,n)) by A6, MATRIX_0:32;
A12: now :: thesis: not j1 + 1 > len (Gauge (C,n))
assume j1 + 1 > len (Gauge (C,n)) ; :: thesis: contradiction
then A13: (len (Gauge (C,n))) + 1 <= j1 + 1 by NAT_1:13;
j1 + 1 <= (len (Gauge (C,n))) + 1 by A4, A10, XREAL_1:6;
then j1 + 1 = (len (Gauge (C,n))) + 1 by A13, XXREAL_0:1;
then cell ((Gauge (C,n)),i1,(len (Gauge (C,n)))) meets C by A1, A5, A6, A7, A8, A9, A3, GOBRD13:23;
hence contradiction by A11, JORDAN8:15; :: thesis: verum
end;
A14: 1 <= j1 + 1 by NAT_1:11;
( 1 <= i1 + 1 & i1 + 1 <= len (Gauge (C,n)) ) by A8, MATRIX_0:32;
hence [(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n)) by A4, A14, A12, MATRIX_0:30; :: thesis: verum