:: deftheorem defines the_mult_induced_by ALGSTR_4:def 11 :
for M being multMagma
for A being stable Subset of M holds the_mult_induced_by A = the multF of M || A;