theorem Th9: :: PROB_3:9

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