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