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