let L be non empty right_complementable add-associative right_zeroed unital right-distributive doubleLoopStr ; :: thesis: for n being Element of NAT st n > 0 holds
(power L) . ((0. L),n) = 0. L
let n be Element of NAT ; :: thesis: ( n > 0 implies (power L) . ((0. L),n) = 0. L )
assume n > 0 ; :: thesis: (power L) . ((0. L),n) = 0. L
then A1: n >= 0 + 1 by NAT_1:13;
n = (n - 1) + 1
.= (n -' 1) + 1 by A1, XREAL_0:def 2, XREAL_1:19 ;
hence (power L) . ((0. L),n) = ((power L) . ((0. L),(n -' 1))) * (0. L) by GROUP_1:def 7
.= 0. L ;
:: thesis: verum