let i, j, m, n be Nat; :: thesis: for X being BCK-algebra of i,j,m,n holds X is BCK-algebra of n,j,m,n
let X be BCK-algebra of i,j,m,n; :: thesis: X is BCK-algebra of n,j,m,n
for x, y being Element of X holds Polynom (n,j,x,y) = Polynom (m,n,y,x)

proof

let x, y be Element of X; :: thesis: Polynom (n,j,x,y) = Polynom (m,n,y,x)
Polynom (i,j,x,y) = Polynom (m,n,y,x) by Def3;
hence Polynom (n,j,x,y) = Polynom (m,n,y,x) by Th19; :: thesis: verum

end;

hence X is BCK-algebra of n,j,m,n by Def3; :: thesis: verum