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 = max 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 = max 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 = max Y implies ((GoB h) * i1,I) `1 >= (h /. i) `1 )
assume A1: ( 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 = max Y ) ; :: thesis: ((GoB h) * i1,I) `1 >= (h /. i) `1
then i1 in Y by XXREAL_2:def 8;
then consider j being Element of NAT such that
A2: ( 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 A1;
A3: i in dom h by A1, FINSEQ_3:27;
then consider i2, j2 being Element of NAT such that
A4: ( [i2,j2] in Indices (GoB h) & h /. i = (GoB h) * i2,j2 ) by GOBOARD5:12;
A5: ( 1 <= i2 & i2 <= len (GoB h) & 1 <= j2 & j2 <= width (GoB h) ) by A4, MATRIX_1:39;
then A6: (h /. i) `2 = ((GoB h) * i2,I) `2 by A1, GOBOARD5:2;
A7: (h /. i) `1 = ((GoB h) * i2,1) `1 by A4, A5, GOBOARD5:3
.= ((GoB h) * i2,I) `1 by A1, A5, GOBOARD5:3 ;
h /. i = |[((h /. i) `1 ),((h /. i) `2 )]| by EUCLID:57;
then A8: h /. i = (GoB h) * i2,I by A6, A7, EUCLID:57;
[i2,I] in Indices (GoB h) by A1, A5, MATRIX_1:37;
then i2 in Y by A1, A3, A8;
then A9: ( 1 <= i1 & i1 >= i2 & i2 <= len (GoB h) & 1 <= width (GoB h) ) by A1, A2, A4, GOBOARD7:35, MATRIX_1:39, XXREAL_2:def 8;
A10: i1 <= len (GoB h) by A2, MATRIX_1:39;

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 A1, A5, A10, GOBOARD5:4; :: 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 A9, XXREAL_0:1; :: thesis: verum

end;

end;

end;

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