let X be BCI-Algebra_with_Condition(S); :: thesis: for x, a being Element of X holds (x,a) to_power 0 = x \ (a |^ 0)
let x, a be Element of X; :: thesis: (x,a) to_power 0 = x \ (a |^ 0)
x \ (a |^ 0) = x \ (0. X) by Def6
.= x by BCIALG_1:2 ;
hence (x,a) to_power 0 = x \ (a |^ 0) by BCIALG_2:1; :: thesis: verum