let h be non constant standard special_circular_sequence; :: thesis: for i being Nat st 1 <= i & i <= len h holds

( S-bound (L~ h) <= (h /. i) `2 & (h /. i) `2 <= N-bound (L~ h) )

let i be Nat; :: thesis: ( 1 <= i & i <= len h implies ( S-bound (L~ h) <= (h /. i) `2 & (h /. i) `2 <= N-bound (L~ h) ) )

A1: len h > 4 by GOBOARD7:34;

assume that

A2: 1 <= i and

A3: i <= len h ; :: thesis: ( S-bound (L~ h) <= (h /. i) `2 & (h /. i) `2 <= N-bound (L~ h) )

i in dom h by A2, A3, FINSEQ_3:25;

then h /. i in L~ h by A1, GOBOARD1:1, XXREAL_0:2;

hence ( S-bound (L~ h) <= (h /. i) `2 & (h /. i) `2 <= N-bound (L~ h) ) by PSCOMP_1:24; :: thesis: verum

( S-bound (L~ h) <= (h /. i) `2 & (h /. i) `2 <= N-bound (L~ h) )

let i be Nat; :: thesis: ( 1 <= i & i <= len h implies ( S-bound (L~ h) <= (h /. i) `2 & (h /. i) `2 <= N-bound (L~ h) ) )

A1: len h > 4 by GOBOARD7:34;

assume that

A2: 1 <= i and

A3: i <= len h ; :: thesis: ( S-bound (L~ h) <= (h /. i) `2 & (h /. i) `2 <= N-bound (L~ h) )

i in dom h by A2, A3, FINSEQ_3:25;

then h /. i in L~ h by A1, GOBOARD1:1, XXREAL_0:2;

hence ( S-bound (L~ h) <= (h /. i) `2 & (h /. i) `2 <= N-bound (L~ h) ) by PSCOMP_1:24; :: thesis: verum