theorem :: FINSEQ_1:85

for X being FinSequence-membered set ex Y being non empty set st X c= Y *