:: deftheorem Def5 defines [: PRALG_1:def 5 :
for U1, U2 being Universal_Algebra st U1,U2 are_similar holds
[:U1,U2:] = UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #);