let n be Nat; :: thesis: sequence_univers . (n + 1) = UNIVERSE n
( sequence_univers . (n + 1) = GrothendieckUniverse ((sequence_univers {}) . n) & UNIVERSE n = (sequence_univers (GrothendieckUniverse {})) . n ) by Th46, Th100, Def9;
hence sequence_univers . (n + 1) = UNIVERSE n by Th101; :: thesis: verum