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