let L be non empty right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ; :: thesis: for x being Element of L
for n being Element of NAT holds <%x%> `^ n = <%((power L) . x,n)%>
let x be Element of L; :: thesis: for n being Element of NAT holds <%x%> `^ n = <%((power L) . x,n)%>
defpred S₁[ Element of NAT ] means <%x%> `^ $1 = <%((power L) . x,$1)%>;
A1: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume <%x%> `^ n = <%((power L) . x,n)%> ; :: thesis: S<sub>1</sub>[n + 1]
hence <%x%> `^ (n + 1) = <%((power L) . x,n)%> *' <%x%> by Th20
.= <%(((power L) . x,n) * x)%> by Th36
.= <%((power L) . x,(n + 1))%> by GROUP_1:def 8 ;
:: thesis: verum

end;

<%x%> `^ 0 = 1_. L by Th16
.= (1. L) * (1_. L) by Th28
.= <%(1_ L)%> by Th30
.= <%((power L) . x,0 )%> by GROUP_1:def 8 ;
then A2: S₁[ 0 ] ;
thus for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A2, A1); :: thesis: verum