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
(X_axis f) . n <= (X_axis f) . m ) holds
f /. n in rng (Line (GoB f),1)
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
(X_axis f) . n <= (X_axis f) . m ) implies f /. n in rng (Line (GoB f),1) )
set x = X_axis f;
set y = Y_axis f;
set r = (X_axis f) . n;
assume A1: ( n in dom f & ( for m being Element of NAT st m in dom f holds
(X_axis f) . n <= (X_axis f) . m ) ) ; :: thesis: f /. n in rng (Line (GoB f),1)
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;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
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;
A10: ( 1 <= i & i <= len (Incr (X_axis f)) & dom (Incr (X_axis f)) = dom (Incr (X_axis f)) & rng (Incr (X_axis f)) c= REAL ) by A8, FINSEQ_1:def 4, FINSEQ_3:27;
then reconsider i1 = i - 1 as Element of NAT by INT_1:18;
A11: dom (Incr (X_axis f)) = dom (GoB f) by A2, A7, FINSEQ_3:31;
A12: dom (Incr (Y_axis f)) = Seg (width (GoB f)) by A2, A7, FINSEQ_1:def 3;

A13: now

assume i <> 1 ; :: thesis: contradiction
then ( 1 < i & 0 <= 1 & 0 < 1 ) by A10, XXREAL_0:1;
then A14: ( 1 + 1 <= i & i1 <= i & i1 < i ) by NAT_1:13, XREAL_1:46;
then ( 1 <= i1 & i1 <= len (Incr (X_axis f)) ) by A10, XREAL_1:21, XXREAL_0:2;
then A15: i1 in dom (Incr (X_axis f)) by FINSEQ_3:27;
then A16: (Incr (X_axis f)) . i1 in rng (Incr (X_axis f)) by FUNCT_1:def 5;
reconsider s = (Incr (X_axis f)) . i1 as Real ;
A17: s < (X_axis f) . n by A6, A8, A14, A15, SEQM_3:def 1;
ex m being Nat st
( m in dom (X_axis f) & (X_axis f) . m = s ) by A7, A16, FINSEQ_2:11;
hence contradiction by A1, A4, A5, A17; :: thesis: verum

end;

then [1,j] in Indices (GoB f) by A3, A8, A9, A11, A12, ZFMISC_1:106;
then ( (GoB f) * 1,j = |[(p `1 ),(p `2 )]| & p = |[(p `1 ),(p `2 )]| ) by A8, A9, A13, Def1, EUCLID:57;
then ( (Line (GoB f),1) . j = f /. n & len (Line (GoB f),1) = width (GoB f) ) by A9, A12, MATRIX_1:def 8;
then ( (Line (GoB f),1) . j = f /. n & dom (Line (GoB f),1) = Seg (width (GoB f)) ) by FINSEQ_1:def 3;
hence f /. n in rng (Line (GoB f),1) by A9, A12, FUNCT_1:def 5; :: thesis: verum