let X be BCI-algebra; :: thesis: for x being Element of X
for n, m being Nat holds (((0. X),x) to_power (m + n)) ` = ((((0. X),x) to_power m) `) \ (((0. X),x) to_power n)
let x be Element of X; :: thesis: for n, m being Nat holds (((0. X),x) to_power (m + n)) ` = ((((0. X),x) to_power m) `) \ (((0. X),x) to_power n)
let n, m be Nat; :: thesis: (((0. X),x) to_power (m + n)) ` = ((((0. X),x) to_power m) `) \ (((0. X),x) to_power n)
(((0. X),x) to_power (m + n)) ` = ((((0. X),x) to_power m) \ ((((0. X),x) to_power n) `)) ` by Th13
.= ((((0. X),x) to_power m) `) \ (((((0. X),x) to_power n) `) `) by BCIALG_1:9 ;
hence (((0. X),x) to_power (m + n)) ` = ((((0. X),x) to_power m) `) \ (((0. X),x) to_power n) by Th12; :: thesis: verum