let t be Element of 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 <= width G holds
(G * 1,t) `1 <= W-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 <= width G holds
(G * 1,t) `1 <= W-bound (L~ f)
let f be non constant standard special_circular_sequence; :: thesis: ( f is_sequence_on G & 1 <= t & t <= width G implies (G * 1,t) `1 <= W-bound (L~ f) )
assume A1: f is_sequence_on G ; :: thesis: ( not 1 <= t or not t <= width G or (G * 1,t) `1 <= W-bound (L~ f) )
assume A2: ( 1 <= t & t <= width G ) ; :: thesis: (G * 1,t) `1 <= W-bound (L~ f)
A3: W-bound (L~ f) = (W-min (L~ f)) `1 by EUCLID:56;
W-min (L~ f) in rng f by SPRECT_2:47;
then consider x being set such that
A4: x in dom f and
A5: f . x = W-min (L~ f) by FUNCT_1:def 5;
reconsider x = x as Element of NAT by A4;
consider i, j being Element of NAT such that
A6: [i,j] in Indices G and
A7: f /. x = G * i,j by A1, A4, GOBOARD1:def 11;
( 1 <= j & j <= width G & 1 <= i & i <= len G ) by A6, MATRIX_1:39;
then (G * 1,t) `1 <= (G * i,j) `1 by A2, Th39;
hence (G * 1,t) `1 <= W-bound (L~ f) by A3, A4, A5, A7, PARTFUN1:def 8; :: thesis: verum