:: deftheorem Def6 defines i_e_s JORDAN5D:def 6 :
for g being non constant standard special_circular_sequence
for b₂ being Nat holds
( b₂ = i_e_s g iff ( [b₂,1] in Indices (GoB g) & (GoB g) * (b₂,1) = S-max (L~ g) ) );