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 n >= 0 + 1 by NAT_1:13;
then A1: n - 1 >= 0 by XREAL_1:21;
n = (n - 1) + 1
.= (n -' 1) + 1 by A1, XREAL_0:def 2 ;
hence (power L) . (0. L),n = ((power L) . (0. L),(n -' 1)) * (0. L) by GROUP_1:def 8
.= 0. L by Th36 ;
:: thesis: verum