:: deftheorem Def3 defines -index_of PUA2MSS1:def 3 :
for X being set
for P being IndexedPartition of X
for x being object st x in X holds
for b₄ being set holds
( b₄ = P -index_of x iff ( b₄ in dom P & x in P . b₄ ) );