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;

now :: thesis: 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

let i be natural number ; :: thesis: ( i in dom (signature U2) implies 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 )
assume A3: i in dom (signature U2) ; :: thesis: 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
let h be non empty homogeneous PartFunc of ( the carrier of U1 *), the carrier of U1; :: thesis: ( h = the charact of U1 . i implies (signature U2) . i = arity h )
assume A4: h = the charact of U1 . i ; :: thesis: (signature U2) . i = arity h
reconsider h2 = h as non empty homogeneous PartFunc of ( the carrier of U2 *), the carrier of U2 by A1;
thus (signature U2) . i = arity h by A1, A3, A4, UNIALG_1:def 4; :: thesis: verum

end;

hence signature U1 = signature U2 by A2, UNIALG_1:def 4; :: thesis: verum