let i, j be Nat; for f being V8() standard special_circular_sequence st 1 <= i & i + 1 <= len (GoB f) & 1 <= j & j <= width (GoB f) & (1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),j))) in L~ f holds
ex k being Nat st
( 1 <= k & k + 1 <= len f & LSeg (((GoB f) * (i,j)),((GoB f) * ((i + 1),j))) = LSeg (f,k) )
let f be V8() standard special_circular_sequence; ( 1 <= i & i + 1 <= len (GoB f) & 1 <= j & j <= width (GoB f) & (1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),j))) in L~ f implies ex k being Nat st
( 1 <= k & k + 1 <= len f & LSeg (((GoB f) * (i,j)),((GoB f) * ((i + 1),j))) = LSeg (f,k) ) )
set mi = (1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),j)));
assume that
A1:
( 1 <= i & i + 1 <= len (GoB f) & 1 <= j & j <= width (GoB f) )
and
A2:
(1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),j))) in L~ f
; ex k being Nat st
( 1 <= k & k + 1 <= len f & LSeg (((GoB f) * (i,j)),((GoB f) * ((i + 1),j))) = LSeg (f,k) )
L~ f = union { (LSeg (f,k)) where k is Nat : ( 1 <= k & k + 1 <= len f ) }
by TOPREAL1:def 4;
then consider x being set such that
A3:
(1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),j))) in x
and
A4:
x in { (LSeg (f,k)) where k is Nat : ( 1 <= k & k + 1 <= len f ) }
by A2, TARSKI:def 4;
consider k being Nat such that
A5:
x = LSeg (f,k)
and
A6:
1 <= k
and
A7:
k + 1 <= len f
by A4;
A8:
f is_sequence_on GoB f
by GOBOARD5:def 5;
A9:
(1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),j))) in LSeg ((f /. k),(f /. (k + 1)))
by A3, A5, A6, A7, TOPREAL1:def 3;
k <= k + 1
by NAT_1:11;
then
k <= len f
by A7, XXREAL_0:2;
then A10:
k in dom f
by A6, FINSEQ_3:25;
then consider i1, j1 being Nat such that
A11:
[i1,j1] in Indices (GoB f)
and
A12:
f /. k = (GoB f) * (i1,j1)
by A8, GOBOARD1:def 9;
A13:
1 <= j1
by A11, MATRIX_0:32;
take
k
; ( 1 <= k & k + 1 <= len f & LSeg (((GoB f) * (i,j)),((GoB f) * ((i + 1),j))) = LSeg (f,k) )
thus
( 1 <= k & k + 1 <= len f )
by A6, A7; LSeg (((GoB f) * (i,j)),((GoB f) * ((i + 1),j))) = LSeg (f,k)
1 <= k + 1
by NAT_1:11;
then A14:
k + 1 in dom f
by A7, FINSEQ_3:25;
then consider i2, j2 being Nat such that
A15:
[i2,j2] in Indices (GoB f)
and
A16:
f /. (k + 1) = (GoB f) * (i2,j2)
by A8, GOBOARD1:def 9;
A17:
1 <= j2
by A15, MATRIX_0:32;
A18:
i2 <= len (GoB f)
by A15, MATRIX_0:32;
|.(j1 - j2).| + |.(i1 - i2).| = 1
by A8, A10, A11, A12, A14, A15, A16, GOBOARD1:def 9;
then A19:
( ( |.(j1 - j2).| = 1 & i1 = i2 ) or ( |.(i1 - i2).| = 1 & j1 = j2 ) )
by SEQM_3:42;
A20:
j1 <= width (GoB f)
by A11, MATRIX_0:32;
A21:
i1 <= len (GoB f)
by A11, MATRIX_0:32;
A22:
1 <= i1
by A11, MATRIX_0:32;
A23:
j2 <= width (GoB f)
by A15, MATRIX_0:32;
A24:
1 <= i2
by A15, MATRIX_0:32;
per cases
( ( i1 = i2 & j1 = j2 + 1 ) or ( i1 = i2 & j1 + 1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) )
by A19, SEQM_3:41;
suppose A25:
(
i1 = i2 &
j1 = j2 + 1 )
;
LSeg (((GoB f) * (i,j)),((GoB f) * ((i + 1),j))) = LSeg (f,k)then
(1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),j))) in LSeg (
((GoB f) * (i2,j2)),
((GoB f) * (i2,(j2 + 1))))
by A3, A5, A6, A7, A12, A16, TOPREAL1:def 3;
hence
LSeg (
((GoB f) * (i,j)),
((GoB f) * ((i + 1),j)))
= LSeg (
f,
k)
by A1, A20, A17, A24, A18, A25, Th27;
verum end; suppose A26:
(
i1 = i2 &
j1 + 1
= j2 )
;
LSeg (((GoB f) * (i,j)),((GoB f) * ((i + 1),j))) = LSeg (f,k)then
(1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),j))) in LSeg (
((GoB f) * (i1,j1)),
((GoB f) * (i1,(j1 + 1))))
by A3, A5, A6, A7, A12, A16, TOPREAL1:def 3;
hence
LSeg (
((GoB f) * (i,j)),
((GoB f) * ((i + 1),j)))
= LSeg (
f,
k)
by A1, A13, A22, A21, A23, A26, Th27;
verum end; suppose A27:
(
i1 = i2 + 1 &
j1 = j2 )
;
LSeg (((GoB f) * (i,j)),((GoB f) * ((i + 1),j))) = LSeg (f,k)then
(
j = j2 &
i = i2 )
by A1, A12, A16, A13, A20, A21, A24, A9, Th26;
hence
LSeg (
((GoB f) * (i,j)),
((GoB f) * ((i + 1),j)))
= LSeg (
f,
k)
by A6, A7, A12, A16, A27, TOPREAL1:def 3;
verum end; suppose A28:
(
i1 + 1
= i2 &
j1 = j2 )
;
LSeg (((GoB f) * (i,j)),((GoB f) * ((i + 1),j))) = LSeg (f,k)then
(
j = j1 &
i = i1 )
by A1, A12, A16, A13, A20, A22, A18, A9, Th26;
hence
LSeg (
((GoB f) * (i,j)),
((GoB f) * ((i + 1),j)))
= LSeg (
f,
k)
by A6, A7, A12, A16, A28, TOPREAL1:def 3;
verum end; end;