let f be constant standard special_circular_sequence; :: thesis: ex i being Nat st
( 1 <= i & i < len (GoB f) & N-min (L~ f) = (GoB f) * (i,(width (GoB f))) )
take i = i_w_n f; :: thesis: ( 1 <= i & i < len (GoB f) & N-min (L~ f) = (GoB f) * (i,(width (GoB f))) )
thus 1 <= i by JORDAN5D:45; :: thesis: ( i < len (GoB f) & N-min (L~ f) = (GoB f) * (i,(width (GoB f))) )
i_e_n f <= len (GoB f) by JORDAN5D:45;
hence i < len (GoB f) by Th27, XXREAL_0:2; :: thesis: N-min (L~ f) = (GoB f) * (i,(width (GoB f)))
thus N-min (L~ f) = (GoB f) * (i,(width (GoB f))) by JORDAN5D:def 7; :: thesis: verum