deffunc H₁( object ) -> set = {( the Sorts of A . $1)};
consider V being ManySortedSet of the carrier of S such that
A1: for s being object st s in the carrier of S holds
V . s = H₁(s) from PBOOLE:sch 4();
V is non-empty

proof

let s be object ; :: according to PBOOLE:def 13 :: thesis: ( not s in the carrier of S or not V . s is empty )
assume s in the carrier of S ; :: thesis: not V . s is empty
then V . s = {( the Sorts of A . s)} by A1;
hence not V . s is empty ; :: thesis: verum

end;

then reconsider V = V as non-empty ManySortedSet of the carrier of S ;
take V ; :: thesis: V misses the Sorts of A
let s be object ; :: according to PBOOLE:def 8 :: thesis: ( not s in the carrier of S or V . s misses the Sorts of A . s )
assume s in the carrier of S ; :: thesis: V . s misses the Sorts of A . s
then A2: V . s = {( the Sorts of A . s)} by A1;

now :: thesis: for x being object st x in V . s holds
not x in the Sorts of A . s

let x be object ; :: thesis: ( x in V . s implies not x in the Sorts of A . s )
assume x in V . s ; :: thesis: not x in the Sorts of A . s
then A: x = the Sorts of A . s by A2, TARSKI:def 1;
then reconsider xx = x as set ;
not xx in xx ;
hence not x in the Sorts of A . s by A; :: thesis: verum

end;

hence V . s misses the Sorts of A . s by XBOOLE_0:3; :: thesis: verum