let X be BCI-algebra; :: thesis: for x being Element of X
for m, n being Element of 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 m, n being Element of NAT holds ((0. X),x to_power (m + n)) ` = (((0. X),x to_power m) ` ) \ ((0. X),x to_power n)
let m, n be Element of 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