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 <= 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) )
W-min (L~ f) in rng f by SPRECT_2:43;
then consider x being object such that
A1: x in dom f and
A2: f . x = W-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 <= width G or (G * (1,t)) `1 <= W-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 <= width G ) ; :: thesis: (G * (1,t)) `1 <= W-bound (L~ f)
( 1 <= j & j <= width G ) by A3, MATRIX_0:32;
then ( W-bound (L~ f) = (W-min (L~ f)) `1 & (G * (1,t)) `1 <= (G * (i,j)) `1 ) by A6, A5, Th18, EUCLID:52;
hence (G * (1,t)) `1 <= W-bound (L~ f) by A1, A2, A4, PARTFUN1:def 6; :: thesis: verum