:: deftheorem defines |. PRALG_2:def 6 :
for S being non empty ManySortedSign
for U1 being MSAlgebra over S holds |.U1.| = union (rng the Sorts of U1);