let n be Nat; :: thesis: for f being non empty FinSequence of () st n in dom f & ( for m being Nat st m in dom f holds
() . m <= () . n ) holds
f /. n in rng (Line ((GoB f),(len (GoB f))))

let f be non empty FinSequence of (); :: thesis: ( n in dom f & ( for m being Nat st m in dom f holds
() . m <= () . n ) implies f /. n in rng (Line ((GoB f),(len (GoB f)))) )

set x = X_axis f;
set y = Y_axis f;
set r = () . n;
assume that
A1: n in dom f and
A2: for m being Nat st m in dom f holds
() . m <= () . n ; :: thesis: f /. n in rng (Line ((GoB f),(len (GoB f))))
reconsider p = f /. n as Point of () ;
A3: dom f = Seg (len f) by FINSEQ_1:def 3;
A4: ( dom () = Seg (len ()) & len () = len f ) by ;
then A5: (X_axis f) . n = p `1 by ;
A6: rng (Incr ()) = rng () by SEQ_4:def 21;
(X_axis f) . n in rng () by ;
then consider i being Nat such that
A7: i in dom (Incr ()) and
A8: (Incr ()) . i = p `1 by ;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
A9: i <= len (Incr ()) by ;
A10: 1 <= i by ;
A11: now :: thesis: not i <> len (Incr ())
reconsider s = (Incr ()) . (i + 1) as Real ;
assume i <> len (Incr ()) ; :: thesis: contradiction
then i < len (Incr ()) by ;
then A12: i + 1 <= len (Incr ()) by NAT_1:13;
1 <= i + 1 by ;
then A13: i + 1 in dom (Incr ()) by ;
then (Incr ()) . (i + 1) in rng (Incr ()) by FUNCT_1:def 3;
then A14: ex m being Nat st
( m in dom () & () . m = s ) by ;
i < i + 1 by NAT_1:13;
then (X_axis f) . n < s by ;
hence contradiction by A2, A3, A4, A14; :: thesis: verum
end;
A15: rng (Incr ()) = rng () by SEQ_4:def 21;
( dom () = Seg (len ()) & len () = len f ) by ;
then ( (Y_axis f) . n = p `2 & () . n in rng () ) by ;
then consider j being Nat such that
A16: j in dom (Incr ()) and
A17: (Incr ()) . j = p `2 by ;
A18: p = |[(p `1),(p `2)]| by EUCLID:53;
len (Line ((GoB f),(len (GoB f)))) = width (GoB f) by MATRIX_0:def 7;
then A19: dom (Line ((GoB f),(len (GoB f)))) = Seg (width (GoB f)) by FINSEQ_1:def 3;
( width (GoB f) = card (rng ()) & len (Incr ()) = card (rng ()) ) by ;
then A20: dom (Incr ()) = Seg (width (GoB f)) by FINSEQ_1:def 3;
A21: ( len (GoB f) = card (rng ()) & len (Incr ()) = card (rng ()) ) by ;
then ( Indices (GoB f) = [:(dom (GoB f)),(Seg (width (GoB f))):] & dom (Incr ()) = dom (GoB f) ) by ;
then [(len (GoB f)),j] in Indices (GoB f) by ;
then (GoB f) * ((len (GoB f)),j) = |[(p `1),(p `2)]| by A21, A8, A17, A11, Def1;
then (Line ((GoB f),(len (GoB f)))) . j = f /. n by ;
hence f /. n in rng (Line ((GoB f),(len (GoB f)))) by ; :: thesis: verum