let f be non constant standard special_circular_sequence; :: thesis: for p being Point of (TOP-REAL 2) st p in rng f holds
left_cell f,(p .. f) = left_cell (Rotate f,p),1
let p be Point of (TOP-REAL 2); :: thesis: ( p in rng f implies left_cell f,(p .. f) = left_cell (Rotate f,p),1 )
assume A1: p in rng f ; :: thesis: left_cell f,(p .. f) = left_cell (Rotate f,p),1
set k = p .. f;
A2: 1 <= p .. f by A1, FINSEQ_4:31;
len f > 1 by GOBOARD7:36, XXREAL_0:2;
then p .. f < len f by A1, SPRECT_5:7;
then A3: (p .. f) + 1 <= len f by NAT_1:13;
set n = 1;
1 + 1 <= len f by GOBOARD7:36, XXREAL_0:2;
then A4: 1 + 1 <= len (Rotate f,p) by REVROT_1:14;
for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB (Rotate f,p)) & [i2,j2] in Indices (GoB (Rotate f,p)) & (Rotate f,p) /. 1 = (GoB (Rotate f,p)) * i1,j1 & (Rotate f,p) /. (1 + 1) = (GoB (Rotate f,p)) * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & left_cell f,(p .. f) = cell (GoB (Rotate f,p)),(i1 -' 1),j1 ) & not ( i1 + 1 = i2 & j1 = j2 & left_cell f,(p .. f) = cell (GoB (Rotate f,p)),i1,j1 ) & not ( i1 = i2 + 1 & j1 = j2 & left_cell f,(p .. f) = cell (GoB (Rotate f,p)),i2,(j2 -' 1) ) holds
( i1 = i2 & j1 = j2 + 1 & left_cell f,(p .. f) = cell (GoB (Rotate f,p)),i1,j2 )

proof

let i1, j1, i2, j2 be Element of NAT ; :: thesis: ( [i1,j1] in Indices (GoB (Rotate f,p)) & [i2,j2] in Indices (GoB (Rotate f,p)) & (Rotate f,p) /. 1 = (GoB (Rotate f,p)) * i1,j1 & (Rotate f,p) /. (1 + 1) = (GoB (Rotate f,p)) * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & left_cell f,(p .. f) = cell (GoB (Rotate f,p)),(i1 -' 1),j1 ) & not ( i1 + 1 = i2 & j1 = j2 & left_cell f,(p .. f) = cell (GoB (Rotate f,p)),i1,j1 ) & not ( i1 = i2 + 1 & j1 = j2 & left_cell f,(p .. f) = cell (GoB (Rotate f,p)),i2,(j2 -' 1) ) implies ( i1 = i2 & j1 = j2 + 1 & left_cell f,(p .. f) = cell (GoB (Rotate f,p)),i1,j2 ) )
assume that
A5: [i1,j1] in Indices (GoB (Rotate f,p)) and
A6: [i2,j2] in Indices (GoB (Rotate f,p)) and
A7: (Rotate f,p) /. 1 = (GoB (Rotate f,p)) * i1,j1 and
A8: (Rotate f,p) /. (1 + 1) = (GoB (Rotate f,p)) * i2,j2 ; :: thesis: ( ( i1 = i2 & j1 + 1 = j2 & left_cell f,(p .. f) = cell (GoB (Rotate f,p)),(i1 -' 1),j1 ) or ( i1 + 1 = i2 & j1 = j2 & left_cell f,(p .. f) = cell (GoB (Rotate f,p)),i1,j1 ) or ( i1 = i2 + 1 & j1 = j2 & left_cell f,(p .. f) = cell (GoB (Rotate f,p)),i2,(j2 -' 1) ) or ( i1 = i2 & j1 = j2 + 1 & left_cell f,(p .. f) = cell (GoB (Rotate f,p)),i1,j2 ) )
A9: GoB (Rotate f,p) = GoB f by REVROT_1:28;
len (Rotate f,p) = len f by REVROT_1:14;
then (Rotate f,p) /. (len f) = (Rotate f,p) /. 1 by FINSEQ_6:def 1;
then (Rotate f,p) /. (((p .. f) + (len f)) -' (p .. f)) = (Rotate f,p) /. 1 by NAT_D:34;
then A10: f /. (p .. f) = (GoB f) * i1,j1 by A1, A2, A7, A9, REVROT_1:18;
(Rotate f,p) /. (((1 + 1) + (p .. f)) -' (p .. f)) = (Rotate f,p) /. (1 + 1) by NAT_D:34;
then A11: (Rotate f,p) /. ((((p .. f) + 1) + 1) -' (p .. f)) = (Rotate f,p) /. (1 + 1) ;
p .. f < (p .. f) + 1 by NAT_1:13;
then A12: f /. ((p .. f) + 1) = (GoB f) * i2,j2 by A1, A3, A8, A9, A11, REVROT_1:10;
A13: left_cell f,(p .. f) = left_cell f,(p .. f) ;
then A14: ( ( i1 = i2 & j1 + 1 = j2 & left_cell f,(p .. f) = cell (GoB f),(i1 -' 1),j1 ) or ( i1 + 1 = i2 & j1 = j2 & left_cell f,(p .. f) = cell (GoB f),i1,j1 ) or ( i1 = i2 + 1 & j1 = j2 & left_cell f,(p .. f) = cell (GoB f),i2,(j2 -' 1) ) or ( i1 = i2 & j1 = j2 + 1 & left_cell f,(p .. f) = cell (GoB f),i1,j2 ) ) by A2, A3, A5, A6, A9, A10, A12, GOBOARD5:def 7;

per cases ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A2, A3, A5, A6, A9, A10, A12, A13, GOBOARD5:def 7;

case ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis: left_cell f,(p .. f) = cell (GoB (Rotate f,p)),(i1 -' 1),j1

hence left_cell f,(p .. f) = cell (GoB (Rotate f,p)),(i1 -' 1),j1 by A14, REVROT_1:28; :: thesis: verum

end;

case ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis: left_cell f,(p .. f) = cell (GoB (Rotate f,p)),i1,j1

hence left_cell f,(p .. f) = cell (GoB (Rotate f,p)),i1,j1 by A14, REVROT_1:28; :: thesis: verum

end;

case ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis: left_cell f,(p .. f) = cell (GoB (Rotate f,p)),i2,(j2 -' 1)

hence left_cell f,(p .. f) = cell (GoB (Rotate f,p)),i2,(j2 -' 1) by A14, REVROT_1:28; :: thesis: verum

end;

case ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis: left_cell f,(p .. f) = cell (GoB (Rotate f,p)),i1,j2

hence left_cell f,(p .. f) = cell (GoB (Rotate f,p)),i1,j2 by A14, REVROT_1:28; :: thesis: verum

end;

end;

end;

hence left_cell f,(p .. f) = left_cell (Rotate f,p),1 by A4, GOBOARD5:def 7; :: thesis: verum