theorem Th105: :: CLASSES4:105

for n being Nat holds sequence_univers . n c= sequence_univers . (n + 1)