deffunc H₁( 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 = H₁(a,b) from BINOP_1:sch 4();
hence ex b₁ being BinOp of {0 ,1,2} st
for a, b being Element of {0 ,1,2} holds b₁ . a,b = a * b ; :: thesis: verum