theorem Th12: :: PUA2MSS1:13

for X being set
for p being FinSequence of SmallestPartition X ex q being FinSequence of X st product p = {q}