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

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

suppose S-min (L~ f) = f /. i ; :: thesis:

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

end;

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

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

end;

suppose A10: ( (S-min (L~ f)) `2 = (f /. i) `2 & (S-min (L~ f)) `2 = (f /. (i + 1)) `2 ) ; :: thesis:

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

end;

end;

end;

hence S-min (L~ f) in rng f ; :: thesis: