theorem :: BCIALG_4:32

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 (<*a*> ^ F) = a * (Product_S F) by Th18, FINSOP_1:6;