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₁[ object , object ] means for u being Element of D st $2 = u holds
Class (R,u) = y . $1;
A1: for e being object st e in dom y holds
ex u being object st
( u in D & S₁[e,u] )

proof

let e be object ; :: thesis: ( e in dom y implies ex u being object st
( u in D & S₁[e,u] ) )
assume e in dom y ; :: thesis: ex u being object 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;
take a ; :: thesis: ( a in D & S₁[e,a] )
thus a in D ; :: thesis: S₁[e,a]
let u be Element of D; :: thesis: ( a = u implies Class (R,u) = y . e )
assume a = 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 object st e in dom y holds
S₁[e,f . e] ) ) from FUNCT_1:sch 6(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, Th27; :: according to FINSEQ_3:def 4 :: thesis: for n being Nat st n in dom f holds
Class (R,(f . n)) = y . n
let n be 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