let A be Universal_Algebra; :: thesis: 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) #)
let f be Function of (dom (signature A)),({0} *); :: thesis: for z being Element of {0} st f = (*--> 0) * (signature A) holds
MSSign A = ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #)
let z be Element of {0}; :: thesis: ( f = (*--> 0) * (signature A) implies MSSign A = ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) )
A1: ( the carrier' of (MSSign A) = dom (signature A) & the Arity of (MSSign A) = (*--> 0) * (signature A) ) by Def8;
( z = 0 & the carrier of (MSSign A) = {0} ) by Def8, TARSKI:def 1;
hence ( f = (*--> 0) * (signature A) implies MSSign A = ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) ) by A1, Def8; :: thesis: verum