let i, j, m, n be Nat; :: thesis: for X being BCK-algebra of i,j,m,n st i = 0 & n <> 0 holds

X is BCK-algebra of 0 ,1, 0 ,1

let X be BCK-algebra of i,j,m,n; :: thesis: ( i = 0 & n <> 0 implies X is BCK-algebra of 0 ,1, 0 ,1 )

reconsider X = X as BCK-algebra of i,j + 1,m + 1,n by Th18;

assume that

A1: i = 0 and

A2: n <> 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)

X is BCK-algebra of 0 ,1, 0 ,1

let X be BCK-algebra of i,j,m,n; :: thesis: ( i = 0 & n <> 0 implies X is BCK-algebra of 0 ,1, 0 ,1 )

reconsider X = X as BCK-algebra of i,j + 1,m + 1,n by Th18;

assume that

A1: i = 0 and

A2: n <> 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

hence
X is BCK-algebra of 0 ,1, 0 ,1
by Def3; :: thesis: verum
let x, y be Element of X; :: thesis: Polynom (0,1,x,y) = Polynom (0,1,y,x)

A3: (m + 1) + 1 > (i + 1) + 0 by A1, XREAL_1:8;

A4: (((y,(y \ x)) to_power (0 + 1)),(x \ y)) to_power (i + 1) = (((y,(y \ x)) to_power (0 + 1)),(x \ y)) to_power (n + 1) by Th19;

A5: n + 1 > i + 1 by A1, A2, XREAL_1:6;

( j + 1 >= i + 1 & (((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power (n + 1) = (((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power (i + 1) ) by A1, Th19, XREAL_1:6;

then A6: (((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power (0 + 1) = (((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power (j + 1) by A1, A5, Th6;

( Polynom (i,(j + 1),x,y) = Polynom ((m + 1),n,y,x) & (y,(y \ x)) to_power (n + 1) = (y,(y \ x)) to_power (i + 1) ) by Def3, Th19;

then (((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power (j + 1) = (((y,(y \ x)) to_power (0 + 1)),(x \ y)) to_power n 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;A3: (m + 1) + 1 > (i + 1) + 0 by A1, XREAL_1:8;

A4: (((y,(y \ x)) to_power (0 + 1)),(x \ y)) to_power (i + 1) = (((y,(y \ x)) to_power (0 + 1)),(x \ y)) to_power (n + 1) by Th19;

A5: n + 1 > i + 1 by A1, A2, XREAL_1:6;

( j + 1 >= i + 1 & (((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power (n + 1) = (((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power (i + 1) ) by A1, Th19, XREAL_1:6;

then A6: (((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power (0 + 1) = (((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power (j + 1) by A1, A5, Th6;

( Polynom (i,(j + 1),x,y) = Polynom ((m + 1),n,y,x) & (y,(y \ x)) to_power (n + 1) = (y,(y \ x)) to_power (i + 1) ) by Def3, Th19;

then (((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power (j + 1) = (((y,(y \ x)) to_power (0 + 1)),(x \ y)) to_power n 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