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)

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

hence
X is BCK-algebra of i,m + 1,m,i
by Def3; :: thesis: verum
( 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;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