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 Nat 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

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 Nat 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