theorem Th62: :: HILB10_7:62

for D being non empty set
for A being BinOp of D
for f being FinSequence of D holds A "**" <*f*> = <*(A "**" f)*>