theorem Th4: :: PUA2MSS1:5

for X being set
for P, Q being a_partition of X
for f being Function of P,Q st ( for a being set st a in P holds
a c= f . a ) holds
for p being FinSequence of P
for q being FinSequence of Q holds
( product p c= product q iff f * p = q )