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

proof

assume {} in rng f ; :: thesis: contradiction
then consider x being object such that
A2: ( x in dom f & {} = f . x ) by FUNCT_1:def 3;
{} = {x} by A1, A2;
hence contradiction ; :: thesis: verum

end;

hence f is non-empty ; :: thesis: f is disjoint_valued
for x, y being object st x <> y holds
f . x misses f . y

proof

let x, y be object ; :: thesis: ( x <> y implies f . x misses f . y )
assume A3: x <> y ; :: thesis: f . x misses f . y

per cases ( not x in dom f or not y in dom f or ( x in dom f & y in dom f ) ) ;

suppose ( not x in dom f or not y in dom f ) ; :: thesis: f . x misses f . y

then ( f . x = {} or f . y = {} ) by FUNCT_1:def 2;
then (f . x) /\ (f . y) = {} ;
hence f . x misses f . y by XBOOLE_0:def 7; :: thesis: verum

end;

suppose ( x in dom f & y in dom f ) ; :: thesis: f . x misses f . y

then A4: ( f . x = {x} & f . y = {y} ) by A1;
{x} /\ {y} = {}

proof

assume {x} /\ {y} <> {} ; :: thesis: contradiction
then consider z being object such that
A5: z in {x} /\ {y} by XBOOLE_0:def 1;
( z in {x} & z in {y} ) by A5, XBOOLE_0:def 4;
then ( z = x & z = y ) by TARSKI:def 1;
hence contradiction by A3; :: thesis: verum

end;

hence f . x misses f . y by A4, XBOOLE_0:def 7; :: thesis: verum

end;

end;

end;

hence f is disjoint_valued ; :: thesis: verum