let i, j, m, n be Nat; :: thesis: for X being BCI-algebra of i,j,m,n

for k being Element of NAT holds X is BCI-algebra of i,j + k,m + k,n

let X be BCI-algebra of i,j,m,n; :: thesis: for k being Element of NAT holds X is BCI-algebra of i,j + k,m + k,n

let k be Element of NAT ; :: thesis: X is BCI-algebra of i,j + k,m + k,n

for x, y being Element of X holds Polynom (i,(j + k),x,y) = Polynom ((m + k),n,y,x)

for k being Element of NAT holds X is BCI-algebra of i,j + k,m + k,n

let X be BCI-algebra of i,j,m,n; :: thesis: for k being Element of NAT holds X is BCI-algebra of i,j + k,m + k,n

let k be Element of NAT ; :: thesis: X is BCI-algebra of i,j + k,m + k,n

for x, y being Element of X holds Polynom (i,(j + k),x,y) = Polynom ((m + k),n,y,x)

proof

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

A1: ((Polynom (m,n,y,x)),(y \ x)) to_power k = (((((y,(y \ x)) to_power (m + 1)),(y \ x)) to_power k),(x \ y)) to_power n by BCIALG_2:11

.= (((y,(y \ x)) to_power ((m + 1) + k)),(x \ y)) to_power n by BCIALG_2:10

.= Polynom ((m + k),n,y,x) ;

((Polynom (i,j,x,y)),(y \ x)) to_power k = Polynom (i,(j + k),x,y) by BCIALG_2:10;

hence Polynom (i,(j + k),x,y) = Polynom ((m + k),n,y,x) by A1, Def3; :: thesis: verum

end;A1: ((Polynom (m,n,y,x)),(y \ x)) to_power k = (((((y,(y \ x)) to_power (m + 1)),(y \ x)) to_power k),(x \ y)) to_power n by BCIALG_2:11

.= (((y,(y \ x)) to_power ((m + 1) + k)),(x \ y)) to_power n by BCIALG_2:10

.= Polynom ((m + k),n,y,x) ;

((Polynom (i,j,x,y)),(y \ x)) to_power k = Polynom (i,(j + k),x,y) by BCIALG_2:10;

hence Polynom (i,(j + k),x,y) = Polynom ((m + k),n,y,x) by A1, Def3; :: thesis: verum