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

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