theorem :: FINSEQOP:80

for D being non empty set
for F being BinOp of D
for u, u9 being Function of D,D holds F * (u,u9) is BinOp of D by Th78;