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