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

( ((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