let A be non empty finite set ; :: thesis:
let PA1, PA2 be a_partition of A; :: thesis:
defpred S₁[ object , object ] means ex A, B being set st
( A = $1 & B = $2 & A c= B );
assume that
A1: PA1 is_finer_than PA2 and
A2: card PA1 = card PA2 ; :: thesis:
A3: for e being object st e in PA1 holds
ex u being object st
( u in PA2 & S₁[e,u] )

let e be object ; :: thesis:
reconsider ee = e as set by TARSKI:1;
assume e in PA1 ; :: thesis:
then ee in PA1 ;
then ex u being set st
( u in PA2 & ee c= u ) by SETFAM_1:def 2, A1;
hence ex u being object st
( u in PA2 & S₁[e,u] ) ; :: thesis:

end;

consider f being Function of PA1,PA2 such that
A4: for e being object st e in PA1 holds
S₁[e,f . e] from FUNCT_2:sch 1(A3);
A5: dom f = PA1 by FUNCT_2:def 1;
A6: PA2 c= rng f

let p2 be object ; :: according to TARSKI:def 3 :: thesis:
assume p2 in PA2 ; :: thesis:
then reconsider p29 = p2 as Element of PA2 ;
consider p1 being Element of PA1 such that
A7: p1 c= p29 by A1, Th88;
reconsider fp1 = f . p1 as Subset of A by TARSKI:def 3;
S₁[p1,f . p1] by A4;
then A8: p1 c= f . p1 ;
p29 meets f . p1

end;

end;

let x be Element of PA1; :: thesis:
reconsider fx = f . x as Subset of A by TARSKI:def 3;
consider E1 being Equivalence_Relation of A such that
A11: PA1 = Class E1 by EQREL_1:34;
assume x <> f . x ; :: thesis:
then consider a being object such that
A12: ( ( a in x & not a in f . x ) or ( a in f . x & not a in x ) ) by TARSKI:2;
A13: fx c= A ;
then A14: a in Class (E1,a) by A12, EQREL_1:20;
reconsider CE1a = Class (E1,a) as Element of PA1 by A13, A12, A11, EQREL_1:def 3;
reconsider fCE1a = f . CE1a as Subset of A by TARSKI:def 3;
S₁[x,f . x] by A4;
then A15: x c= f . x ;
S₁[CE1a,f . CE1a] by A4;
then CE1a c= f . CE1a ;
then fx meets fCE1a by A15, A12, A14, XBOOLE_0:3;
then fx = fCE1a by EQREL_1:def 4;
hence contradiction by A5, A9, A15, A12, A14; :: thesis:

end;

assume x in PA1 ; :: thesis:
then reconsider x9 = x as Element of PA1 ;
set fx = f . x9;
f . x9 in PA2 ;
hence x in PA2 by A10; :: thesis:

end;

assume x in PA2 ; :: thesis:
then consider y being object such that
A16: y in dom f and
A17: x = f . y by A6, FUNCT_1:def 3;
reconsider y9 = y as Element of PA1 by A16, FUNCT_2:def 1;
y9 = f . y9 by A10;
hence x in PA1 by A17; :: thesis:

end;