deffunc H₁( Element of Fin A, Element of Fin A) -> Element of Fin A = $1 \/ $2;
ex IT being BinOp of (Fin A) st
for x, y being Element of Fin A holds IT . x,y = H₁(x,y) from BINOP_1:sch 4();
hence ex b₁ being BinOp of (Fin A) st
for x, y being Element of Fin A holds b₁ . x,y = x \/ y ; :: thesis: verum