theorem Th104: :: CLASSES4:104

for n being Nat holds sequence_univers . (n + 1) in GrothendieckUniverse sequence_univers