:: deftheorem defines is_representatives_FS FINSEQ_3:def 4 :
for D being non empty set
for R being Equivalence_Relation of D
for y being FinSequence of Class R
for x being FinSequence of D holds
( x is_representatives_FS y iff ( len x = len y & ( for n being Nat st n in dom x holds
Class (R,(x . n)) = y . n ) ) );