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