theorem Th8: :: PROB_3:8

for n being Nat
for X being set
for A1 being SetSequence of X holds (Partial_Intersection A1) . n c= A1 . n