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