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