theorem Th98: :: CLASSES4:98

for n being Nat holds Tarski-Class ((sequence_univers FinSETS) . n) = GrothendieckUniverse ((sequence_univers FinSETS) . n)