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