theorem :: FINSEQ_3:122

for D being non empty set
for R being Equivalence_Relation of D
for y being FinSequence of Class R ex x being FinSequence of D st x is_representatives_FS y