for X being non empty set
for P being a_partition of X
for p being FinSequence of P
for q1, q2 being FinSequence
for x, y being set st (q1 ^ <*x*>) ^ q2 in product p & ex a being Element of P st
( x in a & y in a ) holds
(q1 ^ <*y*>) ^ q2 in product p