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

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