A1: ( dom (sequence_univers X) = NAT & (sequence_univers X) . 0 = X & ( for n being Nat holds (sequence_univers X) . (n + 1) = GrothendieckUniverse ((sequence_univers X) . n) ) ) by Def9;
set Y = (sequence_univers X) . (0 + 1);
(sequence_univers X) . (0 + 1) = GrothendieckUniverse ((sequence_univers X) . 0) by Def9;
then not (sequence_univers X) . (0 + 1) is empty ;
then consider x being object such that
A2: x in (sequence_univers X) . (0 + 1) ;
(sequence_univers X) . (0 + 1) in rng (sequence_univers X) by A1, FUNCT_1:3;
hence union (rng (sequence_univers X)) is non empty set by A2, TARSKI:def 4; :: thesis: verum