let it1, it2 be Element of D * ; :: thesis: ( ex g being BinOp of (D *) st
( ( for p, q being Element of D * holds g . (p,q) = p ^ q ) & it1 = g "**" F ) & ex g being BinOp of (D *) st
( ( for p, q being Element of D * holds g . (p,q) = p ^ q ) & it2 = g "**" F ) implies it1 = it2 )
given g1 being BinOp of (D *) such that A2: for p, q being Element of D * holds g1 . (p,q) = p ^ q and
A3: it1 = g1 "**" F ; :: thesis: ( for g being BinOp of (D *) holds
( ex p, q being Element of D * st not g . (p,q) = p ^ q or not it2 = g "**" F ) or it1 = it2 )
given g2 being BinOp of (D *) such that A4: for p, q being Element of D * holds g2 . (p,q) = p ^ q and
A5: it2 = g2 "**" F ; :: thesis: it1 = it2

now :: thesis: for a, b being Element of D * holds g1 . (a,b) = g2 . (a,b)

let a, b be Element of D * ; :: thesis: g1 . (a,b) = g2 . (a,b)
thus g1 . (a,b) = a ^ b by A2
.= g2 . (a,b) by A4 ; :: thesis: verum

end;

hence it1 = it2 by A3, A5, BINOP_1:2; :: thesis: verum