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