theorem :: BCIALG_4:31

for X being BCI-Algebra_with_Condition(S)
for F being FinSequence of the carrier of X
for a being Element of X holds Product_S (F ^ <*a*>) = (Product_S F) * a by Th18, FINSOP_1:4;