:: deftheorem defines mult_2 REALSET2:def 2 :
mult_2 = ((((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0)) +* ((1,1) .--> 1);