theorem :: FINANCE2:10
for A being SetSequence of NAT st ( for n being Nat holds A . n = {n} ) holds
for n being Nat holds (Partial_Union A) . n in Borel_Sets