theorem Th16: :: SETLIM_2:16

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