theorem Th3: :: CARDFIL3:4

for I, X being non empty set
for x being b₂ -valued ManySortedSet of I
for p, q being FinSequence of I holds (p ^ q) * x = (p * x) ^ (q * x)