let X be BCI-Algebra_with_Condition(S); :: thesis: for a1, a2 being Element of X holds Product_S <*a1,a2*> = a1 * a2
let a1, a2 be Element of X; :: thesis: Product_S <*a1,a2*> = a1 * a2
thus Product_S <*a1,a2*> = (Product_S <*a1*>) * a2 by Th18, FINSOP_1:4
.= a1 * a2 by FINSOP_1:11 ; :: thesis: verum