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