theorem Th4: :: SETLIM_2:4

for k being Nat
for X being set
for A1, A2 being SetSequence of X holds (A1 (/\) A2) ^\ k = (A1 ^\ k) (/\) (A2 ^\ k)