set c = ConstOSSet (S,z);
deffunc H₁( Element of the carrier' of S) -> Element of K10(K11(((((ConstOSSet (S,z)) #) * the Arity of S) . $1),{z1})) = ((((ConstOSSet (S,z)) #) * the Arity of S) . $1) --> z1;
consider ch2 being Function such that
A1: ( dom ch2 = the carrier' of S & ( for x being Element of the carrier' of S holds ch2 . x = H₁(x) ) ) from FUNCT_1:sch 4();
reconsider ch4 = ch2 as ManySortedSet of the carrier' of S by A1, PARTFUN1:def 2, RELAT_1:def 18;
for i being set st i in the carrier' of S holds
ch4 . i is Function of ((((ConstOSSet (S,z)) #) * the Arity of S) . i),(((ConstOSSet (S,z)) * the ResultSort of S) . i)

proof

let i be set ; :: thesis: ( i in the carrier' of S implies ch4 . i is Function of ((((ConstOSSet (S,z)) #) * the Arity of S) . i),(((ConstOSSet (S,z)) * the ResultSort of S) . i) )
assume i in the carrier' of S ; :: thesis: ch4 . i is Function of ((((ConstOSSet (S,z)) #) * the Arity of S) . i),(((ConstOSSet (S,z)) * the ResultSort of S) . i)
then reconsider o = i as OperSymbol of S ;
the ResultSort of S . o in the carrier of S ;
then A2: o in the ResultSort of S " the carrier of S by FUNCT_2:38;
((ConstOSSet (S,z)) * the ResultSort of S) . o = (( the ResultSort of S " the carrier of S) --> z) . o by FUNCOP_1:19
.= z by A2, FUNCOP_1:7 ;
then A3: {z1} c= ((ConstOSSet (S,z)) * the ResultSort of S) . i by ZFMISC_1:31;
ch4 . i = H₁(o) by A1;
hence ch4 . i is Function of ((((ConstOSSet (S,z)) #) * the Arity of S) . i),(((ConstOSSet (S,z)) * the ResultSort of S) . i) by A3, FUNCT_2:7; :: thesis: verum

end;

then reconsider ch3 = ch4 as ManySortedFunction of ((ConstOSSet (S,z)) #) * the Arity of S,(ConstOSSet (S,z)) * the ResultSort of S by PBOOLE:def 15;
take T = ConstOSA (S,z,ch3); :: thesis: ( the Sorts of T = ConstOSSet (S,z) & ( for o being OperSymbol of S holds Den (o,T) = (Args (o,T)) --> z1 ) )
thus A4: the Sorts of T = ConstOSSet (S,z) by Def20; :: thesis: for o being OperSymbol of S holds Den (o,T) = (Args (o,T)) --> z1
let o be OperSymbol of S; :: thesis: Den (o,T) = (Args (o,T)) --> z1
Den (o,T) = the Charact of T . o by MSUALG_1:def 6
.= ch3 . o by Def20
.= ((((ConstOSSet (S,z)) #) * the Arity of S) . o) --> z1 by A1
.= (Args (o,T)) --> z1 by A4, MSUALG_1:def 4 ;
hence Den (o,T) = (Args (o,T)) --> z1 ; :: thesis: verum