deffunc H₂( object ) -> set = {S};
consider f being Function such that
A1: ( dom f = S & ( for x being object st x in S holds
f . x = H₂(x) ) ) from FUNCT_1:sch 3();
reconsider f = f as ManySortedSet of S by A1, RELAT_1:def 18, PARTFUN1:def 2;
take f ; :: thesis: ( f is disjoint_valued & f is non-empty )
thus f is disjoint_valued :: thesis: f is non-empty

proof

let x, y be object ; :: according to PROB_2:def 2 :: thesis: ( x = y or f . x misses f . y )
assume A2: x <> y ; :: thesis: f . x misses f . y
( ( x in S or x nin S ) & ( y in S or y nin S ) ) ;
then ( ( f . x = {x} or f . x = {} ) & ( f . y = {y} or f . y = {} ) ) by A1, FUNCT_1:def 2;
hence f . x misses f . y by A2, ZFMISC_1:11; :: thesis: verum

end;

let x be object ; :: according to PBOOLE:def 13 :: thesis: ( not x in S or not f . x is empty )
assume x in S ; :: thesis: not f . x is empty
then f . x = {x} by A1;
hence not f . x is empty ; :: thesis: verum