:: deftheorem Def12 defines equal-signature PRALG_1:def 13 :
for IT being Function holds
( IT is equal-signature iff for x, y being object st x in dom IT & y in dom IT holds
for U1, U2 being Universal_Algebra st U1 = IT . x & U2 = IT . y holds
signature U1 = signature U2 );