let i, j, m, n be Element of NAT ; :: thesis: for X being BCK-algebra of i,j,m,n st i = min i,j,m,n & i < j & i = n & i < m & 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 = min i,j,m,n & i < j & i = n & i < m & m < j implies X is BCK-algebra of i,m + 1,m,i )
assume
i = min i,j,m,n
; :: thesis: ( not i < j or not i = n or not i < m or not m < j or X is BCK-algebra of i,m + 1,m,i )
assume A2:
( i < j & i = n & i < m & 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
let x,
y be
Element of
X;
:: thesis: Polynom i,(m + 1),x,y = Polynom m,i,y,x
D1:
Polynom i,
j,
x,
y = Polynom m,
n,
y,
x
by Def2;
B1:
(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 Th8;
B2:
m + 1
< j + 1
by A2, XREAL_1:8;
B3:
j - m is
Element of
NAT
by A2, NAT_1:21;
consider t being
Element of
NAT such that B4:
t = j - m
by B3;
j - m > m - m
by A2, XREAL_1:11;
then
j - m >= 1
by B4, NAT_1:14;
then
(j - m) + m >= 1
+ m
by XREAL_1:8;
hence
Polynom i,
(m + 1),
x,
y = Polynom m,
i,
y,
x
by D1, A2, Th06, B1, B2;
:: thesis: verum
end;
hence
X is BCK-algebra of i,m + 1,m,i
by Def2; :: thesis: verum