let X be BCI-Algebra_with_Condition(S); :: thesis: ( X is p-Semisimple implies for x, y being Element of X holds x * y = x \ ((0. X) \ y) )
assume A1: X is p-Semisimple ; :: thesis: for x, y being Element of X holds x * y = x \ ((0. X) \ y)
for x, y being Element of X holds x * y = x \ ((0. X) \ y)

proof

let x, y be Element of X; :: thesis: x * y = x \ ((0. X) \ y)
set z1 = x \ ((0. X) \ y);
set z2 = x * y;
((x \ ((0. X) \ y)) \ x) \ y = ((x \ x) \ ((0. X) \ y)) \ y by BCIALG_1:7
.= ((0. X) \ ((0. X) \ y)) \ y by BCIALG_1:def 5
.= ((0. X) \ y) \ ((0. X) \ y) by BCIALG_1:7
.= 0. X by BCIALG_1:def 5 ;
then (x \ ((0. X) \ y)) \ x <= y ;
then x \ ((0. X) \ y) <= x * y by Lm2;
then A2: (x \ ((0. X) \ y)) \ (x * y) = 0. X ;
A3: for t being Element of X st t \ x <= y holds
t <= x \ ((0. X) \ y)

proof

let t be Element of X; :: thesis: ( t \ x <= y implies t <= x \ ((0. X) \ y) )
assume t \ x <= y ; :: thesis: t <= x \ ((0. X) \ y)
then (t \ x) \ y = 0. X ;
then t \ (x \ ((0. X) \ y)) = t \ (x \ ((0. X) \ (t \ x))) by A1, Th4
.= t \ (x \ (x \ (t \ (0. X)))) by A1, BCIALG_1:57
.= t \ (t \ (0. X)) by A1
.= t \ t by BCIALG_1:2
.= 0. X by BCIALG_1:def 5 ;
hence t <= x \ ((0. X) \ y) ; :: thesis: verum

end;

(x * y) \ x <= y by Lm2;
then x * y <= x \ ((0. X) \ y) by A3;
then (x * y) \ (x \ ((0. X) \ y)) = 0. X ;
hence x * y = x \ ((0. X) \ y) by A2, BCIALG_1:def 7; :: thesis: verum

end;

hence for x, y being Element of X holds x * y = x \ ((0. X) \ y) ; :: thesis: verum