let h be non constant standard special_circular_sequence; :: thesis: for I, i being Nat st 1 <= i & i <= len h & 1 <= I & I <= width (GoB h) holds
( ((GoB h) * (1,I)) `1 <= (h /. i) `1 & (h /. i) `1 <= ((GoB h) * ((len (GoB h)),I)) `1 )

let I, i be Nat; :: thesis: ( 1 <= i & i <= len h & 1 <= I & I <= width (GoB h) implies ( ((GoB h) * (1,I)) `1 <= (h /. i) `1 & (h /. i) `1 <= ((GoB h) * ((len (GoB h)),I)) `1 ) )
assume that
A1: 1 <= i and
A2: i <= len h and
A3: 1 <= I and
A4: I <= width (GoB h) ; :: thesis: ( ((GoB h) * (1,I)) `1 <= (h /. i) `1 & (h /. i) `1 <= ((GoB h) * ((len (GoB h)),I)) `1 )
A5: I <= width (GoB ((Incr ()),(Incr ()))) by ;
i <= len () by ;
then A6: i in dom () by ;
then (X_axis h) . i = (h /. i) `1 by GOBOARD1:def 1;
then A7: (h /. i) `1 in rng () by ;
A8: GoB h = GoB ((Incr ()),(Incr ())) by GOBOARD2:def 2;
then 1 <= len (GoB ((Incr ()),(Incr ()))) by GOBOARD7:32;
then A9: [1,I] in Indices (GoB ((Incr ()),(Incr ()))) by ;
A10: 1 <= len (GoB h) by GOBOARD7:32;
len (GoB h) <= len (GoB ((Incr ()),(Incr ()))) by GOBOARD2:def 2;
then A11: [(len (GoB h)),I] in Indices (GoB ((Incr ()),(Incr ()))) by ;
(GoB h) * ((len (GoB h)),I) = (GoB ((Incr ()),(Incr ()))) * ((len (GoB h)),I) by GOBOARD2:def 2
.= |[((Incr ()) . (len (GoB h))),((Incr ()) . I)]| by ;
then A12: ((GoB h) * ((len (GoB h)),I)) `1 = (Incr ()) . (len (GoB h)) by EUCLID:52;
(GoB h) * (1,I) = (GoB ((Incr ()),(Incr ()))) * (1,I) by GOBOARD2:def 2
.= |[((Incr ()) . 1),((Incr ()) . I)]| by ;
then A13: ((GoB h) * (1,I)) `1 = (Incr ()) . 1 by EUCLID:52;
len (GoB h) = len (Incr ()) by ;
hence ( ((GoB h) * (1,I)) `1 <= (h /. i) `1 & (h /. i) `1 <= ((GoB h) * ((len (GoB h)),I)) `1 ) by A12, A13, A7, Th4; :: thesis: verum