:: deftheorem defines [: PRALG_2:def 8 :
for S being non empty ManySortedSign
for U1, U2 being non-empty MSAlgebra over S holds [:U1,U2:] = MSAlgebra(# [| the Sorts of U1, the Sorts of U2|],[[: the Charact of U1, the Charact of U2:]] #);