let L be non empty right_complementable Abelian add-associative right_zeroed commutative well-unital distributive 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 Th20
.= 0_. L by POLYNOM3:35 ; :: thesis: verum