let X be set ; :: thesis: rng (sequence_univers X) c= union_sequence_univers X

now :: thesis: for x being object st x in rng (sequence_univers X) holds
x in union_sequence_univers X

let x be object ; :: thesis: ( x in rng (sequence_univers X) implies x in union_sequence_univers X )
assume x in rng (sequence_univers X) ; :: thesis: x in union_sequence_univers X
then consider y being object such that
A1: y in dom (sequence_univers X) and
A2: x = (sequence_univers X) . y by FUNCT_1:def 3;
reconsider x9 = x as set by TARSKI:1;
y in NAT by A1, Def9;
then reconsider y = y as Nat ;

now :: thesis: ( x9 in (sequence_univers X) . (y + 1) & (sequence_univers X) . (y + 1) in rng (sequence_univers X) )

(sequence_univers X) . (y + 1) = GrothendieckUniverse x9 by A2, Def9;
hence x9 in (sequence_univers X) . (y + 1) by CLASSES3:def 4; :: thesis: (sequence_univers X) . (y + 1) in rng (sequence_univers X)
y + 1 in NAT ;
then y + 1 in dom (sequence_univers X) by Def9;
hence (sequence_univers X) . (y + 1) in rng (sequence_univers X) by FUNCT_1:3; :: thesis: verum

end;

hence x in union_sequence_univers X by TARSKI:def 4; :: thesis: verum

end;

hence rng (sequence_univers X) c= union_sequence_univers X ; :: thesis: verum