for D being non empty set
for F being XFinSequence of D
for D1, D2 being non empty set
for b1 being BinOp of D1
for b2 being BinOp of D2 st len F >= 1 & D c= D1 /\ D2 & ( for x, y being object st x in D & y in D holds
( b1 . (x,y) = b2 . (x,y) & b1 . (x,y) in D ) ) holds
b1 "**" F = b2 "**" F