let f be V22() standard special_circular_sequence; :: thesis: ( f /. 1 = N-min (L~ f) implies (W-max (L~ f)) .. f < len f )
assume A1: f /. 1 = N-min (L~ f) ; :: thesis: (W-max (L~ f)) .. f < len f
then A2: f /. (len f) = N-min (L~ f) by FINSEQ_6:def 1;
A3: W-max (L~ f) in rng f by Th44;
then (W-max (L~ f)) .. f in dom f by FINSEQ_4:20;
then A4: f /. ((W-max (L~ f)) .. f) = f . ((W-max (L~ f)) .. f) by PARTFUN1:def 6
.= W-max (L~ f) by A3, FINSEQ_4:19 ;
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 A1, FINSEQ_6:43;
hence (W-max (L~ f)) .. f < len f by GOBOARD7:34, 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 A3, FINSEQ_4:21;
hence (W-max (L~ f)) .. f < len f by A2, A4, A5, XXREAL_0:1; :: thesis: verum
end;
end;