set c = ConstOSSet S,z;
deffunc H₁( Element of the carrier' of S) -> Element of K6(K7(((((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 4, 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:46;
((ConstOSSet S,z) * the ResultSort of S) . o = ((the ResultSort of S " the carrier of S) --> z) . o by FUNCOP_1:25
.= z by A2, FUNCOP_1:13 ;
then A3: {z1} c= ((ConstOSSet S,z) * the ResultSort of S) . i by ZFMISC_1:37;
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:9; :: 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 18;
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 11
.= ch3 . o by Def20
.= ((((ConstOSSet S,z) # ) * the Arity of S) . o) --> z1 by A1
.= (Args o,T) --> z1 by A4, MSUALG_1:def 9 ;
hence Den o,T = (Args o,T) --> z1 ; :: thesis: verum