let X be set ; :: thesis:
let P be finite a_partition of X; :: thesis:
let S be Subset of X; :: thesis:

end;

thus ( card (P | S) = card P implies for p being set st p in P holds
p meets S ) by S1, EQREL_1:41; :: thesis:

end;

set PS = P | S;
reconsider Pp1 = P as non empty finite set by S1;

assume A1: for p being set st p in P holds
p meets S ; :: thesis:
consider p being Element of P;
p in Pp1 ;
then p meets S by A1;
then p /\ S in P | S ;
then reconsider PSp1 = P | S as non empty finite set ;
defpred S₁[ set , set ] means ( $1 in P & $2 = $1 /\ S );
P: for x being set st x in P holds
ex y being set st
( y in PSp1 & S₁[x,y] )

let x be set ; :: thesis:
assume A2: x in P ; :: thesis:
take x /\ S ; :: thesis:
x meets S by A2, A1;
hence ( x /\ S in PSp1 & S₁[x,x /\ S] ) by A2; :: thesis:

end;

consider f being Function of P,PSp1 such that
Q: for x being set st x in P holds
S₁[x,f . x] from FUNCT_2:sch 1(P);

let x1, x2 be set ; :: thesis:
assume that
A2: x1 in P and
B2: x2 in P and
C2: f . x1 = f . x2 ; :: thesis:
F2: f . x1 = x1 /\ S by A2, Q;
G2: f . x2 = x2 /\ S by B2, Q;
x1 meets S by A2, A1;
then f . x1 in P | S by F2, A2;
then f . x1 <> {} by EQREL_1:def 6;
then consider x being set such that
H2: x in f . x1 by XBOOLE_0:def 1;
( x in x1 & x in x2 ) by H2, C2, F2, G2, XBOOLE_0:def 4;
then x1 meets x2 by XBOOLE_0:3;
hence x1 = x2 by A2, B2, EQREL_1:def 6; :: thesis:

end;

thus rng f c= PSp1 :: according to XBOOLE_0:def 10 :: thesis:

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng f ; :: thesis:
then consider x being set such that
A2: x in P and
B2: f . x = y by FUNCT_2:17;
x meets S by A1, A2;
then x /\ S in P | S by A2;
hence y in PSp1 by B2, A2, Q; :: thesis:

end;

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in PSp1 ; :: thesis:
then consider p being Element of P such that
A2: y = p /\ S and
p meets S ;
C2: p in Pp1 ;
then f . p = p /\ S by Q;
hence y in rng f by A2, C2, FUNCT_2:6; :: thesis:

end;

end;

assume A1: card (P | S) = card P ; :: thesis:
defpred S₁[ set , set ] means ( $1 in P | S & $2 in Pp1 & $1 = $2 /\ S );
P: for x being set st x in P | S holds
ex y being set st
( y in Pp1 & S₁[x,y] )

let x be set ; :: thesis:
assume A0: x in P | S ; :: thesis:
then consider p being Element of P such that
A1: x = p /\ S and
p meets S ;
take p ; :: thesis:
thus ( p in Pp1 & S₁[x,p] ) by A0, A1; :: thesis:

end;

consider f being Function of (P | S),Pp1 such that
Q: for x being set st x in P | S holds
S₁[x,f . x] from FUNCT_2:sch 1(P);
R: f is one-to-one

let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis:
assume that
A1: x1 in dom f and
B1: x2 in dom f and
C1: f . x1 = f . x2 ; :: thesis:
x1 = (f . x1) /\ S by A1, Q;
hence x1 = x2 by C1, B1, Q; :: thesis:

end;

end;