theorem Th63: :: HILB10_7:63

for D being non empty set
for A being BinOp of D
for F, G being b₁ * -valued FinSequence holds A "**" (F ^ G) = (A "**" F) ^ (A "**" G)