let X be set ; :: thesis:
let P be a_partition of X; :: thesis:
defpred S₂[ object , object ] means ex D1 being set st
( D1 = $1 & $2 = the Element of D1 );
A1: for e being object st e in P holds
ex u being object st S₂[e,u]

let e be object ; :: thesis:
assume e in P ; :: thesis:
reconsider ee = e as set by TARSKI:1;
take u = the Element of ee; :: thesis:
thus S₂[e,u] ; :: thesis:

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: f is one-to-one

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A5: x1 in dom f and
A6: x2 in dom f and
A7: f . x1 = f . x2 ; :: thesis:
A8: x1 <> {} by A2, A5;
A9: x2 <> {} by A2, A6;
reconsider xx1 = x1, xx2 = x2 as set by TARSKI:1;
( S₂[x1,f . x1] & S₂[x2,f . x2] ) by A5, A6, A2, A3;
then ( f . x1 = the Element of xx1 & f . x2 = the Element of xx2 ) ;
then xx1 meets xx2 by A7, A8, A9, XBOOLE_0:3;
hence x1 = x2 by A5, A6, A2, EQREL_1:def 4; :: thesis:

end;

rng f c= X

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng f ; :: thesis:
then consider x being object such that
A10: x in dom f and
A11: y = f . x by FUNCT_1:def 3;
reconsider x = x as set by TARSKI:1;
S₂[x,f . x] by A2, A3, A10;
then A12: f . x = the Element of x ;
x <> {} by A2, A10;
then f . x in x by A12;
hence y in X by A10, A2, A11; :: thesis:

end;