let n be Nat; 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) . m <= (X_axis f) . n ) holds
f /. n in rng (Line ((GoB f),(len (GoB f))))
let f be non empty FinSequence of (TOP-REAL 2); ( n in dom f & ( for m being Nat st m in dom f holds
(X_axis f) . m <= (X_axis f) . n ) implies f /. n in rng (Line ((GoB f),(len (GoB f)))) )
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) . m <= (X_axis f) . n
; f /. n in rng (Line ((GoB f),(len (GoB f))))
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:
i <= len (Incr (X_axis f))
by A7, FINSEQ_3:25;
A10:
1 <= i
by A7, FINSEQ_3:25;
A11:
now not i <> len (Incr (X_axis f))reconsider s =
(Incr (X_axis f)) . (i + 1) as
Real ;
assume
i <> len (Incr (X_axis f))
;
contradictionthen
i < len (Incr (X_axis f))
by A9, XXREAL_0:1;
then A12:
i + 1
<= len (Incr (X_axis f))
by NAT_1:13;
1
<= i + 1
by A10, NAT_1:13;
then A13:
i + 1
in dom (Incr (X_axis f))
by A12, FINSEQ_3:25;
then
(Incr (X_axis f)) . (i + 1) 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;
i < i + 1
by NAT_1:13;
then
(X_axis f) . n < s
by A5, A7, A8, A13, SEQM_3:def 1;
hence
contradiction
by A2, A3, A4, A14;
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),(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 (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;
A21:
( 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
[(len (GoB f)),j] in Indices (GoB f)
by A21, A7, A16, A20, A11, ZFMISC_1:87;
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 A16, A20, A18, MATRIX_0:def 7;
hence
f /. n in rng (Line ((GoB f),(len (GoB f))))
by A16, A20, A19, FUNCT_1:def 3; verum