:: deftheorem defines |. PRALG_2:def 7 :
for I being non empty set
for S being non empty ManySortedSign
for A being MSAlgebra-Family of I,S holds |.A.| = union { |.(A . i).| where i is Element of I : verum } ;