let L be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive commutative doubleLoopStr ; :: thesis: for n being Element of NAT holds (0_. L) `^ (n + 1) = 0_. L
let n be Element of NAT ; :: thesis: (0_. L) `^ (n + 1) = 0_. L
thus (0_. L) `^ (n + 1) = ((0_. L) `^ n) *' (0_. L) by Th19
.= 0_. L by POLYNOM3:34 ; :: thesis: verum