theorem Th42: :: AOFA_A00:47

for U1, U2 being Universal_Algebra st UAStr(# the carrier of U1, the charact of U1 #) = UAStr(# the carrier of U2, the charact of U2 #) holds
signature U1 = signature U2