let h be non constant standard special_circular_sequence; :: thesis: for i being Element of NAT st 1 <= i & i <= len h holds
( W-bound (L~ h) <= (h /. i) `1 & (h /. i) `1 <= E-bound (L~ h) )
let i be Element of NAT ; :: thesis: ( 1 <= i & i <= len h implies ( W-bound (L~ h) <= (h /. i) `1 & (h /. i) `1 <= E-bound (L~ h) ) )
A1: len h > 4 by GOBOARD7:36;
assume ( 1 <= i & i <= len h ) ; :: thesis: ( W-bound (L~ h) <= (h /. i) `1 & (h /. i) `1 <= E-bound (L~ h) )
then i in dom h by FINSEQ_3:27;
then h /. i in L~ h by A1, GOBOARD1:16, XXREAL_0:2;
hence ( W-bound (L~ h) <= (h /. i) `1 & (h /. i) `1 <= E-bound (L~ h) ) by PSCOMP_1:71; :: thesis: verum