:: deftheorem Def9 defines chop FSM_3:def 9 :
for E being non empty set
for u, v, b₄ being Element of E ^omega holds
( ( ex w being Element of E ^omega st w ^ v = u implies ( b₄ = chop (u,v) iff for w being Element of E ^omega st w ^ v = u holds
b₄ = w ) ) & ( ( for w being Element of E ^omega holds not w ^ v = u ) implies ( b₄ = chop (u,v) iff b₄ = u ) ) );