theorem Th2: :: SETLIM_2:2

for n being Nat
for X being set
for A1 being SetSequence of X holds (superior_setsequence A1) . n = Union (A1 ^\ n)