let t be Nat; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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 ) ; :: thesis: (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; :: thesis: verum