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 + k,j,m,n + k
let X be BCK-algebra of i,j,m,n; :: thesis: for k being Element of NAT holds X is BCK-algebra of i + k,j,m,n + k
let k be Element of NAT ; :: thesis: X is BCK-algebra of i + k,j,m,n + k
for x, y being Element of X holds Polynom ((i + k),j,x,y) = Polynom (m,(n + k),y,x)

proof

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

end;

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