let f be non trivial FinSequence of (TOP-REAL 2); N-max (L~ f) in rng f
set p = N-max (L~ f);
A1:
len f >= 2
by NAT_D:60;
consider i being Nat such that
A2:
1 <= i
and
A3:
i + 1 <= len f
and
A4:
N-max (L~ f) in LSeg ((f /. i),(f /. (i + 1)))
by SPPOL_2:14, SPRECT_1:11;
i + 1 >= 1
by NAT_1:11;
then A5:
i + 1 in dom f
by A3, FINSEQ_3:25;
then
f /. (i + 1) in L~ f
by A1, GOBOARD1:1;
then A6:
(f /. (i + 1)) `2 <= N-bound (L~ f)
by PSCOMP_1:24;
A7:
(N-max (L~ f)) `2 = N-bound (L~ f)
by EUCLID:52;
i <= i + 1
by NAT_1:11;
then
i <= len f
by A3, XXREAL_0:2;
then A8:
i in dom f
by A2, FINSEQ_3:25;
then
f /. i in L~ f
by A1, GOBOARD1:1;
then A9:
(f /. i) `2 <= N-bound (L~ f)
by PSCOMP_1:24;
now N-max (L~ f) in rng fper cases
( N-max (L~ f) = f /. i or N-max (L~ f) = f /. (i + 1) or ( (N-max (L~ f)) `2 = (f /. i) `2 & (N-max (L~ f)) `2 = (f /. (i + 1)) `2 ) )
by A4, A9, A6, A7, Th18;
suppose A10:
(
(N-max (L~ f)) `2 = (f /. i) `2 &
(N-max (L~ f)) `2 = (f /. (i + 1)) `2 )
;
N-max (L~ f) in rng fthen
f /. (i + 1) in N-most (L~ f)
by A1, A5, A7, Th10, GOBOARD1:1;
then A11:
(f /. (i + 1)) `1 <= (N-max (L~ f)) `1
by PSCOMP_1:39;
(
(f /. i) `1 >= (f /. (i + 1)) `1 or
(f /. (i + 1)) `1 >= (f /. i) `1 )
;
then A12:
(
(f /. i) `1 >= (N-max (L~ f)) `1 or
(f /. (i + 1)) `1 >= (N-max (L~ f)) `1 )
by A4, TOPREAL1:3;
f /. i in N-most (L~ f)
by A1, A8, A7, A10, Th10, GOBOARD1:1;
then
(f /. i) `1 <= (N-max (L~ f)) `1
by PSCOMP_1:39;
then
(
(N-max (L~ f)) `1 = (f /. i) `1 or
(N-max (L~ f)) `1 = (f /. (i + 1)) `1 )
by A11, A12, XXREAL_0:1;
then
(
N-max (L~ f) = f /. i or
N-max (L~ f) = f /. (i + 1) )
by A10, TOPREAL3:6;
hence
N-max (L~ f) in rng f
by A8, A5, PARTFUN2:2;
verum end; end; end;
hence
N-max (L~ f) in rng f
; verum