for x, y being Element of BCI-EXAMPLE holds Polynom (i,j,x,y) = Polynom (m,n,y,x) by STRUCT_0:def 10;
hence ex b₁ being BCI-algebra st
for x, y being Element of b₁ holds Polynom (i,j,x,y) = Polynom (m,n,y,x) ; :: thesis: verum