let X be BCI-Algebra_with_Condition(S); :: thesis: for x, a1, a2, a3 being Element of X holds ((x \ a1) \ a2) \ a3 = x \ (Product_S <*a1,a2,a3*>)
let x, a1, a2, a3 be Element of X; :: thesis: ((x \ a1) \ a2) \ a3 = x \ (Product_S <*a1,a2,a3*>)
((x \ a1) \ a2) \ a3 = (x \ (a1 * a2)) \ a3 by Th11
.= x \ ((a1 * a2) * a3) by Th11 ;
hence ((x \ a1) \ a2) \ a3 = x \ (Product_S <*a1,a2,a3*>) by Th33; :: thesis: verum