let n be Element of NAT ; :: thesis: for f being non empty FinSequence of (TOP-REAL 2) st n in dom f & ( for m being Element of NAT st m in dom f holds
(Y_axis f) . m <= (Y_axis f) . n ) holds
f /. n in rng (Col (GoB f),(width (GoB f)))
let f be non empty FinSequence of (TOP-REAL 2); :: thesis: ( n in dom f & ( for m being Element of NAT st m in dom f holds
(Y_axis f) . m <= (Y_axis f) . n ) implies f /. n in rng (Col (GoB f),(width (GoB f))) )
set x = X_axis f;
set y = Y_axis f;
set r = (Y_axis f) . n;
assume A1: ( n in dom f & ( for m being Element of NAT st m in dom f holds
(Y_axis f) . m <= (Y_axis f) . n ) ) ; :: thesis: f /. n in rng (Col (GoB f),(width (GoB f)))
A2: ( GoB f = GoB (Incr (X_axis f)),(Incr (Y_axis f)) & X_axis f <> {} & Y_axis f <> {} & len (GoB f) = card (rng (X_axis f)) & width (GoB f) = card (rng (Y_axis f)) ) by Th24;
A3: ( Indices (GoB f) = [:(dom (GoB f)),(Seg (width (GoB f))):] & Incr (X_axis f) <> {} & Incr (Y_axis f) <> {} ) by MATRIX_1:def 5;
A4: ( dom f = Seg (len f) & dom (X_axis f) = Seg (len (X_axis f)) & dom (Y_axis f) = Seg (len (Y_axis f)) & rng f c= the carrier of (TOP-REAL 2) ) by FINSEQ_1:def 3, FINSEQ_1:def 4;
reconsider p = f /. n as Point of (TOP-REAL 2) ;
A5: ( len (X_axis f) = len f & len (Y_axis f) = len f ) by GOBOARD1:def 3, GOBOARD1:def 4;
then A6: ( (X_axis f) . n = p `1 & (Y_axis f) . n = p `2 & (X_axis f) . n in rng (X_axis f) & (Y_axis f) . n in rng (Y_axis f) ) by A1, A4, FUNCT_1:def 5, GOBOARD1:def 3, GOBOARD1:def 4;
A7: ( rng (Incr (X_axis f)) = rng (X_axis f) & rng (Incr (Y_axis f)) = rng (Y_axis f) & len (Incr (X_axis f)) = card (rng (X_axis f)) & len (Incr (Y_axis f)) = card (rng (Y_axis f)) ) by Def2;
then consider i being Nat such that
A8: ( i in dom (Incr (X_axis f)) & (Incr (X_axis f)) . i = p `1 ) by A6, FINSEQ_2:11;
consider j being Nat such that
A9: ( j in dom (Incr (Y_axis f)) & (Incr (Y_axis f)) . j = p `2 ) by A6, A7, FINSEQ_2:11;
reconsider j = j as Element of NAT by ORDINAL1:def 13;
A10: ( 1 <= j & j <= len (Incr (Y_axis f)) & dom (Incr (Y_axis f)) = dom (Incr (Y_axis f)) & rng (Incr (Y_axis f)) c= REAL ) by A9, FINSEQ_1:def 4, FINSEQ_3:27;
A11: ( dom (Incr (X_axis f)) = dom (GoB f) & dom (Incr (Y_axis f)) = Seg (width (GoB f)) ) by A2, A7, FINSEQ_1:def 3, FINSEQ_3:31;

A12: now

assume j <> len (Incr (Y_axis f)) ; :: thesis: contradiction
then ( j < len (Incr (Y_axis f)) & j <= j + 1 ) by A10, NAT_1:11, XXREAL_0:1;
then ( 1 <= j + 1 & j + 1 <= len (Incr (Y_axis f)) ) by A10, NAT_1:13;
then A13: ( j + 1 in dom (Incr (Y_axis f)) & j < j + 1 ) by FINSEQ_3:27, NAT_1:13;
then A14: (Incr (Y_axis f)) . (j + 1) in rng (Incr (Y_axis f)) by FUNCT_1:def 5;
reconsider s = (Incr (Y_axis f)) . (j + 1) as Real ;
A15: (Y_axis f) . n < s by A6, A9, A13, SEQM_3:def 1;
ex m being Nat st
( m in dom (Y_axis f) & (Y_axis f) . m = s ) by A7, A14, FINSEQ_2:11;
hence contradiction by A1, A4, A5, A15; :: thesis: verum

end;

then [i,(width (GoB f))] in Indices (GoB f) by A2, A3, A7, A8, A9, A11, ZFMISC_1:106;
then ( (GoB f) * i,(width (GoB f)) = |[(p `1 ),(p `2 )]| & p = |[(p `1 ),(p `2 )]| ) by A2, A7, A8, A9, A12, Def1, EUCLID:57;
then ( (Col (GoB f),(width (GoB f))) . i = f /. n & len (Col (GoB f),(width (GoB f))) = len (GoB f) ) by A8, A11, MATRIX_1:def 9;
then ( (Col (GoB f),(width (GoB f))) . i = f /. n & dom (Col (GoB f),(width (GoB f))) = dom (GoB f) ) by FINSEQ_3:31;
hence f /. n in rng (Col (GoB f),(width (GoB f))) by A8, A11, FUNCT_1:def 5; :: thesis: verum