theorem ThA: :: FINANCE2:14

for AA being SetSequence of REAL ex A being SetSequence of REAL st
for n being Nat holds A . n = (Partial_Union AA) . n