let X be BCI-Algebra_with_Condition(S); 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; 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
; verum