let U1, U2 be Universal_Algebra; :: thesis: ( UAStr(# the carrier of U1, the charact of U1 #) = UAStr(# the carrier of U2, the charact of U2 #) implies signature U1 = signature U2 )
assume A1: UAStr(# the carrier of U1, the charact of U1 #) = UAStr(# the carrier of U2, the charact of U2 #) ; :: thesis: signature U1 = signature U2
A2: len (signature U2) = len the charact of U1 by A1, UNIALG_1:def 4;
for i being natural number st i in dom (signature U2) holds
for h being non empty homogeneous PartFunc of ( the carrier of U1 *), the carrier of U1 st h = the charact of U1 . i holds
(signature U2) . i = arity h by A1, UNIALG_1:def 4;
hence signature U1 = signature U2 by A2, UNIALG_1:def 4; :: thesis: verum