let h be non constant standard special_circular_sequence; :: thesis: for I, i being 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 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 2;
then A6: 1 <= width (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) by GOBOARD7:33;
i <= len (Y_axis h) by A2, GOBOARD1:def 2;
then A7: i in dom (Y_axis h) by A1, FINSEQ_3:25;
then (Y_axis h) . i = (h /. i) `2 by GOBOARD1:def 2;
then A8: (h /. i) `2 in rng (Y_axis h) by A7, FUNCT_1:def 3;
1 <= width (GoB h) by GOBOARD7:33;
then A9: [I,(width (GoB h))] in Indices (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) by A3, A4, A5, MATRIX_0:30;
(GoB h) * (I,(width (GoB h))) = (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) * (I,(width (GoB h))) by GOBOARD2:def 2
.= |[((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:52;
I <= len (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) by A4, GOBOARD2:def 2;
then A11: [I,1] in Indices (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) by A3, A6, MATRIX_0:30;
(GoB h) * (I,1) = (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) * (I,1) by GOBOARD2:def 2
.= |[((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:52;
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, Th4; :: thesis: verum