let i, j, k be Element of NAT ; :: thesis: for f being non constant standard special_circular_sequence st 1 <= i & i + 1 < len (GoB f) & 1 <= j & j <= width (GoB f) & 1 <= k & k + 1 < len f & LSeg ((GoB f) * i,j),((GoB f) * (i + 1),j) = LSeg f,k & LSeg ((GoB f) * (i + 1),j),((GoB f) * (i + 2),j) = LSeg f,(k + 1) holds
( f /. k = (GoB f) * i,j & f /. (k + 1) = (GoB f) * (i + 1),j & f /. (k + 2) = (GoB f) * (i + 2),j )
let f be non constant standard special_circular_sequence; :: thesis: ( 1 <= i & i + 1 < len (GoB f) & 1 <= j & j <= width (GoB f) & 1 <= k & k + 1 < len f & LSeg ((GoB f) * i,j),((GoB f) * (i + 1),j) = LSeg f,k & LSeg ((GoB f) * (i + 1),j),((GoB f) * (i + 2),j) = LSeg f,(k + 1) implies ( f /. k = (GoB f) * i,j & f /. (k + 1) = (GoB f) * (i + 1),j & f /. (k + 2) = (GoB f) * (i + 2),j ) )
assume that
A1: 1 <= i and
A2: i + 1 < len (GoB f) and
A3: ( 1 <= j & j <= width (GoB f) ) and
A4: 1 <= k and
A5: k + 1 < len f and
A6: LSeg ((GoB f) * i,j),((GoB f) * (i + 1),j) = LSeg f,k and
A7: LSeg ((GoB f) * (i + 1),j),((GoB f) * (i + 2),j) = LSeg f,(k + 1) ; :: thesis: ( f /. k = (GoB f) * i,j & f /. (k + 1) = (GoB f) * (i + 1),j & f /. (k + 2) = (GoB f) * (i + 2),j )
A8: i < i + 2 by XREAL_1:31;
i + (1 + 1) = (i + 1) + 1 ;
then i + 2 <= len (GoB f) by A2, NAT_1:13;
then A9: ((GoB f) * i,j) `1 < ((GoB f) * (i + 2),j) `1 by A1, A3, A8, GOBOARD5:4;
A10: 1 <= k + 1 by NAT_1:11;
A11: k + (1 + 1) = (k + 1) + 1 ;
then k + 2 <= len f by A5, NAT_1:13;
then A12: LSeg ((GoB f) * (i + 1),j),((GoB f) * (i + 2),j) = LSeg (f /. (k + 1)),(f /. (k + 2)) by A7, A11, A10, TOPREAL1:def 5;
then A13: ( ( (GoB f) * (i + 1),j = f /. (k + 1) & (GoB f) * (i + 2),j = f /. (k + 2) ) or ( (GoB f) * (i + 1),j = f /. (k + 2) & (GoB f) * (i + 2),j = f /. (k + 1) ) ) by SPPOL_1:25;
A14: LSeg ((GoB f) * i,j),((GoB f) * (i + 1),j) = LSeg (f /. k),(f /. (k + 1)) by A4, A5, A6, TOPREAL1:def 5;
then ( ( (GoB f) * i,j = f /. k & (GoB f) * (i + 1),j = f /. (k + 1) ) or ( (GoB f) * i,j = f /. (k + 1) & (GoB f) * (i + 1),j = f /. k ) ) by SPPOL_1:25;
hence f /. k = (GoB f) * i,j by A12, A9, SPPOL_1:25; :: thesis: ( f /. (k + 1) = (GoB f) * (i + 1),j & f /. (k + 2) = (GoB f) * (i + 2),j )
thus f /. (k + 1) = (GoB f) * (i + 1),j by A14, A13, A9, SPPOL_1:25; :: thesis: f /. (k + 2) = (GoB f) * (i + 2),j
thus f /. (k + 2) = (GoB f) * (i + 2),j by A14, A13, A9, SPPOL_1:25; :: thesis: verum