theorem Th7: :: PRVECT_1:7

for n being Nat
for D being non empty set
for B being BinOp of D st B is associative holds
product (B,n) is associative