theorem :: BCIALG_4:6

for X being BCI-Algebra_with_Condition(S) st X is p-Semisimple holds
for x, y being Element of X holds x * y = x \ ((0. X) \ y)