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

proof

let x, y be Element of X; :: thesis: Polynom (0,1,x,y) = Polynom (0,1,y,x)
A3: (i + 1) + 1 > (m + 1) + 0 by A1, XREAL_1:8;
A4: (((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power (j + 1) = (((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power (m + 1) by Th20;
A5: j + 1 > m + 1 by A1, A2, XREAL_1:6;
( n + 1 >= m + 1 & (((y,(y \ x)) to_power (0 + 1)),(x \ y)) to_power (j + 1) = (((y,(y \ x)) to_power (0 + 1)),(x \ y)) to_power (m + 1) ) by A1, Th20, XREAL_1:6;
then A6: (((y,(y \ x)) to_power (0 + 1)),(x \ y)) to_power (0 + 1) = (((y,(y \ x)) to_power (0 + 1)),(x \ y)) to_power (n + 1) by A1, A5, Th6;
( Polynom ((i + 1),j,x,y) = Polynom (m,(n + 1),y,x) & (x,(x \ y)) to_power (j + 1) = (x,(x \ y)) to_power (m + 1) ) by Def3, Th20;
then (((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power j = (((y,(y \ x)) to_power (0 + 1)),(x \ y)) to_power (n + 1) by A1, A5, A3, Th6;
hence Polynom (0,1,x,y) = Polynom (0,1,y,x) by A1, A5, A6, A4, Th6, NAT_1:14; :: thesis: verum

end;

hence X is BCK-algebra of 0 ,1, 0 ,1 by Def3; :: thesis: verum