deffunc H1( Element of {1,2,3}, Element of {1,2,3}) -> Element of {1,2,3} = $1 example33"/\" $2;
ex o being BinOp of {1,2,3} st
for a, b being Element of {1,2,3} holds o . (a,b) = H1(a,b)
from BINOP_1:sch 4();
hence
ex b1 being BinOp of {1,2,3} st
for x, y being Element of {1,2,3} holds b1 . (x,y) = x example33"/\" y
; verum