for U1 being Universal_Algebra holds U1,U1 are_isomorphic