let n be Element of NAT ; :: thesis: for X being quasi-commutative BCK-algebra holds
( X is BCK-algebra of n,n + 1,n,n + 1 iff for x, y being Element of X holds x,y to_power (n + 1) = x,y to_power (n + 2) )
let X be quasi-commutative BCK-algebra; :: thesis: ( X is BCK-algebra of n,n + 1,n,n + 1 iff for x, y being Element of X holds x,y to_power (n + 1) = x,y to_power (n + 2) )
thus ( X is BCK-algebra of n,n + 1,n,n + 1 implies for x, y being Element of X holds x,y to_power (n + 1) = x,y to_power (n + 2) ) :: thesis: ( ( for x, y being Element of X holds x,y to_power (n + 1) = x,y to_power (n + 2) ) implies X is BCK-algebra of n,n + 1,n,n + 1 )

proof

assume A1: X is BCK-algebra of n,n + 1,n,n + 1 ; :: thesis: for x, y being Element of X holds x,y to_power (n + 1) = x,y to_power (n + 2)
for x, y being Element of X holds x,y to_power (n + 1) = x,y to_power (n + 2)

proof

let x, y be Element of X; :: thesis: x,y to_power (n + 1) = x,y to_power (n + 2)
A2: (x \ y) \ x = (x \ x) \ y by BCIALG_1:7
.= y ` by BCIALG_1:def 5
.= 0. X by BCIALG_1:def 8 ;
then A3: (x,(x \ (x \ y)) to_power (n + 1)),((x \ y) \ x) to_power (n + 1) = (x,y to_power (n + 1)),(0. X) to_power (n + 1) by BCIALG_2:8
.= x,y to_power (n + 1) by BCIALG_2:5 ;
A4: ((x \ y),((x \ y) \ x) to_power (n + 1)),(x \ (x \ y)) to_power (n + 1) = (x \ y),(x \ (x \ y)) to_power (n + 1) by A2, BCIALG_2:5
.= (x,(x \ (x \ y)) to_power (n + 1)) \ y by BCIALG_2:7
.= (x,y to_power (n + 1)) \ y by BCIALG_2:8
.= x,y to_power ((n + 1) + 1) by BCIALG_2:4 ;
Polynom n,(n + 1),x,(x \ y) = Polynom n,(n + 1),(x \ y),x by A1, Def3;
hence x,y to_power (n + 1) = x,y to_power (n + 2) by A3, A4; :: thesis: verum

end;

hence for x, y being Element of X holds x,y to_power (n + 1) = x,y to_power (n + 2) ; :: thesis: verum

end;

assume A5: for x, y being Element of X holds x,y to_power (n + 1) = x,y to_power (n + 2) ; :: thesis: X is BCK-algebra of n,n + 1,n,n + 1
for x, y being Element of X holds Polynom n,(n + 1),x,y = Polynom n,(n + 1),y,x

proof

let x, y be Element of X; :: thesis: Polynom n,(n + 1),x,y = Polynom n,(n + 1),y,x
(x \ y) \ (x \ y) = 0. X by BCIALG_1:def 5;
then (x \ (x \ y)) \ y = 0. X by BCIALG_1:7;
then x \ (x \ y) <= y by BCIALG_1:def 11;
then (x \ (x \ y)),(x \ y) to_power (n + 1) <= y,(x \ y) to_power (n + 1) by BCIALG_2:19;
then (x,(x \ y) to_power 1),(x \ y) to_power (n + 1) <= y,(x \ y) to_power (n + 1) by BCIALG_2:2;
then A6: x,(x \ y) to_power (1 + (n + 1)) <= y,(x \ y) to_power (n + 1) by BCIALG_2:10;
(y \ x) \ (y \ x) = 0. X by BCIALG_1:def 5;
then (y \ (y \ x)) \ x = 0. X by BCIALG_1:7;
then y \ (y \ x) <= x by BCIALG_1:def 11;
then (y \ (y \ x)),(y \ x) to_power (n + 1) <= x,(y \ x) to_power (n + 1) by BCIALG_2:19;
then (y,(y \ x) to_power 1),(y \ x) to_power (n + 1) <= x,(y \ x) to_power (n + 1) by BCIALG_2:2;
then A7: y,(y \ x) to_power (1 + (n + 1)) <= x,(y \ x) to_power (n + 1) by BCIALG_2:10;
y,(y \ x) to_power (n + 1) = y,(y \ x) to_power (n + 2) by A5;
then (y,(y \ x) to_power (n + 1)),(x \ y) to_power (n + 1) <= (x,(y \ x) to_power (n + 1)),(x \ y) to_power (n + 1) by A7, BCIALG_2:19;
then A8: (y,(y \ x) to_power (n + 1)),(x \ y) to_power (n + 1) <= (x,(x \ y) to_power (n + 1)),(y \ x) to_power (n + 1) by BCIALG_2:11;
x,(x \ y) to_power (n + 1) = x,(x \ y) to_power (n + 2) by A5;
then (x,(x \ y) to_power (n + 1)),(y \ x) to_power (n + 1) <= (y,(x \ y) to_power (n + 1)),(y \ x) to_power (n + 1) by A6, BCIALG_2:19;
then (x,(x \ y) to_power (n + 1)),(y \ x) to_power (n + 1) <= (y,(y \ x) to_power (n + 1)),(x \ y) to_power (n + 1) by BCIALG_2:11;
hence Polynom n,(n + 1),x,y = Polynom n,(n + 1),y,x by A8, Th2; :: thesis: verum

end;

hence X is BCK-algebra of n,n + 1,n,n + 1 by Def3; :: thesis: verum