let z be constant standard clockwise_oriented special_circular_sequence; :: thesis: ( z /. 1 = N-min (L~ z) implies (W-min (L~ z)) .. z < len z )
assume A1: z /. 1 = N-min (L~ z) ; :: thesis: (W-min (L~ z)) .. z < len z
A2: W-max (L~ z) in rng z by Th44;
A3: W-min (L~ z) in rng z by Th43;

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

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

then A4: z /. (len z) = W-max (L~ z) by A1, FINSEQ_6:def 1;
A5: (W-min (L~ z)) .. z in dom z by A3, FINSEQ_4:20;
then A6: (W-min (L~ z)) .. z <= len z by FINSEQ_3:25;
z /. ((W-min (L~ z)) .. z) = z . ((W-min (L~ z)) .. z) by A5, PARTFUN1:def 6
.= W-min (L~ z) by A3, FINSEQ_4:19 ;
then (W-min (L~ z)) .. z <> len z by A4, Th58;
hence (W-min (L~ z)) .. z < len z by A6, XXREAL_0:1; :: thesis: verum

end;

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

(W-max (L~ z)) .. z in dom z by A2, FINSEQ_4:20;
then (W-max (L~ z)) .. z <= len z by FINSEQ_3:25;
hence (W-min (L~ z)) .. z < len z by A1, A7, Th75, XXREAL_0:2; :: thesis: verum

end;

end;