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 + 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 non constant 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 & i + 1 <= len (GoB f) ) and
A2: ( 1 <= j & j + 1 <= width (GoB f) ) and
A3: ( 1 <= k & k + 1 < len f ) and
A4: LSeg ((GoB f) * i,(j + 1)),((GoB f) * (i + 1),(j + 1)) = LSeg f,k and
A5: 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 )
A6: LSeg ((GoB f) * i,(j + 1)),((GoB f) * (i + 1),(j + 1)) = LSeg (f /. k),(f /. (k + 1)) by A3, A4, TOPREAL1:def 5;
then A7: ( ( (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:25;
A8: k + (1 + 1) = (k + 1) + 1 ;
then A9: k + 2 <= len f by A3, NAT_1:13;
1 <= k + 1 by NAT_1:11;
then A10: LSeg ((GoB f) * (i + 1),j),((GoB f) * (i + 1),(j + 1)) = LSeg (f /. (k + 1)),(f /. (k + 2)) by A5, A8, A9, TOPREAL1:def 5;
then A11: ( ( (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:25;
A12: 1 <= i + 1 by NAT_1:11;
A13: 1 <= j + 1 by NAT_1:11;
A14: i < len (GoB f) by A1, NAT_1:13;
A15: j < j + 1 by NAT_1:13;
((GoB f) * i,(j + 1)) `2 = ((GoB f) * 1,(j + 1)) `2 by A1, A2, A13, A14, GOBOARD5:2
.= ((GoB f) * (i + 1),(j + 1)) `2 by A1, A2, A12, A13, GOBOARD5:2 ;
then A16: (GoB f) * (i + 1),j <> (GoB f) * i,(j + 1) by A1, A2, A12, A15, GOBOARD5:5;
hence f /. k = (GoB f) * i,(j + 1) by A7, A10, SPPOL_1:25; :: 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 A6, A11, A16, SPPOL_1:25; :: thesis: f /. (k + 2) = (GoB f) * (i + 1),j
thus f /. (k + 2) = (GoB f) * (i + 1),j by A6, A11, A16, SPPOL_1:25; :: thesis: verum