let X be BCI-algebra; :: thesis: ( X is p-Semisimple BCI-algebra implies X is BCI-algebra of 0 ,1, 0 , 0 )
assume A1: X is p-Semisimple BCI-algebra ; :: thesis: X is BCI-algebra of 0 ,1, 0 , 0
for x, y being Element of X holds Polynom (0,1,x,y) = Polynom (0,0,y,x)

proof

let x, y be Element of X; :: thesis: Polynom (0,1,x,y) = Polynom (0,0,y,x)
(((x,(x \ y)) to_power 1),(y \ x)) to_power 1 = ((x \ (x \ y)),(y \ x)) to_power 1 by BCIALG_2:2
.= (y,(y \ x)) to_power 1 by A1, BCIALG_1:def 26
.= (((y,(y \ x)) to_power 1),(x \ y)) to_power 0 by BCIALG_2:1 ;
hence Polynom (0,1,x,y) = Polynom (0,0,y,x) ; :: thesis: verum

end;

hence X is BCI-algebra of 0 ,1, 0 , 0 by Def3; :: thesis: verum