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, j2 being Nat st front_left_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,(j2 -' 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, j2 being Nat st front_left_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,(j2 -' 1)] in Indices (Gauge (C,n))
set G = Gauge (C,n);
let f be FinSequence of (TOP-REAL 2); ( f is_sequence_on Gauge (C,n) & len f > 1 implies for i1, j2 being Nat st front_left_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,(j2 -' 1)] in Indices (Gauge (C,n)) )
assume that
A1:
f is_sequence_on Gauge (C,n)
and
A2:
len f > 1
; for i1, j2 being Nat st front_left_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,(j2 -' 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;
let i1, j2 be Nat; ( front_left_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,(j2 -' 1)] in Indices (Gauge (C,n)) )
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)
; [i1,(j2 -' 1)] in Indices (Gauge (C,n))
A9:
1 <= j2
by A7, MATRIX_0:32;
A10:
i1 <= len (Gauge (C,n))
by A5, MATRIX_0:32;
A11:
now not j2 -' 1 < 1assume
j2 -' 1
< 1
;
contradictionthen
j2 <= 1
by NAT_1:14, NAT_D:36;
then
j2 = 1
by A9, XXREAL_0:1;
then
cell (
(Gauge (C,n)),
i1,
(1 -' 1))
meets C
by A1, A4, A5, A6, A7, A8, A3, GOBRD13:40;
then
cell (
(Gauge (C,n)),
i1,
0)
meets C
by XREAL_1:232;
hence
contradiction
by A10, JORDAN8:17;
verum end;
j2 <= width (Gauge (C,n))
by A7, MATRIX_0:32;
then A12:
j2 -' 1 <= width (Gauge (C,n))
by NAT_D:44;
( 1 <= i1 & i1 <= len (Gauge (C,n)) )
by A7, MATRIX_0:32;
hence
[i1,(j2 -' 1)] in Indices (Gauge (C,n))
by A12, A11, MATRIX_0:30; verum