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 (X_axis h)),(Incr (Y_axis h)))) by A4, GOBOARD2:def 2;

i <= len (X_axis h) by A2, GOBOARD1:def 1;

then A6: i in dom (X_axis h) by A1, FINSEQ_3:25;

then (X_axis h) . i = (h /. i) `1 by GOBOARD1:def 1;

then A7: (h /. i) `1 in rng (X_axis h) by A6, FUNCT_1:def 3;

A8: GoB h = GoB ((Incr (X_axis h)),(Incr (Y_axis h))) by GOBOARD2:def 2;

then 1 <= len (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) by GOBOARD7:32;

then A9: [1,I] in Indices (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) by A3, A5, MATRIX_0:30;

A10: 1 <= len (GoB h) by GOBOARD7:32;

len (GoB h) <= len (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) by GOBOARD2:def 2;

then A11: [(len (GoB h)),I] in Indices (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) by A3, A5, A10, MATRIX_0:30;

(GoB h) * ((len (GoB h)),I) = (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) * ((len (GoB h)),I) by GOBOARD2:def 2

.= |[((Incr (X_axis h)) . (len (GoB h))),((Incr (Y_axis h)) . I)]| by A11, GOBOARD2:def 1 ;

then A12: ((GoB h) * ((len (GoB h)),I)) `1 = (Incr (X_axis h)) . (len (GoB h)) by EUCLID:52;

(GoB h) * (1,I) = (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) * (1,I) by GOBOARD2:def 2

.= |[((Incr (X_axis h)) . 1),((Incr (Y_axis h)) . I)]| by A9, GOBOARD2:def 1 ;

then A13: ((GoB h) * (1,I)) `1 = (Incr (X_axis h)) . 1 by EUCLID:52;

len (GoB h) = len (Incr (X_axis h)) by A8, GOBOARD2:def 1;

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

( ((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 (X_axis h)),(Incr (Y_axis h)))) by A4, GOBOARD2:def 2;

i <= len (X_axis h) by A2, GOBOARD1:def 1;

then A6: i in dom (X_axis h) by A1, FINSEQ_3:25;

then (X_axis h) . i = (h /. i) `1 by GOBOARD1:def 1;

then A7: (h /. i) `1 in rng (X_axis h) by A6, FUNCT_1:def 3;

A8: GoB h = GoB ((Incr (X_axis h)),(Incr (Y_axis h))) by GOBOARD2:def 2;

then 1 <= len (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) by GOBOARD7:32;

then A9: [1,I] in Indices (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) by A3, A5, MATRIX_0:30;

A10: 1 <= len (GoB h) by GOBOARD7:32;

len (GoB h) <= len (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) by GOBOARD2:def 2;

then A11: [(len (GoB h)),I] in Indices (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) by A3, A5, A10, MATRIX_0:30;

(GoB h) * ((len (GoB h)),I) = (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) * ((len (GoB h)),I) by GOBOARD2:def 2

.= |[((Incr (X_axis h)) . (len (GoB h))),((Incr (Y_axis h)) . I)]| by A11, GOBOARD2:def 1 ;

then A12: ((GoB h) * ((len (GoB h)),I)) `1 = (Incr (X_axis h)) . (len (GoB h)) by EUCLID:52;

(GoB h) * (1,I) = (GoB ((Incr (X_axis h)),(Incr (Y_axis h)))) * (1,I) by GOBOARD2:def 2

.= |[((Incr (X_axis h)) . 1),((Incr (Y_axis h)) . I)]| by A9, GOBOARD2:def 1 ;

then A13: ((GoB h) * (1,I)) `1 = (Incr (X_axis h)) . 1 by EUCLID:52;

len (GoB h) = len (Incr (X_axis h)) by A8, GOBOARD2:def 1;

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