theorem Th18: :: PROB_3:18

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