theorem Th3: :: CARDFIL3:4
for I, X being non empty set
for x being b2 -valued ManySortedSet of I
for p, q being FinSequence of I holds (p ^ q) * x = (p * x) ^ (q * x)