let h be non constant standard special_circular_sequence; :: thesis: for i, I, i1 being Element of 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 Element of 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, I, i1 be Element of NAT ; :: thesis: 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 Element of 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; :: thesis: ( 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 Element of 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 Element of NAT st
( k in dom h & h /. k = (GoB h) * (j,I) ) ) } & (h /. i) `2 = ((GoB h) * (1,I)) `2 & i1 = min Y ) ; :: thesis: ((GoB h) * (i1,I)) `1 <= (h /. i) `1
then A3: i in dom h by FINSEQ_3:25;
then consider i2, j2 being Element of 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_1:38;
A7: 1 <= i2 by A4, MATRIX_1:38;
then A8: [i2,I] in Indices (GoB h) by A2, A6, MATRIX_1:36;
A9: j2 <= width (GoB h) by A4, MATRIX_1:38;
1 <= j2 by A4, MATRIX_1:38;
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 Element of NAT st
( k in dom h & h /. k = (GoB h) * (j,I) ) ) by A2;
then A11: 1 <= i1 by MATRIX_1:38;
(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;
then A12: i1 <= i2 by A2, XXREAL_2:def 7;
A13: i2 <= len (GoB h) by A4, MATRIX_1:38;

now

per cases ( i1 < i2 or i1 >= i2 ) ;

case i1 < i2 ; :: thesis: ((GoB h) * (i1,I)) `1 <= ((GoB h) * (i2,I)) `1

hence ((GoB h) * (i1,I)) `1 <= ((GoB h) * (i2,I)) `1 by A2, A11, A13, GOBOARD5:3; :: thesis: verum

end;

case i1 >= i2 ; :: thesis: ((GoB h) * (i1,I)) `1 <= ((GoB h) * (i2,I)) `1

hence ((GoB h) * (i1,I)) `1 <= ((GoB h) * (i2,I)) `1 by A12, XXREAL_0:1; :: thesis: verum

end;

end;

end;

hence ((GoB h) * (i1,I)) `1 <= (h /. i) `1 by A10; :: thesis: verum