defpred S₂[ object , object ] means ex D1 being set st
( D1 = X & P = D1 /\ S );
A1: for e being object st e in P holds
ex u being object st S₂[e,u]

proof

let e be object ; :: thesis: ( e in P implies ex u being object st S₂[e,u] )
assume e in P ; :: thesis: ex u being object st S₂[e,u]
reconsider ee = e as set by TARSKI:1;
take ee /\ S ; :: thesis: S₂[e,ee /\ S]
thus S₂[e,ee /\ S] ; :: thesis: verum

end;

consider f being Function such that
A2: dom f = P and
A3: for e being object st e in P holds
S₂[e,f . e] from CLASSES1:sch 1(A1);
A4: rng f is finite by A2, FINSET_1:8;
P | S c= rng f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P | S or x in rng f )
assume x in P | S ; :: thesis: x in rng f
then consider xx being Element of P such that
A5: x = xx /\ S and
A6: xx meets S ;
consider y being object such that
y in xx and
A7: y in S by A6, XBOOLE_0:3;
reconsider Xp1 = X as non empty set by A7;
A8: P is a_partition of Xp1 ;
then S₂[xx,f . xx] by A3;
then x = f . xx by A5;
hence x in rng f by A8, A2, FUNCT_1:def 3; :: thesis: verum

end;

hence P | S is finite by A4; :: thesis: verum