let i, j, m, n be Nat; :: thesis: for X being BCK-algebra of i,j,m,n st i = n & m < j holds
X is BCK-algebra of i,m + 1,m,i
let X be BCK-algebra of i,j,m,n; :: thesis: ( i = n & m < j implies X is BCK-algebra of i,m + 1,m,i )
assume that
A1: i = n and
A2: m < j ; :: thesis: X is BCK-algebra of i,m + 1,m,i
for x, y being Element of X holds Polynom (i,(m + 1),x,y) = Polynom (m,i,y,x)

proof

( j - m is Element of NAT & j - m > m - m ) by A2, NAT_1:21, XREAL_1:9;
then j - m >= 1 by NAT_1:14;
then A3: (j - m) + m >= 1 + m by XREAL_1:6;
let x, y be Element of X; :: thesis: Polynom (i,(m + 1),x,y) = Polynom (m,i,y,x)
A4: m + 1 < j + 1 by A2, XREAL_1:6;
( Polynom (i,j,x,y) = Polynom (m,n,y,x) & (((x,(x \ y)) to_power (i + 1)),(y \ x)) to_power (j + 1) = (((x,(x \ y)) to_power (i + 1)),(y \ x)) to_power (m + 1) ) by Def3, Th20;
hence Polynom (i,(m + 1),x,y) = Polynom (m,i,y,x) by A1, A4, A3, Th6; :: thesis: verum

end;

hence X is BCK-algebra of i,m + 1,m,i by Def3; :: thesis: verum