for f being non empty FinSequence of (TOP-REAL 2)
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 = max Y holds
((GoB f) * (I,i1)) `2 >= (f /. i) `2