let it1, it2 be Element of D * ; ( 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
; ( 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
; it1 = it2
now for a, b being Element of D * holds g1 . (a,b) = g2 . (a,b)let a,
b be
Element of
D * ;
g1 . (a,b) = g2 . (a,b)thus g1 . (
a,
b) =
a ^ b
by A2
.=
g2 . (
a,
b)
by A4
;
verum end;
hence
it1 = it2
by A3, A5, BINOP_1:2; verum