deffunc H1( Element of {0,1,2}, Element of {0,1,2}) -> Element of {0,1,2} = $1 + $2;
ex o being BinOp of {0,1,2} st
for a, b being Element of {0,1,2} holds o . (a,b) = H1(a,b)
from BINOP_1:sch 4();
hence
ex b1 being BinOp of {0,1,2} st
for a, b being Element of {0,1,2} holds b1 . (a,b) = a + b
; verum