let f be non constant standard special_circular_sequence; :: thesis: ex i being Element of 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:47; :: thesis: ( i < len (GoB f) & N-min (L~ f) = (GoB f) * i,(width (GoB f)) )
i_e_n f <= len (GoB f) by JORDAN5D:47;
hence i < len (GoB f) by Th44, 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