let i, j, m, n be Element of NAT ; :: thesis: for X being BCK-algebra of i,j,m,n st j = 0 & m > 0 holds
X is BCK-algebra of 0 , 0 , 0 , 0
let X be BCK-algebra of i,j,m,n; :: thesis: ( j = 0 & m > 0 implies X is BCK-algebra of 0 , 0 , 0 , 0 )
assume that
A1: j = 0 and
A2: m > 0 ; :: thesis: X is BCK-algebra of 0 , 0 , 0 , 0
for x, y being Element of X holds Polynom 0 ,0 ,x,y = Polynom 0 ,n,y,x

proof

let x, y be Element of X; :: thesis: Polynom 0 ,0 ,x,y = Polynom 0 ,n,y,x
A3: Polynom i,j,x,y = Polynom m,n,y,x by Def3;
A4: i + 1 >= j + 1 by A1, XREAL_1:8;
( x,(x \ y) to_power (j + 1) = x,(x \ y) to_power (m + 1) & j + 1 < m + 1 ) by A1, A2, Th20, XREAL_1:8;
then x,(x \ y) to_power (i + 1) = x,(x \ y) to_power (0 + 1) by A1, A4, Th6;
hence Polynom 0 ,0 ,x,y = Polynom 0 ,n,y,x by A1, A3, Th20; :: thesis: verum

end;

then reconsider X = X as BCK-algebra of 0 , 0 , 0 ,n by Def3;
A5: for x, y being Element of X holds Polynom 0 ,0 ,x,y <= Polynom 0 ,0 ,y,x

proof

let x, y be Element of X; :: thesis: Polynom 0 ,0 ,x,y <= Polynom 0 ,0 ,y,x
Polynom 0 ,0 ,x,y = Polynom 0 ,n,y,x by Def3;
hence Polynom 0 ,0 ,x,y <= Polynom 0 ,0 ,y,x by Th5; :: thesis: verum

end;

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

proof

let x, y be Element of X; :: thesis: Polynom 0 ,0 ,y,x = Polynom 0 ,0 ,x,y
Polynom 0 ,0 ,x,y <= Polynom 0 ,0 ,y,x by A5;
then A6: (Polynom 0 ,0 ,x,y) \ (Polynom 0 ,0 ,y,x) = 0. X by BCIALG_1:def 11;
Polynom 0 ,0 ,y,x <= Polynom 0 ,0 ,x,y by A5;
then (Polynom 0 ,0 ,y,x) \ (Polynom 0 ,0 ,x,y) = 0. X by BCIALG_1:def 11;
hence Polynom 0 ,0 ,y,x = Polynom 0 ,0 ,x,y by A6, BCIALG_1:def 7; :: thesis: verum

end;

hence X is BCK-algebra of 0 , 0 , 0 , 0 by Def3; :: thesis: verum