let X be FinSequence-membered set ; :: thesis: ex Y being non empty set st X c= Y *
set Z = { (rng f) where f is Element of X : f in X } ;
take Y = succ (union { (rng f) where f is Element of X : f in X } ); :: thesis: X c= Y *
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Y * )
assume Z: x in X ; :: thesis: x in Y *
then reconsider x = x as FinSequence by Def19;
A: union { (rng f) where f is Element of X : f in X } c= Y by ORDINAL3:1;
rng x in { (rng f) where f is Element of X : f in X } by Z;
then rng x c= union { (rng f) where f is Element of X : f in X } by SETFAM_1:56;
then rng x c= Y by A, XBOOLE_1:1;
then x is FinSequence of Y by Def4;
hence x in Y * by Def11; :: thesis: verum