for X being BCI-Algebra_with_Condition(S)
for a1, a2 being Element of X holds Product_S <*a1,a2*> = a1 * a2