set SU = sequence_univers {};
( dom (sequence_univers {}) = NAT & rng (sequence_univers {}) c= union_sequence_univers {} & sequence_univers {} is Function of (dom (sequence_univers {})),(rng (sequence_univers {})) ) by Th93, Def9, FUNCT_2:1;
hence sequence_univers {} is sequence of (union_sequence_univers {}) by FUNCT_2:2; :: thesis: verum