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

proof

let s be set ; :: 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 V16() ManySortedSet of the carrier of S ;
take V ; :: thesis: V misses the Sorts of A
let s be set ; :: 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

let x be set ; :: 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 x = the Sorts of A . s by A2, TARSKI:def 1;
hence not x in the Sorts of A . s ; :: thesis: verum

end;

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