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 ) & 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 A3: ( ( for p, q being Element of D * holds g2 . p,q = p ^ q ) & 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 A3 ; :: thesis: verum

end;

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