let i, j, m, n be Nat; :: thesis: for X being BCK-algebra of i,j,m,n st i = n holds

X is BCK-algebra of i,j,j,i

let X be BCK-algebra of i,j,m,n; :: thesis: ( i = n implies X is BCK-algebra of i,j,j,i )

assume i = n ; :: thesis: X is BCK-algebra of i,j,j,i

then reconsider X = X as BCK-algebra of i,j,m,i ;

for x, y being Element of X holds Polynom (i,j,x,y) = Polynom (j,i,y,x)

X is BCK-algebra of i,j,j,i

let X be BCK-algebra of i,j,m,n; :: thesis: ( i = n implies X is BCK-algebra of i,j,j,i )

assume i = n ; :: thesis: X is BCK-algebra of i,j,j,i

then reconsider X = X as BCK-algebra of i,j,m,i ;

for x, y being Element of X holds Polynom (i,j,x,y) = Polynom (j,i,y,x)

proof

hence
X is BCK-algebra of i,j,j,i
by Def3; :: thesis: verum
let x, y be Element of X; :: thesis: Polynom (i,j,x,y) = Polynom (j,i,y,x)

Polynom (i,j,x,y) = Polynom (m,i,y,x) by Def3;

hence Polynom (i,j,x,y) = Polynom (j,i,y,x) by Th20; :: thesis: verum

end;Polynom (i,j,x,y) = Polynom (m,i,y,x) by Def3;

hence Polynom (i,j,x,y) = Polynom (j,i,y,x) by Th20; :: thesis: verum