let X be BCI-Algebra_with_Condition(S); :: thesis: for x, a1, a2 being Element of X holds (x \ a1) \ a2 = x \ (Product_S <*a1,a2*>)

let x, a1, a2 be Element of X; :: thesis: (x \ a1) \ a2 = x \ (Product_S <*a1,a2*>)

(x \ a1) \ a2 = x \ (a1 * a2) by Th11;

hence (x \ a1) \ a2 = x \ (Product_S <*a1,a2*>) by Th32; :: thesis: verum

let x, a1, a2 be Element of X; :: thesis: (x \ a1) \ a2 = x \ (Product_S <*a1,a2*>)

(x \ a1) \ a2 = x \ (a1 * a2) by Th11;

hence (x \ a1) \ a2 = x \ (Product_S <*a1,a2*>) by Th32; :: thesis: verum