deffunc H₁( Element of D ^omega , Element of D ^omega ) -> Element of D ^omega = $1 ^ $2;
consider g being BinOp of (D ^omega) such that
A1: for a, b being Element of D ^omega holds g . (a,b) = H₁(a,b) from BINOP_1:sch 4();
take g "**" F ; :: thesis: ex g being BinOp of (D ^omega) st
( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) & g "**" F = g "**" F )
take g ; :: thesis: ( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) & g "**" F = g "**" F )
thus ( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) & g "**" F = g "**" F ) by A1; :: thesis: verum