theorem Th13: :: PROB_3:13

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