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