theorem Th17: :: PROB_3:17

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