deffunc H₂( object ) -> set = {S};
consider X being ManySortedSet of S such that
A1: for x being object st x in the carrier of S holds
X . x = H₂(x) from PBOOLE:sch 4();
set o = the ManySortedFunction of (X #) * the Arity of S,X * the ResultSort of S;
take A = MSAlgebra(# X, the ManySortedFunction of (X #) * the Arity of S,X * the ResultSort of S #); :: thesis: ( A is trivial & A is disjoint_valued & A is non-empty )
thus the Sorts of A is trivial-yielding :: according to MSAFREE4:def 3 :: thesis: ( A is disjoint_valued & A is non-empty )

proof

let x be set ; :: according to MSAFREE4:def 2 :: thesis: ( x in the carrier of S implies the Sorts of A . x is trivial )
assume x in the carrier of S ; :: thesis: the Sorts of A . x is trivial
then X . x = H₂(x) by A1;
hence the Sorts of A . x is trivial ; :: thesis: verum

end;

thus the Sorts of A is disjoint_valued :: according to MSAFREE1:def 2 :: thesis: A is non-empty

proof

let x, y be object ; :: according to PROB_2:def 2 :: thesis: ( x = y or the Sorts of A . x misses the Sorts of A . y )
assume A2: x <> y ; :: thesis: the Sorts of A . x misses the Sorts of A . y
( ( x in the carrier of S or x nin the carrier of S ) & ( y in the carrier of S or y nin the carrier of S ) & dom the Sorts of A = the carrier of S ) by PARTFUN1:def 2;
then ( ( H₂(x) = X . x or X . x = {} ) & ( H₂(y) = X . y or X . y = {} ) ) by A1, FUNCT_1:def 2;
hence the Sorts of A . x misses the Sorts of A . y by A2, ZFMISC_1:11; :: thesis: verum

end;

thus the Sorts of A is non-empty :: according to MSUALG_1:def 3 :: thesis: verum

proof

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

end;

thus verum ; :: thesis: verum