let f be non constant standard special_circular_sequence; :: thesis: ( f /. 1 = N-min (L~ f) implies (W-max (L~ f)) .. f < len f )
A1: W-max (L~ f) in rng f by Th48;
assume A2: f /. 1 = N-min (L~ f) ; :: thesis: (W-max (L~ f)) .. f < len f
then A3: f /. (len f) = N-min (L~ f) by FINSEQ_6:def 1;
(W-max (L~ f)) .. f in dom f by A1, FINSEQ_4:30;
then A4: f /. ((W-max (L~ f)) .. f) = f . ((W-max (L~ f)) .. f) by PARTFUN1:def 8
.= W-max (L~ f) by A1, FINSEQ_4:29 ;

per cases ( N-min (L~ f) = W-max (L~ f) or N-min (L~ f) <> W-max (L~ f) ) ;

suppose N-min (L~ f) = W-max (L~ f) ; :: thesis: (W-max (L~ f)) .. f < len f

then (W-max (L~ f)) .. f = 1 by A2, FINSEQ_6:47;
hence (W-max (L~ f)) .. f < len f by GOBOARD7:36, XXREAL_0:2; :: thesis: verum

end;

suppose A5: N-min (L~ f) <> W-max (L~ f) ; :: thesis: (W-max (L~ f)) .. f < len f

(W-max (L~ f)) .. f <= len f by A1, FINSEQ_4:31;
hence (W-max (L~ f)) .. f < len f by A3, A4, A5, XXREAL_0:1; :: thesis: verum

end;

end;