:: deftheorem defines -prefix FOMODEL0:def 19 :
for U being non empty set
for X being set holds
( X is U -prefix iff for p1, q1, p2, q2 being b₁ -valued FinSequence st p1 in X & p2 in X & p1 ^ q1 = p2 ^ q2 holds
( p1 = p2 & q1 = q2 ) );