let i, j 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) & LSeg (((GoB f) * (i,j)),((GoB f) * (i,(j + 1)))) c= L~ f & LSeg (((GoB f) * (i,(j + 1))),((GoB f) * ((i + 1),(j + 1)))) c= L~ f & not ( f /. 1 = (GoB f) * (i,(j + 1)) & ( ( f /. 2 = (GoB f) * (i,j) & f /. ((len f) -' 1) = (GoB f) * ((i + 1),(j + 1)) ) or ( f /. 2 = (GoB f) * ((i + 1),(j + 1)) & f /. ((len f) -' 1) = (GoB f) * (i,j) ) ) ) holds

ex k being Nat st

( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * (i,(j + 1)) & ( ( f /. k = (GoB f) * (i,j) & f /. (k + 2) = (GoB f) * ((i + 1),(j + 1)) ) or ( f /. k = (GoB f) * ((i + 1),(j + 1)) & f /. (k + 2) = (GoB f) * (i,j) ) ) )

let f be V8() standard special_circular_sequence; :: thesis: ( 1 <= i & i + 1 <= len (GoB f) & 1 <= j & j + 1 <= width (GoB f) & LSeg (((GoB f) * (i,j)),((GoB f) * (i,(j + 1)))) c= L~ f & LSeg (((GoB f) * (i,(j + 1))),((GoB f) * ((i + 1),(j + 1)))) c= L~ f & not ( f /. 1 = (GoB f) * (i,(j + 1)) & ( ( f /. 2 = (GoB f) * (i,j) & f /. ((len f) -' 1) = (GoB f) * ((i + 1),(j + 1)) ) or ( f /. 2 = (GoB f) * ((i + 1),(j + 1)) & f /. ((len f) -' 1) = (GoB f) * (i,j) ) ) ) implies ex k being Nat st

( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * (i,(j + 1)) & ( ( f /. k = (GoB f) * (i,j) & f /. (k + 2) = (GoB f) * ((i + 1),(j + 1)) ) or ( f /. k = (GoB f) * ((i + 1),(j + 1)) & f /. (k + 2) = (GoB f) * (i,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: LSeg (((GoB f) * (i,j)),((GoB f) * (i,(j + 1)))) c= L~ f and

A6: LSeg (((GoB f) * (i,(j + 1))),((GoB f) * ((i + 1),(j + 1)))) c= L~ f ; :: thesis: ( ( f /. 1 = (GoB f) * (i,(j + 1)) & ( ( f /. 2 = (GoB f) * (i,j) & f /. ((len f) -' 1) = (GoB f) * ((i + 1),(j + 1)) ) or ( f /. 2 = (GoB f) * ((i + 1),(j + 1)) & f /. ((len f) -' 1) = (GoB f) * (i,j) ) ) ) or ex k being Nat st

( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * (i,(j + 1)) & ( ( f /. k = (GoB f) * (i,j) & f /. (k + 2) = (GoB f) * ((i + 1),(j + 1)) ) or ( f /. k = (GoB f) * ((i + 1),(j + 1)) & f /. (k + 2) = (GoB f) * (i,j) ) ) ) )

A7: i < len (GoB f) by A2, NAT_1:13;

A8: j < width (GoB f) by A4, NAT_1:13;

A9: 1 <= i + 1 by NAT_1:11;

(1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * (i,(j + 1)))) in LSeg (((GoB f) * (i,j)),((GoB f) * (i,(j + 1)))) by RLTOPSP1:69;

then consider k1 being Nat such that

A10: 1 <= k1 and

A11: k1 + 1 <= len f and

A12: LSeg (((GoB f) * (i,j)),((GoB f) * (i,(j + 1)))) = LSeg (f,k1) by A1, A3, A4, A5, A7, Th39;

A13: k1 < len f by A11, NAT_1:13;

(1 / 2) * (((GoB f) * (i,(j + 1))) + ((GoB f) * ((i + 1),(j + 1)))) in LSeg (((GoB f) * (i,(j + 1))),((GoB f) * ((i + 1),(j + 1)))) by RLTOPSP1:69;

then consider k2 being Nat such that

A16: 1 <= k2 and

A17: k2 + 1 <= len f and

A18: LSeg (((GoB f) * (i,(j + 1))),((GoB f) * ((i + 1),(j + 1)))) = LSeg (f,k2) by A1, A2, A4, A6, A15, Th40;

A19: k2 < len f by A17, NAT_1:13;

( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * (i,(j + 1)) & ( ( f /. k = (GoB f) * (i,j) & f /. (k + 2) = (GoB f) * ((i + 1),(j + 1)) ) or ( f /. k = (GoB f) * ((i + 1),(j + 1)) & f /. (k + 2) = (GoB f) * (i,j) ) ) ) ) ; :: thesis: verum

ex k being Nat st

( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * (i,(j + 1)) & ( ( f /. k = (GoB f) * (i,j) & f /. (k + 2) = (GoB f) * ((i + 1),(j + 1)) ) or ( f /. k = (GoB f) * ((i + 1),(j + 1)) & f /. (k + 2) = (GoB f) * (i,j) ) ) )

let f be V8() standard special_circular_sequence; :: thesis: ( 1 <= i & i + 1 <= len (GoB f) & 1 <= j & j + 1 <= width (GoB f) & LSeg (((GoB f) * (i,j)),((GoB f) * (i,(j + 1)))) c= L~ f & LSeg (((GoB f) * (i,(j + 1))),((GoB f) * ((i + 1),(j + 1)))) c= L~ f & not ( f /. 1 = (GoB f) * (i,(j + 1)) & ( ( f /. 2 = (GoB f) * (i,j) & f /. ((len f) -' 1) = (GoB f) * ((i + 1),(j + 1)) ) or ( f /. 2 = (GoB f) * ((i + 1),(j + 1)) & f /. ((len f) -' 1) = (GoB f) * (i,j) ) ) ) implies ex k being Nat st

( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * (i,(j + 1)) & ( ( f /. k = (GoB f) * (i,j) & f /. (k + 2) = (GoB f) * ((i + 1),(j + 1)) ) or ( f /. k = (GoB f) * ((i + 1),(j + 1)) & f /. (k + 2) = (GoB f) * (i,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: LSeg (((GoB f) * (i,j)),((GoB f) * (i,(j + 1)))) c= L~ f and

A6: LSeg (((GoB f) * (i,(j + 1))),((GoB f) * ((i + 1),(j + 1)))) c= L~ f ; :: thesis: ( ( f /. 1 = (GoB f) * (i,(j + 1)) & ( ( f /. 2 = (GoB f) * (i,j) & f /. ((len f) -' 1) = (GoB f) * ((i + 1),(j + 1)) ) or ( f /. 2 = (GoB f) * ((i + 1),(j + 1)) & f /. ((len f) -' 1) = (GoB f) * (i,j) ) ) ) or ex k being Nat st

( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * (i,(j + 1)) & ( ( f /. k = (GoB f) * (i,j) & f /. (k + 2) = (GoB f) * ((i + 1),(j + 1)) ) or ( f /. k = (GoB f) * ((i + 1),(j + 1)) & f /. (k + 2) = (GoB f) * (i,j) ) ) ) )

A7: i < len (GoB f) by A2, NAT_1:13;

A8: j < width (GoB f) by A4, NAT_1:13;

A9: 1 <= i + 1 by NAT_1:11;

(1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * (i,(j + 1)))) in LSeg (((GoB f) * (i,j)),((GoB f) * (i,(j + 1)))) by RLTOPSP1:69;

then consider k1 being Nat such that

A10: 1 <= k1 and

A11: k1 + 1 <= len f and

A12: LSeg (((GoB f) * (i,j)),((GoB f) * (i,(j + 1)))) = LSeg (f,k1) by A1, A3, A4, A5, A7, Th39;

A13: k1 < len f by A11, NAT_1:13;

A14: now :: thesis: ( not k1 > 1 or k1 = 2 or k1 > 2 )

A15:
1 <= j + 1
by NAT_1:11;assume
k1 > 1
; :: thesis: ( k1 = 2 or k1 > 2 )

then k1 >= 1 + 1 by NAT_1:13;

hence ( k1 = 2 or k1 > 2 ) by XXREAL_0:1; :: thesis: verum

end;then k1 >= 1 + 1 by NAT_1:13;

hence ( k1 = 2 or k1 > 2 ) by XXREAL_0:1; :: thesis: verum

(1 / 2) * (((GoB f) * (i,(j + 1))) + ((GoB f) * ((i + 1),(j + 1)))) in LSeg (((GoB f) * (i,(j + 1))),((GoB f) * ((i + 1),(j + 1)))) by RLTOPSP1:69;

then consider k2 being Nat such that

A16: 1 <= k2 and

A17: k2 + 1 <= len f and

A18: LSeg (((GoB f) * (i,(j + 1))),((GoB f) * ((i + 1),(j + 1)))) = LSeg (f,k2) by A1, A2, A4, A6, A15, Th40;

A19: k2 < len f by A17, NAT_1:13;

A20: now :: thesis: ( not k2 > 1 or k2 = 2 or k2 > 2 )

A21:
( k1 = 1 or k1 > 1 )
by A10, XXREAL_0:1;assume
k2 > 1
; :: thesis: ( k2 = 2 or k2 > 2 )

then k2 >= 1 + 1 by NAT_1:13;

hence ( k2 = 2 or k2 > 2 ) by XXREAL_0:1; :: thesis: verum

end;then k2 >= 1 + 1 by NAT_1:13;

hence ( k2 = 2 or k2 > 2 ) by XXREAL_0:1; :: thesis: verum

now :: thesis: ( ( k1 = 1 & k2 = 2 & 1 <= 1 & 1 + 1 < len f & f /. (1 + 1) = (GoB f) * (i,(j + 1)) & f /. 1 = (GoB f) * (i,j) & f /. (1 + 2) = (GoB f) * ((i + 1),(j + 1)) ) or ( k1 = 1 & k2 > 2 & f /. 1 = (GoB f) * (i,(j + 1)) & f /. 2 = (GoB f) * (i,j) & f /. ((len f) -' 1) = (GoB f) * ((i + 1),(j + 1)) ) or ( k2 = 1 & k1 = 2 & 1 <= 1 & 1 + 1 < len f & f /. (1 + 1) = (GoB f) * (i,(j + 1)) & f /. 1 = (GoB f) * ((i + 1),(j + 1)) & f /. (1 + 2) = (GoB f) * (i,j) ) or ( k2 = 1 & k1 > 2 & f /. 1 = (GoB f) * (i,(j + 1)) & f /. 2 = (GoB f) * ((i + 1),(j + 1)) & f /. ((len f) -' 1) = (GoB f) * (i,j) ) or ( k1 = k2 & contradiction ) or ( k1 > 1 & k2 > k1 & 1 <= k1 & k1 + 1 < len f & f /. (k1 + 1) = (GoB f) * (i,(j + 1)) & f /. k1 = (GoB f) * (i,j) & f /. (k1 + 2) = (GoB f) * ((i + 1),(j + 1)) ) or ( k2 > 1 & k1 > k2 & 1 <= k2 & k2 + 1 < len f & f /. (k2 + 1) = (GoB f) * (i,(j + 1)) & f /. k2 = (GoB f) * ((i + 1),(j + 1)) & f /. (k2 + 2) = (GoB f) * (i,j) ) )end;

hence
( ( f /. 1 = (GoB f) * (i,(j + 1)) & ( ( f /. 2 = (GoB f) * (i,j) & f /. ((len f) -' 1) = (GoB f) * ((i + 1),(j + 1)) ) or ( f /. 2 = (GoB f) * ((i + 1),(j + 1)) & f /. ((len f) -' 1) = (GoB f) * (i,j) ) ) ) or ex k being Nat st per cases
( ( k1 = 1 & k2 = 2 ) or ( k1 = 1 & k2 > 2 ) or ( k2 = 1 & k1 = 2 ) or ( k2 = 1 & k1 > 2 ) or k1 = k2 or ( k1 > 1 & k2 > k1 ) or ( k2 > 1 & k1 > k2 ) )
by A16, A14, A20, A21, XXREAL_0:1;

end;

case that A22:
k1 = 1
and

A23: k2 = 2 ; :: thesis: ( 1 <= 1 & 1 + 1 < len f & f /. (1 + 1) = (GoB f) * (i,(j + 1)) & f /. 1 = (GoB f) * (i,j) & f /. (1 + 2) = (GoB f) * ((i + 1),(j + 1)) )

A23: k2 = 2 ; :: thesis: ( 1 <= 1 & 1 + 1 < len f & f /. (1 + 1) = (GoB f) * (i,(j + 1)) & f /. 1 = (GoB f) * (i,j) & f /. (1 + 2) = (GoB f) * ((i + 1),(j + 1)) )

A24:
LSeg (f,2) = LSeg ((f /. 2),(f /. (2 + 1)))
by A17, A23, TOPREAL1:def 3;

then A25: ( ( (GoB f) * (i,(j + 1)) = f /. 2 & (GoB f) * ((i + 1),(j + 1)) = f /. (2 + 1) ) or ( (GoB f) * (i,(j + 1)) = f /. (2 + 1) & (GoB f) * ((i + 1),(j + 1)) = f /. 2 ) ) by A18, A23, SPPOL_1:8;

thus ( 1 <= 1 & 1 + 1 < len f ) by A17, A23, NAT_1:13; :: thesis: ( f /. (1 + 1) = (GoB f) * (i,(j + 1)) & f /. 1 = (GoB f) * (i,j) & f /. (1 + 2) = (GoB f) * ((i + 1),(j + 1)) )

A26: 3 < len f by Th34, XXREAL_0:2;

then A27: f /. 1 <> f /. 3 by Th36;

A28: LSeg (f,1) = LSeg ((f /. 1),(f /. (1 + 1))) by A11, A22, TOPREAL1:def 3;

then A29: ( ( (GoB f) * (i,j) = f /. 1 & (GoB f) * (i,(j + 1)) = f /. 2 ) or ( (GoB f) * (i,j) = f /. 2 & (GoB f) * (i,(j + 1)) = f /. 1 ) ) by A12, A22, SPPOL_1:8;

hence f /. (1 + 1) = (GoB f) * (i,(j + 1)) by A25, A26, Th36; :: thesis: ( f /. 1 = (GoB f) * (i,j) & f /. (1 + 2) = (GoB f) * ((i + 1),(j + 1)) )

thus f /. 1 = (GoB f) * (i,j) by A18, A23, A29, A24, A27, SPPOL_1:8; :: thesis: f /. (1 + 2) = (GoB f) * ((i + 1),(j + 1))

thus f /. (1 + 2) = (GoB f) * ((i + 1),(j + 1)) by A12, A22, A28, A25, A27, SPPOL_1:8; :: thesis: verum

end;then A25: ( ( (GoB f) * (i,(j + 1)) = f /. 2 & (GoB f) * ((i + 1),(j + 1)) = f /. (2 + 1) ) or ( (GoB f) * (i,(j + 1)) = f /. (2 + 1) & (GoB f) * ((i + 1),(j + 1)) = f /. 2 ) ) by A18, A23, SPPOL_1:8;

thus ( 1 <= 1 & 1 + 1 < len f ) by A17, A23, NAT_1:13; :: thesis: ( f /. (1 + 1) = (GoB f) * (i,(j + 1)) & f /. 1 = (GoB f) * (i,j) & f /. (1 + 2) = (GoB f) * ((i + 1),(j + 1)) )

A26: 3 < len f by Th34, XXREAL_0:2;

then A27: f /. 1 <> f /. 3 by Th36;

A28: LSeg (f,1) = LSeg ((f /. 1),(f /. (1 + 1))) by A11, A22, TOPREAL1:def 3;

then A29: ( ( (GoB f) * (i,j) = f /. 1 & (GoB f) * (i,(j + 1)) = f /. 2 ) or ( (GoB f) * (i,j) = f /. 2 & (GoB f) * (i,(j + 1)) = f /. 1 ) ) by A12, A22, SPPOL_1:8;

hence f /. (1 + 1) = (GoB f) * (i,(j + 1)) by A25, A26, Th36; :: thesis: ( f /. 1 = (GoB f) * (i,j) & f /. (1 + 2) = (GoB f) * ((i + 1),(j + 1)) )

thus f /. 1 = (GoB f) * (i,j) by A18, A23, A29, A24, A27, SPPOL_1:8; :: thesis: f /. (1 + 2) = (GoB f) * ((i + 1),(j + 1))

thus f /. (1 + 2) = (GoB f) * ((i + 1),(j + 1)) by A12, A22, A28, A25, A27, SPPOL_1:8; :: thesis: verum

case that A30:
k1 = 1
and

A31: k2 > 2 ; :: thesis: ( f /. 1 = (GoB f) * (i,(j + 1)) & f /. 2 = (GoB f) * (i,j) & f /. ((len f) -' 1) = (GoB f) * ((i + 1),(j + 1)) )

A31: k2 > 2 ; :: thesis: ( f /. 1 = (GoB f) * (i,(j + 1)) & f /. 2 = (GoB f) * (i,j) & f /. ((len f) -' 1) = (GoB f) * ((i + 1),(j + 1)) )

A32:
LSeg (f,1) = LSeg ((f /. 1),(f /. (1 + 1)))
by A11, A30, TOPREAL1:def 3;

then A33: ( ( (GoB f) * (i,j) = f /. 1 & (GoB f) * (i,(j + 1)) = f /. 2 ) or ( (GoB f) * (i,j) = f /. 2 & (GoB f) * (i,(j + 1)) = f /. 1 ) ) by A12, A30, SPPOL_1:8;

A34: 2 < k2 + 1 by A31, NAT_1:13;

then A35: f /. (k2 + 1) <> f /. 2 by A17, Th37;

LSeg (f,k2) = LSeg ((f /. k2),(f /. (k2 + 1))) by A16, A17, TOPREAL1:def 3;

then A36: ( ( (GoB f) * (i,(j + 1)) = f /. k2 & (GoB f) * ((i + 1),(j + 1)) = f /. (k2 + 1) ) or ( (GoB f) * (i,(j + 1)) = f /. (k2 + 1) & (GoB f) * ((i + 1),(j + 1)) = f /. k2 ) ) by A18, SPPOL_1:8;

A37: f /. k2 <> f /. 2 by A19, A31, Th36;

hence f /. 1 = (GoB f) * (i,(j + 1)) by A12, A30, A32, A36, A35, SPPOL_1:8; :: thesis: ( f /. 2 = (GoB f) * (i,j) & f /. ((len f) -' 1) = (GoB f) * ((i + 1),(j + 1)) )

thus f /. 2 = (GoB f) * (i,j) by A12, A30, A32, A36, A37, A35, SPPOL_1:8; :: thesis: f /. ((len f) -' 1) = (GoB f) * ((i + 1),(j + 1))

A38: k2 > 1 by A31, XXREAL_0:2;

then A39: k2 + 1 > 1 by NAT_1:13;

then k2 + 1 = len f by A17, A19, A31, A33, A36, A38, A34, Th37, Th38;

then k2 + 1 = ((len f) -' 1) + 1 by A39, XREAL_1:235;

hence f /. ((len f) -' 1) = (GoB f) * ((i + 1),(j + 1)) by A19, A31, A33, A36, A38, Th36; :: thesis: verum

end;then A33: ( ( (GoB f) * (i,j) = f /. 1 & (GoB f) * (i,(j + 1)) = f /. 2 ) or ( (GoB f) * (i,j) = f /. 2 & (GoB f) * (i,(j + 1)) = f /. 1 ) ) by A12, A30, SPPOL_1:8;

A34: 2 < k2 + 1 by A31, NAT_1:13;

then A35: f /. (k2 + 1) <> f /. 2 by A17, Th37;

LSeg (f,k2) = LSeg ((f /. k2),(f /. (k2 + 1))) by A16, A17, TOPREAL1:def 3;

then A36: ( ( (GoB f) * (i,(j + 1)) = f /. k2 & (GoB f) * ((i + 1),(j + 1)) = f /. (k2 + 1) ) or ( (GoB f) * (i,(j + 1)) = f /. (k2 + 1) & (GoB f) * ((i + 1),(j + 1)) = f /. k2 ) ) by A18, SPPOL_1:8;

A37: f /. k2 <> f /. 2 by A19, A31, Th36;

hence f /. 1 = (GoB f) * (i,(j + 1)) by A12, A30, A32, A36, A35, SPPOL_1:8; :: thesis: ( f /. 2 = (GoB f) * (i,j) & f /. ((len f) -' 1) = (GoB f) * ((i + 1),(j + 1)) )

thus f /. 2 = (GoB f) * (i,j) by A12, A30, A32, A36, A37, A35, SPPOL_1:8; :: thesis: f /. ((len f) -' 1) = (GoB f) * ((i + 1),(j + 1))

A38: k2 > 1 by A31, XXREAL_0:2;

then A39: k2 + 1 > 1 by NAT_1:13;

then k2 + 1 = len f by A17, A19, A31, A33, A36, A38, A34, Th37, Th38;

then k2 + 1 = ((len f) -' 1) + 1 by A39, XREAL_1:235;

hence f /. ((len f) -' 1) = (GoB f) * ((i + 1),(j + 1)) by A19, A31, A33, A36, A38, Th36; :: thesis: verum

case that A40:
k2 = 1
and

A41: k1 = 2 ; :: thesis: ( 1 <= 1 & 1 + 1 < len f & f /. (1 + 1) = (GoB f) * (i,(j + 1)) & f /. 1 = (GoB f) * ((i + 1),(j + 1)) & f /. (1 + 2) = (GoB f) * (i,j) )

A41: k1 = 2 ; :: thesis: ( 1 <= 1 & 1 + 1 < len f & f /. (1 + 1) = (GoB f) * (i,(j + 1)) & f /. 1 = (GoB f) * ((i + 1),(j + 1)) & f /. (1 + 2) = (GoB f) * (i,j) )

A42:
LSeg (f,2) = LSeg ((f /. 2),(f /. (2 + 1)))
by A11, A41, TOPREAL1:def 3;

then A43: ( ( (GoB f) * (i,(j + 1)) = f /. 2 & (GoB f) * (i,j) = f /. (2 + 1) ) or ( (GoB f) * (i,(j + 1)) = f /. (2 + 1) & (GoB f) * (i,j) = f /. 2 ) ) by A12, A41, SPPOL_1:8;

thus ( 1 <= 1 & 1 + 1 < len f ) by A11, A41, NAT_1:13; :: thesis: ( f /. (1 + 1) = (GoB f) * (i,(j + 1)) & f /. 1 = (GoB f) * ((i + 1),(j + 1)) & f /. (1 + 2) = (GoB f) * (i,j) )

A44: 3 < len f by Th34, XXREAL_0:2;

then A45: f /. 1 <> f /. 3 by Th36;

A46: LSeg (f,1) = LSeg ((f /. 1),(f /. (1 + 1))) by A17, A40, TOPREAL1:def 3;

then A47: ( ( (GoB f) * ((i + 1),(j + 1)) = f /. 1 & (GoB f) * (i,(j + 1)) = f /. 2 ) or ( (GoB f) * ((i + 1),(j + 1)) = f /. 2 & (GoB f) * (i,(j + 1)) = f /. 1 ) ) by A18, A40, SPPOL_1:8;

hence f /. (1 + 1) = (GoB f) * (i,(j + 1)) by A43, A44, Th36; :: thesis: ( f /. 1 = (GoB f) * ((i + 1),(j + 1)) & f /. (1 + 2) = (GoB f) * (i,j) )

thus f /. 1 = (GoB f) * ((i + 1),(j + 1)) by A12, A41, A47, A42, A45, SPPOL_1:8; :: thesis: f /. (1 + 2) = (GoB f) * (i,j)

thus f /. (1 + 2) = (GoB f) * (i,j) by A18, A40, A46, A43, A45, SPPOL_1:8; :: thesis: verum

end;then A43: ( ( (GoB f) * (i,(j + 1)) = f /. 2 & (GoB f) * (i,j) = f /. (2 + 1) ) or ( (GoB f) * (i,(j + 1)) = f /. (2 + 1) & (GoB f) * (i,j) = f /. 2 ) ) by A12, A41, SPPOL_1:8;

thus ( 1 <= 1 & 1 + 1 < len f ) by A11, A41, NAT_1:13; :: thesis: ( f /. (1 + 1) = (GoB f) * (i,(j + 1)) & f /. 1 = (GoB f) * ((i + 1),(j + 1)) & f /. (1 + 2) = (GoB f) * (i,j) )

A44: 3 < len f by Th34, XXREAL_0:2;

then A45: f /. 1 <> f /. 3 by Th36;

A46: LSeg (f,1) = LSeg ((f /. 1),(f /. (1 + 1))) by A17, A40, TOPREAL1:def 3;

then A47: ( ( (GoB f) * ((i + 1),(j + 1)) = f /. 1 & (GoB f) * (i,(j + 1)) = f /. 2 ) or ( (GoB f) * ((i + 1),(j + 1)) = f /. 2 & (GoB f) * (i,(j + 1)) = f /. 1 ) ) by A18, A40, SPPOL_1:8;

hence f /. (1 + 1) = (GoB f) * (i,(j + 1)) by A43, A44, Th36; :: thesis: ( f /. 1 = (GoB f) * ((i + 1),(j + 1)) & f /. (1 + 2) = (GoB f) * (i,j) )

thus f /. 1 = (GoB f) * ((i + 1),(j + 1)) by A12, A41, A47, A42, A45, SPPOL_1:8; :: thesis: f /. (1 + 2) = (GoB f) * (i,j)

thus f /. (1 + 2) = (GoB f) * (i,j) by A18, A40, A46, A43, A45, SPPOL_1:8; :: thesis: verum

case that A48:
k2 = 1
and

A49: k1 > 2 ; :: thesis: ( f /. 1 = (GoB f) * (i,(j + 1)) & f /. 2 = (GoB f) * ((i + 1),(j + 1)) & f /. ((len f) -' 1) = (GoB f) * (i,j) )

A49: k1 > 2 ; :: thesis: ( f /. 1 = (GoB f) * (i,(j + 1)) & f /. 2 = (GoB f) * ((i + 1),(j + 1)) & f /. ((len f) -' 1) = (GoB f) * (i,j) )

A50:
LSeg (f,1) = LSeg ((f /. 1),(f /. (1 + 1)))
by A17, A48, TOPREAL1:def 3;

then A51: ( ( (GoB f) * ((i + 1),(j + 1)) = f /. 1 & (GoB f) * (i,(j + 1)) = f /. 2 ) or ( (GoB f) * ((i + 1),(j + 1)) = f /. 2 & (GoB f) * (i,(j + 1)) = f /. 1 ) ) by A18, A48, SPPOL_1:8;

A52: 2 < k1 + 1 by A49, NAT_1:13;

then A53: f /. (k1 + 1) <> f /. 2 by A11, Th37;

LSeg (f,k1) = LSeg ((f /. k1),(f /. (k1 + 1))) by A10, A11, TOPREAL1:def 3;

then A54: ( ( (GoB f) * (i,(j + 1)) = f /. k1 & (GoB f) * (i,j) = f /. (k1 + 1) ) or ( (GoB f) * (i,(j + 1)) = f /. (k1 + 1) & (GoB f) * (i,j) = f /. k1 ) ) by A12, SPPOL_1:8;

A55: f /. k1 <> f /. 2 by A13, A49, Th36;

hence f /. 1 = (GoB f) * (i,(j + 1)) by A18, A48, A50, A54, A53, SPPOL_1:8; :: thesis: ( f /. 2 = (GoB f) * ((i + 1),(j + 1)) & f /. ((len f) -' 1) = (GoB f) * (i,j) )

thus f /. 2 = (GoB f) * ((i + 1),(j + 1)) by A18, A48, A50, A54, A55, A53, SPPOL_1:8; :: thesis: f /. ((len f) -' 1) = (GoB f) * (i,j)

A56: k1 > 1 by A49, XXREAL_0:2;

then A57: k1 + 1 > 1 by NAT_1:13;

then k1 + 1 = len f by A11, A13, A49, A51, A54, A56, A52, Th37, Th38;

then k1 + 1 = ((len f) -' 1) + 1 by A57, XREAL_1:235;

hence f /. ((len f) -' 1) = (GoB f) * (i,j) by A13, A49, A51, A54, A56, Th36; :: thesis: verum

end;then A51: ( ( (GoB f) * ((i + 1),(j + 1)) = f /. 1 & (GoB f) * (i,(j + 1)) = f /. 2 ) or ( (GoB f) * ((i + 1),(j + 1)) = f /. 2 & (GoB f) * (i,(j + 1)) = f /. 1 ) ) by A18, A48, SPPOL_1:8;

A52: 2 < k1 + 1 by A49, NAT_1:13;

then A53: f /. (k1 + 1) <> f /. 2 by A11, Th37;

LSeg (f,k1) = LSeg ((f /. k1),(f /. (k1 + 1))) by A10, A11, TOPREAL1:def 3;

then A54: ( ( (GoB f) * (i,(j + 1)) = f /. k1 & (GoB f) * (i,j) = f /. (k1 + 1) ) or ( (GoB f) * (i,(j + 1)) = f /. (k1 + 1) & (GoB f) * (i,j) = f /. k1 ) ) by A12, SPPOL_1:8;

A55: f /. k1 <> f /. 2 by A13, A49, Th36;

hence f /. 1 = (GoB f) * (i,(j + 1)) by A18, A48, A50, A54, A53, SPPOL_1:8; :: thesis: ( f /. 2 = (GoB f) * ((i + 1),(j + 1)) & f /. ((len f) -' 1) = (GoB f) * (i,j) )

thus f /. 2 = (GoB f) * ((i + 1),(j + 1)) by A18, A48, A50, A54, A55, A53, SPPOL_1:8; :: thesis: f /. ((len f) -' 1) = (GoB f) * (i,j)

A56: k1 > 1 by A49, XXREAL_0:2;

then A57: k1 + 1 > 1 by NAT_1:13;

then k1 + 1 = len f by A11, A13, A49, A51, A54, A56, A52, Th37, Th38;

then k1 + 1 = ((len f) -' 1) + 1 by A57, XREAL_1:235;

hence f /. ((len f) -' 1) = (GoB f) * (i,j) by A13, A49, A51, A54, A56, Th36; :: thesis: verum

case
k1 = k2
; :: thesis: contradiction

then A58:
( (GoB f) * (i,j) = (GoB f) * ((i + 1),(j + 1)) or (GoB f) * (i,j) = (GoB f) * (i,(j + 1)) )
by A12, A18, SPPOL_1:8;

A59: [(i + 1),(j + 1)] in Indices (GoB f) by A2, A4, A15, A9, MATRIX_0:30;

( [i,j] in Indices (GoB f) & [i,(j + 1)] in Indices (GoB f) ) by A1, A3, A4, A15, A8, A7, MATRIX_0:30;

then j = j + 1 by A58, A59, GOBOARD1:5;

hence contradiction ; :: thesis: verum

end;A59: [(i + 1),(j + 1)] in Indices (GoB f) by A2, A4, A15, A9, MATRIX_0:30;

( [i,j] in Indices (GoB f) & [i,(j + 1)] in Indices (GoB f) ) by A1, A3, A4, A15, A8, A7, MATRIX_0:30;

then j = j + 1 by A58, A59, GOBOARD1:5;

hence contradiction ; :: thesis: verum

case that A60:
k1 > 1
and

A61: k2 > k1 ; :: thesis: ( 1 <= k1 & k1 + 1 < len f & f /. (k1 + 1) = (GoB f) * (i,(j + 1)) & f /. k1 = (GoB f) * (i,j) & f /. (k1 + 2) = (GoB f) * ((i + 1),(j + 1)) )

A61: k2 > k1 ; :: thesis: ( 1 <= k1 & k1 + 1 < len f & f /. (k1 + 1) = (GoB f) * (i,(j + 1)) & f /. k1 = (GoB f) * (i,j) & f /. (k1 + 2) = (GoB f) * ((i + 1),(j + 1)) )

A62:
( 1 < k1 + 1 & k1 + 1 < k2 + 1 )
by A60, A61, NAT_1:13, XREAL_1:6;

A63: k1 < k2 + 1 by A61, NAT_1:13;

then A64: f /. k1 <> f /. (k2 + 1) by A17, A60, Th37;

A65: k1 + 1 <= k2 by A61, NAT_1:13;

LSeg (f,k2) = LSeg ((f /. k2),(f /. (k2 + 1))) by A16, A17, TOPREAL1:def 3;

then A66: ( ( (GoB f) * (i,(j + 1)) = f /. k2 & (GoB f) * ((i + 1),(j + 1)) = f /. (k2 + 1) ) or ( (GoB f) * (i,(j + 1)) = f /. (k2 + 1) & (GoB f) * ((i + 1),(j + 1)) = f /. k2 ) ) by A18, SPPOL_1:8;

A67: k2 < len f by A17, NAT_1:13;

then A68: f /. k1 <> f /. k2 by A60, A61, Th37;

A69: LSeg (f,k1) = LSeg ((f /. k1),(f /. (k1 + 1))) by A10, A11, TOPREAL1:def 3;

then ( ( (GoB f) * (i,j) = f /. k1 & (GoB f) * (i,(j + 1)) = f /. (k1 + 1) ) or ( (GoB f) * (i,j) = f /. (k1 + 1) & (GoB f) * (i,(j + 1)) = f /. k1 ) ) by A12, SPPOL_1:8;

then k1 + 1 >= k2 by A17, A60, A61, A66, A63, A67, A62, Th37;

then A70: k1 + 1 = k2 by A65, XXREAL_0:1;

hence ( 1 <= k1 & k1 + 1 < len f ) by A17, A60, NAT_1:13; :: thesis: ( f /. (k1 + 1) = (GoB f) * (i,(j + 1)) & f /. k1 = (GoB f) * (i,j) & f /. (k1 + 2) = (GoB f) * ((i + 1),(j + 1)) )

thus f /. (k1 + 1) = (GoB f) * (i,(j + 1)) by A12, A69, A66, A64, A68, SPPOL_1:8; :: thesis: ( f /. k1 = (GoB f) * (i,j) & f /. (k1 + 2) = (GoB f) * ((i + 1),(j + 1)) )

thus f /. k1 = (GoB f) * (i,j) by A12, A69, A66, A64, A68, SPPOL_1:8; :: thesis: f /. (k1 + 2) = (GoB f) * ((i + 1),(j + 1))

thus f /. (k1 + 2) = (GoB f) * ((i + 1),(j + 1)) by A12, A69, A66, A64, A70, SPPOL_1:8; :: thesis: verum

end;A63: k1 < k2 + 1 by A61, NAT_1:13;

then A64: f /. k1 <> f /. (k2 + 1) by A17, A60, Th37;

A65: k1 + 1 <= k2 by A61, NAT_1:13;

LSeg (f,k2) = LSeg ((f /. k2),(f /. (k2 + 1))) by A16, A17, TOPREAL1:def 3;

then A66: ( ( (GoB f) * (i,(j + 1)) = f /. k2 & (GoB f) * ((i + 1),(j + 1)) = f /. (k2 + 1) ) or ( (GoB f) * (i,(j + 1)) = f /. (k2 + 1) & (GoB f) * ((i + 1),(j + 1)) = f /. k2 ) ) by A18, SPPOL_1:8;

A67: k2 < len f by A17, NAT_1:13;

then A68: f /. k1 <> f /. k2 by A60, A61, Th37;

A69: LSeg (f,k1) = LSeg ((f /. k1),(f /. (k1 + 1))) by A10, A11, TOPREAL1:def 3;

then ( ( (GoB f) * (i,j) = f /. k1 & (GoB f) * (i,(j + 1)) = f /. (k1 + 1) ) or ( (GoB f) * (i,j) = f /. (k1 + 1) & (GoB f) * (i,(j + 1)) = f /. k1 ) ) by A12, SPPOL_1:8;

then k1 + 1 >= k2 by A17, A60, A61, A66, A63, A67, A62, Th37;

then A70: k1 + 1 = k2 by A65, XXREAL_0:1;

hence ( 1 <= k1 & k1 + 1 < len f ) by A17, A60, NAT_1:13; :: thesis: ( f /. (k1 + 1) = (GoB f) * (i,(j + 1)) & f /. k1 = (GoB f) * (i,j) & f /. (k1 + 2) = (GoB f) * ((i + 1),(j + 1)) )

thus f /. (k1 + 1) = (GoB f) * (i,(j + 1)) by A12, A69, A66, A64, A68, SPPOL_1:8; :: thesis: ( f /. k1 = (GoB f) * (i,j) & f /. (k1 + 2) = (GoB f) * ((i + 1),(j + 1)) )

thus f /. k1 = (GoB f) * (i,j) by A12, A69, A66, A64, A68, SPPOL_1:8; :: thesis: f /. (k1 + 2) = (GoB f) * ((i + 1),(j + 1))

thus f /. (k1 + 2) = (GoB f) * ((i + 1),(j + 1)) by A12, A69, A66, A64, A70, SPPOL_1:8; :: thesis: verum

case that A71:
k2 > 1
and

A72: k1 > k2 ; :: thesis: ( 1 <= k2 & k2 + 1 < len f & f /. (k2 + 1) = (GoB f) * (i,(j + 1)) & f /. k2 = (GoB f) * ((i + 1),(j + 1)) & f /. (k2 + 2) = (GoB f) * (i,j) )

A72: k1 > k2 ; :: thesis: ( 1 <= k2 & k2 + 1 < len f & f /. (k2 + 1) = (GoB f) * (i,(j + 1)) & f /. k2 = (GoB f) * ((i + 1),(j + 1)) & f /. (k2 + 2) = (GoB f) * (i,j) )

A73:
( 1 < k2 + 1 & k2 + 1 < k1 + 1 )
by A71, A72, NAT_1:13, XREAL_1:6;

A74: k2 < k1 + 1 by A72, NAT_1:13;

then A75: f /. k2 <> f /. (k1 + 1) by A11, A71, Th37;

A76: k2 + 1 <= k1 by A72, NAT_1:13;

LSeg (f,k1) = LSeg ((f /. k1),(f /. (k1 + 1))) by A10, A11, TOPREAL1:def 3;

then A77: ( ( (GoB f) * (i,(j + 1)) = f /. k1 & (GoB f) * (i,j) = f /. (k1 + 1) ) or ( (GoB f) * (i,(j + 1)) = f /. (k1 + 1) & (GoB f) * (i,j) = f /. k1 ) ) by A12, SPPOL_1:8;

A78: k1 < len f by A11, NAT_1:13;

then A79: f /. k2 <> f /. k1 by A71, A72, Th37;

A80: LSeg (f,k2) = LSeg ((f /. k2),(f /. (k2 + 1))) by A16, A17, TOPREAL1:def 3;

then ( ( (GoB f) * ((i + 1),(j + 1)) = f /. k2 & (GoB f) * (i,(j + 1)) = f /. (k2 + 1) ) or ( (GoB f) * ((i + 1),(j + 1)) = f /. (k2 + 1) & (GoB f) * (i,(j + 1)) = f /. k2 ) ) by A18, SPPOL_1:8;

then k2 + 1 >= k1 by A11, A71, A72, A77, A74, A78, A73, Th37;

then A81: k2 + 1 = k1 by A76, XXREAL_0:1;

hence ( 1 <= k2 & k2 + 1 < len f ) by A11, A71, NAT_1:13; :: thesis: ( f /. (k2 + 1) = (GoB f) * (i,(j + 1)) & f /. k2 = (GoB f) * ((i + 1),(j + 1)) & f /. (k2 + 2) = (GoB f) * (i,j) )

thus f /. (k2 + 1) = (GoB f) * (i,(j + 1)) by A18, A80, A77, A75, A79, SPPOL_1:8; :: thesis: ( f /. k2 = (GoB f) * ((i + 1),(j + 1)) & f /. (k2 + 2) = (GoB f) * (i,j) )

thus f /. k2 = (GoB f) * ((i + 1),(j + 1)) by A18, A80, A77, A75, A79, SPPOL_1:8; :: thesis: f /. (k2 + 2) = (GoB f) * (i,j)

thus f /. (k2 + 2) = (GoB f) * (i,j) by A18, A80, A77, A75, A81, SPPOL_1:8; :: thesis: verum

end;A74: k2 < k1 + 1 by A72, NAT_1:13;

then A75: f /. k2 <> f /. (k1 + 1) by A11, A71, Th37;

A76: k2 + 1 <= k1 by A72, NAT_1:13;

LSeg (f,k1) = LSeg ((f /. k1),(f /. (k1 + 1))) by A10, A11, TOPREAL1:def 3;

then A77: ( ( (GoB f) * (i,(j + 1)) = f /. k1 & (GoB f) * (i,j) = f /. (k1 + 1) ) or ( (GoB f) * (i,(j + 1)) = f /. (k1 + 1) & (GoB f) * (i,j) = f /. k1 ) ) by A12, SPPOL_1:8;

A78: k1 < len f by A11, NAT_1:13;

then A79: f /. k2 <> f /. k1 by A71, A72, Th37;

A80: LSeg (f,k2) = LSeg ((f /. k2),(f /. (k2 + 1))) by A16, A17, TOPREAL1:def 3;

then ( ( (GoB f) * ((i + 1),(j + 1)) = f /. k2 & (GoB f) * (i,(j + 1)) = f /. (k2 + 1) ) or ( (GoB f) * ((i + 1),(j + 1)) = f /. (k2 + 1) & (GoB f) * (i,(j + 1)) = f /. k2 ) ) by A18, SPPOL_1:8;

then k2 + 1 >= k1 by A11, A71, A72, A77, A74, A78, A73, Th37;

then A81: k2 + 1 = k1 by A76, XXREAL_0:1;

hence ( 1 <= k2 & k2 + 1 < len f ) by A11, A71, NAT_1:13; :: thesis: ( f /. (k2 + 1) = (GoB f) * (i,(j + 1)) & f /. k2 = (GoB f) * ((i + 1),(j + 1)) & f /. (k2 + 2) = (GoB f) * (i,j) )

thus f /. (k2 + 1) = (GoB f) * (i,(j + 1)) by A18, A80, A77, A75, A79, SPPOL_1:8; :: thesis: ( f /. k2 = (GoB f) * ((i + 1),(j + 1)) & f /. (k2 + 2) = (GoB f) * (i,j) )

thus f /. k2 = (GoB f) * ((i + 1),(j + 1)) by A18, A80, A77, A75, A79, SPPOL_1:8; :: thesis: f /. (k2 + 2) = (GoB f) * (i,j)

thus f /. (k2 + 2) = (GoB f) * (i,j) by A18, A80, A77, A75, A81, SPPOL_1:8; :: thesis: verum

( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * (i,(j + 1)) & ( ( f /. k = (GoB f) * (i,j) & f /. (k + 2) = (GoB f) * ((i + 1),(j + 1)) ) or ( f /. k = (GoB f) * ((i + 1),(j + 1)) & f /. (k + 2) = (GoB f) * (i,j) ) ) ) ) ; :: thesis: verum