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