let i, j, k be Nat; :: thesis: for f being V8() standard special_circular_sequence st 1 <= i & i + 1 <= len (GoB f) & 1 <= j & j + 1 <= width (GoB f) & 1 <= k & k + 1 < len f & LSeg (((GoB f) * (i,(j + 1))),((GoB f) * ((i + 1),(j + 1)))) = LSeg (f,k) & LSeg (((GoB f) * ((i + 1),j)),((GoB f) * ((i + 1),(j + 1)))) = LSeg (f,(k + 1)) holds
( f /. k = (GoB f) * (i,(j + 1)) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & f /. (k + 2) = (GoB f) * ((i + 1),j) )

let f be V8() standard special_circular_sequence; :: thesis: ( 1 <= i & i + 1 <= len (GoB f) & 1 <= j & j + 1 <= width (GoB f) & 1 <= k & k + 1 < len f & LSeg (((GoB f) * (i,(j + 1))),((GoB f) * ((i + 1),(j + 1)))) = LSeg (f,k) & LSeg (((GoB f) * ((i + 1),j)),((GoB f) * ((i + 1),(j + 1)))) = LSeg (f,(k + 1)) implies ( f /. k = (GoB f) * (i,(j + 1)) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & f /. (k + 2) = (GoB f) * ((i + 1),j) ) )
assume that
A1: 1 <= i and
A2: i + 1 <= len (GoB f) and
A3: 1 <= j and
A4: j + 1 <= width (GoB f) and
A5: 1 <= k and
A6: k + 1 < len f and
A7: LSeg (((GoB f) * (i,(j + 1))),((GoB f) * ((i + 1),(j + 1)))) = LSeg (f,k) and
A8: LSeg (((GoB f) * ((i + 1),j)),((GoB f) * ((i + 1),(j + 1)))) = LSeg (f,(k + 1)) ; :: thesis: ( f /. k = (GoB f) * (i,(j + 1)) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & f /. (k + 2) = (GoB f) * ((i + 1),j) )
A9: 1 <= i + 1 by NAT_1:11;
A10: j < j + 1 by NAT_1:13;
A11: 1 <= j + 1 by NAT_1:11;
i < len (GoB f) by ;
then ((GoB f) * (i,(j + 1))) `2 = ((GoB f) * (1,(j + 1))) `2 by
.= ((GoB f) * ((i + 1),(j + 1))) `2 by ;
then A12: (GoB f) * ((i + 1),j) <> (GoB f) * (i,(j + 1)) by ;
A13: 1 <= k + 1 by NAT_1:11;
A14: k + (1 + 1) = (k + 1) + 1 ;
then k + 2 <= len f by ;
then A15: LSeg (((GoB f) * ((i + 1),j)),((GoB f) * ((i + 1),(j + 1)))) = LSeg ((f /. (k + 1)),(f /. (k + 2))) by ;
then A16: ( ( (GoB f) * ((i + 1),(j + 1)) = f /. (k + 1) & (GoB f) * ((i + 1),j) = f /. (k + 2) ) or ( (GoB f) * ((i + 1),(j + 1)) = f /. (k + 2) & (GoB f) * ((i + 1),j) = f /. (k + 1) ) ) by SPPOL_1:8;
A17: LSeg (((GoB f) * (i,(j + 1))),((GoB f) * ((i + 1),(j + 1)))) = LSeg ((f /. k),(f /. (k + 1))) by ;
then ( ( (GoB f) * (i,(j + 1)) = f /. k & (GoB f) * ((i + 1),(j + 1)) = f /. (k + 1) ) or ( (GoB f) * (i,(j + 1)) = f /. (k + 1) & (GoB f) * ((i + 1),(j + 1)) = f /. k ) ) by SPPOL_1:8;
hence f /. k = (GoB f) * (i,(j + 1)) by ; :: thesis: ( f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & f /. (k + 2) = (GoB f) * ((i + 1),j) )
thus f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) by ; :: thesis: f /. (k + 2) = (GoB f) * ((i + 1),j)
thus f /. (k + 2) = (GoB f) * ((i + 1),j) by ; :: thesis: verum