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