theorem Th41: :: HILB10_7:41

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