let h be non constant standard special_circular_sequence; :: thesis: for i, I being Element of NAT st 1 <= i & i <= len h & 1 <= I & I <= len (GoB h) holds
( ((GoB h) * I,1) `2 <= (h /. i) `2 & (h /. i) `2 <= ((GoB h) * I,(width (GoB h))) `2 )
let i, I be Element of NAT ; :: thesis: ( 1 <= i & i <= len h & 1 <= I & I <= len (GoB h) implies ( ((GoB h) * I,1) `2 <= (h /. i) `2 & (h /. i) `2 <= ((GoB h) * I,(width (GoB h))) `2 ) )
assume A1: ( 1 <= i & i <= len h & 1 <= I & I <= len (GoB h) ) ; :: thesis: ( ((GoB h) * I,1) `2 <= (h /. i) `2 & (h /. i) `2 <= ((GoB h) * I,(width (GoB h))) `2 )
A2: GoB h = GoB (Incr (X_axis h)),(Incr (Y_axis h)) by GOBOARD2:def 3;
A3: ( 1 <= I & I <= len (GoB (Incr (X_axis h)),(Incr (Y_axis h))) ) by A1, GOBOARD2:def 3;
A4: 1 <= width (GoB h) by GOBOARD7:35;
( width (GoB h) <= width (GoB (Incr (X_axis h)),(Incr (Y_axis h))) & 1 <= width (GoB (Incr (X_axis h)),(Incr (Y_axis h))) ) by A2, GOBOARD7:35;
then A5: [I,1] in Indices (GoB (Incr (X_axis h)),(Incr (Y_axis h))) by A3, MATRIX_1:37;
A6: [I,(width (GoB h))] in Indices (GoB (Incr (X_axis h)),(Incr (Y_axis h))) by A1, A2, A4, MATRIX_1:37;
(GoB h) * I,(width (GoB h)) = (GoB (Incr (X_axis h)),(Incr (Y_axis h))) * I,(width (GoB h)) by GOBOARD2:def 3
.= |[((Incr (X_axis h)) . I),((Incr (Y_axis h)) . (width (GoB h)))]| by A6, GOBOARD2:def 1 ;
then A7: ((GoB h) * I,(width (GoB h))) `2 = (Incr (Y_axis h)) . (width (GoB h)) by EUCLID:56;
(GoB h) * I,1 = (GoB (Incr (X_axis h)),(Incr (Y_axis h))) * I,1 by GOBOARD2:def 3
.= |[((Incr (X_axis h)) . I),((Incr (Y_axis h)) . 1)]| by A5, GOBOARD2:def 1 ;
then A8: ((GoB h) * I,1) `2 = (Incr (Y_axis h)) . 1 by EUCLID:56;
A9: width (GoB h) = len (Incr (Y_axis h)) by A2, GOBOARD2:def 1;
i <= len (Y_axis h) by A1, GOBOARD1:def 4;
then A10: i in dom (Y_axis h) by A1, FINSEQ_3:27;
then (Y_axis h) . i = (h /. i) `2 by GOBOARD1:def 4;
then (h /. i) `2 in rng (Y_axis h) by A10, FUNCT_1:def 5;
hence ( ((GoB h) * I,1) `2 <= (h /. i) `2 & (h /. i) `2 <= ((GoB h) * I,(width (GoB h))) `2 ) by A7, A8, A9, Th6; :: thesis: verum