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

proof

let x, y be Element of X; :: thesis: Polynom (i,(j + k),x,y) = Polynom ((m + k),n,y,x)
A1: ((Polynom (m,n,y,x)),(y \ x)) to_power k = (((((y,(y \ x)) to_power (m + 1)),(y \ x)) to_power k),(x \ y)) to_power n by BCIALG_2:11
.= (((y,(y \ x)) to_power ((m + 1) + k)),(x \ y)) to_power n by BCIALG_2:10
.= Polynom ((m + k),n,y,x) ;
((Polynom (i,j,x,y)),(y \ x)) to_power k = Polynom (i,(j + k),x,y) by BCIALG_2:10;
hence Polynom (i,(j + k),x,y) = Polynom ((m + k),n,y,x) by A1, Def3; :: thesis: verum

end;

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