:: deftheorem Def8 defines i_e_n JORDAN5D:def 8 :
for g being non constant standard special_circular_sequence
for b₂ being Nat holds
( b₂ = i_e_n g iff ( [b₂,(width (GoB g))] in Indices (GoB g) & (GoB g) * (b₂,(width (GoB g))) = N-max (L~ g) ) );