let X be BCI-algebra; :: thesis: for i, j, k being Nat st X is BCI-algebra of i,j,j + k,i + k holds
X is BCK-algebra
let i, j, k be Nat; :: thesis: ( X is BCI-algebra of i,j,j + k,i + k implies X is BCK-algebra )
assume A1: X is BCI-algebra of i,j,j + k,i + k ; :: thesis: X is BCK-algebra
for y being Element of X holds (0. X) \ y = 0. X

proof

let y be Element of X; :: thesis: (0. X) \ y = 0. X
A2: (((y,y) to_power ((j + k) + 1)),((0. X) \ y)) to_power (i + k) = ((((y,y) to_power (j + k)) \ y),((0. X) \ y)) to_power (i + k) by BCIALG_2:4
.= ((((y \ y),y) to_power (j + k)),((0. X) \ y)) to_power (i + k) by BCIALG_2:7
.= ((((0. X),y) to_power (j + k)),((0. X) \ y)) to_power (i + k) by BCIALG_1:def 5
.= ((((0. X),((0. X) \ y)) to_power (i + k)),y) to_power (j + k) by BCIALG_2:11
.= (((((0. X),(0. X)) to_power (i + k)) \ (((0. X),y) to_power (i + k))),y) to_power (j + k) by BCIALG_2:18
.= (((0. X) \ (((0. X),y) to_power (i + k))),y) to_power (j + k) by BCIALG_2:6
.= (((0. X),y) to_power (j + k)) \ (((0. X),y) to_power (i + k)) by BCIALG_2:7
.= (((((0. X),y) to_power j),y) to_power k) \ (((0. X),y) to_power (i + k)) by BCIALG_2:10
.= (((((0. X),y) to_power j),y) to_power k) \ (((((0. X),y) to_power i),y) to_power k) by BCIALG_2:10 ;
A3: (((((0. X),y) to_power j),y) to_power k) \ (((((0. X),y) to_power i),y) to_power k) <= (((0. X),y) to_power j) \ (((0. X),y) to_power i) by BCIALG_2:21;
Polynom (i,j,(0. X),y) = Polynom ((j + k),(i + k),y,(0. X)) by A1, Def3;
then ((((0. X),((0. X) \ y)) to_power (i + 1)),y) to_power j = (((y,(y \ (0. X))) to_power ((j + k) + 1)),((0. X) \ y)) to_power (i + k) by BCIALG_1:2;
then ((((0. X),((0. X) \ y)) to_power (i + 1)),y) to_power j = (((y,y) to_power ((j + k) + 1)),((0. X) \ y)) to_power (i + k) by BCIALG_1:2;
then A4: ((((0. X),y) to_power j),((0. X) \ y)) to_power (i + 1) = (((y,y) to_power ((j + k) + 1)),((0. X) \ y)) to_power (i + k) by BCIALG_2:11;
((((0. X),y) to_power j),((0. X) \ y)) to_power (i + 1) = ((((0. X),((0. X) \ y)) to_power (i + 1)),y) to_power j by BCIALG_2:11
.= (((((0. X),(0. X)) to_power (i + 1)) \ (((0. X),y) to_power (i + 1))),y) to_power j by BCIALG_2:18
.= (((0. X) \ (((0. X),y) to_power (i + 1))),y) to_power j by BCIALG_2:6
.= (((0. X),y) to_power j) \ (((0. X),y) to_power (i + 1)) by BCIALG_2:7 ;
then ((((0. X),y) to_power j) \ (((0. X),y) to_power (i + 1))) \ ((((0. X),y) to_power j) \ (((0. X),y) to_power i)) = 0. X by A4, A2, A3;
then (0. X) \ ((((0. X),y) to_power i) \ (((0. X),y) to_power (i + 1))) = 0. X by BCIALG_1:11;
then A5: 0. X <= (((0. X),y) to_power i) \ (((0. X),y) to_power (i + 1)) ;
(((0. X),y) to_power i) \ (((0. X),y) to_power (i + 1)) = (((0. X),y) to_power i) \ ((((0. X),y) to_power i) \ y) by BCIALG_2:4
.= (((0. X),y) to_power i) \ ((((0. X) \ y),y) to_power i) by BCIALG_2:7 ;
then (((0. X),y) to_power i) \ (((0. X),y) to_power (i + 1)) <= (0. X) \ ((0. X) \ y) by BCIALG_2:21;
then 0. X <= (0. X) \ ((0. X) \ y) by A5, Th1;
then (0. X) \ ((0. X) \ ((0. X) \ y)) = 0. X ;
hence (0. X) \ y = 0. X by BCIALG_1:8; :: thesis: verum

end;

then for x being Element of X holds x ` = 0. X ;
hence X is BCK-algebra by BCIALG_1:def 8; :: thesis: verum