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) #) )
z = 0 by TARSKI:def 1;
then ( the carrier of (MSSign A) = {0 } & the carrier' of (MSSign A) = dom (signature A) & the Arity of (MSSign A) = (*--> 0 ) * (signature A) & the ResultSort of (MSSign A) = (dom (signature A)) --> z ) by Def13;
hence ( f = (*--> 0 ) * (signature A) implies MSSign A = ManySortedSign(# {0 },(dom (signature A)),f,((dom (signature A)) --> z) #) ) ; :: thesis: verum