set n = 1;

let f be V22() 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;

len f > 1 by GOBOARD7:34, XXREAL_0:2;

then p .. f < len f by A1, SPRECT_5:7;

then A2: (p .. f) + 1 <= len f by NAT_1:13;

A3: 1 <= p .. f by A1, FINSEQ_4:21;

A4: for i1, j1, i2, j2 being 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) )

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

let f be V22() 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;

len f > 1 by GOBOARD7:34, XXREAL_0:2;

then p .. f < len f by A1, SPRECT_5:7;

then A2: (p .. f) + 1 <= len f by NAT_1:13;

A3: 1 <= p .. f by A1, FINSEQ_4:21;

A4: for i1, j1, i2, j2 being 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

1 + 1 <= len (Rotate (f,p))
by GOBOARD7:34, XXREAL_0:2;
(Rotate (f,p)) /. (((1 + 1) + (p .. f)) -' (p .. f)) = (Rotate (f,p)) /. (1 + 1)
by NAT_D:34;

then A5: (Rotate (f,p)) /. ((((p .. f) + 1) + 1) -' (p .. f)) = (Rotate (f,p)) /. (1 + 1) ;

A6: left_cell (f,(p .. f)) = left_cell (f,(p .. f)) ;

let i1, j1, i2, j2 be 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

A7: ( [i1,j1] in Indices (GoB (Rotate (f,p))) & [i2,j2] in Indices (GoB (Rotate (f,p))) ) and

A8: (Rotate (f,p)) /. 1 = (GoB (Rotate (f,p))) * (i1,j1) and

A9: (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) ) )

A10: GoB (Rotate (f,p)) = GoB f by REVROT_1:28;

len (Rotate (f,p)) = len f by FINSEQ_6:179;

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 A11: f /. (p .. f) = (GoB f) * (i1,j1) by A1, A3, A8, A10, FINSEQ_6:183;

p .. f < (p .. f) + 1 by NAT_1:13;

then A12: f /. ((p .. f) + 1) = (GoB f) * (i2,j2) by A1, A2, A9, A10, A5, FINSEQ_6:175;

then A13: ( ( 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 A3, A2, A7, A10, A11, A6, GOBOARD5:def 7;

end;then A5: (Rotate (f,p)) /. ((((p .. f) + 1) + 1) -' (p .. f)) = (Rotate (f,p)) /. (1 + 1) ;

A6: left_cell (f,(p .. f)) = left_cell (f,(p .. f)) ;

let i1, j1, i2, j2 be 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

A7: ( [i1,j1] in Indices (GoB (Rotate (f,p))) & [i2,j2] in Indices (GoB (Rotate (f,p))) ) and

A8: (Rotate (f,p)) /. 1 = (GoB (Rotate (f,p))) * (i1,j1) and

A9: (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) ) )

A10: GoB (Rotate (f,p)) = GoB f by REVROT_1:28;

len (Rotate (f,p)) = len f by FINSEQ_6:179;

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 A11: f /. (p .. f) = (GoB f) * (i1,j1) by A1, A3, A8, A10, FINSEQ_6:183;

p .. f < (p .. f) + 1 by NAT_1:13;

then A12: f /. ((p .. f) + 1) = (GoB f) * (i2,j2) by A1, A2, A9, A10, A5, FINSEQ_6:175;

then A13: ( ( 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 A3, A2, A7, A10, A11, A6, 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 A3, A2, A7, A10, A11, A12, A6, GOBOARD5:def 7;

end;

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 A13, 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 A13, REVROT_1:28; :: thesis: verum

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