let f be non trivial FinSequence of (TOP-REAL 2); :: thesis:
set p = E-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: E-max (L~ f) in LSeg ((f /. i),(f /. (i + 1))) by SPPOL_2:14, SPRECT_1:14;
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)) `1 <= E-bound (L~ f) by PSCOMP_1:24;
A7: (E-max (L~ f)) `1 = E-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) `1 <= E-bound (L~ f) by PSCOMP_1:24;

per cases by A4, A9, A6, A7, Th17;

suppose E-max (L~ f) = f /. i ; :: thesis:

hence E-max (L~ f) in rng f by A8, PARTFUN2:2; :: thesis:

end;

suppose E-max (L~ f) = f /. (i + 1) ; :: thesis:

hence E-max (L~ f) in rng f by A5, PARTFUN2:2; :: thesis:

end;

suppose A10: ( (E-max (L~ f)) `1 = (f /. i) `1 & (E-max (L~ f)) `1 = (f /. (i + 1)) `1 ) ; :: thesis:

then f /. (i + 1) in E-most (L~ f) by A1, A5, A7, Th13, GOBOARD1:1;
then A11: (f /. (i + 1)) `2 <= (E-max (L~ f)) `2 by PSCOMP_1:47;
( (f /. i) `2 >= (f /. (i + 1)) `2 or (f /. (i + 1)) `2 >= (f /. i) `2 ) ;
then A12: ( (f /. i) `2 >= (E-max (L~ f)) `2 or (f /. (i + 1)) `2 >= (E-max (L~ f)) `2 ) by A4, TOPREAL1:4;
f /. i in E-most (L~ f) by A1, A8, A7, A10, Th13, GOBOARD1:1;
then (f /. i) `2 <= (E-max (L~ f)) `2 by PSCOMP_1:47;
then ( (E-max (L~ f)) `2 = (f /. i) `2 or (E-max (L~ f)) `2 = (f /. (i + 1)) `2 ) by A11, A12, XXREAL_0:1;
then ( E-max (L~ f) = f /. i or E-max (L~ f) = f /. (i + 1) ) by A10, TOPREAL3:6;
hence E-max (L~ f) in rng f by A8, A5, PARTFUN2:2; :: thesis:

end;

end;

end;

hence E-max (L~ f) in rng f ; :: thesis: