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 3;
then consider a being Element of D such that
A2: y . e = Class (R,a) by EQREL_1:36;
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 FUNCT_1:sch 5(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, Th31; :: according to FINSEQ_3:def 4 :: 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 3;
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