let X be BCI-algebra; :: thesis: ( X is associative BCI-algebra implies ( X is BCI-algebra of 0 ,1, 0 , 0 & X is BCI-algebra of 1, 0 , 0 , 0 ) )

assume A1: X is associative BCI-algebra ; :: thesis: ( X is BCI-algebra of 0 ,1, 0 , 0 & X is BCI-algebra of 1, 0 , 0 , 0 )

for x being Element of X holds (x `) ` = x

for x, y being Element of X holds Polynom (1,0,x,y) = Polynom (0,0,y,x)

assume A1: X is associative BCI-algebra ; :: thesis: ( X is BCI-algebra of 0 ,1, 0 , 0 & X is BCI-algebra of 1, 0 , 0 , 0 )

for x being Element of X holds (x `) ` = x

proof

then A2:
X is p-Semisimple
by BCIALG_1:54;
let x be Element of X; :: thesis: (x `) ` = x

x ` = x by A1, BCIALG_1:47;

hence (x `) ` = x ; :: thesis: verum

end;x ` = x by A1, BCIALG_1:47;

hence (x `) ` = x ; :: thesis: verum

for x, y being Element of X holds Polynom (1,0,x,y) = Polynom (0,0,y,x)

proof

hence
( X is BCI-algebra of 0 ,1, 0 , 0 & X is BCI-algebra of 1, 0 , 0 , 0 )
by A2, Def3, Th42; :: thesis: verum
let x, y be Element of X; :: thesis: Polynom (1,0,x,y) = Polynom (0,0,y,x)

x \ (x \ y) = y by A2;

then A3: (x \ (x \ y)) \ (x \ y) = y \ (y \ x) by A1, BCIALG_1:48;

(((x,(x \ y)) to_power (1 + 1)),(y \ x)) to_power 0 = (x,(x \ y)) to_power 2 by BCIALG_2:1

.= (x \ (x \ y)) \ (x \ y) by BCIALG_2:3

.= (y,(y \ x)) to_power 1 by A3, BCIALG_2:2

.= (((y,(y \ x)) to_power 1),(x \ y)) to_power 0 by BCIALG_2:1 ;

hence Polynom (1,0,x,y) = Polynom (0,0,y,x) ; :: thesis: verum

end;x \ (x \ y) = y by A2;

then A3: (x \ (x \ y)) \ (x \ y) = y \ (y \ x) by A1, BCIALG_1:48;

(((x,(x \ y)) to_power (1 + 1)),(y \ x)) to_power 0 = (x,(x \ y)) to_power 2 by BCIALG_2:1

.= (x \ (x \ y)) \ (x \ y) by BCIALG_2:3

.= (y,(y \ x)) to_power 1 by A3, BCIALG_2:2

.= (((y,(y \ x)) to_power 1),(x \ y)) to_power 0 by BCIALG_2:1 ;

hence Polynom (1,0,x,y) = Polynom (0,0,y,x) ; :: thesis: verum