let f be non trivial FinSequence of (TOP-REAL 2); :: thesis: E-max (L~ f) in rng f
set p = E-max (L~ f);
A1: len f >= 2 by REALSET1:13;
E-max (L~ f) in L~ f by SPRECT_1:16;
then consider i being Element of NAT such that
A2: ( 1 <= i & i + 1 <= len f ) and
A3: E-max (L~ f) in LSeg (f /. i),(f /. (i + 1)) by SPPOL_2:14;
i <= i + 1 by NAT_1:11;
then ( i + 1 >= 1 & i <= len f ) by A2, XXREAL_0:2;
then A4: ( i in dom f & i + 1 in dom f ) by A2, FINSEQ_3:27;
then ( f /. i in L~ f & f /. (i + 1) in L~ f ) by A1, GOBOARD1:16;
then A5: ( (f /. i) `1 <= E-bound (L~ f) & (f /. (i + 1)) `1 <= E-bound (L~ f) ) by PSCOMP_1:71;
A6: (E-max (L~ f)) `1 = E-bound (L~ f) by EUCLID:56;

now

per cases ( E-max (L~ f) = f /. i or E-max (L~ f) = f /. (i + 1) or ( (E-max (L~ f)) `1 = (f /. i) `1 & (E-max (L~ f)) `1 = (f /. (i + 1)) `1 ) ) by A3, A5, A6, Th21;

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

hence E-max (L~ f) in rng f by A4, PARTFUN2:4; :: thesis: verum

end;

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

hence E-max (L~ f) in rng f by A4, PARTFUN2:4; :: thesis: verum

end;

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

then ( f /. i in E-most (L~ f) & f /. (i + 1) in E-most (L~ f) ) by A1, A4, A6, Th17, GOBOARD1:16;
then A8: ( (f /. i) `2 <= (E-max (L~ f)) `2 & (f /. (i + 1)) `2 <= (E-max (L~ f)) `2 ) by PSCOMP_1:108;
( (f /. i) `2 >= (f /. (i + 1)) `2 or (f /. (i + 1)) `2 >= (f /. i) `2 ) ;
then ( (f /. i) `2 >= (E-max (L~ f)) `2 or (f /. (i + 1)) `2 >= (E-max (L~ f)) `2 ) by A3, TOPREAL1:10;
then ( (E-max (L~ f)) `2 = (f /. i) `2 or (E-max (L~ f)) `2 = (f /. (i + 1)) `2 ) by A8, XXREAL_0:1;
then ( E-max (L~ f) = f /. i or E-max (L~ f) = f /. (i + 1) ) by A7, TOPREAL3:11;
hence E-max (L~ f) in rng f by A4, PARTFUN2:4; :: thesis: verum

end;

end;

end;

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