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

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

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

A5: (W-min (L~ z)) .. z in dom z by A1, FINSEQ_4:30;
then A6: (W-min (L~ z)) .. z <= len z by FINSEQ_3:27;
A7: z /. ((W-min (L~ z)) .. z) = z . ((W-min (L~ z)) .. z) by A5, PARTFUN1:def 8
.= W-min (L~ z) by A1, FINSEQ_4:29 ;
z /. (len z) = W-max (L~ z) by A3, A4, FINSEQ_6:def 1;
then (W-min (L~ z)) .. z <> len z by A7, Th62;
hence (W-min (L~ z)) .. z < len z by A6, XXREAL_0:1; :: thesis: verum

end;

suppose A8: 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:30;
then (W-max (L~ z)) .. z <= len z by FINSEQ_3:27;
hence (W-min (L~ z)) .. z < len z by A3, A8, Th79, XXREAL_0:2; :: thesis: verum

end;

end;