let f be non empty FinSequence of (TOP-REAL 2); :: thesis: for I, i1, i being 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 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, i1, i be 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 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 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 )

A1: f /. i = |[((f /. i) `1),((f /. i) `2)]| by EUCLID:53;

assume A2: ( 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 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 A3: i in dom f by FINSEQ_3:25;

then consider i2, j2 being Nat such that

A4: [i2,j2] in Indices (GoB f) and

A5: f /. i = (GoB f) * (i2,j2) by GOBOARD5:11;

A6: j2 <= width (GoB f) by A4, MATRIX_0:32;

A7: 1 <= j2 by A4, MATRIX_0:32;

then A8: [I,j2] in Indices (GoB f) by A2, A6, MATRIX_0:30;

A9: i2 <= len (GoB f) by A4, MATRIX_0:32;

1 <= i2 by A4, MATRIX_0:32;

then A10: (f /. i) `2 = ((GoB f) * (1,j2)) `2 by A5, A9, A7, A6, GOBOARD5:1

.= ((GoB f) * (I,j2)) `2 by A2, A7, A6, GOBOARD5:1 ;

i1 in Y by A2, XXREAL_2:def 7;

then ex j being Element of NAT st

( i1 = j & [I,j] in Indices (GoB f) & ex k being Nat st

( k in dom f & f /. k = (GoB f) * (I,j) ) ) by A2;

then A11: 1 <= i1 by MATRIX_0:32;

A12: j2 in NAT by ORDINAL1:def 12;

(f /. i) `1 = ((GoB f) * (I,j2)) `1 by A2, A7, A6, GOBOARD5:2;

then f /. i = (GoB f) * (I,j2) by A10, A1, EUCLID:53;

then j2 in Y by A2, A3, A8, A12;

then A13: i1 <= j2 by A2, XXREAL_2:def 7;

A14: j2 <= width (GoB f) by A4, MATRIX_0:32;

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 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, i1, i be 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 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 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 )

A1: f /. i = |[((f /. i) `1),((f /. i) `2)]| by EUCLID:53;

assume A2: ( 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 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 A3: i in dom f by FINSEQ_3:25;

then consider i2, j2 being Nat such that

A4: [i2,j2] in Indices (GoB f) and

A5: f /. i = (GoB f) * (i2,j2) by GOBOARD5:11;

A6: j2 <= width (GoB f) by A4, MATRIX_0:32;

A7: 1 <= j2 by A4, MATRIX_0:32;

then A8: [I,j2] in Indices (GoB f) by A2, A6, MATRIX_0:30;

A9: i2 <= len (GoB f) by A4, MATRIX_0:32;

1 <= i2 by A4, MATRIX_0:32;

then A10: (f /. i) `2 = ((GoB f) * (1,j2)) `2 by A5, A9, A7, A6, GOBOARD5:1

.= ((GoB f) * (I,j2)) `2 by A2, A7, A6, GOBOARD5:1 ;

i1 in Y by A2, XXREAL_2:def 7;

then ex j being Element of NAT st

( i1 = j & [I,j] in Indices (GoB f) & ex k being Nat st

( k in dom f & f /. k = (GoB f) * (I,j) ) ) by A2;

then A11: 1 <= i1 by MATRIX_0:32;

A12: j2 in NAT by ORDINAL1:def 12;

(f /. i) `1 = ((GoB f) * (I,j2)) `1 by A2, A7, A6, GOBOARD5:2;

then f /. i = (GoB f) * (I,j2) by A10, A1, EUCLID:53;

then j2 in Y by A2, A3, A8, A12;

then A13: i1 <= j2 by A2, XXREAL_2:def 7;

A14: j2 <= width (GoB f) by A4, MATRIX_0:32;

now :: thesis: ( ( i1 < j2 & ((GoB f) * (I,i1)) `2 <= ((GoB f) * (I,j2)) `2 ) or ( i1 >= j2 & ((GoB f) * (I,i1)) `2 <= ((GoB f) * (I,j2)) `2 ) )

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