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:
A2: len () = len the charact of U1 by ;
now :: thesis: for i being natural number st i in dom () 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
() . i = arity h
let i be natural number ; :: thesis: ( i in dom () 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
() . i = arity h )

assume A3: i in dom () ; :: 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
() . 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 () . i = arity h )
assume A4: h = the charact of U1 . i ; :: thesis: () . 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 ; :: thesis: verum
end;
hence signature U1 = signature U2 by ; :: thesis: verum