let D be non empty set ; :: thesis: 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
let R be Equivalence_Relation of D; :: thesis: for y being FinSequence of Class R ex x being FinSequence of D st x is_representatives_FS y
let y be FinSequence of Class R; :: thesis: ex x being FinSequence of D st x is_representatives_FS y
defpred S₁[ set , set ] means for u being Element of D st $2 = u holds
Class R,u = y . $1;
A1: for e being set st e in dom y holds
ex u being set st
( u in D & S₁[e,u] )

proof

let e be set ; :: thesis: ( e in dom y implies ex u being set st
( u in D & S₁[e,u] ) )
assume e in dom y ; :: thesis: ex u being set st
( u in D & S₁[e,u] )
then y . e in rng y by FUNCT_1:def 5;
then consider a being Element of D such that
A2: y . e = Class R,a by EQREL_1:45;
reconsider b = a as set ;
take b ; :: thesis: ( b in D & S₁[e,b] )
thus b in D ; :: thesis: S₁[e,b]
let u be Element of D; :: thesis: ( b = u implies Class R,u = y . e )
assume b = u ; :: thesis: Class R,u = y . e
hence Class R,u = y . e by A2; :: thesis: verum

end;

consider f being Function such that
A3: ( dom f = dom y & rng f c= D & ( for e being set st e in dom y holds
S₁[e,f . e] ) ) from WELLORD2:sch 1(A1);
dom f = Seg (len y) by A3, FINSEQ_1:def 3;
then reconsider f = f as FinSequence by FINSEQ_1:def 2;
reconsider f = f as FinSequence of D by A3, FINSEQ_1:def 4;
take f ; :: thesis: f is_representatives_FS y
thus len f = len y by A3, FINSEQ_3:31; :: according to ALG_1:def 11 :: thesis: for n being Element of NAT st n in dom f holds
Class R,(f . n) = y . n
let n be Element of NAT ; :: thesis: ( n in dom f implies Class R,(f . n) = y . n )
assume A4: n in dom f ; :: thesis: Class R,(f . n) = y . n
then f . n in rng f by FUNCT_1:def 5;
then reconsider u = f . n as Element of D ;
Class R,u = y . n by A3, A4;
hence Class R,(f . n) = y . n ; :: thesis: verum