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 + k,j,m,n + k

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

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

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

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

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

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

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

proof

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

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

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

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

.= Polynom ((i + k),j,x,y) ;

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

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

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

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

.= Polynom ((i + k),j,x,y) ;

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