deffunc H₁( object ) -> set = {$1};
consider f being ManySortedSet of the carrier of S such that
A1: for i being object st i in the carrier of S holds
f . i = H₁(i) from PBOOLE:sch 4();
set Ch = the ManySortedFunction of (f #) * the Arity of S,f * the ResultSort of S;
take MSAlgebra(# f, the ManySortedFunction of (f #) * the Arity of S,f * the ResultSort of S #) ; :: thesis: for i being set st i in the carrier of S holds
the Sorts of MSAlgebra(# f, the ManySortedFunction of (f #) * the Arity of S,f * the ResultSort of S #) . i = {i}
thus for i being set st i in the carrier of S holds
the Sorts of MSAlgebra(# f, the ManySortedFunction of (f #) * the Arity of S,f * the ResultSort of S #) . i = {i} by A1; :: thesis: verum