:: deftheorem Def2 defines IndexedPartition PUA2MSS1:def 2 :
for X being set
for b₂ being Function holds
( b₂ is IndexedPartition of X iff ( rng b₂ is a_partition of X & b₂ is one-to-one ) );