theorem Th100: :: CLASSES4:100

for n being Nat holds (sequence_univers FinSETS) . n = UNIVERSE n