theorem Th101: :: CLASSES4:101

for n being Nat holds GrothendieckUniverse ((sequence_univers {}) . n) = (sequence_univers (GrothendieckUniverse {})) . n