let h be non constant standard special_circular_sequence; 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; ( 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)
; ( ((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; verum