let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); 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 front_right_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,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds
[(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n))
let n be 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 front_right_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,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds
[(i1 + 1),(j1 + 1)] 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); ( f is_sequence_on Gauge (C,n) & len f > 1 implies for i1, j1 being Nat st front_right_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,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds
[(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n)) )
assume that
A2:
f is_sequence_on Gauge (C,n)
and
A3:
len f > 1
; for i1, j1 being Nat st front_right_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,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds
[(i1 + 1),(j1 + 1)] 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, j1 be Nat; ( front_right_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,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) implies [(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n)) )
assume that
A5:
( front_right_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) )
and
A6:
[i1,(j1 + 1)] in Indices (Gauge (C,n))
and
A7:
f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1))
; [(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n))
A8:
j1 + 1 <= width (Gauge (C,n))
by A6, MATRIX_0:32;
A9:
i1 <= len (Gauge (C,n))
by A6, MATRIX_0:32;
A10:
now not i1 + 1 > len (Gauge (C,n))assume
i1 + 1
> len (Gauge (C,n))
;
contradictionthen A11:
(len (Gauge (C,n))) + 1
<= i1 + 1
by NAT_1:13;
i1 + 1
<= (len (Gauge (C,n))) + 1
by A9, XREAL_1:6;
then
i1 + 1
= (len (Gauge (C,n))) + 1
by A11, XXREAL_0:1;
then
cell (
(Gauge (C,n)),
(len (Gauge (C,n))),
(j1 + 1))
meets C
by A2, A5, A6, A7, A4, GOBRD13:35;
hence
contradiction
by A1, A8, JORDAN8:16;
verum end;
A12:
1 <= i1 + 1
by NAT_1:11;
1 <= j1 + 1
by A6, MATRIX_0:32;
hence
[(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n))
by A8, A12, A10, MATRIX_0:30; verum