:: deftheorem defines multiplication NOMIN_5:def 8 :
for V, A being set
for x, y being Element of V holds multiplication (A,x,y) = lift_binary_op ((multiplication A),x,y);