theorem Th42: :: HILB10_7:42

for P1, P2, S1 being FinSequence-membered set holds (P1 \/ P2) ^ S1 = (P1 ^ S1) \/ (P2 ^ S1)