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 that
A1: 1 <= i and
A2: i <= len h and
A3: 1 <= I and
A4: I <= len (GoB h) ; :: thesis: ( ((GoB h) * I,1) `2 <= (h /. i) `2 & (h /. i) `2 <= ((GoB h) * I,(width (GoB h))) `2 )
A5: GoB h = GoB (Incr (X_axis h)),(Incr (Y_axis h)) by GOBOARD2:def 3;
then A6: 1 <= width (GoB (Incr (X_axis h)),(Incr (Y_axis h))) by GOBOARD7:35;
i <= len (Y_axis h) by A2, GOBOARD1:def 4;
then A7: i in dom (Y_axis h) by A1, FINSEQ_3:27;
then (Y_axis h) . i = (h /. i) `2 by GOBOARD1:def 4;
then A8: (h /. i) `2 in rng (Y_axis h) by A7, FUNCT_1:def 5;
1 <= width (GoB h) by GOBOARD7:35;
then A9: [I,(width (GoB h))] in Indices (GoB (Incr (X_axis h)),(Incr (Y_axis h))) by A3, A4, A5, 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 A9, GOBOARD2:def 1 ;
then A10: ((GoB h) * I,(width (GoB h))) `2 = (Incr (Y_axis h)) . (width (GoB h)) by EUCLID:56;
I <= len (GoB (Incr (X_axis h)),(Incr (Y_axis h))) by A4, GOBOARD2:def 3;
then A11: [I,1] in Indices (GoB (Incr (X_axis h)),(Incr (Y_axis h))) by A3, A6, MATRIX_1:37;
(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 A11, GOBOARD2:def 1 ;
then A12: ((GoB h) * I,1) `2 = (Incr (Y_axis h)) . 1 by EUCLID:56;
width (GoB h) = len (Incr (Y_axis h)) by A5, GOBOARD2:def 1;
hence ( ((GoB h) * I,1) `2 <= (h /. i) `2 & (h /. i) `2 <= ((GoB h) * I,(width (GoB h))) `2 ) by A10, A12, A8, Th6; :: thesis: verum