:: deftheorem defines Trivial-multMagma ALGSTR_0:def 19 :
Trivial-multMagma = multMagma(# {0},op2 #);