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 ()),(Incr ())) by GOBOARD2:def 2;
then A6: 1 <= width (GoB ((Incr ()),(Incr ()))) by GOBOARD7:33;
i <= len () by ;
then A7: i in dom () by ;
then (Y_axis h) . i = (h /. i) `2 by GOBOARD1:def 2;
then A8: (h /. i) `2 in rng () by ;
1 <= width (GoB h) by GOBOARD7:33;
then A9: [I,(width (GoB h))] in Indices (GoB ((Incr ()),(Incr ()))) by ;
(GoB h) * (I,(width (GoB h))) = (GoB ((Incr ()),(Incr ()))) * (I,(width (GoB h))) by GOBOARD2:def 2
.= |[((Incr ()) . I),((Incr ()) . (width (GoB h)))]| by ;
then A10: ((GoB h) * (I,(width (GoB h)))) `2 = (Incr ()) . (width (GoB h)) by EUCLID:52;
I <= len (GoB ((Incr ()),(Incr ()))) by ;
then A11: [I,1] in Indices (GoB ((Incr ()),(Incr ()))) by ;
(GoB h) * (I,1) = (GoB ((Incr ()),(Incr ()))) * (I,1) by GOBOARD2:def 2
.= |[((Incr ()) . I),((Incr ()) . 1)]| by ;
then A12: ((GoB h) * (I,1)) `2 = (Incr ()) . 1 by EUCLID:52;
width (GoB h) = len (Incr ()) by ;
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