theorem Th16: :: PROB_3:16

for n being Nat
for x being object
for X being set
for A1 being SetSequence of X holds
( x in (Partial_Diff_Union A1) . n iff ( x in A1 . n & ( for k being Nat st k < n holds
not x in A1 . k ) ) )