let X be BCI-algebra; :: thesis: for x being Element of X
for n being Nat holds ((0. X),(x `)) to_power n is minimal
let x be Element of X; :: thesis: for n being Nat holds ((0. X),(x `)) to_power n is minimal
let n be 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