deffunc H₁( Element of S) -> a_partition of the Sorts of U1 . $1 = Class (R . $1);
consider f being Function such that
A1: ( dom f = the carrier of S & ( for d being Element of S holds f . d = H₁(d) ) ) from FUNCT_1:sch 4();
reconsider f = f as ManySortedSet of the carrier of S by A1, PARTFUN1:def 2, RELAT_1:def 18;
for i being object st i in the carrier of S holds
not f . i is empty

proof

let i be object ; :: thesis: ( i in the carrier of S implies not f . i is empty )
assume i in the carrier of S ; :: thesis: not f . i is empty
then reconsider s = i as Element of S ;
consider x being object such that
A2: x in the Sorts of U1 . s by XBOOLE_0:def 1;
reconsider y = x as Element of the Sorts of U1 . s by A2;
f . s = Class (R . s) by A1;
then Class ((R . s),y) in f . s by EQREL_1:def 3;
hence not f . i is empty ; :: thesis: verum

end;

then reconsider f = f as non-empty ManySortedSet of the carrier of S by PBOOLE:def 13;
take f ; :: thesis: for s being Element of S holds f . s = Class (R . s)
thus for s being Element of S holds f . s = Class (R . s) by A1; :: thesis: verum