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)

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

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