let h be non constant standard special_circular_sequence; for I, i1, i being Nat
for Y being non empty finite Subset of NAT st 1 <= i & i <= len h & 1 <= I & I <= width (GoB h) & Y = { j where j is Element of NAT : ( [j,I] in Indices (GoB h) & ex k being Nat st
( k in dom h & h /. k = (GoB h) * (j,I) ) ) } & (h /. i) `2 = ((GoB h) * (1,I)) `2 & i1 = min Y holds
((GoB h) * (i1,I)) `1 <= (h /. i) `1
let I, i1, i be Nat; for Y being non empty finite Subset of NAT st 1 <= i & i <= len h & 1 <= I & I <= width (GoB h) & Y = { j where j is Element of NAT : ( [j,I] in Indices (GoB h) & ex k being Nat st
( k in dom h & h /. k = (GoB h) * (j,I) ) ) } & (h /. i) `2 = ((GoB h) * (1,I)) `2 & i1 = min Y holds
((GoB h) * (i1,I)) `1 <= (h /. i) `1
let Y be non empty finite Subset of NAT; ( 1 <= i & i <= len h & 1 <= I & I <= width (GoB h) & Y = { j where j is Element of NAT : ( [j,I] in Indices (GoB h) & ex k being Nat st
( k in dom h & h /. k = (GoB h) * (j,I) ) ) } & (h /. i) `2 = ((GoB h) * (1,I)) `2 & i1 = min Y implies ((GoB h) * (i1,I)) `1 <= (h /. i) `1 )
A1:
h /. i = |[((h /. i) `1),((h /. i) `2)]|
by EUCLID:53;
assume A2:
( 1 <= i & i <= len h & 1 <= I & I <= width (GoB h) & Y = { j where j is Element of NAT : ( [j,I] in Indices (GoB h) & ex k being Nat st
( k in dom h & h /. k = (GoB h) * (j,I) ) ) } & (h /. i) `2 = ((GoB h) * (1,I)) `2 & i1 = min Y )
; ((GoB h) * (i1,I)) `1 <= (h /. i) `1
then A3:
i in dom h
by FINSEQ_3:25;
then consider i2, j2 being Nat such that
A4:
[i2,j2] in Indices (GoB h)
and
A5:
h /. i = (GoB h) * (i2,j2)
by GOBOARD5:11;
A6:
i2 <= len (GoB h)
by A4, MATRIX_0:32;
A7:
1 <= i2
by A4, MATRIX_0:32;
then A8:
[i2,I] in Indices (GoB h)
by A2, A6, MATRIX_0:30;
A9:
j2 <= width (GoB h)
by A4, MATRIX_0:32;
1 <= j2
by A4, MATRIX_0:32;
then A10: (h /. i) `1 =
((GoB h) * (i2,1)) `1
by A5, A7, A6, A9, GOBOARD5:2
.=
((GoB h) * (i2,I)) `1
by A2, A7, A6, GOBOARD5:2
;
i1 in Y
by A2, XXREAL_2:def 7;
then
ex j being Element of NAT st
( i1 = j & [j,I] in Indices (GoB h) & ex k being Nat st
( k in dom h & h /. k = (GoB h) * (j,I) ) )
by A2;
then A11:
1 <= i1
by MATRIX_0:32;
A12:
i2 in NAT
by ORDINAL1:def 12;
(h /. i) `2 = ((GoB h) * (i2,I)) `2
by A2, A7, A6, GOBOARD5:1;
then
h /. i = (GoB h) * (i2,I)
by A10, A1, EUCLID:53;
then
i2 in Y
by A2, A3, A8, A12;
then A13:
i1 <= i2
by A2, XXREAL_2:def 7;
A14:
i2 <= len (GoB h)
by A4, MATRIX_0:32;
hence
((GoB h) * (i1,I)) `1 <= (h /. i) `1
by A10; verum