for U1, U2 being Universal_Algebra st U1,U2 are_similar holds
Inv ( the carrier of U1, the carrier of U2) is Function of the carrier of [:U1,U2:], the carrier of [:U2,U1:]