let n be Nat; :: thesis: for f being non empty FinSequence of (TOP-REAL 2) st n in dom f & ( for m being 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 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 that
A1: n in dom f and
A2: for m being Nat st m in dom f holds
(X_axis f) . n <= (X_axis f) . m ; :: thesis: f /. n in rng (Line ((GoB f),1))
reconsider p = f /. n as Point of (TOP-REAL 2) ;
A3: dom f = Seg (len f) by FINSEQ_1:def 3;
A4: ( dom (X_axis f) = Seg (len (X_axis f)) & len (X_axis f) = len f ) by FINSEQ_1:def 3, GOBOARD1:def 1;
then A5: (X_axis f) . n = p `1 by A1, A3, GOBOARD1:def 1;
A6: rng (Incr (X_axis f)) = rng (X_axis f) by SEQ_4:def 21;
(X_axis f) . n in rng (X_axis f) by A1, A3, A4, FUNCT_1:def 3;
then consider i being Nat such that
A7: i in dom (Incr (X_axis f)) and
A8: (Incr (X_axis f)) . i = p `1 by A5, A6, FINSEQ_2:10;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
A9: 1 <= i by A7, FINSEQ_3:25;
then reconsider i1 = i - 1 as Element of NAT by INT_1:5;
A10: i <= len (Incr (X_axis f)) by A7, FINSEQ_3:25;

A11: now :: thesis: not i <> 1

reconsider s = (Incr (X_axis f)) . i1 as Real ;
assume i <> 1 ; :: thesis: contradiction
then 1 < i by A9, XXREAL_0:1;
then 1 + 1 <= i by NAT_1:13;
then A12: 1 <= i1 by XREAL_1:19;
i1 <= i by XREAL_1:44;
then i1 <= len (Incr (X_axis f)) by A10, XXREAL_0:2;
then A13: i1 in dom (Incr (X_axis f)) by A12, FINSEQ_3:25;
then (Incr (X_axis f)) . i1 in rng (Incr (X_axis f)) by FUNCT_1:def 3;
then A14: ex m being Nat st
( m in dom (X_axis f) & (X_axis f) . m = s ) by A6, FINSEQ_2:10;
i1 < i by XREAL_1:44;
then s < (X_axis f) . n by A5, A7, A8, A13, SEQM_3:def 1;
hence contradiction by A2, A3, A4, A14; :: thesis: verum

end;

A15: rng (Incr (Y_axis f)) = rng (Y_axis f) by SEQ_4:def 21;
( dom (Y_axis f) = Seg (len (Y_axis f)) & len (Y_axis f) = len f ) by FINSEQ_1:def 3, GOBOARD1:def 2;
then ( (Y_axis f) . n = p `2 & (Y_axis f) . n in rng (Y_axis f) ) by A1, A3, FUNCT_1:def 3, GOBOARD1:def 2;
then consider j being Nat such that
A16: j in dom (Incr (Y_axis f)) and
A17: (Incr (Y_axis f)) . j = p `2 by A15, FINSEQ_2:10;
A18: p = |[(p `1),(p `2)]| by EUCLID:53;
len (Line ((GoB f),1)) = width (GoB f) by MATRIX_0:def 7;
then A19: dom (Line ((GoB f),1)) = Seg (width (GoB f)) by FINSEQ_1:def 3;
( width (GoB f) = card (rng (Y_axis f)) & len (Incr (Y_axis f)) = card (rng (Y_axis f)) ) by Th13, SEQ_4:def 21;
then A20: dom (Incr (Y_axis f)) = Seg (width (GoB f)) by FINSEQ_1:def 3;
( len (GoB f) = card (rng (X_axis f)) & len (Incr (X_axis f)) = card (rng (X_axis f)) ) by Th13, SEQ_4:def 21;
then ( Indices (GoB f) = [:(dom (GoB f)),(Seg (width (GoB f))):] & dom (Incr (X_axis f)) = dom (GoB f) ) by FINSEQ_3:29, MATRIX_0:def 4;
then [1,j] in Indices (GoB f) by A7, A16, A20, A11, ZFMISC_1:87;
then (GoB f) * (1,j) = |[(p `1),(p `2)]| by A8, A17, A11, Def1;
then (Line ((GoB f),1)) . j = f /. n by A16, A20, A18, MATRIX_0:def 7;
hence f /. n in rng (Line ((GoB f),1)) by A16, A20, A19, FUNCT_1:def 3; :: thesis: verum