deffunc H2( 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 = H2(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 V276() :: 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 = H2(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 ( ( H2(x) = X . x or X . x = {} ) & ( H2(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 V5() :: 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 = H2(x) by A1;
hence not the Sorts of A . x is empty ; :: thesis: verum
end;
thus verum ; :: thesis: verum