let X be BCI-algebra; :: thesis: for x being Element of X
for n being Element of NAT holds (0. X),(x ` ) to_power n is minimal
let x be Element of X; :: thesis: for n being Element of NAT holds (0. X),(x ` ) to_power n is minimal
let n be Element of NAT ; :: thesis: (0. X),(x ` ) to_power n is minimal
(0. X),(x ` ) to_power n = ((0. X),x to_power n) ` by Th9;
hence (0. X),(x ` ) to_power n is minimal by Th30; :: thesis: verum