set c = ConstOSSet (S,z);
deffunc H1( 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 = H1(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 object 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
object ;
( 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
;
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 = H1(
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;
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); ( 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 Def18; for o being OperSymbol of S holds Den (o,T) = (Args (o,T)) --> z1
let o be OperSymbol of S; Den (o,T) = (Args (o,T)) --> z1
Den (o,T) =
the Charact of T . o
by MSUALG_1:def 6
.=
ch3 . o
by Def18
.=
((((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
; verum