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

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

end;