let h be non constant standard special_circular_sequence; for i, I being Element of 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 Element of 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 3;
i <= len (X_axis h)
by A2, GOBOARD1:def 3;
then A6:
i in dom (X_axis h)
by A1, FINSEQ_3:27;
then
(X_axis h) . i = (h /. i) `1
by GOBOARD1:def 3;
then A7:
(h /. i) `1 in rng (X_axis h)
by A6, FUNCT_1:def 5;
A8:
GoB h = GoB (Incr (X_axis h)),(Incr (Y_axis h))
by GOBOARD2:def 3;
then
1 <= len (GoB (Incr (X_axis h)),(Incr (Y_axis h)))
by GOBOARD7:34;
then A9:
[1,I] in Indices (GoB (Incr (X_axis h)),(Incr (Y_axis h)))
by A3, A5, MATRIX_1:37;
A10:
1 <= len (GoB h)
by GOBOARD7:34;
len (GoB h) <= len (GoB (Incr (X_axis h)),(Incr (Y_axis h)))
by GOBOARD2:def 3;
then A11:
[(len (GoB h)),I] in Indices (GoB (Incr (X_axis h)),(Incr (Y_axis h)))
by A3, A5, A10, MATRIX_1:37;
(GoB h) * (len (GoB h)),I =
(GoB (Incr (X_axis h)),(Incr (Y_axis h))) * (len (GoB h)),I
by GOBOARD2:def 3
.=
|[((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:56;
(GoB h) * 1,I =
(GoB (Incr (X_axis h)),(Incr (Y_axis h))) * 1,I
by GOBOARD2:def 3
.=
|[((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:56;
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, Th6; verum