let i, j, m, n be Element of NAT ; :: thesis: for X being BCI-algebra of i,j,m,n
for k being Element of NAT holds X is BCI-algebra of i,j + k,m + k,n
let X be BCI-algebra of i,j,m,n; :: thesis: for k being Element of NAT holds X is BCI-algebra of i,j + k,m + k,n
let k be Element of NAT ; :: thesis: X is BCI-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 BCI-algebra of i,j + k,m + k,n by Def3; :: thesis: verum