let X be BCI-algebra; :: thesis: for m, n being Nat st X is BCI-algebra of n, 0 ,m,m holds
X is BCI-commutative BCI-algebra
let m, n be 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₁[ 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 :: thesis: for k being Nat st ( k <= m implies (y,(y \ x)) to_power (k + 1) <= (y,(y \ x)) to_power 1 ) & k + 1 <= m holds
(y,(y \ x)) to_power ((k + 1) + 1) <= (y,(y \ x)) to_power 1

((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 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 ;
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 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 Nat holds S₁[m] from NAT_1:sch 2(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 ;
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