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;

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

hence
signature U1 = signature U2
by A2, UNIALG_1:def 4; :: thesis: verumfor 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;(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