let R be with_finite_stability# RelStr ; :: thesis:
let A be StableSet of R; :: thesis:
let C be Clique-partition of R; :: thesis:
assume A1: card C = card A ; :: thesis:
set cR = the carrier of R;

per cases ;

suppose A2: R is empty ; :: thesis:

then the carrier of R is empty ;
then A3: C = {} ;
set f = the Function of A,C;
dom the Function of A,C = {} by A2;
then reconsider f = {} as Function of A,C by RELAT_1:41;
A4: f is onto by A3, FUNCT_2:def 3, RELAT_1:38;
take f ; :: thesis:
thus f is bijective by A4; :: thesis:
thus for x being set st x in A holds
x in f . x ; :: thesis:

end;

suppose A5: not R is empty ; :: thesis:

defpred S₁[ object , object ] means ex D2 being set st
( D2 = $2 & $1 in A & $2 in C & $1 in D2 );
A6: for x being object st x in A holds
ex y being object st
( y in C & S₁[x,y] )

proof

let x be object ; :: thesis:
assume A7: x in A ; :: thesis:
then reconsider x9 = x as Element of R ;
not the carrier of R is empty by A5;
then x9 in the carrier of R ;
then x9 in union C by EQREL_1:def 4;
then consider y being set such that
A8: x in y and
A9: y in C by TARSKI:def 4;
take y ; :: thesis:
thus ( y in C & S₁[x,y] ) by A7, A8, A9; :: thesis:

end;

consider f being Function of A,C such that
A10: for x being object st x in A holds
S₁[x,f . x] from FUNCT_2:sch 1(A6);
take f ; :: thesis:
A11: f is one-to-one

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A12: x1 in dom f and
A13: x2 in dom f and
A14: f . x1 = f . x2 ; :: thesis:
S₁[x1,f . x1] by A12, A10;
then A15: x1 in f . x1 ;
S₁[x2,f . x2] by A13, A10;
then A16: x2 in f . x2 ;
f . x1 in C by A5, A12, FUNCT_2:5;
then f . x1 is Clique of R by Def11;
hence x1 = x2 by A12, A13, A15, A16, A14, Th15; :: thesis:

end;

C is finite by A1;
then f is onto by A1, A11, FINSEQ_4:63;
hence f is bijective by A11; :: thesis:
let x be set ; :: thesis:
assume x in A ; :: thesis:
then S₁[x,f . x] by A10;
hence x in f . x ; :: thesis:

end;

end;