for X being BCI-Algebra_with_Condition(S)
for F1, F2 being FinSequence of the carrier of X holds Product_S (F1 ^ F2) = (Product_S F1) * (Product_S F2) by Th18, FINSOP_1:5;