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

proof

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

end;

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