:: deftheorem defines MULT314 GATE_5:def 9 :
for x0, x1, x2, y0, y1 being set holds MULT314 (x2,x1,y1,x0,y0) = CARR3 ({},(AND2 (x2,y1)),(AND2 (x2,y0)),(AND2 (x1,y1)),(AND2 (x1,y0)),(AND2 (x0,y1)),{});