let f be non empty FinSequence of (TOP-REAL 2); :: thesis: for i, I, i1 being Element of NAT
for Y being non empty finite Subset of NAT st 1 <= i & i <= len f & 1 <= I & I <= len (GoB f) & Y = { j where j is Element of NAT : ( [I,j] in Indices (GoB f) & ex k being Element of NAT st
( k in dom f & f /. k = (GoB f) * I,j ) ) } & (f /. i) `1 = ((GoB f) * I,1) `1 & i1 = min Y holds
((GoB f) * I,i1) `2 <= (f /. i) `2
let i, I, i1 be Element of NAT ; :: thesis: for Y being non empty finite Subset of NAT st 1 <= i & i <= len f & 1 <= I & I <= len (GoB f) & Y = { j where j is Element of NAT : ( [I,j] in Indices (GoB f) & ex k being Element of NAT st
( k in dom f & f /. k = (GoB f) * I,j ) ) } & (f /. i) `1 = ((GoB f) * I,1) `1 & i1 = min Y holds
((GoB f) * I,i1) `2 <= (f /. i) `2
let Y be non empty finite Subset of NAT ; :: thesis: ( 1 <= i & i <= len f & 1 <= I & I <= len (GoB f) & Y = { j where j is Element of NAT : ( [I,j] in Indices (GoB f) & ex k being Element of NAT st
( k in dom f & f /. k = (GoB f) * I,j ) ) } & (f /. i) `1 = ((GoB f) * I,1) `1 & i1 = min Y implies ((GoB f) * I,i1) `2 <= (f /. i) `2 )
assume A1: ( 1 <= i & i <= len f & 1 <= I & I <= len (GoB f) & Y = { j where j is Element of NAT : ( [I,j] in Indices (GoB f) & ex k being Element of NAT st
( k in dom f & f /. k = (GoB f) * I,j ) ) } & (f /. i) `1 = ((GoB f) * I,1) `1 & i1 = min Y ) ; :: thesis: ((GoB f) * I,i1) `2 <= (f /. i) `2
then i1 in Y by XXREAL_2:def 7;
then consider j being Element of NAT such that
A2: ( i1 = j & [I,j] in Indices (GoB f) & ex k being Element of NAT st
( k in dom f & f /. k = (GoB f) * I,j ) ) by A1;
A3: i in dom f by A1, FINSEQ_3:27;
then consider i2, j2 being Element of NAT such that
A4: ( [i2,j2] in Indices (GoB f) & f /. i = (GoB f) * i2,j2 ) by GOBOARD5:12;
A5: ( 1 <= i2 & i2 <= len (GoB f) & 1 <= j2 & j2 <= width (GoB f) ) by A4, MATRIX_1:39;
then A6: (f /. i) `1 = ((GoB f) * I,j2) `1 by A1, GOBOARD5:3;
A7: (f /. i) `2 = ((GoB f) * 1,j2) `2 by A4, A5, GOBOARD5:2
.= ((GoB f) * I,j2) `2 by A1, A5, GOBOARD5:2 ;
f /. i = |[((f /. i) `1 ),((f /. i) `2 )]| by EUCLID:57;
then A8: f /. i = (GoB f) * I,j2 by A6, A7, EUCLID:57;
[I,j2] in Indices (GoB f) by A1, A5, MATRIX_1:37;
then j2 in Y by A1, A3, A8;
then A9: ( 1 <= i1 & i1 <= j2 & j2 <= width (GoB f) & 1 <= 1 & 1 <= len (GoB f) ) by A1, A2, A4, MATRIX_1:39, XXREAL_0:2, XXREAL_2:def 7;

now

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

case i1 < j2 ; :: thesis: ((GoB f) * I,i1) `2 <= ((GoB f) * I,j2) `2

hence ((GoB f) * I,i1) `2 <= ((GoB f) * I,j2) `2 by A1, A9, GOBOARD5:5; :: thesis: verum

end;

case i1 >= j2 ; :: thesis: ((GoB f) * I,i1) `2 <= ((GoB f) * I,j2) `2

hence ((GoB f) * I,i1) `2 <= ((GoB f) * I,j2) `2 by A9, XXREAL_0:1; :: thesis: verum

end;

end;

end;

hence ((GoB f) * I,i1) `2 <= (f /. i) `2 by A7; :: thesis: verum