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