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