let i, j, m, n be Nat; for X being BCK-algebra of i,j,m,n holds X is BCK-algebra of n,j,m,n
let X be BCK-algebra of i,j,m,n; X is BCK-algebra of n,j,m,n
for x, y being Element of X holds Polynom (n,j,x,y) = Polynom (m,n,y,x)
proof
let x,
y be
Element of
X;
Polynom (n,j,x,y) = Polynom (m,n,y,x)
Polynom (
i,
j,
x,
y)
= Polynom (
m,
n,
y,
x)
by Def3;
hence
Polynom (
n,
j,
x,
y)
= Polynom (
m,
n,
y,
x)
by Th19;
verum
end;
hence
X is BCK-algebra of n,j,m,n
by Def3; verum