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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Y * )
assume A1: x in X ; :: thesis: x in Y *
then reconsider x = x as FinSequence by Def18;
rng x in { (rng f) where f is Element of X : f in X } by A1;
then rng x c= Y by ORDINAL3:1, SETFAM_1:41;
then x is FinSequence of Y by Def4;
hence x in Y * by Def11; :: thesis: verum