let X be BCI-algebra; :: thesis: for n, m being Element of NAT st X is BCI-algebra of n, 0 ,m,m holds
X is BCI-commutative BCI-algebra
let n, m be Element of NAT ; :: thesis: ( X is BCI-algebra of n, 0 ,m,m implies X is BCI-commutative BCI-algebra )
A1: for x, y being Element of X st x \ y = 0. X holds
y,(y \ x) to_power (m + 1) <= y,(y \ x) to_power 1

proof

let x, y be Element of X; :: thesis: ( x \ y = 0. X implies y,(y \ x) to_power (m + 1) <= y,(y \ x) to_power 1 )
defpred S₁[ Element of NAT ] means ( $1 <= m implies y,(y \ x) to_power ($1 + 1) <= y,(y \ x) to_power 1 );
assume A2: x \ y = 0. X ; :: thesis: y,(y \ x) to_power (m + 1) <= y,(y \ x) to_power 1

now

(0. X),(y \ x) to_power 1 = ((0. X),y to_power 1) \ ((0. X),x to_power 1) by BCIALG_2:18;
then (0. X) \ (y \ x) = ((0. X),y to_power 1) \ ((0. X),x to_power 1) by BCIALG_2:2;
then A3: (0. X) \ (y \ x) = ((0. X) \ y) \ ((0. X),x to_power 1) by BCIALG_2:2;
let k be Element of NAT ; :: thesis: ( ( k <= m implies y,(y \ x) to_power (k + 1) <= y,(y \ x) to_power 1 ) & k + 1 <= m implies y,(y \ x) to_power ((k + 1) + 1) <= y,(y \ x) to_power 1 )
assume A4: ( k <= m implies y,(y \ x) to_power (k + 1) <= y,(y \ x) to_power 1 ) ; :: thesis: ( k + 1 <= m implies y,(y \ x) to_power ((k + 1) + 1) <= y,(y \ x) to_power 1 )
(((0. X) \ y) \ ((0. X) \ x)) \ (x \ y) = 0. X by BCIALG_1:1;
then ((0. X) \ y) \ ((0. X) \ x) = 0. X by A2, BCIALG_1:2;
then (0. X) \ (y \ x) = 0. X by A3, BCIALG_2:2;
then (y \ y) \ (y \ x) = 0. X by BCIALG_1:def 5;
then (y \ (y \ x)) \ y = 0. X by BCIALG_1:7;
then y \ (y \ x) <= y by BCIALG_1:def 11;
then (y \ (y \ x)),(y \ x) to_power (k + 1) <= y,(y \ x) to_power (k + 1) by BCIALG_2:19;
then (y,(y \ x) to_power 1),(y \ x) to_power (k + 1) <= y,(y \ x) to_power (k + 1) by BCIALG_2:2;
then A5: y,(y \ x) to_power ((k + 1) + 1) <= y,(y \ x) to_power (k + 1) by BCIALG_2:10;
set m1 = k + 1;
assume k + 1 <= m ; :: thesis: y,(y \ x) to_power ((k + 1) + 1) <= y,(y \ x) to_power 1
hence y,(y \ x) to_power ((k + 1) + 1) <= y,(y \ x) to_power 1 by A4, A5, Th1, NAT_1:13; :: thesis: verum

end;

then A6: for k being Element of NAT st S₁[k] holds
S₁[k + 1] ;
(y,(y \ x) to_power (0 + 1)) \ (y,(y \ x) to_power 1) = 0. X by BCIALG_1:def 5;
then A7: S₁[ 0 ] by BCIALG_1:def 11;
for m being Element of NAT holds S₁[m] from NAT_1:sch 1(A7, A6);
hence y,(y \ x) to_power (m + 1) <= y,(y \ x) to_power 1 ; :: thesis: verum

end;

assume A8: X is BCI-algebra of n, 0 ,m,m ; :: thesis: X is BCI-commutative BCI-algebra
for x, y being Element of X st x \ y = 0. X holds
x = y \ (y \ x)

proof

let x, y be Element of X; :: thesis: ( x \ y = 0. X implies x = y \ (y \ x) )
assume A9: x \ y = 0. X ; :: thesis: x = y \ (y \ x)
Polynom n,0 ,x,y = Polynom m,m,y,x by A8, Def3;
then x,(y \ x) to_power 0 = (y,(y \ x) to_power (m + 1)),(0. X) to_power m by A9, BCIALG_2:5;
then x,(y \ x) to_power 0 = ((y,(y \ x) to_power (m + 1)),(0. X) to_power m) \ (0. X) by BCIALG_1:2;
then x,(y \ x) to_power 0 = (y,(y \ x) to_power (m + 1)),(0. X) to_power (m + 1) by BCIALG_2:4;
then x,(y \ x) to_power 0 = y,(y \ x) to_power (m + 1) by BCIALG_2:5;
then x = y,(y \ x) to_power (m + 1) by BCIALG_2:1;
then x <= y,(y \ x) to_power 1 by A1, A9;
then A10: x <= y \ (y \ x) by BCIALG_2:2;
(y \ (y \ x)) \ x = (y \ x) \ (y \ x) by BCIALG_1:7;
then (y \ (y \ x)) \ x = 0. X by BCIALG_1:def 5;
then y \ (y \ x) <= x by BCIALG_1:def 11;
hence x = y \ (y \ x) by A10, Th2; :: thesis: verum

end;

hence X is BCI-commutative BCI-algebra by BCIALG_3:def 4; :: thesis: verum