let i, j, m, n be Element of 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:11;
then j - m >= 1 by NAT_1:14;
then A3: (j - m) + m >= 1 + m by XREAL_1:8;
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:8;
( 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