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

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