theorem :: MSUALG_1:10

for A being Universal_Algebra
for f being Function of (dom (signature A)),({0} *)
for z being Element of {0} st f = (*--> 0) * (signature A) holds
MSSign A = ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #)