let t be Nat; for G being Go-board
for f being non constant standard special_circular_sequence st f is_sequence_on G & 1 <= t & t <= len G holds
(G * (t,(width G))) `2 >= N-bound (L~ f)
let G be Go-board; for f being non constant standard special_circular_sequence st f is_sequence_on G & 1 <= t & t <= len G holds
(G * (t,(width G))) `2 >= N-bound (L~ f)
let f be non constant standard special_circular_sequence; ( f is_sequence_on G & 1 <= t & t <= len G implies (G * (t,(width G))) `2 >= N-bound (L~ f) )
N-min (L~ f) in rng f
by SPRECT_2:39;
then consider x being object such that
A1:
x in dom f
and
A2:
f . x = N-min (L~ f)
by FUNCT_1:def 3;
reconsider x = x as Nat by A1;
assume
f is_sequence_on G
; ( not 1 <= t or not t <= len G or (G * (t,(width G))) `2 >= N-bound (L~ f) )
then consider i, j being Nat such that
A3:
[i,j] in Indices G
and
A4:
f /. x = G * (i,j)
by A1, GOBOARD1:def 9;
A5:
( 1 <= i & i <= len G )
by A3, MATRIX_0:32;
assume A6:
( 1 <= t & t <= len G )
; (G * (t,(width G))) `2 >= N-bound (L~ f)
( 1 <= j & j <= width G )
by A3, MATRIX_0:32;
then
( N-bound (L~ f) = (N-min (L~ f)) `2 & (G * (t,(width G))) `2 >= (G * (i,j)) `2 )
by A6, A5, Th19, EUCLID:52;
hence
(G * (t,(width G))) `2 >= N-bound (L~ f)
by A1, A2, A4, PARTFUN1:def 6; verum