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

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

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

assume that

A1: n = 0 and

A2: i <> 0 ; :: thesis: X is BCK-algebra of 0 , 0 , 0 , 0

for x, y being Element of X holds Polynom (0,j,x,y) = Polynom (0,0,y,x)

A5: for x, y being Element of X holds Polynom (0,0,y,x) <= Polynom (0,0,x,y)

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

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

assume that

A1: n = 0 and

A2: i <> 0 ; :: thesis: X is BCK-algebra of 0 , 0 , 0 , 0

for x, y being Element of X holds Polynom (0,j,x,y) = Polynom (0,0,y,x)

proof

then reconsider X = X as BCK-algebra of 0 ,j, 0 , 0 by Def3;
let x, y be Element of X; :: thesis: Polynom (0,j,x,y) = Polynom (0,0,y,x)

A3: Polynom (i,j,x,y) = Polynom (m,n,y,x) by Def3;

A4: m + 1 >= n + 1 by A1, XREAL_1:6;

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

then (y,(y \ x)) to_power (m + 1) = (y,(y \ x)) to_power (0 + 1) by A1, A4, Th6;

hence Polynom (0,j,x,y) = Polynom (0,0,y,x) by A1, A3, Th19; :: thesis: verum

end;A3: Polynom (i,j,x,y) = Polynom (m,n,y,x) by Def3;

A4: m + 1 >= n + 1 by A1, XREAL_1:6;

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

then (y,(y \ x)) to_power (m + 1) = (y,(y \ x)) to_power (0 + 1) by A1, A4, Th6;

hence Polynom (0,j,x,y) = Polynom (0,0,y,x) by A1, A3, Th19; :: thesis: verum

A5: for x, y being Element of X holds Polynom (0,0,y,x) <= Polynom (0,0,x,y)

proof

for x, y being Element of X holds Polynom (0,0,y,x) = Polynom (0,0,x,y)
let x, y be Element of X; :: thesis: Polynom (0,0,y,x) <= Polynom (0,0,x,y)

Polynom (0,j,x,y) = Polynom (0,0,y,x) by Def3;

hence Polynom (0,0,y,x) <= Polynom (0,0,x,y) by Th5; :: thesis: verum

end;Polynom (0,j,x,y) = Polynom (0,0,y,x) by Def3;

hence Polynom (0,0,y,x) <= Polynom (0,0,x,y) by Th5; :: thesis: verum

proof

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

Polynom (0,0,x,y) <= Polynom (0,0,y,x) by A5;

then A6: (Polynom (0,0,x,y)) \ (Polynom (0,0,y,x)) = 0. X ;

Polynom (0,0,y,x) <= Polynom (0,0,x,y) by A5;

then (Polynom (0,0,y,x)) \ (Polynom (0,0,x,y)) = 0. X ;

hence Polynom (0,0,y,x) = Polynom (0,0,x,y) by A6, BCIALG_1:def 7; :: thesis: verum

end;Polynom (0,0,x,y) <= Polynom (0,0,y,x) by A5;

then A6: (Polynom (0,0,x,y)) \ (Polynom (0,0,y,x)) = 0. X ;

Polynom (0,0,y,x) <= Polynom (0,0,x,y) by A5;

then (Polynom (0,0,y,x)) \ (Polynom (0,0,x,y)) = 0. X ;

hence Polynom (0,0,y,x) = Polynom (0,0,x,y) by A6, BCIALG_1:def 7; :: thesis: verum