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