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